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.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b6c8fc95d405a9081bef5660623193c688ea74c4..9705757b9e6a041f7c2bd2ca7ed8b773ae7a1e50 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6750,7 +6750,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
 std::vector<Term> 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 7bce3bca535eabfe0135b94f75c6eff5fb3829a7..2bff621ca8207abe2861ca11a8e01095e7498616 100644 (file)
--- 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 2ecafdaa208f269a2538d9bdc8298aae8d9d2a57..6e47b6b8fd75cfb40dcd0f2966202d35b738cb52 100644 (file)
--- 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 ec1edceec7500eca32254268182b10641c5a677f..04e5b80d166548dc2f0bfa3aac2c54e4f897ee6e 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -443,8 +443,8 @@ bool Solver::addClause_(vec<Lit>& 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<Lit>& 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<Lit>& 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 55eade3b35e6473bb349334cc0cc8900ee080220..afd736fe5fec355aaabc6dfac26c004e2cac8ec3 100644 (file)
--- 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 879fb51c60e2f8da52042b3a6cc25f2b86f1907f..bd1bc7c358f65d3f72d1f0a5673bf629f3503514 100644 (file)
--- 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 1266a517a255ad8858f0ca0d5afaf3146a63d6ba..90e645c57f93ad31c9c76dee1a01b4988e1b8e43 100644 (file)
--- 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 9b713b40bfe0345b24b69ee5f69d2243b4e63888..942af84e844c5c87f28a3981aa347ea1d318155f 100644 (file)
--- 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 059a9fe1d8d42d77cd2cb3b1815d204c5a955d61..ed5fb7a43c746d7e1585bcf10e696260d6838e10 100644 (file)
--- 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<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& 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<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& 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 f6847c964a18436fd6d2e239e3e76fdbc828c540..080a47d48e772872995b2e89d928cdb0c3b48fe1 100644 (file)
--- 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 12f8fd4c86dedb6eaa6df47c99fd0b87f1764b68..2dc30a0f6b401d5773e8d2733d8757a46fc9a6c9 100644 (file)
--- 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 (file)
index 0000000..192a678
--- /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 30a6554c1213544ea71f3fd74fd546774f538e8b..3216cb89777089f888a7e8bad264e0f9c5e8ca9f 100644 (file)
--- 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 4a132a39b6e7d8a262e8ebc6169cf4fc45a16f23..9aed423fb98586453fb74338aebc046f128f4592 100644 (file)
--- 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))))