diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-09 11:58:30 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-09 11:58:30 +0200 |
commit | ed5052c7672bd59f8a8ef28d980d56a4f036f97d (patch) | |
tree | 4dc71d165b171915ceee94fbf42ff470c9eb78d8 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | f6f4c8ca3aa9b426d72b89cb9fd37110a2a59702 (diff) |
Refactor quantifier prenex option. By default, do not pull quantifiers with user patterns.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 754bfacb1..d142007c6 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -577,7 +577,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){ if( body.getKind()==FORALL ){ - if( pol ){ + if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ std::vector< Node > terms; std::vector< Node > subs; //for doing prenexing of same-signed quantifiers @@ -950,7 +950,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ return options::simpleIteLiftQuant(); }else if( computeOption==COMPUTE_PRENEX ){ - return options::prenexQuant() && !options::aggressiveMiniscopeQuant(); + return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant() || options::dtVarExpandQuant(); }else if( computeOption==COMPUTE_CNF ){ |