diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 15:48:11 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 15:48:11 -0500 |
| commit | ca1b17c8bba3681643a1a3de19d32b038c38aceb (patch) | |
| tree | ff02dc2314a3c1e86d19ca9bc2bbe8a57ef1856b /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 685b1f3769decafbff1c5b929d4ce01169ff9d81 (diff) | |
Refactor prenex modes.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2423caaee..90a22f4b7 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -59,7 +59,7 @@ public: //cache is dependent upon currCond, icache is not, new_conds are negated conditions static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ); static Node computeCondSplit( Node body, QAttributes& qa ); - static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol ); + static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); static Node computePrenexAgg( Node n, bool topLevel ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); |