From 0958ceced1107fe4be1c9f585bf5fad8fa73a7a7 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 16 Oct 2017 21:26:30 -0700 Subject: [PATCH] Fix for issue 1247 (#1257) * Fix for bug 1247: in incremental mode, there was a corner case where a skolem variable introduced during ITE removal became a solved-for variable (part of the substitution map). But then if the same skolem was introduced again as part of a subsequent ITE removal pass, the substitution was not properly applied and an incorrect result was obtained. The handling of substitutions in incremental mode is quite kludgey - I opened an issue to revisit this. * fixing regression --- src/smt/smt_engine.cpp | 54 ++++++++++++++++++++++-------- test/regress/regress0/Makefile.am | 3 +- test/regress/regress0/bug1247.smt2 | 14 ++++++++ 3 files changed, 56 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress0/bug1247.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5c3786108..4bcb78867 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -807,6 +807,12 @@ public: return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); } + /** + * Apply the substitutions in d_topLevelAssertions and the rewriter to each of + * the assertions in d_assertions, and store the result back in d_assertions. + */ + void applySubstitutionsToAssertions(); + /** * Process the assertions that have been asserted. */ @@ -3909,6 +3915,30 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map 0 ? d_substitutionsIndex : d_assertions.size(); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + if (i == substitutionAssertion) { + continue; + } + Trace("simplify") << "applying to " << d_assertions[i] << endl; + spendResource(options::preprocessStep()); + d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]))); + Trace("simplify") << " got " << d_assertions[i] << endl; + } + } +} + void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); spendResource(options::preprocessStep()); @@ -3929,6 +3959,9 @@ void SmtEnginePrivate::processAssertions() { } if (d_assertionsProcessed && options::incrementalSolving()) { + // TODO(b/1255): Substitutions in incremental mode should be managed with a + // proper data structure. + // Placeholder for storing substitutions d_substitutionsIndex = d_assertions.size(); d_assertions.push_back(NodeManager::currentNM()->mkConst(true)); @@ -4062,18 +4095,7 @@ void SmtEnginePrivate::processAssertions() { d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); } } else { - // Apply the substitutions we already have, and normalize - if(!options::unsatCores()) { - Chat() << "applying substitutions..." << endl; - Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " - << "applying substitutions" << endl; - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Trace("simplify") << "applying to " << d_assertions[i] << endl; - spendResource(options::preprocessStep()); - d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]))); - Trace("simplify") << " got " << d_assertions[i] << endl; - } - } + applySubstitutionsToAssertions(); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl; dumpAssertions("post-substitution", d_assertions); @@ -4216,6 +4238,10 @@ void SmtEnginePrivate::processAssertions() { // Remove ITEs, updating d_iteSkolemMap d_smt.d_stats->d_numAssertionsPre += d_assertions.size(); removeITEs(); + // This is needed because when solving incrementally, removeITEs may introduce + // skolems that were solved for earlier and thus appear in the substitution + // map. + applySubstitutionsToAssertions(); d_smt.d_stats->d_numAssertionsPost += d_assertions.size(); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl; @@ -4283,10 +4309,10 @@ void SmtEnginePrivate::processAssertions() { } d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder)); } - // For some reason this is needed for some benchmarks, such as + // TODO(b/1256): For some reason this is needed for some benchmarks, such as // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 - // Figure it out later removeITEs(); + applySubstitutionsToAssertions(); // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl; diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 43c7ae3b1..879fd9fc8 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -186,7 +186,8 @@ BUG_TESTS = \ bug605.cvc \ bug639.smt2 \ bt-test-00.smt2 \ - bt-test-01.smt2 + bt-test-01.smt2 \ + bug1247.smt2 #bug590.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug1247.smt2 b/test/regress/regress0/bug1247.smt2 new file mode 100644 index 000000000..e73e42fb5 --- /dev/null +++ b/test/regress/regress0/bug1247.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +(set-logic QF_ABV) +(set-info :status unsat) + +(declare-const p Bool) +(declare-const u (_ BitVec 8)) +(declare-const v (_ BitVec 8)) +(define-const t (_ BitVec 8) (ite p u v)) +(assert (= t #x01)) + +(push) +(assert (= t #x00)) +(check-sat) -- 2.30.2