Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:introductory_remarks_on_smt_provers [2009/05/06 00:24] vkuncak |
sav08:introductory_remarks_on_smt_provers [2009/05/06 09:43] 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]]) | ||