diff options
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/expr/lazy_proof.cpp | 2 | ||||
| -rw-r--r-- | src/expr/lazy_proof_chain.cpp | 1 | ||||
| -rw-r--r-- | src/expr/proof_ensure_closed.cpp | 177 | ||||
| -rw-r--r-- | src/expr/proof_ensure_closed.h | 71 | ||||
| -rw-r--r-- | src/expr/proof_generator.cpp | 155 | ||||
| -rw-r--r-- | src/expr/proof_generator.h | 43 | ||||
| -rw-r--r-- | src/expr/proof_node_updater.cpp | 1 |
8 files changed, 254 insertions, 198 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index f0825f180..ea35284fb 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -55,6 +55,8 @@ libcvc4_add_sources( proof.h proof_checker.cpp proof_checker.h + proof_ensure_closed.cpp + proof_ensure_closed.h proof_generator.cpp proof_generator.h proof_node.cpp diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 267da2607..0c209f393 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -14,6 +14,8 @@ #include "expr/lazy_proof.h" +#include "expr/proof_ensure_closed.h" + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index a98ba7453..c58bb78e4 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -15,6 +15,7 @@ #include "expr/lazy_proof_chain.h" #include "expr/proof.h" +#include "expr/proof_ensure_closed.h" #include "expr/proof_node_algorithm.h" #include "options/smt_options.h" diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp new file mode 100644 index 000000000..14b7f06f1 --- /dev/null +++ b/src/expr/proof_ensure_closed.cpp @@ -0,0 +1,177 @@ +/********************* */ +/*! \file proof_ensure_closed.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of debug checks for ensuring proofs are closed + **/ + +#include "expr/proof_ensure_closed.h" + +#include "expr/proof_node_algorithm.h" +#include "options/smt_options.h" + +namespace CVC4 { + +/** + * Ensure closed with respect to assumptions, internal version, which + * generalizes the check for a proof generator or a proof node. + */ +void ensureClosedWrtInternal(Node proven, + ProofGenerator* pg, + ProofNode* pnp, + const std::vector<Node>& assumps, + const char* c, + const char* ctx, + bool reqGen) +{ + if (!options::proofNew()) + { + // proofs not enabled, do not do check + return; + } + bool isTraceDebug = Trace.isOn(c); + if (!options::proofNewEagerChecking() && !isTraceDebug) + { + // trace is off and proof new eager checking is off, do not do check + return; + } + std::stringstream sdiag; + bool isTraceOn = Trace.isOn(c); + if (!isTraceOn) + { + sdiag << ", use -t " << c << " for details"; + } + bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); + if (!dumpProofTraceOn) + { + sdiag << ", use -t dump-proof-error for details on proof"; + } + // get the proof node in question, which is either provided or built by the + // proof generator + std::shared_ptr<ProofNode> pn; + std::stringstream ss; + if (pnp != nullptr) + { + Assert(pg == nullptr); + ss << "ProofNode in context " << ctx; + } + else + { + ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify()) + << " in context " << ctx; + if (pg == nullptr) + { + // only failure if flag is true + if (reqGen) + { + Unreachable() << "...ensureClosed: no generator in context " << ctx + << sdiag.str(); + } + } + else + { + Assert(!proven.isNull()); + pn = pg->getProofFor(proven); + pnp = pn.get(); + } + } + Trace(c) << "=== ensureClosed: " << ss.str() << std::endl; + Trace(c) << "Proven: " << proven << std::endl; + if (pnp == nullptr) + { + if (pg == nullptr) + { + // did not require generator + Assert(!reqGen); + Trace(c) << "...ensureClosed: no generator in context " << ctx + << std::endl; + return; + } + } + // if we don't have a proof node, a generator failed + if (pnp == nullptr) + { + Assert(pg != nullptr); + AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str() + << sdiag.str(); + } + std::vector<Node> fassumps; + expr::getFreeAssumptions(pnp, fassumps); + bool isClosed = true; + std::stringstream ssf; + for (const Node& fa : fassumps) + { + if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end()) + { + isClosed = false; + ssf << "- " << fa << std::endl; + } + } + if (!isClosed) + { + Trace(c) << "Free assumptions:" << std::endl; + Trace(c) << ssf.str(); + if (!assumps.empty()) + { + Trace(c) << "Expected assumptions:" << std::endl; + for (const Node& a : assumps) + { + Trace(c) << "- " << a << std::endl; + } + } + if (dumpProofTraceOn) + { + Trace("dump-proof-error") << " Proof: " << *pnp << std::endl; + } + } + AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str() + << sdiag.str(); + Trace(c) << "...ensureClosed: success" << std::endl; + Trace(c) << "====" << std::endl; +} + +void pfgEnsureClosed(Node proven, + ProofGenerator* pg, + const char* c, + const char* ctx, + bool reqGen) +{ + Assert(!proven.isNull()); + // proof generator may be null + std::vector<Node> assumps; + ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); +} + +void pfgEnsureClosedWrt(Node proven, + ProofGenerator* pg, + const std::vector<Node>& assumps, + const char* c, + const char* ctx, + bool reqGen) +{ + Assert(!proven.isNull()); + // proof generator may be null + ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); +} + +void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx) +{ + ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false); +} + +void pfnEnsureClosedWrt(ProofNode* pn, + const std::vector<Node>& assumps, + const char* c, + const char* ctx) +{ + ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false); +} + +} // namespace CVC4 diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h new file mode 100644 index 000000000..03ee1e717 --- /dev/null +++ b/src/expr/proof_ensure_closed.h @@ -0,0 +1,71 @@ +/********************* */ +/*! \file proof_ensure_closed.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Debug checks for ensuring proofs are closed + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_ENSURE_CLOSED_H +#define CVC4__EXPR__PROOF_ENSURE_CLOSED_H + +#include "expr/node.h" +#include "expr/proof_generator.h" +#include "expr/proof_node.h" + +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 + * is enabled or the Trace c is enabled. + * + * @param reqGen Whether we consider a null generator to be a failure. + */ +void pfgEnsureClosed(Node proven, + ProofGenerator* pg, + const char* c, + const char* ctx, + bool reqGen = true); + +/** + * Debug check closed with Trace c. Context ctx is string for debugging and + * assumps is the set of allowed open assertions. This method throws an + * assertion failure if pg cannot provide a proof for fact proven whose + * free assumptions are contained in assumps. + * + * @param reqGen Whether we consider a null generator to be a failure. + */ +void pfgEnsureClosedWrt(Node proven, + ProofGenerator* pg, + const std::vector<Node>& assumps, + const char* c, + const char* ctx, + bool reqGen = true); + +/** + * Debug check closed with Trace c, proof node versions. This gives an + * assertion failure if pn is not closed. Detailed information is printed + * on trace c. Context ctx is a string used for debugging. + */ +void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx); +/** + * Same as above, but throws an assertion failure only if the free assumptions + * of pn are not contained in assumps. + */ +void pfnEnsureClosedWrt(ProofNode* pn, + const std::vector<Node>& assumps, + const char* c, + const char* ctx); +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_ENSURE_CLOSED_H */ diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index 68a819122..d2206a570 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -70,159 +70,4 @@ bool ProofGenerator::addProofTo(Node f, return false; } -/** - * Ensure closed with respect to assumptions, internal version, which - * generalizes the check for a proof generator or a proof node. - */ -void ensureClosedWrtInternal(Node proven, - ProofGenerator* pg, - ProofNode* pnp, - const std::vector<Node>& assumps, - const char* c, - const char* ctx, - bool reqGen) -{ - if (!options::proofNew()) - { - // proofs not enabled, do not do check - return; - } - bool isTraceDebug = Trace.isOn(c); - if (!options::proofNewEagerChecking() && !isTraceDebug) - { - // trace is off and proof new eager checking is off, do not do check - return; - } - std::stringstream sdiag; - bool isTraceOn = Trace.isOn(c); - if (!isTraceOn) - { - sdiag << ", use -t " << c << " for details"; - } - bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); - if (!dumpProofTraceOn) - { - sdiag << ", use -t dump-proof-error for details on proof"; - } - // get the proof node in question, which is either provided or built by the - // proof generator - std::shared_ptr<ProofNode> pn; - std::stringstream ss; - if (pnp != nullptr) - { - Assert(pg == nullptr); - ss << "ProofNode in context " << ctx; - } - else - { - ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify()) - << " in context " << ctx; - if (pg == nullptr) - { - // only failure if flag is true - if (reqGen) - { - Unreachable() << "...ensureClosed: no generator in context " << ctx - << sdiag.str(); - } - } - else - { - Assert(!proven.isNull()); - pn = pg->getProofFor(proven); - pnp = pn.get(); - } - } - Trace(c) << "=== ensureClosed: " << ss.str() << std::endl; - Trace(c) << "Proven: " << proven << std::endl; - if (pnp == nullptr) - { - if (pg == nullptr) - { - // did not require generator - Assert(!reqGen); - Trace(c) << "...ensureClosed: no generator in context " << ctx - << std::endl; - return; - } - } - // if we don't have a proof node, a generator failed - if (pnp == nullptr) - { - Assert(pg != nullptr); - AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str() - << sdiag.str(); - } - std::vector<Node> fassumps; - expr::getFreeAssumptions(pnp, fassumps); - bool isClosed = true; - std::stringstream ssf; - for (const Node& fa : fassumps) - { - if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end()) - { - isClosed = false; - ssf << "- " << fa << std::endl; - } - } - if (!isClosed) - { - Trace(c) << "Free assumptions:" << std::endl; - Trace(c) << ssf.str(); - if (!assumps.empty()) - { - Trace(c) << "Expected assumptions:" << std::endl; - for (const Node& a : assumps) - { - Trace(c) << "- " << a << std::endl; - } - } - if (dumpProofTraceOn) - { - Trace("dump-proof-error") << " Proof: " << *pnp << std::endl; - } - } - AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str() - << sdiag.str(); - Trace(c) << "...ensureClosed: success" << std::endl; - Trace(c) << "====" << std::endl; -} - -void pfgEnsureClosed(Node proven, - ProofGenerator* pg, - const char* c, - const char* ctx, - bool reqGen) -{ - Assert(!proven.isNull()); - // proof generator may be null - std::vector<Node> assumps; - ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); -} - -void pfgEnsureClosedWrt(Node proven, - ProofGenerator* pg, - const std::vector<Node>& assumps, - const char* c, - const char* ctx, - bool reqGen) -{ - Assert(!proven.isNull()); - // proof generator may be null - ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); -} - -void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx) -{ - ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false); -} - -void pfnEnsureClosedWrt(ProofNode* pn, - const std::vector<Node>& assumps, - const char* c, - const char* ctx) -{ - ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false); -} - } // namespace CVC4 diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 6e6316356..869f226b8 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -107,49 +107,6 @@ class ProofGenerator virtual std::string identify() const = 0; }; -/** - * 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 - * is enabled or the Trace c is enabled. - * - * @param reqGen Whether we consider a null generator to be a failure. - */ -void pfgEnsureClosed(Node proven, - ProofGenerator* pg, - const char* c, - const char* ctx, - bool reqGen = true); - -/** - * Debug check closed with Trace c. Context ctx is string for debugging and - * assumps is the set of allowed open assertions. This method throws an - * assertion failure if pg cannot provide a proof for fact proven whose - * free assumptions are contained in assumps. - * - * @param reqGen Whether we consider a null generator to be a failure. - */ -void pfgEnsureClosedWrt(Node proven, - ProofGenerator* pg, - const std::vector<Node>& assumps, - const char* c, - const char* ctx, - bool reqGen = true); - -/** - * Debug check closed with Trace c, proof node versions. This gives an - * assertion failure if pn is not closed. Detailed information is printed - * on trace c. Context ctx is a string used for debugging. - */ -void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx); -/** - * Same as above, but throws an assertion failure only if the free assumptions - * of pn are not contained in assumps. - */ -void pfnEnsureClosedWrt(ProofNode* pn, - const std::vector<Node>& assumps, - const char* c, - const char* ctx); } // namespace CVC4 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */ diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 834f4381f..af32c223d 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -15,6 +15,7 @@ #include "expr/proof_node_updater.h" #include "expr/lazy_proof.h" +#include "expr/proof_ensure_closed.h" #include "expr/proof_node_algorithm.h" namespace CVC4 { |