[proof-new] Renaming proof option to be in sync with SMT-LIB (#6154)

diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
index 451a6a530fa9a039947b9dfab10021b93aefa5db..e4a59c8f0a685dea6ff355b331a0f440f115961c 100644 (file)
--- a/src/expr/proof_ensure_closed.cpp
+++ b/src/expr/proof_ensure_closed.cpp
@@ -36,7 +36,7 @@ void ensureClosedWrtInternal(Node proven,
                              const char* ctx,
                              bool reqGen)
 {
-  if (!options::proof())
+  if (!options::produceProofs())
   {
     // proofs not enabled, do not do check
     return;

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index c29fe5e502a26fba248d32699899e9f10994eb49..787a60e783a15b6e67097993f236686da6eb355e 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -131,9 +131,9 @@ header = "options/smt_options.h"
   help = "Block models based on the concrete model values for the free variables."
 
 [[option]]
-  name       = "proof"
+  name       = "produceProofs"
   category   = "regular"
-  long       = "proof"
+  long       = "produce-proofs"
   type       = "bool"
   default    = "false"
   help       = "produce proofs, support check-proofs and get-proof"

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index f823ff929a206f53250e2e9e472b88f8d6d58d63..afa1d3ba23b7a2b4eeabe7eef85fc81333821e7c 100644 (file)
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -61,7 +61,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
       imap[assertions->size()] = newSkolems[j];
       assertions->pushBackTrusted(newAsserts[j]);
       // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCores() && !options::proof())
+      if (options::unsatCores() && !options::produceProofs())
       {
         ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
                                                  assertion);

diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 32dc2208a8733a55a0f056b687aaf8c90b9d627f..f0b51e6a5a74e398e8517b440b9c090492f7cbf0 100644 (file)
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -86,7 +86,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
     for( int i=0; i<(int)assertions.size(); i++ ){
       Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
       if( processAssertion( assertions[i] ) ){
-        if (options::unsatCores() && !options::proof()
+        if (options::unsatCores() && !options::produceProofs()
             && std::find(macro_assertions.begin(),
                          macro_assertions.end(),
                          assertions[i])
@@ -112,7 +112,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
           // is an over-approximation. a more fine-grained unsat core
           // computation would require caching dependencies for each subterm of
           // the formula, which is expensive.
-          if (options::unsatCores() && !options::proof())
+          if (options::unsatCores() && !options::produceProofs())
           {
             ProofManager::currentPM()->addDependence(curr, assertions[i]);
             for (unsigned j = 0; j < macro_assertions.size(); j++)

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b36fe9517896315002735280527d166b0e789c09..8c27e2bdd82224f9bf1a4927e63afdcceb9e1abb 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -56,7 +56,7 @@ namespace {
  */
 bool assertionLevelOnly()
 {
-  return (options::proof() || options::unsatCores())
+  return (options::produceProofs() || options::unsatCores())
          && options::incrementalSolving();
 }
 

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 935c08e9bb40ae7b3a37547f02ed754593fcf518..694c73e5e4aeb12d43fe0a32da680f3029e3fba6 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -160,7 +160,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::unsatCores() || options::proof()
+  Assert(!options::unsatCores() || options::produceProofs()
          || clause_id != ClauseIdError);
   return clause_id;
 }

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index bcdcdf6236025d5713da66ae9b79e2a22975f3e4..5ee472b93bcf80115d68e42b9cd0102b0289a561 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -81,7 +81,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (CVC4::options::proof())
+  if (CVC4::options::produceProofs())
   {
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index f37b406b40b1673ef570eaf98a72a0696d4984a1..f2c6c33873a533263e274550b53d96a01666aa1c 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -75,7 +75,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::checkProofs() || options::checkUnsatCoresNew())
   {
     Notice() << "SmtEngine: setting proof" << std::endl;
-    options::proof.set(true);
+    options::produceProofs.set(true);
   }
   if (options::bitvectorAigSimplifications.wasSetByUser())
   {
@@ -312,7 +312,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
        || options::produceInterpols() != options::ProduceInterpols::NONE
        || options::modelCoresMode() != options::ModelCoresMode::NONE
        || options::blockModelsMode() != options::BlockModelsMode::NONE
-       || options::proof())
+       || options::produceProofs())
       && !options::produceAssertions())
   {
     Notice() << "SmtEngine: turning on produce-assertions to support "

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3fdf67ed7465ffed738120384adf5cdf5933d16c..aac8ceab71d369618d70ae5ea3407f0fc95efad8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -223,7 +223,7 @@ void SmtEngine::finishInit()
   d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver);
 
   ProofNodeManager* pnm = nullptr;
-  if (options::proof())
+  if (options::produceProofs())
   {
     // ensure bound variable uses canonical bound variables
     getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
@@ -332,7 +332,7 @@ SmtEngine::~SmtEngine()
 
     // d_proofManager is always created when proofs are enabled at configure
     // time.  Because of this, this code should not be wrapped in PROOF() which
-    // additionally checks flags such as options::proof().
+    // additionally checks flags such as options::produceProofs().
     //
     // Note: the proof manager must be destroyed before the theory engine.
     // Because the destruction of the proofs depends on contexts owned be the
@@ -971,7 +971,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
         if ((options::checkProofs() || options::proofEagerChecking())
-            && !options::proof())
+            && !options::produceProofs())
         {
           throw ModalException(
               "Cannot check-proofs because proofs were disabled.");
@@ -1388,7 +1388,7 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
 void SmtEngine::checkProof()
 {
-  Assert(options::proof());
+  Assert(options::produceProofs());
   // internal check the proof
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
@@ -1457,9 +1457,8 @@ void SmtEngine::checkUnsatCore() {
   initializeSubsolver(coreChecker);
   coreChecker->getOptions().set(options::checkUnsatCores, false);
   // disable all proof options
-  coreChecker->getOptions().set(options::proof, false);
+  coreChecker->getOptions().set(options::produceProofs, false);
   coreChecker->getOptions().set(options::checkUnsatCoresNew, false);
-
   // set up separation logic heap if necessary
   TypeNode sepLocType, sepDataType;
   if (getSepHeapTypes(sepLocType, sepDataType))
@@ -1546,7 +1545,7 @@ std::string SmtEngine::getProof()
     getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
   }
 #if IS_PROOFS_BUILD
-  if (!options::proof())
+  if (!options::produceProofs())
   {
     throw ModalException("Cannot get a proof when proof option is off.");
   }
@@ -1647,7 +1646,7 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (options::proof() && getSmtMode() == SmtMode::UNSAT)
+  if (options::produceProofs() && getSmtMode() == SmtMode::UNSAT)
   {
     // minimize instantiations based on proof manager
     getRelevantInstantiationTermVectors(insts);

diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h
index dfb3ddad800d9737959dcbefcf81da372c668374..d453285d6e4f5df7c3c96c090745e958d91970e5 100644 (file)
--- a/src/theory/arith/proof_macros.h
+++ b/src/theory/arith/proof_macros.h
@@ -21,11 +21,11 @@
 #include "options/smt_options.h"
 
 #define ARITH_PROOF(x)        \
-  if (CVC4::options::proof()) \
+  if (CVC4::options::produceProofs()) \
   {                           \
     x;                        \
   }
-#define ARITH_NULLPROOF(x) (CVC4::options::proof()) ? x : NULL
-#define ARITH_PROOF_ON() CVC4::options::proof()
+#define ARITH_NULLPROOF(x) (CVC4::options::produceProofs()) ? x : NULL
+#define ARITH_PROOF_ON() CVC4::options::produceProofs()
 
 #endif  // CVC4__THEORY__ARITH__PROOF_MACROS_H

diff --git a/test/regress/regress1/non-fatal-errors.smt2 b/test/regress/regress1/non-fatal-errors.smt2
index ec3d0292715bb1a0e998d625d038a516b75105b5..f3e2f3fdbf2561f529c1d33be65bbfb0cbea8ab9 100644 (file)
--- a/test/regress/regress1/non-fatal-errors.smt2
+++ b/test/regress/regress1/non-fatal-errors.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success
-; EXPECT: unsupported
+; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success

diff --git a/test/regress/regress1/push-pop/arith_lra_01.smt2 b/test/regress/regress1/push-pop/arith_lra_01.smt2
index 79c95b4ab26487ba288473f988ea95465895996e..02e22d685e3da686026ab7691da97a64c0be1682 100644 (file)
--- a/test/regress/regress1/push-pop/arith_lra_01.smt2
+++ b/test/regress/regress1/push-pop/arith_lra_01.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-proof
+; COMMAND-LINE: --incremental --no-produce-proofs
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat

diff --git a/test/regress/regress1/push-pop/fuzz_3_1.smt2 b/test/regress/regress1/push-pop/fuzz_3_1.smt2
index ad132adcfd2d70e0e7236437e4efb2e8582d3eb2..1f3488b16f2ce1ad303a06c37e04fc1cd15fa128 100644 (file)
--- a/test/regress/regress1/push-pop/fuzz_3_1.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-proof
+; COMMAND-LINE: --incremental --no-produce-proofs
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat

diff --git a/test/regress/regress1/push-pop/fuzz_3_11.smt2 b/test/regress/regress1/push-pop/fuzz_3_11.smt2
index c76a3dfd7e15e4a9ed49d170cfdf53d127894295..4e3ebb62516e9dd67cbe74ffaa453d0bd98ac84d 100644 (file)
--- a/test/regress/regress1/push-pop/fuzz_3_11.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_11.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-proof
+; COMMAND-LINE: --incremental --no-produce-proofs
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat

diff --git a/test/regress/regress1/push-pop/fuzz_3_6.smt2 b/test/regress/regress1/push-pop/fuzz_3_6.smt2
index f645bae0fbd8c008722302784d64325950ac4c1c..4ad68440297b3674aec20f05b818b1ae4daf209e 100644 (file)
--- a/test/regress/regress1/push-pop/fuzz_3_6.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-proof
+; COMMAND-LINE: --incremental --no-produce-proofs
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat

diff --git a/test/regress/regress1/push-pop/fuzz_3_9.smt2 b/test/regress/regress1/push-pop/fuzz_3_9.smt2
index 5afabc868cb70efb77787c1c42fbfc73f2d8c9c6..f7d2ae60e0a0d2a9aad760c8999d343c9ef358f5 100644 (file)
--- a/test/regress/regress1/push-pop/fuzz_3_9.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_9.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-proof
+; COMMAND-LINE: --incremental --no-produce-proofs
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat

diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
index 86d2d7b4e76172e77be231e3ca885e097b9ebee9..68748d4a5cb23ee77f4a7ea5b8f78af343385797 100644 (file)
--- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
+++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-proof
+; COMMAND-LINE: --no-check-unsat-cores --no-produce-proofs
 (set-logic AUFLIRA)
 (set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
 

diff --git a/test/regress/regress1/strings/stoi-400million.smt2 b/test/regress/regress1/strings/stoi-400million.smt2
index 05f7ed213728e7105298fc2b1bd06d00d46c3419..709bd7549bac39f9375a4d340147a29a1c92744a 100644 (file)
--- a/test/regress/regress1/strings/stoi-400million.smt2
+++ b/test/regress/regress1/strings/stoi-400million.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-proof
+; COMMAND-LINE: --strings-exp --no-produce-proofs
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic ALL)

diff --git a/test/regress/regress2/instance_1444.smtv1.smt2 b/test/regress/regress2/instance_1444.smtv1.smt2
index 66984c7428e32a735e28f13abc6cbc3630a97729..47d3fda529d36148cb61b5cb3ae8f8ca5c60c431 100644 (file)
--- a/test/regress/regress2/instance_1444.smtv1.smt2
+++ b/test/regress/regress2/instance_1444.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-proof
+; COMMAND-LINE: --no-produce-proofs
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_UF)