diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-12 02:51:22 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-12 09:51:22 +0100 |
commit | dd89a91a12afb86ae34497f2e8b2ebe95ec377a5 (patch) | |
tree | 30a4bbd74b1eb527e47d8211432fc3d59914fa40 | |
parent | 3b041eff6aea7ac17d47c968405a96a9e6c97680 (diff) |
(proof-new) Option to not automatically consider symmetry in CDProof (#5895)
There are compelling use cases not to automatically introduce SYMM steps in CDProof, e.g. in CDProofs used within ProofNodeUpdater for external conversions.
-rw-r--r-- | src/expr/proof.cpp | 24 | ||||
-rw-r--r-- | src/expr/proof.h | 12 |
2 files changed, 33 insertions, 3 deletions
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 94ca26dd6..1c21a59e7 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -18,8 +18,15 @@ using namespace CVC4::kind; namespace CVC4 { -CDProof::CDProof(ProofNodeManager* pnm, context::Context* c, std::string name) - : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context), d_name(name) +CDProof::CDProof(ProofNodeManager* pnm, + context::Context* c, + std::string name, + bool autoSymm) + : d_manager(pnm), + d_context(), + d_nodes(c ? c : &d_context), + d_name(name), + d_autoSymm(autoSymm) { } @@ -60,6 +67,11 @@ std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact) Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl; return pf; } + else if (!d_autoSymm) + { + Trace("cdproof") << "...not auto considering symmetry" << std::endl; + return pf; + } Node symFact = getSymmFact(fact); if (symFact.isNull()) { @@ -212,6 +224,10 @@ bool CDProof::addStep(Node expected, void CDProof::notifyNewProof(Node expected) { + if (!d_autoSymm) + { + return; + } // ensure SYMM proof is also linked to an existing proof, if it is an // assumption. Node symExpected = getSymmFact(expected); @@ -353,6 +369,10 @@ bool CDProof::hasStep(Node fact) { return true; } + else if (!d_autoSymm) + { + return false; + } Node symFact = getSymmFact(fact); if (symFact.isNull()) { diff --git a/src/expr/proof.h b/src/expr/proof.h index b5bcc7d50..8350b4954 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -134,9 +134,17 @@ namespace CVC4 { class CDProof : public ProofGenerator { public: + /** + * @param pnm The proof node manager responsible for constructor ProofNode + * @param c The context this proof depends on + * @param name The name of this proof (for debugging) + * @param autoSymm Whether this proof automatically adds symmetry steps based + * on policy documented above. + */ CDProof(ProofNodeManager* pnm, context::Context* c = nullptr, - std::string name = "CDProof"); + std::string name = "CDProof", + bool autoSymm = true); virtual ~CDProof(); /** * Make proof for fact. @@ -247,6 +255,8 @@ class CDProof : public ProofGenerator NodeProofNodeMap d_nodes; /** Name identifier */ std::string d_name; + /** Whether we automatically add symmetry steps */ + bool d_autoSymm; /** Ensure fact sym */ std::shared_ptr<ProofNode> getProofSymm(Node fact); /** |