diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-04 10:41:49 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-04 10:42:01 +0100 |
| commit | f9e109b0ac12ffbfd167a19dcd60f16241a0542c (patch) | |
| tree | 07547a834d60cbbbd75c91e1695c5518774c813e /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 5fae5ff49bfc9c96c03c52f5e2a5caa52ac40d03 (diff) | |
Better combination of UF with cbqi, refactor quantifiers intialization.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 98a83b7de..0ad79587a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -39,6 +39,7 @@ private: static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); static Node computeClause( Node n ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); + static bool isConditionalVariableElim( Node n, int pol=0 ); private: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); @@ -48,7 +49,7 @@ private: static Node computeProcessTerms( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds ); - static Node computeProcessIte( Node body ); + static Node computeProcessIte( Node body, Node ipl ); static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); @@ -60,9 +61,9 @@ private: COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, COMPUTE_PROCESS_TERMS, - COMPUTE_PROCESS_ITE, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, + COMPUTE_PROCESS_ITE, //COMPUTE_FLATTEN_ARGS_UF, //COMPUTE_CNF, COMPUTE_LAST |