From: Tim King Date: Sat, 13 Jun 2015 22:51:19 +0000 (+0200) Subject: Turning off aggressive arith ite simplifications during incremental solving. X-Git-Tag: cvc5-1.0.0~6276 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d101e7fed051685673c13317cb45166ba5ef7798;p=cvc5.git Turning off aggressive arith ite simplifications during incremental solving. --- diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 757dab8fb..2b31831e2 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -15,6 +15,7 @@ ** \todo document this file **/ +#include "smt/options.h" #include "theory/arith/arith_ite_utils.h" #include "theory/arith/normal_form.h" #include "theory/arith/arith_utilities.h" @@ -272,6 +273,7 @@ void ArithIteUtils::addSubstitution(TNode f, TNode t){ } Node ArithIteUtils::applySubstitutions(TNode f){ + AlwaysAssert(!options::incrementalSolving()); return d_subs->apply(f); } @@ -285,6 +287,7 @@ Node ArithIteUtils::selectForCmp(Node n) const{ } void ArithIteUtils::learnSubstitutions(const std::vector& assertions){ + AlwaysAssert(!options::incrementalSolving()); for(size_t i=0, N=assertions.size(); i < N; ++i){ collectAssertions(assertions[i]); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8d36d9e05..d34f0cd12 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1530,7 +1530,12 @@ void TheoryEngine::mkAckermanizationAsssertions(std::vector& assertions) { Node TheoryEngine::ppSimpITE(TNode assertion) { - if(!d_iteRemover.containsTermITE(assertion)){ + if(options::incrementalSolving()){ + // disabling the d_iteUtilities->simpITE(assertion) pass for incremental solving. + // This is paranoia. We do not actually know of a bug coming from this. + // TODO re-enable + return assertion; + } else if(!d_iteRemover.containsTermITE(assertion)){ return assertion; }else{ @@ -1575,7 +1580,8 @@ bool TheoryEngine::donePPSimpITE(std::vector& assertions){ } // Do theory specific preprocessing passes - if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)){ + if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH) + && !options::incrementalSolving() ){ if(!simpDidALotOfWork){ ContainsTermITEVisitor& contains = *d_iteRemover.getContainsVisitor(); arith::ArithIteUtils aiteu(contains, d_userContext, getModel());