summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/preprocess_proof_generator.cpp117
-rw-r--r--src/smt/preprocess_proof_generator.h24
-rw-r--r--src/smt/proof_manager.cpp4
-rw-r--r--src/smt/proof_manager.h2
-rw-r--r--src/smt/smt_engine.cpp2
5 files changed, 115 insertions, 34 deletions
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 5c7ed0356..1739a4e7d 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -21,15 +21,24 @@
namespace CVC4 {
namespace smt {
-PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm)
- : d_pnm(pnm)
+PreprocessProofGenerator::PreprocessProofGenerator(context::UserContext* u,
+ ProofNodeManager* pnm)
+ : d_pnm(pnm), d_src(u), d_helperProofs(u)
{
}
void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
{
- Trace("smt-proof-pp-debug") << "- notifyNewAssert: " << n << std::endl;
- d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
+ Trace("smt-proof-pp-debug")
+ << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl;
+ if (d_src.find(n) == d_src.end())
+ {
+ d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
+ }
+ else
+ {
+ Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
+ }
}
void PreprocessProofGenerator::notifyPreprocessed(Node n,
@@ -40,14 +49,22 @@ void PreprocessProofGenerator::notifyPreprocessed(Node n,
if (n != np)
{
Trace("smt-proof-pp-debug")
- << "- notifyPreprocessed: " << n << "..." << np << std::endl;
- d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg);
+ << "PreprocessProofGenerator::notifyPreprocessed: " << n << "..." << np
+ << std::endl;
+ if (d_src.find(np) == d_src.end())
+ {
+ d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg);
+ }
+ else
+ {
+ Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
+ }
}
}
std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
{
- std::map<Node, theory::TrustNode>::iterator it = d_src.find(f);
+ NodeTrustNodeMap::iterator it = d_src.find(f);
if (it == d_src.end())
{
// could be an assumption, return nullptr
@@ -56,67 +73,102 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
// make CDProof to construct the proof below
CDProof cdp(d_pnm);
+ Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: input " << f
+ << std::endl;
Node curr = f;
std::vector<Node> transChildren;
+ std::unordered_set<Node, NodeHashFunction> processed;
bool success;
+ // we connect the proof of f to its source via the map d_src until we
+ // discover that its source is a preprocessing lemma (a lemma stored in d_src)
+ // or otherwise it is assumed to be an input assumption.
do
{
success = false;
if (it != d_src.end())
{
- Assert(it->second.getNode() == curr);
+ Assert((*it).second.getNode() == curr);
+ // get the proven node
+ Node proven = (*it).second.getProven();
+ Assert(!proven.isNull());
+ Trace("smt-pppg") << "...process proven " << proven << std::endl;
+ if (processed.find(proven) != processed.end())
+ {
+ Unhandled() << "Cyclic steps in preprocess proof generator";
+ continue;
+ }
+ processed.insert(proven);
bool proofStepProcessed = false;
- std::shared_ptr<ProofNode> pfr = it->second.toProofNode();
+
+ // if a generator for the step was provided, it is stored in the proof
+ Trace("smt-pppg") << "...get provided proof" << std::endl;
+ std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
if (pfr != nullptr)
{
- Assert(pfr->getResult() == it->second.getProven());
+ Trace("smt-pppg") << "...add provided" << std::endl;
+ Assert(pfr->getResult() == proven);
cdp.addProof(pfr);
proofStepProcessed = true;
}
- if (it->second.getKind() == theory::TrustNodeKind::REWRITE)
+ Trace("smt-pppg") << "...update" << std::endl;
+ theory::TrustNodeKind tnk = (*it).second.getKind();
+ if (tnk == theory::TrustNodeKind::REWRITE)
{
- Node eq = it->second.getProven();
- Assert(eq.getKind() == kind::EQUAL);
+ Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl;
+ Assert(proven.getKind() == kind::EQUAL);
if (!proofStepProcessed)
{
// maybe its just a simple rewrite?
- if (eq[1] == theory::Rewriter::rewrite(eq[0]))
+ if (proven[1] == theory::Rewriter::rewrite(proven[0]))
{
- cdp.addStep(eq, PfRule::REWRITE, {}, {eq[0]});
+ cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]});
proofStepProcessed = true;
}
}
- transChildren.push_back(eq);
+ transChildren.push_back(proven);
// continue with source
- curr = eq[0];
+ curr = proven[0];
success = true;
// find the next node
it = d_src.find(curr);
}
else
{
- Assert(it->second.getKind() == theory::TrustNodeKind::LEMMA);
+ Trace("smt-pppg") << "...lemma" << std::endl;
+ Assert(tnk == theory::TrustNodeKind::LEMMA);
}
if (!proofStepProcessed)
{
- // add trusted step
- Node proven = it->second.getProven();
- cdp.addStep(proven, PfRule::PREPROCESS, {}, {proven});
+ Trace("smt-pppg") << "...add missing step" << std::endl;
+ // add trusted step, the rule depends on the kind of trust node
+ cdp.addStep(proven,
+ tnk == theory::TrustNodeKind::LEMMA
+ ? PfRule::PREPROCESS_LEMMA
+ : PfRule::PREPROCESS,
+ {},
+ {proven});
}
}
} while (success);
- Assert(curr != f);
- // prove ( curr == f )
- Node fullRewrite = curr.eqNode(f);
- if (transChildren.size() >= 2)
+ // prove ( curr == f ), which is not necessary if they are the same
+ // modulo symmetry.
+ if (!CDProof::isSame(f, curr))
{
- cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
+ Node fullRewrite = curr.eqNode(f);
+ if (transChildren.size() >= 2)
+ {
+ Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
+ std::reverse(transChildren.begin(), transChildren.end());
+ cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
+ }
+ Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
+ // prove f
+ cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
+ Trace("smt-pppg") << "...finished" << std::endl;
}
- // prove f
- cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
// overall, proof is:
// --------- from proof generator ---------- from proof generator
@@ -130,6 +182,15 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
return cdp.getProofFor(f);
}
+ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
+
+LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
+{
+ std::shared_ptr<LazyCDProof> helperPf = std::make_shared<LazyCDProof>(d_pnm);
+ d_helperProofs.push_back(helperPf);
+ return helperPf.get();
+}
+
std::string PreprocessProofGenerator::identify() const
{
return "PreprocessProofGenerator";
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 5319071f0..b71187188 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -19,8 +19,12 @@
#include <map>
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "expr/lazy_proof.h"
#include "expr/proof_generator.h"
#include "expr/proof_node_manager.h"
+#include "theory/eager_proof_generator.h"
#include "theory/trust_node.h"
namespace CVC4 {
@@ -41,8 +45,11 @@ namespace smt {
*/
class PreprocessProofGenerator : public ProofGenerator
{
+ typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction>
+ NodeTrustNodeMap;
+
public:
- PreprocessProofGenerator(ProofNodeManager* pnm);
+ PreprocessProofGenerator(context::UserContext* u, ProofNodeManager* pnm);
~PreprocessProofGenerator() {}
/**
* Notify that n is a new assertion, where pg can provide a proof of n.
@@ -61,6 +68,17 @@ class PreprocessProofGenerator : public ProofGenerator
std::shared_ptr<ProofNode> getProofFor(Node f) override;
/** Identify */
std::string identify() const override;
+ /** Get the proof manager */
+ ProofNodeManager* getManager();
+ /**
+ * Allocate a helper proof. This returns a fresh lazy proof object that
+ * remains alive in this user context. This feature is used to construct
+ * helper proofs for preprocessing, e.g. to support the skeleton of proofs
+ * that connect AssertionPipeline::conjoin steps.
+ *
+ * Internally, this adds a LazyCDProof to the list d_helperProofs below.
+ */
+ LazyCDProof* allocateHelperProof();
private:
/** The proof node manager */
@@ -72,7 +90,9 @@ class PreprocessProofGenerator : public ProofGenerator
* (1) A trust node REWRITE proving (n_src = n) for some n_src, or
* (2) A trust node LEMMA proving n.
*/
- std::map<Node, theory::TrustNode> d_src;
+ NodeTrustNodeMap d_src;
+ /** A context-dependent list of LazyCDProof, allocated for conjoin steps */
+ context::CDList<std::shared_ptr<LazyCDProof> > d_helperProofs;
};
} // namespace smt
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index f51a116b7..df7b6bf4d 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -22,10 +22,10 @@
namespace CVC4 {
namespace smt {
-PfManager::PfManager(SmtEngine* smte)
+PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
: d_pchecker(new ProofChecker(options::proofNewPedantic())),
d_pnm(new ProofNodeManager(d_pchecker.get())),
- d_pppg(new PreprocessProofGenerator(d_pnm.get())),
+ d_pppg(new PreprocessProofGenerator(u, d_pnm.get())),
d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())),
d_finalProof(nullptr)
{
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index bda741a05..118b82bec 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -41,7 +41,7 @@ class Assertions;
class PfManager
{
public:
- PfManager(SmtEngine* smte);
+ PfManager(context::UserContext* u, SmtEngine* smte);
~PfManager();
/**
* Print the proof on the output channel of the current options in scope.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3caf03946..755822d2a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -270,7 +270,7 @@ void SmtEngine::finishInit()
ProofNodeManager* pnm = nullptr;
if (options::proofNew())
{
- d_pfManager.reset(new PfManager(this));
+ d_pfManager.reset(new PfManager(getUserContext(), this));
// use this proof node manager
pnm = d_pfManager->getProofNodeManager();
// enable proof support in the rewriter
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback