diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-08 08:13:05 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-08 08:13:05 -0500 |
| commit | ce831651caf58c1005fd3ebfdd2b75923d594328 (patch) | |
| tree | 8787737dde71b80722bbf39718c38e739596d9fd /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 2ca4e063ca007851ebf73ccb2ac6b7c85e73133d (diff) | |
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
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 0cb76f686..a6a8a6780 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -69,7 +69,7 @@ private: COMPUTE_SPLIT, COMPUTE_LAST }; - static Node computeOperation( Node f, int computeOption ); + static Node computeOperation( Node f, bool isNested, int computeOption ); public: static RewriteResponse preRewrite(TNode in); static RewriteResponse postRewrite(TNode in); |