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 [2008/04/17 11:08] vkuncak |
sav08:introductory_remarks_on_smt_provers [2009/05/06 09:45] 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 | + | * SAT solver to 'enumerate' conjunctions of disjunctive normal form ([[sav09:Lecture 08a]]) |
* **specialized algorithms for quantifier-free formulas** - this is what we will talk about today | * **specialized algorithms for quantifier-free formulas** - this is what we will talk about today | ||
* heuristic quantifier instantiation (instantiation rule) | * heuristic quantifier instantiation (instantiation rule) | ||
Line 29: | Line 30: | ||
Consider the following formula, where $f$ denotes functions from integers to integers and $a,b$ are integers. | Consider the following formula, where $f$ denotes functions from integers to integers and $a,b$ are integers. | ||
\[\begin{array}{l} | \[\begin{array}{l} | ||
- | (\forall x. x \le y \rightarrow f(x) \le f(y))\ \land \\[0.5ex] | + | (\forall x.\forall y.\ x \le y \rightarrow f(x) \le f(y))\ \land \\ |
- | (\forall x. f(x)=f(y) \rightarrow x=y)\ \land\\[0.5ex] | + | (\forall x.\forall y. f(x)=f(y) \rightarrow x=y)\ \land\\ |
- | 2 f(a) \le 2f(b)+1\ \land\\[0.5ex] | + | 2 f(a) \le 2f(b)+1\ \land\\ |
b < a | b < a | ||
\end{array} | \end{array} | ||
\] | \] | ||
+ | Is this formula satisfiable? ++|yes. Why?++ |