summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/eager_proof_generator.cpp5
-rw-r--r--src/theory/rewriter_tables_template.h2
-rw-r--r--src/theory/theory.cpp8
-rw-r--r--src/theory/theory.h6
-rw-r--r--src/theory/theory_preprocessor.cpp2
-rw-r--r--src/theory/theory_proof_step_buffer.cpp27
-rw-r--r--src/theory/theory_proof_step_buffer.h11
-rw-r--r--src/theory/theory_test_utils.h8
-rw-r--r--src/theory/trust_node.cpp3
9 files changed, 60 insertions, 12 deletions
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index bc101595f..c49c33790 100644
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -30,7 +30,10 @@ EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf)
{
// pf should prove f
- Assert(pf->getResult() == f);
+ Assert(pf->getResult() == f)
+ << "EagerProofGenerator::setProofFor: unexpected result" << std::endl
+ << "Expected: " << f << std::endl
+ << "Actual: " << pf->getResult() << std::endl;
d_proofs[f] = pf;
}
void EagerProofGenerator::setProofForConflict(Node conf,
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 48ae21347..4e350dca9 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -61,7 +61,7 @@ ${post_rewrite_set_cache}
}
}
-Rewriter::Rewriter()
+Rewriter::Rewriter() : d_tpg(nullptr)
{
for (size_t i = 0; i < kind::LAST_KIND; ++i)
{
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 757f94d5b..681f3bca1 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -65,7 +65,6 @@ Theory::Theory(TheoryId id,
d_satContext(satContext),
d_userContext(userContext),
d_logicInfo(logicInfo),
- d_pnm(pnm),
d_facts(satContext),
d_factsHead(satContext, 0),
d_sharedTermsIndex(satContext, 0),
@@ -82,7 +81,8 @@ Theory::Theory(TheoryId id,
d_equalityEngine(nullptr),
d_allocEqualityEngine(nullptr),
d_theoryState(nullptr),
- d_inferManager(nullptr)
+ d_inferManager(nullptr),
+ d_pnm(pnm)
{
smtStatisticsRegistry()->registerStat(&d_checkTime);
smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
@@ -388,13 +388,13 @@ Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
if (in[0].isVar() && isLegalElimination(in[0], in[1])
&& in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
{
- outSubstitutions.addSubstitution(in[0], in[1]);
+ outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
return PP_ASSERT_STATUS_SOLVED;
}
if (in[1].isVar() && isLegalElimination(in[1], in[0])
&& in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
{
- outSubstitutions.addSubstitution(in[1], in[0]);
+ outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
return PP_ASSERT_STATUS_SOLVED;
}
if (in[0].isConst() && in[1].isConst())
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 86dbb60d6..9519624b7 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -123,9 +123,6 @@ class Theory {
/** Information about the logic we're operating within. */
const LogicInfo& d_logicInfo;
- /** Pointer to proof node manager */
- ProofNodeManager* d_pnm;
-
/**
* The assertFact() queue.
*
@@ -237,6 +234,9 @@ class Theory {
*/
TheoryInferenceManager* d_inferManager;
+ /** Pointer to proof node manager */
+ ProofNodeManager* d_pnm;
+
/**
* Returns the next assertion in the assertFact() queue.
*
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 80b824ca0..e7cdb8f2c 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -57,8 +57,6 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
{
if (isProofEnabled())
{
- // enable proofs in the term formula remover
- d_tfr.setProofNodeManager(pnm);
// push the proof context, since proof steps may be cleared on calls to
// clearCache() below.
d_pfContext.push();
diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp
index aa7e10370..5aa909a37 100644
--- a/src/theory/theory_proof_step_buffer.cpp
+++ b/src/theory/theory_proof_step_buffer.cpp
@@ -26,6 +26,33 @@ TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
{
}
+bool TheoryProofStepBuffer::applyEqIntro(Node src,
+ Node tgt,
+ const std::vector<Node>& exp,
+ MethodId ids,
+ MethodId idr)
+{
+ std::vector<Node> args;
+ args.push_back(src);
+ builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
+ Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
+ if (res.isNull())
+ {
+ // failed to apply
+ return false;
+ }
+ // should have concluded the expected equality
+ Node expected = src.eqNode(tgt);
+ if (res != expected)
+ {
+ // did not provide the correct target
+ popStep();
+ return false;
+ }
+ // successfully proved src == tgt.
+ return true;
+}
+
bool TheoryProofStepBuffer::applyPredTransform(Node src,
Node tgt,
const std::vector<Node>& exp,
diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h
index 7a4cb368d..d67781428 100644
--- a/src/theory/theory_proof_step_buffer.h
+++ b/src/theory/theory_proof_step_buffer.h
@@ -37,6 +37,17 @@ class TheoryProofStepBuffer : public ProofStepBuffer
~TheoryProofStepBuffer() {}
//---------------------------- utilities builtin proof rules
/**
+ * Apply equality introduction. If this method returns true, it adds proof
+ * step(s) to the buffer that conclude (= src tgt) from premises exp. In
+ * particular, it may attempt to apply the rule MACRO_SR_EQ_INTRO. This
+ * method should be applied when tgt is equivalent to src assuming exp.
+ */
+ bool applyEqIntro(Node src,
+ Node tgt,
+ const std::vector<Node>& exp,
+ MethodId ids = MethodId::SB_DEFAULT,
+ MethodId idr = MethodId::RW_REWRITE);
+ /**
* Apply predicate transform. If this method returns true, it adds (at most
* one) proof step to the buffer that conclude tgt from premises src, exp. In
* particular, it may attempt to apply MACRO_SR_PRED_TRANSFORM. This method
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 1adaae887..5d2711f1d 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -70,6 +70,8 @@ public:
void safePoint(ResourceManager::Resource r) override {}
void conflict(TNode n) override { push(CONFLICT, n); }
+ void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); }
+
bool propagate(TNode n) override {
push(PROPAGATE, n);
return true;
@@ -81,6 +83,12 @@ public:
return LemmaStatus(Node::null(), 0);
}
+ LemmaStatus trustedLemma(TrustNode n, LemmaProperty p) override
+ {
+ push(LEMMA, n.getNode());
+ return LemmaStatus(Node::null(), 0);
+ }
+
void requirePhase(TNode, bool) override {}
void setIncomplete() override {}
void handleUserAttribute(const char* attr, theory::Theory* t) override {}
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index b0c8f3b79..6c792e355 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -139,7 +139,8 @@ std::string TrustNode::identifyGenerator() const
std::ostream& operator<<(std::ostream& out, TrustNode n)
{
- out << "(" << n.getKind() << " " << n.getProven() << ")";
+ out << "(" << n.getKind() << " " << n.getProven() << " "
+ << n.identifyGenerator() << ")";
return out;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback