From 71d72df0437607723256bbd7b4f28cd6c89fe40f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Feb 2021 16:07:16 -0600 Subject: [PATCH] (proof-new) Change proof-new option to proof (#5955) Also moves several proof-specific options to proof_options. --- src/expr/lazy_proof_chain.cpp | 6 +- src/expr/proof_checker.cpp | 14 ++--- src/expr/proof_ensure_closed.cpp | 5 +- src/expr/proof_ensure_closed.h | 2 +- src/expr/proof_node_algorithm.cpp | 2 +- src/expr/proof_node_manager.cpp | 4 +- src/expr/proof_node_to_sexpr.cpp | 2 +- src/expr/proof_node_updater.cpp | 2 +- src/options/proof_options.toml | 38 +++++++++++++ src/options/smt_options.toml | 57 +++---------------- src/preprocessing/passes/ite_removal.cpp | 2 +- .../passes/quantifier_macros.cpp | 4 +- src/prop/minisat/core/Solver.cc | 2 +- src/prop/minisat/minisat.cpp | 2 +- src/prop/prop_engine.cpp | 5 +- src/prop/sat_proof_manager.cpp | 4 +- src/prop/theory_proxy.cpp | 2 +- src/smt/preprocess_proof_generator.cpp | 4 +- src/smt/proof_manager.cpp | 4 +- src/smt/proof_post_processor.cpp | 3 +- src/smt/set_defaults.cpp | 28 ++------- src/smt/smt_engine.cpp | 33 +++++++---- src/theory/arith/congruence_manager.h | 2 +- src/theory/arith/constraint.cpp | 4 +- src/theory/arith/proof_macros.h | 15 ++--- test/regress/regress0/arith/non-normal.smt2 | 2 +- 26 files changed, 117 insertions(+), 131 deletions(-) diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index 665e68d28..2edad1647 100644 --- 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 a60a82b60..dc87d1795 100644 --- 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 14b7f06f1..6eebcd3ec 100644 --- 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 03ee1e717..7b970a71a 100644 --- 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 c3e0aa5b0..2af296813 100644 --- 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 cacd2c101..f5e15f6d6 100644 --- 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 visited; for (const std::shared_ptr& cpc : children) diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp index 71c75ceae..fbfc3e3d4 100644 --- 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 16e339645..e0f096075 100644 --- 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 c744b237b..631a27604 100644 --- 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 ed056ac9f..c29fe5e50 100644 --- 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 0a35e32eb..f788338be 100644 --- 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 eef0326b6..840cb4c66 100644 --- 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 ab3b0cfe7..dbf734a3c 100644 --- 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 c48df4998..d87b6fc45 100644 --- 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 e99e11eb2..738b4dc9c 100644 --- 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 newLemmas; std::vector newSkolems; diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index dd7e94f03..3def16b22 100644 --- 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 assumptionsVec; for (const Node& a : d_assumptions) diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index beb2651bf..3065d6b07 100644 --- 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 cb2887ec0..ef80ebdae 100644 --- 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 b8f68af88..cb7943aed 100644 --- 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 ab8dd8f92..0898096f5 100644 --- 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 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 93196fde4..98fbfe1b3 100644 --- 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 09d54d6d8..941fd111a 100644 --- 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& 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 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 80e1ef8be..8b4d49f90 100644 --- 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 c1db8e55a..02580083b 100644 --- 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& 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 4760760ef..6f24d3601 100644 --- 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 389bd6d2b..ccd0b7634 100644 --- 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) -- 2.30.2