diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 02:04:51 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 02:07:39 -0600 |
| commit | 841b7951f41f399859afab13a81e04599308da61 (patch) | |
| tree | 8c6eb70b498b0a01f00c1a77b96d00ff2f61c21b /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 18fed5592fb769d12ba2901a0fdc00c5c02863b9 (diff) | |
Add new method --quant-cf for finding conflicts eagerly for quantified formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 40234904f..e97d84701 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -44,6 +44,7 @@ private: static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ); static Node computeClause( Node n ); private: + static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false ); static Node computeNNF( Node body ); @@ -54,7 +55,8 @@ private: static Node computeSplit( Node f, Node body, std::vector< Node >& args ); private: enum{ - COMPUTE_MINISCOPING = 0, + COMPUTE_ELIM_SYMBOLS = 0, + COMPUTE_MINISCOPING, COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, COMPUTE_SIMPLE_ITE_LIFT, |