diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 47 |
1 files changed, 44 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 68485ca8a..14b3e3b42 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -159,6 +159,9 @@ class SmtEnginePrivate { // Simplify ITE structure void simpITE(); + // Simplify based on unconstrained values + void unconstrainedSimp(); + /** * Any variable in a assertion that is declared as a subtype type * (predicate subtype or integer subrange type) must be constrained @@ -255,6 +258,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_staticLearningTime("smt::SmtEngine::staticLearningTime"), d_simpITETime("smt::SmtEngine::simpITETime"), + d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), @@ -268,6 +272,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime); StatisticsRegistry::registerStat(&d_staticLearningTime); StatisticsRegistry::registerStat(&d_simpITETime); + StatisticsRegistry::registerStat(&d_unconstrainedSimpTime); StatisticsRegistry::registerStat(&d_iteRemovalTime); StatisticsRegistry::registerStat(&d_theoryPreprocessTime); StatisticsRegistry::registerStat(&d_cnfConversionTime); @@ -373,6 +378,7 @@ SmtEngine::~SmtEngine() throw() { StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); StatisticsRegistry::unregisterStat(&d_staticLearningTime); StatisticsRegistry::unregisterStat(&d_simpITETime); + StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime); StatisticsRegistry::unregisterStat(&d_iteRemovalTime); StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime); StatisticsRegistry::unregisterStat(&d_cnfConversionTime); @@ -449,6 +455,13 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() { Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp; } + // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode + if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) { + bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified(); + bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving; + Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; + NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp; + } // Turn on arith rewrite equalities only for pure arithmetic if(! Options::current()->arithRewriteEqSetByUser) { bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified(); @@ -886,16 +899,24 @@ void SmtEnginePrivate::nonClausalSimplify() { d_nonClausalLearnedLiterals.resize(j); } + hash_set<TNode, TNodeHashFunction> s; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]))); + Node assertion = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); + s.insert(assertion); + d_assertionsToCheck.push_back(assertion); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "non-clausal preprocessed: " - << d_assertionsToCheck.back() << endl; + << assertion << endl; } d_assertionsToPreprocess.clear(); for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) { - d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i]))); + Node learned = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i])); + if (s.find(learned) != s.end()) { + continue; + } + s.insert(learned); + d_assertionsToCheck.push_back(learned); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "non-clausal learned : " << d_assertionsToCheck.back() << endl; @@ -916,6 +937,16 @@ void SmtEnginePrivate::simpITE() } } + +void SmtEnginePrivate::unconstrainedSimp() +{ + TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_unconstrainedSimpTime); + + Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; + d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertionsToCheck); +} + + void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions) throw(AssertionException) { @@ -993,7 +1024,10 @@ void SmtEnginePrivate::simplifyAssertions() // Perform non-clausal simplification Trace("simplify") << "SmtEnginePrivate::simplify(): " << "performing non-clausal simplification" << endl; + // Abuse the user context to make sure circuit propagator gets backtracked + d_smt.d_userContext->push(); nonClausalSimplify(); + d_smt.d_userContext->pop(); } else { Assert(d_assertionsToCheck.empty()); d_assertionsToCheck.swap(d_assertionsToPreprocess); @@ -1004,9 +1038,16 @@ void SmtEnginePrivate::simplifyAssertions() simpITE(); } + if(Options::current()->unconstrainedSimp) { + unconstrainedSimp(); + } + if(Options::current()->repeatSimp) { d_assertionsToCheck.swap(d_assertionsToPreprocess); + // Abuse the user context to make sure circuit propagator gets backtracked + d_smt.d_userContext->push(); nonClausalSimplify(); + d_smt.d_userContext->pop(); } if(Options::current()->doStaticLearning) { |