diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-18 22:33:22 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-18 22:33:22 +0100 |
| commit | 4d3e24e52765b03d8e6f36afe7de6168e8740693 (patch) | |
| tree | c5b3e7230e56db21cef630bbc95d94b7e3476618 /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 9d677333439c15677b6891ee8f6bd368a5df9f0a (diff) | |
Bug fix rewriter for fun defs.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index f07b635dc..38c1bdd58 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -41,6 +41,9 @@ private: static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); + static Node computeProcessTerms2( 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 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 ); @@ -56,9 +59,7 @@ private: static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); static Node computeNNF( Node body ); //cache is dependent upon currCond, icache is not, new_conds are negated conditions - 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 computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q ); static Node computeCondSplit( Node body, 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 ); @@ -102,3 +103,4 @@ public: #endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ + |