(proof-new) Change proof-new option to proof (#5955)

Also moves several proof-specific options to proof_options.

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 665e68d285d8d67bcf0ba677f5583841c0566e0b..2edad1647778b3956ad1b10d52a8d357d225814d 100644 (file)
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -17,7 +17,7 @@
 #include "expr/proof.h"
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 
 namespace CVC4 {
 
@@ -261,8 +261,8 @@ void LazyCDProofChain::addLazyStep(Node expected,
                              << " set to generator " << pg->identify() << "\n";
   // note this will rewrite the generator for expected, if any
   d_gens.insert(expected, pg);
-  // check if chain is closed if options::proofNewEagerChecking() is on
-  if (options::proofNewEagerChecking())
+  // check if chain is closed if options::proofEagerChecking() is on
+  if (options::proofEagerChecking())
   {
     Trace("lazy-cdproofchain")
         << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";

diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index a60a82b601f3af4ae7d00dbbe6ec6c9c7425bb8e..dc87d1795bba00480e3ad190ae1ad2a89dcab042 100644 (file)
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -15,7 +15,7 @@
 #include "expr/proof_checker.h"
 
 #include "expr/skolem_manager.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "smt/smt_statistics_registry.h"
 
 using namespace CVC4::kind;
@@ -243,7 +243,7 @@ Node ProofChecker::checkInternal(PfRule id,
     }
   }
   // fails if pedantic level is not met
-  if (options::proofNewEagerChecking())
+  if (options::proofEagerChecking())
   {
     std::stringstream serr;
     if (isPedanticFailure(id, serr, enableOutput))
@@ -251,11 +251,11 @@ Node ProofChecker::checkInternal(PfRule id,
       if (enableOutput)
       {
         out << serr.str() << std::endl;
-        if (Trace.isOn("proof-new-pedantic"))
+        if (Trace.isOn("proof-pedantic"))
         {
-          Trace("proof-new-pedantic")
+          Trace("proof-pedantic")
               << "Failed pedantic check for " << id << std::endl;
-          Trace("proof-new-pedantic") << "Expected: " << expected << std::endl;
+          Trace("proof-pedantic") << "Expected: " << expected << std::endl;
           out << "Expected: " << expected << std::endl;
         }
       }
@@ -334,10 +334,10 @@ bool ProofChecker::isPedanticFailure(PfRule id,
         out << "pedantic level for " << id << " not met (rule level is "
             << itp->second << " which is at or below the pedantic level "
             << d_pclevel << ")";
-        bool pedanticTraceEnabled = Trace.isOn("proof-new-pedantic");
+        bool pedanticTraceEnabled = Trace.isOn("proof-pedantic");
         if (!pedanticTraceEnabled)
         {
-          out << ", use -t proof-new-pedantic for details";
+          out << ", use -t proof-pedantic for details";
         }
       }
       return true;

diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
index 14b7f06f15000c94660396da2fb706409275f3c8..6eebcd3ec2777abc28e5c959a111e2c9364a6435 100644 (file)
--- a/src/expr/proof_ensure_closed.cpp
+++ b/src/expr/proof_ensure_closed.cpp
@@ -15,6 +15,7 @@
 #include "expr/proof_ensure_closed.h"
 
 #include "expr/proof_node_algorithm.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 
 namespace CVC4 {
@@ -31,13 +32,13 @@ void ensureClosedWrtInternal(Node proven,
                              const char* ctx,
                              bool reqGen)
 {
-  if (!options::proofNew())
+  if (!options::proof())
   {
     // proofs not enabled, do not do check
     return;
   }
   bool isTraceDebug = Trace.isOn(c);
-  if (!options::proofNewEagerChecking() && !isTraceDebug)
+  if (!options::proofEagerChecking() && !isTraceDebug)
   {
     // trace is off and proof new eager checking is off, do not do check
     return;

diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index 03ee1e71759ca9caf9079b802458925f34888426..7b970a71adea4a11b78b42427705d2defe541325 100644 (file)
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -26,7 +26,7 @@ namespace CVC4 {
 /**
  * Debug check closed on Trace c. Context ctx is string for debugging.
  * This method throws an assertion failure if pg cannot provide a closed
- * proof for fact proven. This is checked only if --proof-new-eager-checking
+ * proof for fact proven. This is checked only if --proof-eager-checking
  * is enabled or the Trace c is enabled.
  *
  * @param reqGen Whether we consider a null generator to be a failure.

diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index c3e0aa5b02738675e636e8f939f89ecb776c75e6..2af2968130ef5eb1d76a18dbee1925cd37aaf258 100644 (file)
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -103,7 +103,7 @@ void getFreeAssumptionsMap(
               != traversing.end())
           {
             Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
-                           "--proof-new-eager-checking)"
+                           "--proof-eager-checking)"
                         << std::endl;
           }
           visit.push_back(cp);

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index cacd2c101695af4f1233569d8ed7b950b06474be..f5e15f6d6aaff2a2fffbfad9596e258bbbba1786 100644 (file)
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/proof.h"
 #include "expr/proof_node_algorithm.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;
@@ -304,7 +304,7 @@ bool ProofNodeManager::updateNodeInternal(
 {
   Assert(pn != nullptr);
   // ---------------- check for cyclic
-  if (options::proofNewEagerChecking())
+  if (options::proofEagerChecking())
   {
     std::unordered_set<const ProofNode*> visited;
     for (const std::shared_ptr<ProofNode>& cpc : children)

diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index 71c75ceaec46e2cae7edc0cda147cf094143742d..fbfc3e3d41d970b66654e7000af3a11c2129728c 100644 (file)
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -56,7 +56,7 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
             != traversing.end())
         {
           Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
-                         "--proof-new-eager-checking)"
+                         "--proof-eager-checking)"
                       << std::endl;
           return Node::null();
         }

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index 16e339645a7dedecf9849e6ba07d80123c741e6e..e0f09607523e3e7af354d8330fcafb75572ca761 100644 (file)
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -156,7 +156,7 @@ void ProofNodeUpdater::processInternal(
         {
           Unhandled()
               << "ProofNodeUpdater::processInternal: cyclic proof! (use "
-                 "--proof-new-eager-checking)"
+                 "--proof-eager-checking)"
               << std::endl;
         }
         visit.push_back(cp);

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index c744b237bd725a69b5bceb69b65fb79c8c6d3dec..631a27604d6c539cd947c935eaf1bd2f0c55001d 100644 (file)
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -10,3 +10,41 @@ header = "options/proof_options.h"
   default    = "false"
   read_only  = true
   help       = "Print conclusion of proof steps when printing AST"
+
+[[option]]
+  name       = "proofPedantic"
+  category   = "regular"
+  long       = "proof-pedantic=N"
+  type       = "uint32_t"
+  default    = "0"
+  read_only  = true
+  help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
+
+[[option]]
+  name       = "proofEagerChecking"
+  category   = "regular"
+  long       = "proof-eager-checking"
+  type       = "bool"
+  default    = "false"
+  help       = "check proofs eagerly with proof for local debugging"
+
+[[option]]
+  name       = "proofGranularityMode"
+  category   = "regular"
+  long       = "proof-granularity=MODE"
+  type       = "ProofGranularityMode"
+  default    = "THEORY_REWRITE"
+  help       = "modes for proof granularity"
+  help_mode  = "Modes for proof granularity."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not improve the granularity of proofs."
+[[option.mode.REWRITE]]
+  name = "rewrite"
+  help = "Allow rewrite or substitution steps, expand macros."
+[[option.mode.THEORY_REWRITE]]
+  name = "theory-rewrite"
+  help = "Allow theory rewrite steps, expand macros, rewrite and substitution steps."
+[[option.mode.DSL_REWRITE]]
+  name = "dsl-rewrite"
+  help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index ed056ac9f4dda466f536352e2402a273e1bbc9db..c29fe5e502a26fba248d32699899e9f10994eb49 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -131,67 +131,28 @@ header = "options/smt_options.h"
   help = "Block models based on the concrete model values for the free variables."
 
 [[option]]
-  name       = "dumpProofs"
-  category   = "regular"
-  long       = "dump-proofs"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "output proofs after every UNSAT/VALID response"
-
-[[option]]
-  name       = "proofNew"
+  name       = "proof"
   category   = "regular"
-  long       = "proof-new"
+  long       = "proof"
   type       = "bool"
   default    = "false"
-  help       = "do proof production using the new infrastructure"
+  help       = "produce proofs, support check-proofs and get-proof"
 
 [[option]]
-  name       = "proofNewPedantic"
-  category   = "regular"
-  long       = "proof-new-pedantic=N"
-  type       = "uint32_t"
-  default    = "0"
-  read_only  = true
-  help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof-new"
-
-[[option]]
-  name       = "proofNewEagerChecking"
+  name       = "dumpProofs"
   category   = "regular"
-  long       = "proof-new-eager-checking"
+  long       = "dump-proofs"
   type       = "bool"
   default    = "false"
   read_only  = true
-  help       = "check proofs eagerly with proof-new for local debugging"
-
-[[option]]
-  name       = "proofGranularityMode"
-  category   = "regular"
-  long       = "proof-granularity=MODE"
-  type       = "ProofGranularityMode"
-  default    = "THEORY_REWRITE"
-  help       = "modes for proof granularity"
-  help_mode  = "Modes for proof granularity."
-[[option.mode.OFF]]
-  name = "off"
-  help = "Do not improve the granularity of proofs."
-[[option.mode.REWRITE]]
-  name = "rewrite"
-  help = "allow rewrite or substitution steps, expand macros."
-[[option.mode.THEORY_REWRITE]]
-  name = "theory-rewrite"
-  help = "allow theory rewrite steps, expand macros, rewrite and substitution steps."
-[[option.mode.DSL_REWRITE]]
-  name = "dsl-rewrite"
-  help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."
+  help       = "output proofs after every UNSAT/VALID response"
 
 [[option]]
-  name       = "checkProofsNew"
+  name       = "checkProofs"
   category   = "regular"
-  long       = "check-proofs-new"
+  long       = "check-proofs"
   type       = "bool"
-  help       = "after UNSAT/VALID, check the generated proof (with proof-new)"
+  help       = "after UNSAT/VALID, check the generated proof (with proof)"
 
 [[option]]
   name       = "dumpInstantiations"

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 0a35e32eb4319c965a549423fb2d793f039ed8b7..f788338be263849c002fafc75ae89a2e1b734936 100644 (file)
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -57,7 +57,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::proofNew())
+      if (options::unsatCores() && !options::proof())
       {
         ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
                                                  assertion);

diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index eef0326b6895a27a7ef0bd7df5f5cfd5855776ab..840cb4c6601a483fb7bae9938afb423dd1b8004b 100644 (file)
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -81,7 +81,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::proofNew()
+        if (options::unsatCores() && !options::proof()
             && std::find(macro_assertions.begin(),
                          macro_assertions.end(),
                          assertions[i])
@@ -107,7 +107,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::proofNew())
+          if (options::unsatCores() && !options::proof())
           {
             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 ab3b0cfe7adbbcb0241e2e0de91ed9cfc08d997d..dbf734a3c3b21f001cb0ad73631f6da64ed03281 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -55,7 +55,7 @@ namespace {
  */
 bool assertionLevelOnly()
 {
-  return (options::proofNew() || options::unsatCores())
+  return (options::proof() || options::unsatCores())
          && options::incrementalSolving();
 }
 

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index c48df499869fd2d9410026778a1bff4a43f79d13..d87b6fc4572c0f075d6653141afaafc0e8cb882f 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::proofNew()
+  Assert(!options::unsatCores() || options::proof()
          || clause_id != ClauseIdError);
   return clause_id;
 }

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e99e11eb22e728f0e3c5473154da2e616a7cca01..738b4dc9c7732c5eb46f1969c63431f9d07164c3 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -27,6 +27,7 @@
 #include "options/decision_options.h"
 #include "options/main_options.h"
 #include "options/options.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 #include "prop/cnf_stream.h"
@@ -36,7 +37,6 @@
 #include "prop/theory_proxy.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
-#include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
@@ -205,7 +205,7 @@ void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
   Assert(ppSkolems.size() == ppLemmas.size());
 
   // do final checks on the lemmas we are about to send
-  if (isProofEnabled() && options::proofNewEagerChecking())
+  if (isProofEnabled() && options::proofEagerChecking())
   {
     Assert(tplemma.getGenerator() != nullptr);
     // ensure closed, make the proof node eagerly here to debug
@@ -444,7 +444,6 @@ Node PropEngine::ensureLiteral(TNode n)
 
 Node PropEngine::getPreprocessedTerm(TNode n)
 {
-  Node rewritten = theory::Rewriter::rewrite(n);
   // must preprocess
   std::vector<theory::TrustNode> newLemmas;
   std::vector<Node> newSkolems;

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index dd7e94f0398e879b66acbd3c1197b6d3c2752738..3def16b227d8512d683c6b3dd9c6473d5f4a471e 100644 (file)
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -15,7 +15,7 @@
 #include "prop/sat_proof_manager.h"
 
 #include "expr/proof_node_algorithm.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
 #include "theory/theory_proof_step_buffer.h"
@@ -650,7 +650,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
     }
   } while (expanded);
   // now we should be able to close it
-  if (options::proofNewEagerChecking())
+  if (options::proofEagerChecking())
   {
     std::vector<Node> assumptionsVec;
     for (const Node& a : d_assumptions)

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index beb2651bf614f7c73b73b1efdb07ca61b408e571..3065d6b07dcfcb54f47c9d038f632cb6a8610a7f 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::proofNew())
+  if (CVC4::options::proof())
   {
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index cb2887ec0640b5f0a83104448e29d5d64a711d13..ef80ebdae374bde2d6ecc12f8e39e9b34f844fcc 100644 (file)
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -16,7 +16,7 @@
 #include "smt/preprocess_proof_generator.h"
 
 #include "expr/proof.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -235,7 +235,7 @@ std::string PreprocessProofGenerator::identify() const { return d_name; }
 
 void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
 {
-  if (options::proofNewEagerChecking())
+  if (options::proofEagerChecking())
   {
     // catch a pedantic failure now, which otherwise would not be
     // triggered since we are doing lazy proof generation

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index b8f68af8848bd3b9a865b30d29a70b3b92bb6c7c..cb7943aedff72695a46f66233bb4347a797f7a43 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/proof_node_algorithm.h"
 #include "options/base_options.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "smt/assertions.h"
 #include "smt/defined_function.h"
 
@@ -24,7 +24,7 @@ namespace CVC4 {
 namespace smt {
 
 PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
-    : d_pchecker(new ProofChecker(options::proofNewPedantic())),
+    : d_pchecker(new ProofChecker(options::proofPedantic())),
       d_pnm(new ProofNodeManager(d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
           d_pnm.get(), u, "smt::PreprocessProofGenerator")),

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index ab8dd8f92d9751f55e160fcf90c3de4356bbc8d2..0898096f5dc6a0b94ff8a54cffec750a3cf60bec 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -15,6 +15,7 @@
 #include "smt/proof_post_processor.h"
 
 #include "expr/skolem_manager.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "smt/smt_engine.h"
@@ -1110,7 +1111,7 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
 {
   PfRule r = pn->getRule();
   // if not doing eager pedantic checking, fail if below threshold
-  if (!options::proofNewEagerChecking())
+  if (!options::proofEagerChecking())
   {
     if (!d_pedanticFailure)
     {

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 93196fde4ee644aec2aa15cbaa78f841f5a65c65..98fbfe1b3009b8b154109e1580b28aee0c6ec637 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -73,7 +73,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   if (options::checkUnsatCoresNew())
   {
-    options::proofNew.set(true);
+    options::proof.set(true);
   }
   if (options::bitvectorAigSimplifications.wasSetByUser())
   {
@@ -872,16 +872,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   if (options::ufHo())
   {
-    // if higher-order, disable proof production
-    if (options::proofNew())
-    {
-      if (options::proofNew.wasSetByUser())
-      {
-        Warning() << "SmtEngine: turning off proof production (not yet "
-                     "supported with --uf-ho)\n";
-      }
-      options::proofNew.set(false);
-    }
     // if higher-order, then current variants of model-based instantiation
     // cannot be used
     if (options::mbqiMode() != options::MbqiMode::NONE)
@@ -1095,16 +1085,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::nlExtTangentPlanes.set(true);
     }
-    // not compatible with proofs
-    if (options::proofNew())
-    {
-      if (options::proofNew.wasSetByUser())
-      {
-        Notice() << "SmtEngine: setting proof-new to false to support SyGuS"
-                 << std::endl;
-      }
-      options::proofNew.set(false);
-    }
   }
   // counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
@@ -1394,10 +1374,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
         "division. "
         "Try --bv-div-zero-const to interpret division by zero as a constant.");
   }
-  // !!!!!!!!!!!!!!!! temporary, until proof-new is functional
-  if (options::proofNew())
+  // !!!!!!!!!!!!!!!! temporary, until proofs are functional
+  if (options::proof())
   {
-    throw OptionException("--proof-new is not yet supported.");
+    throw OptionException("--proof is not yet supported.");
   }
 
   if (logic == LogicInfo("QF_UFNRA"))

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 09d54d6d82c83559271a05c78960e7c0025e0f8f..941fd111a4a68c5dceb204cf649be805b0d897b6 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -22,11 +22,13 @@
 #include "base/modal_exception.h"
 #include "base/output.h"
 #include "decision/decision_engine.h"
+#include "expr/bound_var_manager.h"
 #include "expr/node.h"
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
 #include "options/printer_options.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
@@ -56,10 +58,10 @@
 #include "smt/unsat_core_manager.h"
 #include "theory/quantifiers/instantiation_list.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 #include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
 #include "util/random.h"
 #include "util/resource_manager.h"
 
@@ -222,8 +224,11 @@ void SmtEngine::finishInit()
   d_optm->finishInit(d_logic, d_isInternalSubsolver);
 
   ProofNodeManager* pnm = nullptr;
-  if (options::proofNew())
+  if (options::proof())
   {
+    // ensure bound variable uses canonical bound variables
+    d_nodeManager->getBoundVarManager()->enableKeepCacheValues();
+    // make the proof manager
     d_pfManager.reset(new PfManager(getUserContext(), this));
     PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
     // start the unsat core manager
@@ -979,15 +984,15 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate a proof correctly.
-    if (options::checkProofsNew() || options::proofNewEagerChecking())
+    if (options::checkProofs() || options::proofEagerChecking())
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
-        if ((options::checkProofsNew() || options::proofNewEagerChecking())
-            && !options::proofNew())
+        if ((options::checkProofs() || options::proofEagerChecking())
+            && !options::proof())
         {
           throw ModalException(
-              "Cannot check-proofs-new because proof-new was disabled.");
+              "Cannot check-proofs because proofs were disabled.");
         }
         checkProof();
       }
@@ -1398,13 +1403,17 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
 void SmtEngine::checkProof()
 {
-  Assert(options::proofNew());
+  Assert(options::proof());
   // internal check the proof
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
+  if (options::proofEagerChecking())
+  {
+    pe->checkProof(d_asserts->getAssertionList());
+  }
   Assert(pe->getProof() != nullptr);
   std::shared_ptr<ProofNode> pePfn = pe->getProof();
-  if (options ::checkProofsNew())
+  if (options::checkProofs())
   {
     d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
   }
@@ -1458,7 +1467,7 @@ void SmtEngine::checkUnsatCore() {
   initializeSubsolver(coreChecker);
   coreChecker->getOptions().set(options::checkUnsatCores, false);
   // disable all proof options
-  coreChecker->getOptions().set(options::proofNew, false);
+  coreChecker->getOptions().set(options::proof, false);
   coreChecker->getOptions().set(options::checkUnsatCoresNew, false);
 
   // set up separation logic heap if necessary
@@ -1536,9 +1545,9 @@ std::string SmtEngine::getProof()
         getOutputManager().getDumpOut());
   }
 #if IS_PROOFS_BUILD
-  if (!options::proofNew())
+  if (!options::proof())
   {
-    throw ModalException("Cannot get a proof when proof-new option is off.");
+    throw ModalException("Cannot get a proof when proof option is off.");
   }
   if (d_state->getMode() != SmtMode::UNSAT)
   {
@@ -1637,7 +1646,7 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (options::proofNew() && getSmtMode() == SmtMode::UNSAT)
+  if (options::proof() && getSmtMode() == SmtMode::UNSAT)
   {
     // TODO (project #37): minimize instantiations based on proof manager
   }

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 80e1ef8befed32065b0539f4b323be3ebd151a35..8b4d49f90c0e80f4ea9c24a08029c475b3845815 100644 (file)
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -166,7 +166,7 @@ private:
    *   * assertionToEqualityEngine(..)
    *   * equalsConstant(c)
    *   * equalsConstant(lb, ub)
-   * If proofNew is off, then just asserts.
+   * If proof is off, then just asserts.
    */
   void assertLitToEqualityEngine(Node lit,
                                  TNode reason,

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index c1db8e55a6d9e3263ad573cbc06fe2f20e815591..02580083b1b36e7ff800892307e9b8904e5325d8 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -1081,7 +1081,7 @@ TrustNode Constraint::split()
   Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode;
 
   TrustNode trustedLemma;
-  if (options::proofNew())
+  if (d_database->isProofEnabled())
   {
     // Farkas proof that this works.
     auto nm = NodeManager::currentNM();
@@ -2068,7 +2068,7 @@ void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
   Node la = a->getLiteral();
   Node lb = b->getLiteral();
   Node orN = (la < lb) ? la.orNode(lb) : lb.orNode(la);
-  if (options::proofNew())
+  if (isProofEnabled())
   {
     Assert(b->getNegation()->getType() != ConstraintType::Disequality);
     auto nm = NodeManager::currentNM();

diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h
index 4760760efbb3ab05896b599df958b762745f93d2..6f24d3601fd30b76fcef2e24ec18defffc2ae9f5 100644 (file)
--- a/src/theory/arith/proof_macros.h
+++ b/src/theory/arith/proof_macros.h
@@ -20,15 +20,12 @@
 
 #include "options/smt_options.h"
 
-#define ARITH_PROOF(x)                                      \
-  if (CVC4::options::proofNew())                            \
-  {                                                         \
-    x;                                                      \
+#define ARITH_PROOF(x)        \
+  if (CVC4::options::proof()) \
+  {                           \
+    x;                        \
   }
-#define ARITH_NULLPROOF(x)                                  \
-  (CVC4::options::proofNew())                               \
-      ? x                                                   \
-      : NULL
-#define ARITH_PROOF_ON() CVC4::options::proofNew()
+#define ARITH_NULLPROOF(x) (CVC4::options::proof()) ? x : NULL
+#define ARITH_PROOF_ON() CVC4::options::proof()
 
 #endif  // CVC4__THEORY__ARITH__PROOF_MACROS_H

diff --git a/test/regress/regress0/arith/non-normal.smt2 b/test/regress/regress0/arith/non-normal.smt2
index 389bd6d2bf88953db8e92191eecfed9f7459fc78..ccd0b7634e9b58ca06bf943df8a3e7d303b95692 100644 (file)
--- a/test/regress/regress0/arith/non-normal.smt2
+++ b/test/regress/regress0/arith/non-normal.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --proof-new-eager-checking
+; COMMAND-LINE: --proof-eager-checking
 ; EXPECT: sat
 (set-logic QF_UFLRA)
 (declare-fun v1 () Real)