Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:introductory_remarks_on_smt_provers [2009/05/06 00:24] vkuncak |
sav08:introductory_remarks_on_smt_provers [2009/05/06 09:46] vkuncak |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| Meaning of name (recent): | Meaning of name (recent): | ||
| - | * satisfiability: check satisfiability of formulas (could as well be validity) | + | * satisfiability: check satisfiability of formulas (to check validity, check satisfiability of negation) |
| - | * modulo theories: built-in support for arithmetic and some algebraic data types (Herbrand interpretations) | + | * modulo theories: built-in support for arithmetic, arrays, algebraic data types |
| Example provers: | Example provers: | ||
| Line 13: | Line 13: | ||
| * [[http://www.cs.nyu.edu/acsys/cvc3/|CVC3]] | * [[http://www.cs.nyu.edu/acsys/cvc3/|CVC3]] | ||
| * [[http://people.csail.mit.edu/vganesh/stp.html|STP]] | * [[http://people.csail.mit.edu/vganesh/stp.html|STP]] | ||
| + | * [[http://code.google.com/p/opensmt/|OpenSMT]] | ||
| ===== SMT Prover Architecture ===== | ===== SMT Prover Architecture ===== | ||
| - | Two layers: | + | Layers: |
| * fast solving of quantifier-free formulas (see [[http://citeseer.ist.psu.edu/671087.html|DPLL(T) paper]]) | * fast solving of quantifier-free formulas (see [[http://citeseer.ist.psu.edu/671087.html|DPLL(T) paper]]) | ||
| * SAT solver to 'enumerate' conjunctions of disjunctive normal form ([[sav09:Lecture 08a]]) | * SAT solver to 'enumerate' conjunctions of disjunctive normal form ([[sav09:Lecture 08a]]) | ||
| Line 24: | Line 25: | ||
| Note: formulas that are valid in the combination of quantifiers, linear integers, and uninterpreted functions are not enumerable (and neither are formulas that are not valid). The situation is worse than in pure first-order logic. | Note: formulas that are valid in the combination of quantifiers, linear integers, and uninterpreted functions are not enumerable (and neither are formulas that are not valid). The situation is worse than in pure first-order logic. | ||
| + | |||
| ===== Example ===== | ===== Example ===== | ||
| Line 35: | Line 37: | ||
| \end{array} | \end{array} | ||
| \] | \] | ||
| + | Is this formula satisfiable? | ||
| + | * over integers ++|No. Why?++ | ||
| + | * over reals ++|Yes. Why?++ | ||