summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/options/proof_options.toml23
-rw-r--r--src/proof/lazy_proof_chain.cpp4
-rw-r--r--src/proof/proof_checker.cpp8
-rw-r--r--src/proof/proof_checker.h6
-rw-r--r--src/proof/proof_ensure_closed.cpp2
-rw-r--r--src/proof/proof_node.cpp1
-rw-r--r--src/proof/proof_node.h2
-rw-r--r--src/proof/proof_node_manager.cpp58
-rw-r--r--src/proof/proof_node_manager.h10
-rw-r--r--src/prop/prop_engine.cpp3
-rw-r--r--src/prop/sat_proof_manager.cpp2
-rw-r--r--src/smt/preprocess_proof_generator.cpp2
-rw-r--r--src/smt/proof_final_callback.cpp6
-rw-r--r--src/smt/proof_manager.cpp4
-rw-r--r--src/smt/set_defaults.cpp1
-rw-r--r--src/smt/smt_engine.cpp10
16 files changed, 101 insertions, 41 deletions
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 071f14dec..b741ec5d5 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -39,12 +39,25 @@ name = "Proof"
help = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
[[option]]
- name = "proofEagerChecking"
+ name = "proofCheck"
category = "regular"
- long = "proof-eager-checking"
- type = "bool"
- default = "false"
- help = "check proofs eagerly with proof for local debugging"
+ long = "proof-check=MODE"
+ type = "ProofCheckMode"
+ default = "LAZY"
+ help = "select proof checking mode"
+ help_mode = "Proof checking modes."
+[[option.mode.EAGER]]
+ name = "eager"
+ help = "check rule applications and proofs from generators eagerly for local debugging"
+[[option.mode.EAGER_SIMPLE]]
+ name = "eager-simple"
+ help = "check rule applications during construction"
+[[option.mode.LAZY]]
+ name = "lazy"
+ help = "check rule applications only during final proof construction"
+[[option.mode.NONE]]
+ name = "none"
+ help = "do not check rule applications"
[[option]]
name = "proofGranularityMode"
diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp
index c835ca03d..4cb39cc40 100644
--- a/src/proof/lazy_proof_chain.cpp
+++ b/src/proof/lazy_proof_chain.cpp
@@ -272,8 +272,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::proofEagerChecking() is on
- if (options::proofEagerChecking())
+ // check if chain is closed if eager checking is on
+ if (options::proofCheck() == options::ProofCheckMode::EAGER)
{
Trace("lazy-cdproofchain")
<< "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 1d5aa61b4..28a09fc9c 100644
--- a/src/proof/proof_checker.cpp
+++ b/src/proof/proof_checker.cpp
@@ -85,8 +85,10 @@ ProofCheckerStatistics::ProofCheckerStatistics()
{
}
-ProofChecker::ProofChecker(uint32_t pclevel, rewriter::RewriteDb* rdb)
- : d_pclevel(pclevel), d_rdb(rdb)
+ProofChecker::ProofChecker(bool eagerCheck,
+ uint32_t pclevel,
+ rewriter::RewriteDb* rdb)
+ : d_eagerCheck(eagerCheck), d_pclevel(pclevel), d_rdb(rdb)
{
}
@@ -245,7 +247,7 @@ Node ProofChecker::checkInternal(PfRule id,
}
}
// fails if pedantic level is not met
- if (options::proofEagerChecking())
+ if (d_eagerCheck)
{
std::stringstream serr;
if (isPedanticFailure(id, serr, enableOutput))
diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h
index 6092a1932..a32f23fe4 100644
--- a/src/proof/proof_checker.h
+++ b/src/proof/proof_checker.h
@@ -105,7 +105,9 @@ class ProofCheckerStatistics
class ProofChecker
{
public:
- ProofChecker(uint32_t pclevel = 0, rewriter::RewriteDb* rdb = nullptr);
+ ProofChecker(bool eagerCheck,
+ uint32_t pclevel = 0,
+ rewriter::RewriteDb* rdb = nullptr);
~ProofChecker() {}
/**
* Return the formula that is proven by proof node pn, or null if pn is not
@@ -189,6 +191,8 @@ class ProofChecker
std::map<PfRule, ProofRuleChecker*> d_checker;
/** Maps proof trusted rules to their pedantic level */
std::map<PfRule, uint32_t> d_plevel;
+ /** Whether we check for pedantic failures eagerly */
+ bool d_eagerCheck;
/** The pedantic level of this checker */
uint32_t d_pclevel;
/** Pointer to the rewrite database */
diff --git a/src/proof/proof_ensure_closed.cpp b/src/proof/proof_ensure_closed.cpp
index 774b25ef6..3e91aa799 100644
--- a/src/proof/proof_ensure_closed.cpp
+++ b/src/proof/proof_ensure_closed.cpp
@@ -43,7 +43,7 @@ void ensureClosedWrtInternal(Node proven,
return;
}
bool isTraceDebug = Trace.isOn(c);
- if (!options::proofEagerChecking() && !isTraceDebug)
+ if (options::proofCheck() != options::ProofCheckMode::EAGER && !isTraceDebug)
{
// trace is off and proof new eager checking is off, do not do check
return;
diff --git a/src/proof/proof_node.cpp b/src/proof/proof_node.cpp
index e3affb306..2a141919d 100644
--- a/src/proof/proof_node.cpp
+++ b/src/proof/proof_node.cpp
@@ -23,6 +23,7 @@ namespace cvc5 {
ProofNode::ProofNode(PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args)
+ : d_provenChecked(false)
{
setValue(id, children, args);
}
diff --git a/src/proof/proof_node.h b/src/proof/proof_node.h
index db82cc63d..f4552ae43 100644
--- a/src/proof/proof_node.h
+++ b/src/proof/proof_node.h
@@ -123,6 +123,8 @@ class ProofNode
std::vector<Node> d_args;
/** The cache of the fact that has been proven, modifiable by ProofChecker */
Node d_proven;
+ /** Was d_proven actually checked, or is it trusted? */
+ bool d_provenChecked;
};
inline size_t ProofNodeHashFunction::operator()(
diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index 7e41a9057..a3ef944e0 100644
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -31,6 +31,8 @@ namespace cvc5 {
ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc)
{
d_true = NodeManager::currentNM()->mkConst(true);
+ // we always allocate a proof checker, regardless of the proof checking mode
+ Assert(d_checker != nullptr);
}
std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
@@ -41,7 +43,8 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
{
Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId()
<< "} " << expected << "\n";
- Node res = checkInternal(id, children, args, expected);
+ bool didCheck = false;
+ Node res = checkInternal(id, children, args, expected, didCheck);
if (res.isNull())
{
// if it was invalid, then we return the null node
@@ -51,6 +54,7 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
std::shared_ptr<ProofNode> pn =
std::make_shared<ProofNode>(id, children, args);
pn->d_proven = res;
+ pn->d_provenChecked = didCheck;
return pn;
}
@@ -291,32 +295,49 @@ bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
{
return false;
}
+ // copy whether we did the check
+ pn->d_provenChecked = pnr->d_provenChecked;
// can shortcut re-check of rule
return updateNodeInternal(
pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
}
+void ProofNodeManager::ensureChecked(ProofNode* pn)
+{
+ if (pn->d_provenChecked)
+ {
+ // already checked
+ return;
+ }
+ // directly call the proof checker
+ Node res = d_checker->check(pn, pn->getResult());
+ pn->d_provenChecked = true;
+ // should have the correct result
+ Assert(res == pn->d_proven);
+}
+
Node ProofNodeManager::checkInternal(
PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args,
- Node expected)
+ Node expected,
+ bool& didCheck)
{
- Node res;
- if (d_checker)
+ // if the user supplied an expected result, then we trust it if we are in
+ // a proof checking mode that does not eagerly check rule applications
+ if (!expected.isNull())
{
- // check with the checker, which takes expected as argument
- res = d_checker->check(id, children, args, expected);
- Assert(!res.isNull())
- << "ProofNodeManager::checkInternal: failed to check proof";
- }
- else
- {
- // otherwise we trust the expected value, if it exists
- Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker "
- "or expected value provided";
- res = expected;
+ if (options::proofCheck() == options::ProofCheckMode::LAZY
+ || options::proofCheck() == options::ProofCheckMode::NONE)
+ {
+ return expected;
+ }
}
+ // check with the checker, which takes expected as argument
+ Node res = d_checker->check(id, children, args, expected);
+ didCheck = true;
+ Assert(!res.isNull())
+ << "ProofNodeManager::checkInternal: failed to check proof";
return res;
}
@@ -371,6 +392,7 @@ std::shared_ptr<ProofNode> ProofNodeManager::clone(
visited[cur] = cloned;
// we trust the above cloning does not change what is proven
cloned->d_proven = cur->d_proven;
+ cloned->d_provenChecked = cur->d_provenChecked;
}
}
Assert(visited.find(orig) != visited.end());
@@ -403,7 +425,7 @@ bool ProofNodeManager::updateNodeInternal(
{
Assert(pn != nullptr);
// ---------------- check for cyclic
- if (options::proofEagerChecking())
+ if (options::proofCheck() == options::ProofCheckMode::EAGER)
{
std::unordered_set<const ProofNode*> visited;
for (const std::shared_ptr<ProofNode>& cpc : children)
@@ -436,7 +458,8 @@ bool ProofNodeManager::updateNodeInternal(
if (needsCheck)
{
// We expect to prove the same thing as before
- Node res = checkInternal(id, children, args, pn->d_proven);
+ bool didCheck = false;
+ Node res = checkInternal(id, children, args, pn->d_proven, didCheck);
if (res.isNull())
{
// if it was invalid, then we do not update
@@ -444,6 +467,7 @@ bool ProofNodeManager::updateNodeInternal(
}
// proven field should already be the same as the result
Assert(res == pn->d_proven);
+ pn->d_provenChecked = didCheck;
}
// we update its value
diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h
index 541686a30..928aabb76 100644
--- a/src/proof/proof_node_manager.h
+++ b/src/proof/proof_node_manager.h
@@ -163,6 +163,10 @@ class ProofNodeManager
* unchanged.
*/
bool updateNode(ProofNode* pn, ProofNode* pnr);
+ /**
+ * Ensure that pn is checked, regardless of the proof check format.
+ */
+ void ensureChecked(ProofNode* pn);
/** Get the underlying proof checker */
ProofChecker* getChecker() const;
/**
@@ -193,11 +197,15 @@ class ProofNodeManager
* This throws an assertion error if we fail to check such a proof node, or
* if expected is provided (non-null) and is different what is proven by the
* other arguments.
+ *
+ * The flag didCheck is set to true if the underlying proof checker was
+ * invoked. This may be false if e.g. the proof checking mode is lazy.
*/
Node checkInternal(PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args,
- Node expected);
+ Node expected,
+ bool& didCheck);
/**
* Update node internal, return true if successful. This is called by
* the update node methods above. The argument needsCheck is whether we
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index dd22416db..9060c318c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -220,7 +220,8 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
Assert(ppSkolems.size() == ppLemmas.size());
// do final checks on the lemmas we are about to send
- if (isProofEnabled() && options::proofEagerChecking())
+ if (isProofEnabled()
+ && options::proofCheck() == options::ProofCheckMode::EAGER)
{
Assert(tplemma.getGenerator() != nullptr);
// ensure closed, make the proof node eagerly here to debug
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 8891016a4..da49a5990 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -685,7 +685,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
}
} while (expanded);
// now we should be able to close it
- if (options::proofEagerChecking())
+ if (options::proofCheck() == options::ProofCheckMode::EAGER)
{
std::vector<Node> assumptionsVec;
for (const Node& a : d_assumptions)
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 1eea6286b..1e322ccd3 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -256,7 +256,7 @@ std::string PreprocessProofGenerator::identify() const { return d_name; }
void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
{
- if (options::proofEagerChecking())
+ if (options::proofCheck() == options::ProofCheckMode::EAGER)
{
// catch a pedantic failure now, which otherwise would not be
// triggered since we are doing lazy proof generation
diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
index ae35b346c..93b4cae19 100644
--- a/src/smt/proof_final_callback.cpp
+++ b/src/smt/proof_final_callback.cpp
@@ -59,7 +59,7 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
{
PfRule r = pn->getRule();
// if not doing eager pedantic checking, fail if below threshold
- if (!options::proofEagerChecking())
+ if (options::proofCheck() != options::ProofCheckMode::EAGER)
{
if (!d_pedanticFailure)
{
@@ -70,6 +70,10 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
}
}
}
+ if (options::proofCheck() != options::ProofCheckMode::NONE)
+ {
+ d_pnm->ensureChecked(pn.get());
+ }
uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
if (plevel != 0)
{
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 49f67e94c..ae5de49e9 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -33,7 +33,9 @@ namespace smt {
PfManager::PfManager(Env& env, SmtEngine* smte)
: d_env(env),
- d_pchecker(new ProofChecker(options::proofPedantic())),
+ d_pchecker(new ProofChecker(
+ d_env.getOptions().proof.proofCheck == options::ProofCheckMode::EAGER,
+ d_env.getOptions().proof.proofPedantic)),
d_pnm(new ProofNodeManager(d_pchecker.get())),
d_pppg(new PreprocessProofGenerator(
d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 3c9a82a61..65762a50b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -369,7 +369,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
<< reasonNoProofs.str() << "." << std::endl;
opts.smt.produceProofs = false;
opts.smt.checkProofs = false;
- opts.proof.proofEagerChecking = false;
}
}
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 27e7b8530..5403928ec 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -876,12 +876,14 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
}
// Check that UNSAT results generate a proof correctly.
if (d_env->getOptions().smt.checkProofs
- || d_env->getOptions().proof.proofEagerChecking)
+ || d_env->getOptions().proof.proofCheck
+ == options::ProofCheckMode::EAGER)
{
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
if ((d_env->getOptions().smt.checkProofs
- || d_env->getOptions().proof.proofEagerChecking)
+ || d_env->getOptions().proof.proofCheck
+ == options::ProofCheckMode::EAGER)
&& !d_env->getOptions().smt.produceProofs)
{
throw ModalException(
@@ -1368,7 +1370,7 @@ void SmtEngine::checkProof()
// internal check the proof
PropEngine* pe = getPropEngine();
Assert(pe != nullptr);
- if (d_env->getOptions().proof.proofEagerChecking)
+ if (d_env->getOptions().proof.proofCheck == options::ProofCheckMode::EAGER)
{
pe->checkProof(d_asserts->getAssertionList());
}
@@ -1439,7 +1441,6 @@ std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
// disable all proof options
coreChecker->getOptions().smt.produceProofs = false;
coreChecker->getOptions().smt.checkProofs = false;
- coreChecker->getOptions().proof.proofEagerChecking = false;
for (const Node& ucAssertion : core)
{
@@ -1504,7 +1505,6 @@ void SmtEngine::checkUnsatCore() {
// disable all proof options
coreChecker->getOptions().smt.produceProofs = false;
coreChecker->getOptions().smt.checkProofs = false;
- coreChecker->getOptions().proof.proofEagerChecking = false;
// set up separation logic heap if necessary
TypeNode sepLocType, sepDataType;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback