diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index c397e9d05..800fa910c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,6 +15,7 @@ **/ #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; @@ -690,14 +691,14 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit } bool QuantifiersRewriter::doMiniscopingNoFreeVar(){ - return Options::current()->miniscopeQuantFreeVar; + return options::miniscopeQuantFreeVar(); } bool QuantifiersRewriter::doMiniscopingAnd(){ - if( Options::current()->miniscopeQuant ){ + if( options::miniscopeQuant() ){ return true; }else{ - if( Options::current()->cbqi ){ + if( options::cbqi() ){ return true; }else{ return false; @@ -709,13 +710,13 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) }else if( computeOption==COMPUTE_PRE_SKOLEM ){ - return Options::current()->preSkolemQuant && !duringRewrite; + return options::preSkolemQuant() && !duringRewrite; }else if( computeOption==COMPUTE_PRENEX ){ - return Options::current()->prenexQuant; + return options::prenexQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - return Options::current()->varElimQuant; + return options::varElimQuant(); }else if( computeOption==COMPUTE_CNF ){ - return Options::current()->cnfQuant && !duringRewrite;// || Options::current()->finiteModelFind; + return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind(); }else{ return false; } |