From: Haniel Barbosa Date: Tue, 16 Mar 2021 15:19:46 +0000 (-0300) Subject: [proof-new] Renaming proof option to be in sync with SMT-LIB (#6154) X-Git-Tag: cvc5-1.0.0~2070 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0d3ea6f2dcaf80d386c7765ee8a708c18e3ed574;p=cvc5.git [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 451a6a530..e4a59c8f0 100644 --- 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 c29fe5e50..787a60e78 100644 --- 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 f823ff929..afa1d3ba2 100644 --- 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 32dc2208a..f0b51e6a5 100644 --- 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 b36fe9517..8c27e2bdd 100644 --- 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 935c08e9b..694c73e5e 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::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 bcdcdf623..5ee472b93 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::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 f37b406b4..f2c6c3387 100644 --- 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 3fdf67ed7..aac8ceab7 100644 --- 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& 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 dfb3ddad8..d453285d6 100644 --- 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 ec3d02927..f3e2f3fdb 100644 --- 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 79c95b4ab..02e22d685 100644 --- 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 ad132adcf..1f3488b16 100644 --- 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 c76a3dfd7..4e3ebb625 100644 --- 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 f645bae0f..4ad684402 100644 --- 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 5afabc868..f7d2ae60e 100644 --- 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 86d2d7b4e..68748d4a5 100644 --- 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 05f7ed213..709bd7549 100644 --- 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 66984c742..47d3fda52 100644 --- 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)