From 03305bfae27642ed714eab144cf977d1943bb88d Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 30 May 2012 20:33:40 +0000 Subject: [PATCH] Added BitwiseEq bitvector rewrite Added option "--repeat-simp" which repeats nonclausal simplification: 4 times, twice before ite removal and twice after Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant speedup on dwp examples --- src/smt/smt_engine.cpp | 42 +++++++++++++++++++++------- src/theory/bv/theory_bv_rewriter.cpp | 9 ++++-- src/util/options.cpp | 18 ++++++++++++ src/util/options.h | 8 ++++++ 4 files changed, 64 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 90d21c60d..0d3a220c9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -424,13 +424,22 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() { } else { theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF); } - // Turn on ite simplification only for QF_LIA + // Turn on ite simplification for QF_LIA and QF_AUFBV if(! Options::current()->doITESimpSetByUser) { - bool iteSimp = logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() && !logic.isQuantified() && !logic.areRealsUsed(); + bool iteSimp = !logic.isQuantified() && + ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() && !logic.areRealsUsed()) || + (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV))); Trace("smt") << "setting ite simplification to " << iteSimp << std::endl; NodeManager::currentNM()->getOptions()->doITESimp = iteSimp; } - // Turn on ite simplification only for pure arithmetic + // Turn on multiple-pass non-clausal simplification for QF_AUFBV + if(! Options::current()->repeatSimpSetByUser) { + bool repeatSimp = !logic.isQuantified() && + (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV)); + Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; + NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp; + } + // Turn on arith rewrite equalities only for pure arithmetic if(! Options::current()->arithRewriteEqSetByUser) { bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified(); Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl; @@ -867,6 +876,14 @@ void SmtEnginePrivate::nonClausalSimplify() { d_nonClausalLearnedLiterals.resize(j); } + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]))); + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "non-clausal preprocessed: " + << d_assertionsToCheck.back() << 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]))); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " @@ -875,13 +892,6 @@ void SmtEnginePrivate::nonClausalSimplify() { } d_nonClausalLearnedLiterals.clear(); - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]))); - Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " - << "non-clausal preprocessed: " - << d_assertionsToCheck.back() << endl; - } - d_assertionsToPreprocess.clear(); } void SmtEnginePrivate::simpITE() @@ -984,6 +994,11 @@ void SmtEnginePrivate::simplifyAssertions() simpITE(); } + if(Options::current()->repeatSimp) { + d_assertionsToCheck.swap(d_assertionsToPreprocess); + nonClausalSimplify(); + } + if(Options::current()->doStaticLearning) { // Perform static learning Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -1100,6 +1115,12 @@ void SmtEnginePrivate::processAssertions() { // skipping for now --K } + if(Options::current()->repeatSimp) { + d_assertionsToCheck.swap(d_assertionsToPreprocess); + simplifyAssertions(); + removeITEs(); + } + // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones #ifdef CVC4_ASSERTIONS @@ -1112,6 +1133,7 @@ void SmtEnginePrivate::processAssertions() { if(Dump.isOn("assertions")) { // Push the simplified assertions to the dump output stream + cout << "###Finished second removeITEs"; for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { Dump("assertions") << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())); diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 567f9dc46..d6de6edbd 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -516,17 +516,20 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule, RewriteRule, - RewriteRule + RewriteRule, + RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } - + else if(RewriteRule::applies(node)) { + Node resultNode = RewriteRule::run(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } else { Node resultNode = LinearRewriteStrategy < RewriteRule, RewriteRule, RewriteRule, - // ,RewriteRule, RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); diff --git a/src/util/options.cpp b/src/util/options.cpp index a510f35f8..01b9648ff 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -85,6 +85,8 @@ Options::Options() : doStaticLearning(true), doITESimp(false), doITESimpSetByUser(false), + repeatSimp(false), + repeatSimpSetByUser(false), interactive(false), interactiveSetByUser(false), perCallResourceLimit(0), @@ -187,6 +189,8 @@ Additional CVC4 options:\n\ --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ --ite-simp turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ --no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ + --repeat-simp make multiple passes with nonclausal simplifier\n\ + --no-repeat-simp do not make multiple passes with nonclausal simplifier\n\ --replay=file replay decisions from file\n\ --replay-log=file log decisions and propagations to file\n\ SAT:\n\ @@ -426,6 +430,8 @@ enum OptionValue { NO_STATIC_LEARNING, ITE_SIMP, NO_ITE_SIMP, + REPEAT_SIMP, + NO_REPEAT_SIMP, INTERACTIVE, NO_INTERACTIVE, PRODUCE_ASSIGNMENTS, @@ -524,6 +530,8 @@ static struct option cmdlineOptions[] = { { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING }, { "ite-simp", no_argument, NULL, ITE_SIMP }, { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP }, + { "repeat-simp", no_argument, NULL, REPEAT_SIMP }, + { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, 'm' }, @@ -847,6 +855,16 @@ throw(OptionException) { doITESimpSetByUser = true; break; + case REPEAT_SIMP: + repeatSimp = true; + repeatSimpSetByUser = true; + break; + + case NO_REPEAT_SIMP: + repeatSimp = false; + repeatSimpSetByUser = true; + break; + case INTERACTIVE: interactive = true; interactiveSetByUser = true; diff --git a/src/util/options.h b/src/util/options.h index 9c36a471d..e6135dacb 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -154,6 +154,14 @@ struct CVC4_PUBLIC Options { */ bool doITESimpSetByUser; + /** Whether to do multiple rounds of nonclausal simplification */ + bool repeatSimp; + + /** + * Whether the user explicitly requested multiple rounds of nonclausal simplification + */ + bool repeatSimpSetByUser; + /** Whether we're in interactive mode or not */ bool interactive; -- 2.30.2