diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-03 17:40:18 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-03 17:40:18 -0500 |
| commit | ce883ca9296c872affb47547304a9ecc0ec5224d (patch) | |
| tree | 2e797668f07fa045bde9f1b690e8402fb8238f97 /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 9aaa7ca741199f73e70149f8309cd7cd9a12e69f (diff) | |
Miniscope top level conjunctions for prenex normal form, allow one level miniscoping in prenex normal form.
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 bb352f65c..2423caaee 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -60,7 +60,7 @@ public: 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 computePrenexAgg( Node n ); + 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 ); private: |