summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/proof_ensure_closed.cpp2
-rw-r--r--src/options/smt_options.toml4
-rw-r--r--src/preprocessing/passes/ite_removal.cpp2
-rw-r--r--src/preprocessing/passes/quantifier_macros.cpp4
-rw-r--r--src/prop/minisat/core/Solver.cc2
-rw-r--r--src/prop/minisat/minisat.cpp2
-rw-r--r--src/prop/theory_proxy.cpp2
-rw-r--r--src/smt/set_defaults.cpp4
-rw-r--r--src/smt/smt_engine.cpp15
-rw-r--r--src/theory/arith/proof_macros.h6
-rw-r--r--test/regress/regress1/non-fatal-errors.smt22
-rw-r--r--test/regress/regress1/push-pop/arith_lra_01.smt22
-rw-r--r--test/regress/regress1/push-pop/fuzz_3_1.smt22
-rw-r--r--test/regress/regress1/push-pop/fuzz_3_11.smt22
-rw-r--r--test/regress/regress1/push-pop/fuzz_3_6.smt22
-rw-r--r--test/regress/regress1/push-pop/fuzz_3_9.smt22
-rw-r--r--test/regress/regress1/quantifiers/symmetric_unsat_7.smt22
-rw-r--r--test/regress/regress1/strings/stoi-400million.smt22
-rw-r--r--test/regress/regress2/instance_1444.smtv1.smt22
19 files changed, 30 insertions, 31 deletions
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<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 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback