From 7b8fb66753f2f2fc02a4bab5faf4bc21802cf1e9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Jun 2022 09:51:37 -0500 Subject: [PATCH] Disable arithmetic static learning when unsat cores are enabled (#8830) The arithmetic static learner uses non-local reasoning and does not have proof support. Thus it may rewrite A ^ B to A ^ B' where ( A ^ B ) => B', but the preprocessor by default assumes that the replacement is such that B => B'. This disables the arithmetic static learner when unsat cores are enabled. Other static learning appears to be local and is still enabled. This further corrects an issue in set_defaults that checked incompatibility with unsat cores based on whether proofs are enabled. We now check compatibility independent of whether proofs are enabled. This also corrects several restrictions on things that previously were treated as being incompatible with unsat cores (but not proof unsat cores) that were spurious. Fixes #8822. --- src/api/cpp/cvc5.cpp | 2 +- src/options/arith_options.toml | 8 ++ src/options/smt_options.toml | 4 +- src/prop/minisat/core/Solver.cc | 12 +- src/prop/minisat/minisat.cpp | 2 +- src/prop/minisat/simp/SimpSolver.cc | 4 +- src/smt/process_assertions.cpp | 2 +- src/smt/set_defaults.cpp | 131 +++++------------- src/smt/solver_engine.cpp | 6 +- src/theory/arith/theory_arith.cpp | 5 +- test/regress/cli/CMakeLists.txt | 1 + .../cores/issue8822-arith-static-learn.smt2 | 9 ++ .../cli/regress1/nl/issue4791-llr.smt2 | 1 + .../quantifiers/cee-event-wrong-sat.smt2 | 1 + 14 files changed, 71 insertions(+), 117 deletions(-) create mode 100644 test/regress/cli/regress0/cores/issue8822-arith-static-learn.smt2 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b6c8fc95d..9705757b9 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -6750,7 +6750,7 @@ std::vector Solver::getUnsatAssumptions(void) const std::vector Solver::getUnsatCore(void) const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_slv->getOptions().smt.unsatCores) + CVC5_API_CHECK(d_slv->getOptions().smt.produceUnsatCores) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == internal::SmtMode::UNSAT) diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 7bce3bca5..2bff621ca 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -590,3 +590,11 @@ name = "Arithmetic Theory" type = "bool" default = "false" help = "whether to use the equality solver in the theory of arithmetic" + +[[option]] + name = "arithStaticLearning" + category = "regular" + long = "arith-static-learning" + type = "bool" + default = "true" + help = "do arithmetic static learning for ite terms based on bounds when static learning is enabled" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 2ecafdaa2..6e47b6b8f 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -34,7 +34,7 @@ name = "SMT Layer" help = "apply Boolean constant propagation as a substituion during simplification" [[option]] - name = "doStaticLearning" + name = "staticLearning" category = "regular" long = "static-learning" type = "bool" @@ -142,7 +142,7 @@ name = "SMT Layer" help = "after UNSAT/VALID, check the generated proof (with proof)" [[option]] - name = "unsatCores" + name = "produceUnsatCores" category = "regular" long = "produce-unsat-cores" type = "bool" diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index ec1edceec..04e5b80d1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -443,8 +443,8 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // If a literal is false at 0 level (both sat and user level) we also // ignore it, unless we are tracking the SAT solver's reasoning if (value(ps[i]) == l_False) { - if (!options().smt.unsatCores && !needProof() && level(var(ps[i])) == 0 - && user_level(var(ps[i])) == 0) + if (!options().smt.produceUnsatCores && !needProof() + && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { continue; } @@ -481,7 +481,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { - if (options().smt.unsatCores || needProof()) + if (options().smt.produceUnsatCores || needProof()) { // Take care of false units here; otherwise, we need to // construct the clause below to give to the proof manager @@ -527,7 +527,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) MinisatSatSolver::toSatClause(ca[cr], satClause); d_proxy->notifyClauseInsertedAtLevel(satClause, clauseLevel); } - if (options().smt.unsatCores || needProof()) + if (options().smt.produceUnsatCores || needProof()) { if (ps.size() == falseLiteralsCount) { @@ -2072,7 +2072,7 @@ CRef Solver::updateLemmas() { // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { - Assert(!options().smt.unsatCores && !needProof()); + Assert(!options().smt.produceUnsatCores && !needProof()); conflict = CRef_Lazy; backtrackLevel = 0; Trace("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -2240,7 +2240,7 @@ bool Solver::needProof() const bool Solver::assertionLevelOnly() const { - return options().smt.unsatCores && !needProof() + return options().smt.produceUnsatCores && !needProof() && options().base.incrementalSolving; } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 55eade3b3..afd736fe5 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -167,7 +167,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { } d_minisat->addClause(minisat_clause, removable, clause_id); // FIXME: to be deleted when we kill old proof code for unsat cores - Assert(!options().smt.unsatCores || options().smt.produceProofs + Assert(!options().smt.produceUnsatCores || options().smt.produceProofs || clause_id != ClauseIdError); return clause_id; } diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 879fb51c6..bd1bc7c35 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -60,14 +60,14 @@ SimpSolver::SimpSolver(Env& env, simp_garbage_frac(opt_simp_garbage_frac), use_asymm(opt_use_asymm), // make sure this is not enabled if unsat cores or proofs are on - use_rcheck(opt_use_rcheck && !options().smt.unsatCores && !pnm), + use_rcheck(opt_use_rcheck && !options().smt.produceUnsatCores && !pnm), merges(0), asymm_lits(0), eliminated_vars(0), elimorder(1), use_simplification( options().prop.minisatSimpMode != options::MinisatSimpMode::NONE - && !enableIncremental && !options().smt.unsatCores && !pnm), + && !enableIncremental && !options().smt.produceUnsatCores && !pnm), occurs(ClauseDeleted(ca)), elim_heap(ElimLt(n_occ)), bwdsub_assigns(0), diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 1266a517a..90e645c57 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -276,7 +276,7 @@ bool ProcessAssertions::apply(Assertions& as) dumpAssertions("assertions::post-simplify", as); Trace("assertions::post-simplify") << std::endl; - if (options().smt.doStaticLearning) + if (options().smt.staticLearning) { applyPass("static-learning", as); } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 9b713b40b..942af84e8 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -85,9 +85,9 @@ void SetDefaults::setDefaultsPre(Options& opts) || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF) { - opts.writeSmt().unsatCores = true; + opts.writeSmt().produceUnsatCores = true; } - if (opts.smt.unsatCores + if (opts.smt.produceUnsatCores && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) { if (opts.smt.unsatCoresModeWasSetByUser) @@ -117,7 +117,7 @@ void SetDefaults::setDefaultsPre(Options& opts) { notifyModifyOption("unsatCoresMode", "sat-proof", "enabling proofs"); } - opts.writeSmt().unsatCores = true; + opts.writeSmt().produceUnsatCores = true; opts.writeSmt().unsatCoresMode = options::UnsatCoresMode::SAT_PROOF; } } @@ -140,7 +140,7 @@ void SetDefaults::setDefaultsPre(Options& opts) } } // if proofs weren't enabled by user, and we are producing unsat cores - if (opts.smt.unsatCores) + if (opts.smt.produceUnsatCores) { opts.writeSmt().produceProofs = true; if (opts.smt.unsatCoresMode == options::UnsatCoresMode::SAT_PROOF) @@ -159,7 +159,7 @@ void SetDefaults::setDefaultsPre(Options& opts) // if unsat cores are disabled, then unsat cores mode should be OFF. Similarly // for proof mode. - Assert(opts.smt.unsatCores + Assert(opts.smt.produceUnsatCores == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)); Assert(opts.smt.produceProofs == (opts.smt.proofMode != options::ProofMode::OFF)); @@ -419,7 +419,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const // Disable options incompatible with unsat cores or output an error if enabled // explicitly - if (safeUnsatCores(opts)) + if (opts.smt.produceUnsatCores) { // check if the options are not compatible with unsat cores std::stringstream reasonNoUc; @@ -1085,24 +1085,24 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, bool SetDefaults::incompatibleWithUnsatCores(Options& opts, std::ostream& reason) const { - if (opts.smt.simplificationMode != options::SimplificationMode::NONE) + // All techniques that are incompatible with unsat cores are listed here. + // A preprocessing pass is incompatible with unsat cores if + // (A) its reasoning is not local, i.e. it may replace an assertion A by A' + // where A does not imply A', or if it adds new assertions B that are not + // tautologies, AND + // (B) it does not track proofs. + if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) { - if (opts.smt.simplificationModeWasSetByUser) + if (opts.smt.deepRestartModeWasSetByUser) { - reason << "simplification"; + reason << "deep restarts"; return true; } - notifyModifyOption("simplificationMode", "none", "unsat cores"); - opts.writeSmt().simplificationMode = options::SimplificationMode::NONE; - if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) - { - verbose(1) << "SolverEngine: turning off deep restart to support unsat " - "cores" - << std::endl; - opts.writeSmt().deepRestartMode = options::DeepRestartMode::NONE; - } + verbose(1) << "SolverEngine: turning off deep restart to support unsat " + "cores" + << std::endl; + opts.writeSmt().deepRestartMode = options::DeepRestartMode::NONE; } - if (opts.smt.learnedRewrite) { if (opts.smt.learnedRewriteWasSetByUser) @@ -1113,82 +1113,28 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, notifyModifyOption("learnedRewrite", "false", "unsat cores"); opts.writeSmt().learnedRewrite = false; } - - if (opts.arith.pbRewrites) - { - if (opts.arith.pbRewritesWasSetByUser) - { - reason << "pseudoboolean rewrites"; - return true; - } - notifyModifyOption("pbRewrites", "false", "unsat cores"); - opts.writeArith().pbRewrites = false; - } - - if (opts.smt.sortInference) - { - if (opts.smt.sortInferenceWasSetByUser) - { - reason << "sort inference"; - return true; - } - notifyModifyOption("sortInference", "false", "unsat cores"); - opts.writeSmt().sortInference = false; - } - - if (opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF) - { - if (opts.quantifiers.preSkolemQuantWasSetByUser) - { - reason << "pre-skolemization"; - return true; - } - notifyModifyOption("preSkolemQuant", "off", "unsat cores"); - opts.writeQuantifiers().preSkolemQuant = options::PreSkolemQuantMode::OFF; - } - - if (opts.bv.bitvectorToBool) - { - if (opts.bv.bitvectorToBoolWasSetByUser) - { - reason << "bv-to-bool"; - return true; - } - notifyModifyOption("bitvectorToBool", "false", "unsat cores"); - opts.writeBv().bitvectorToBool = false; - } - - if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) - { - if (opts.bv.boolToBitvectorWasSetByUser) - { - reason << "bool-to-bv != off"; - return true; - } - notifyModifyOption("boolToBitvector", "off", "unsat cores"); - opts.writeBv().boolToBitvector = options::BoolToBVMode::OFF; - } - - if (opts.bv.bvIntroducePow2) + // most static learning techniques are local, although arithmetic static + // learning is not. + if (opts.arith.arithStaticLearning) { - if (opts.bv.bvIntroducePow2WasSetByUser) + if (opts.arith.arithStaticLearningWasSetByUser) { - reason << "bv-intro-pow2"; + reason << "arith static learning"; return true; } - notifyModifyOption("bvIntroducePow2", "false", "unsat cores"); - opts.writeBv().bvIntroducePow2 = false; + notifyModifyOption("arithStaticLearning", "false", "proofs"); + opts.writeArith().arithStaticLearning = false; } - if (opts.smt.repeatSimp) + if (opts.arith.pbRewrites) { - if (opts.smt.repeatSimpWasSetByUser) + if (opts.arith.pbRewritesWasSetByUser) { - reason << "repeat-simp"; + reason << "pseudoboolean rewrites"; return true; } - notifyModifyOption("repeatSimp", "false", "unsat cores"); - opts.writeSmt().repeatSimp = false; + notifyModifyOption("pbRewrites", "false", "unsat cores"); + opts.writeArith().pbRewrites = false; } if (opts.quantifiers.globalNegate) @@ -1207,21 +1153,6 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, reason << "ITE simp"; return true; } - if (opts.smt.unconstrainedSimp) - { - if (opts.smt.unconstrainedSimpWasSetByUser) - { - reason << "unconstrained simplification"; - return true; - } - notifyModifyOption("unconstrainedSimp", "false", "unsat cores"); - opts.writeSmt().unconstrainedSimp = false; - } - if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE) - { - reason << "deep restarts"; - return true; - } return false; } diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 059a9fe1d..ed5fb7a43 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1340,7 +1340,7 @@ StatisticsRegistry& SolverEngine::getStatisticsRegistry() UnsatCore SolverEngine::getUnsatCoreInternal() { - if (!d_env->getOptions().smt.unsatCores) + if (!d_env->getOptions().smt.produceUnsatCores) { throw ModalException( "Cannot get an unsat core when produce-unsat-cores or produce-proofs " @@ -1378,7 +1378,7 @@ UnsatCore SolverEngine::getUnsatCoreInternal() std::vector SolverEngine::reduceUnsatCore(const std::vector& core) { - Assert(options().smt.unsatCores) + Assert(options().smt.produceUnsatCores) << "cannot reduce unsat core if unsat cores are turned off"; d_env->verbose(1) << "SolverEngine::reduceUnsatCore(): reducing unsat core" @@ -1446,7 +1446,7 @@ std::vector SolverEngine::reduceUnsatCore(const std::vector& core) void SolverEngine::checkUnsatCore() { - Assert(d_env->getOptions().smt.unsatCores) + Assert(d_env->getOptions().smt.produceUnsatCores) << "cannot check unsat core if unsat cores are turned off"; d_env->verbose(1) << "SolverEngine::checkUnsatCore(): generating unsat core" diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index f6847c964..080a47d48 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -188,7 +188,10 @@ Theory::PPAssertStatus TheoryArith::ppAssert( void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned) { - d_internal->ppStaticLearn(n, learned); + if (options().arith.arithStaticLearning) + { + d_internal->ppStaticLearn(n, learned); + } } bool TheoryArith::preCheck(Effort level) diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 12f8fd4c8..2dc30a0f6 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -489,6 +489,7 @@ set(regress_0_tests regress0/cores/issue5902.smt2 regress0/cores/issue5908.smt2 regress0/cores/issue8705-bool-ppassert.smt2 + regress0/cores/issue8822-arith-static-learn.smt2 regress0/cvc-rerror-print.cvc.smt2 regress0/cvc3-bug15.cvc.smt2 regress0/cvc3.userdoc.01.cvc.smt2 diff --git a/test/regress/cli/regress0/cores/issue8822-arith-static-learn.smt2 b/test/regress/cli/regress0/cores/issue8822-arith-static-learn.smt2 new file mode 100644 index 000000000..192a67802 --- /dev/null +++ b/test/regress/cli/regress0/cores/issue8822-arith-static-learn.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () Int) +(declare-fun b () Bool) +(declare-fun c () Int) +(assert (< a 0)) +(assert (< 0 c)) +(assert (= a (- (ite (not (= 0 (+ 1 (ite b c 0)))) 1 0) 1))) +(check-sat) diff --git a/test/regress/cli/regress1/nl/issue4791-llr.smt2 b/test/regress/cli/regress1/nl/issue4791-llr.smt2 index 30a6554c1..3216cb897 100644 --- a/test/regress/cli/regress1/nl/issue4791-llr.smt2 +++ b/test/regress/cli/regress1/nl/issue4791-llr.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: --learned-rewrite ; EXPECT: unsat ; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof ; ;!(a,b,c).( 0<=b & 1<=c & 0<=a & 1<=c ; => diff --git a/test/regress/cli/regress2/quantifiers/cee-event-wrong-sat.smt2 b/test/regress/cli/regress2/quantifiers/cee-event-wrong-sat.smt2 index 4a132a39b..9aed423fb 100644 --- a/test/regress/cli/regress2/quantifiers/cee-event-wrong-sat.smt2 +++ b/test/regress/cli/regress2/quantifiers/cee-event-wrong-sat.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: -q --full-saturate-quant --ee-mode=distributed ; COMMAND-LINE: -q --full-saturate-quant --ee-mode=central ; EXPECT: unsat +; DISABLE-TESTER: unsat-core (set-logic ALL) (set-info :status unsat) (declare-datatypes ((T@$TypeValue 0) (T@A 0)) (((A)) ((T)))) -- 2.30.2