(proof-new) Miscellaneous minor improvements and fixes to proofs in theory files...

diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index bc101595f3a2fa013cc73a495d47960381ec0bed..c49c33790e65607d414133051697651361e944ce 100644 (file)
--- 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 48ae21347219254eedd0ed171eca3f77dd3dbccf..4e350dca95377063cf57b8c93020252358cd77d3 100644 (file)
--- 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 757f94d5bcb4da146e06cb8dde3aca9b9487a8f0..681f3bca1b0ee58fad4fd5ab758a6a3348316949 100644 (file)
--- 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 86dbb60d644129d29d3d0df797ce0fa7e209c6b2..9519624b771603d54d187162b08afcf7a7a2596e 100644 (file)
--- 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 80b824ca0234563f6c0c3a879fa0bd88930b270a..e7cdb8f2c353f7db8c708cff7cd112213b4d6db9 100644 (file)
--- 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 aa7e10370955ea4a885b302f65c4e52242981d53..5aa909a375c3a907dba0602e03a69c6d1636bc5b 100644 (file)
--- 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 7a4cb368d37612f07a772ff363d93a227e283bcc..d67781428b0067ecbf774988c59ebdd93a4b7f0b 100644 (file)
--- a/src/theory/theory_proof_step_buffer.h
+++ b/src/theory/theory_proof_step_buffer.h
@@ -36,6 +36,17 @@ class TheoryProofStepBuffer : public ProofStepBuffer
   TheoryProofStepBuffer(ProofChecker* pc = nullptr);
   ~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

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 1adaae887cac79b8a5379e59acf907f486d49eac..5d2711f1def786fb530d3b7cb72c6458f2c9b0f4 100644 (file)
--- 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 b0c8f3b79147b353576ceb7f0b7c0b0c90077772..6c792e35527dd3d8897185cebdc5c446c21f43a6 100644 (file)
--- 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;
 }