diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-07 09:21:00 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-07 09:21:00 -0600 |
commit | 473b375e3eabefba0a59800f010befb8a4f99ea1 (patch) | |
tree | 97a55182c17f9c8c70f41847e464771f16759d97 /src/smt/smt_engine.h | |
parent | 7add98ae1348d71e364d2407a18d40a007ce1f0b (diff) |
Allow FORALL in quantifier elimination command (#1322)
* Allow FORALL passed as an argument to get-qe.
* Document
* Format
* Minor
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 46 |
1 files changed, 44 insertions, 2 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 48ae24898..8961fbee0 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -538,8 +538,50 @@ public: void printSynthSolution( std::ostream& out ); /** - * Do quantifier elimination, doFull false means just output one disjunct, - * strict is whether to output warnings. + * Do quantifier elimination. + * + * This function takes as input a quantified formula e + * of the form: + * Q x1...xn. P( x1...xn, y1...yn ) + * where P( x1...xn, y1...yn ) is a quantifier-free + * formula in a logic that supports quantifier elimination. + * Currently, the only logics supported by quantifier + * elimination is LRA and LIA. + * + * This function returns a formula ret such that, given + * the current set of formulas A asserted to this SmtEngine : + * + * If doFull = true, then + * - ( A ^ e ) and ( A ^ ret ) are equivalent + * - ret is quantifier-free formula containing + * only free variables in y1...yn. + * + * If doFull = false, then + * - (A ^ e) => (A ^ ret) if Q is forall or + * (A ^ ret) => (A ^ e) if Q is exists, + * - ret is quantifier-free formula containing + * only free variables in y1...yn, + * - If Q is exists, let A^Q_n be the formula + * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n + * where for each i=1,...n, formula ret^Q_i + * is the result of calling doQuantifierElimination + * for e with the set of assertions A^Q_{i-1}. + * Similarly, if Q is forall, then let A^Q_n be + * A ^ ret^Q_1 ^ ... ^ ret^Q_n + * where ret^Q_i is the same as above. + * In either case, we have that ret^Q_j will + * eventually be true or false, for some finite j. + * + * The former feature is quantifier elimination, and + * is run on invocations of the smt2 extended command get-qe. + * The latter feature is referred to as partial quantifier + * elimination, and is run on invocations of the smt2 + * extended command get-qe-disjunct, which can be used + * for incrementally computing the result of a + * quantifier elimination. + * + * The argument strict is whether to output + * warnings, such as when an unexpected logic is used. */ Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true) throw(Exception); |