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
#include "expr/lazy_proof.h"
+#include "expr/proof_ensure_closed.h"
+
using namespace CVC4::kind;
namespace CVC4 {
#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"
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
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
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 */
#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 {
#include "prop/prop_proof_manager.h"
+#include "expr/proof_ensure_closed.h"
#include "expr/proof_node_algorithm.h"
namespace CVC4 {
#include "expr/node.h"
#include "expr/node_builder.h"
#include "expr/node_visitor.h"
+#include "expr/proof_ensure_closed.h"
#include "options/bv_options.h"
#include "options/options.h"
#include "options/quantifiers_options.h"
#include "theory/trust_node.h"
+#include "expr/proof_ensure_closed.h"
#include "expr/proof_generator.h"
namespace CVC4 {
projects / cvc5.git / commitdiff