Minor

7 files changed, 39 insertions, 12 deletions

diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index cb15761ab..3d331588d 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -158,4 +158,24 @@ bool LazyCDProof::hasGenerators() const
   return !d_gens.empty() || d_defaultGen != nullptr;
 }
 
+bool LazyCDProof::hasGenerator(Node fact) const
+{
+  if (d_defaultGen!=nullptr)
+  {
+    return true;
+  }
+  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
+  if (it != d_gens.end())
+  {
+    return true;
+  }
+  if (fact.getKind() != EQUAL || fact[0] == fact[1])
+  {
+    return false;
+  }
+  Node factSym = fact[1].eqNode(fact[0]);
+  it = d_gens.find(factSym);
+  return it != d_gens.end();
+}
+
 }  // namespace CVC4
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 1a0e6adf8..72a789216 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -52,6 +52,8 @@ class LazyCDProof : public CDProof
                    bool forceOverwrite = false);
   /** Does this have any proof generators? */
   bool hasGenerators() const;
+  /** Does the given fact have a generator? */
+  bool hasGenerator(Node fact) const;
 
  protected:
   typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
diff --git a/src/theory/builtin/proof_kinds b/src/theory/builtin/proof_kinds
index b2dc6f33b..404dfbc06 100644
--- a/src/theory/builtin/proof_kinds
+++ b/src/theory/builtin/proof_kinds
@@ -148,7 +148,7 @@ macro MACRO_SR_PRED_TRANSFORM 1: 1:2 {
 
 // ======== Untrustworthy theory lemma
 // Children: none
-// Arguments: (tid)
+// Arguments: (F, tid)
 // ---------------------------------------------------------------
 // Conclusion: F
 // where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
diff --git a/src/theory/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp
index 43f0038d6..4f35a7639 100644
--- a/src/theory/proof_engine_output_channel.cpp
+++ b/src/theory/proof_engine_output_channel.cpp
@@ -88,6 +88,7 @@ bool ProofEngineOutputChannel::addTheoryLemmaStep(Node f)
   Assert(!f.isNull());
   std::vector<Node> children;
   std::vector<Node> args;
+  args.push_back(f);
   unsigned tid = static_cast<unsigned>(d_theory);
   Node tidn = NodeManager::currentNM()->mkConst(Rational(tid));
   args.push_back(tidn);
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index cc8ef016e..2df13d1a8 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -986,7 +986,6 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
 
   // The terms must be there already
   Assert(hasTerm(t1) && hasTerm(t2));
-  ;
 
   // Get the ids
   EqualityNodeId t1Id = getNodeId(t1);
@@ -1007,7 +1006,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
     Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end())
         << "Don't ask for stuff I didn't notify you about";
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
-
+    if (eqp) {
+      Debug("pf::ee") << "Deq reason for "<< eqp->d_node << " " << reasonRef.d_mergesStart << "..." << reasonRef.d_mergesEnd << std::endl;
+    }
     for (unsigned i = reasonRef.d_mergesStart; i < reasonRef.d_mergesEnd; ++i)
     {
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
@@ -1016,6 +1017,7 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
       // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x.
       if (eqp && toExplain.first != toExplain.second) {
         eqpc = std::make_shared<EqProof>();
+        Debug("pf::ee") << "Deq getExplanation #" << i << " for " << eqp->d_node << " : " << toExplain.first << " " << toExplain.second << std::endl;
       }
 
       getExplanation(
@@ -1074,6 +1076,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
         Assert(eqp->d_node[0][1].isConst());
         eqp->d_id = MERGED_THROUGH_CONSTANTS;
       } else if (eqp->d_children.size() == 1) {
+        Trace("ajr-temp") << "Simplifying " << eqp->d_children[0]->d_node << " from " << eqp->d_node << std::endl;
+        // FIXME
         // The transitivity proof has just one child. Simplify.
         std::shared_ptr<EqProof> temp = eqp->d_children[0];
         eqp->d_children.clear();
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index d621f0b35..3ba250714 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -213,7 +213,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
   {
     PRefProofGenerator prg(&d_proof);
     LazyCDProof tmpProof(d_pnm, &prg);
-    CDProof* curr;
+    LazyCDProof* curr;
     if (conc == d_false)
     {
       curr = &d_proof;
@@ -246,7 +246,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
   {
     PRefProofGenerator prg(&d_proof);
     LazyCDProof tmpProof(d_pnm, &prg);
-    CDProof* curr;
+    LazyCDProof* curr;
     if (conc == d_false)
     {
       curr = &d_proof;
@@ -281,7 +281,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
   {
     PRefProofGenerator prg(&d_proof);
     LazyCDProof tmpProof(d_pnm, &prg);
-    CDProof* curr;
+    LazyCDProof* curr;
     if (conc == d_false)
     {
       curr = &d_proof;
@@ -327,7 +327,7 @@ std::string ProofEqEngine::identify() const
 TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
                                              const std::vector<Node>& exp,
                                              const std::vector<Node>& noExplain,
-                                             CDProof* curr)
+                                             LazyCDProof* curr)
 {
   // We are a conflict if the conclusion is false and all literals are
   // explained.
@@ -357,7 +357,7 @@ TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
 TrustNode ProofEqEngine::ensureProofForFact(Node conc,
                                             const std::vector<TNode>& assumps,
                                             TrustNodeKind tnk,
-                                            CDProof* curr)
+                                            LazyCDProof* curr)
 {
   Trace("pfee-proof") << std::endl;
   Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
@@ -604,7 +604,7 @@ bool ProofEqEngine::addProofStep(Node lit,
 
 void ProofEqEngine::explainWithProof(Node lit,
                                      std::vector<TNode>& assumps,
-                                     CDProof* curr)
+                                     LazyCDProof* curr)
 {
   if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end())
   {
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 8acc13d7b..2ff846a63 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -169,12 +169,12 @@ class ProofEqEngine : public EagerProofGenerator
   TrustNode assertLemmaInternal(Node conc,
                                 const std::vector<Node>& exp,
                                 const std::vector<Node>& noExplain,
-                                CDProof* curr);
+                                LazyCDProof* curr);
   /** ensure proof for fact */
   TrustNode ensureProofForFact(Node conc,
                                const std::vector<TNode>& assumps,
                                TrustNodeKind tnk,
-                               CDProof* curr);
+                               LazyCDProof* curr);
   /**
    * Make the conjunction of nodes in a. Returns true if a is empty, and a
    * single literal if a has size 1.
@@ -219,7 +219,7 @@ class ProofEqEngine : public EagerProofGenerator
    * This additionally registers the equality proof steps required to
    * regress the explanation of lit.
    */
-  void explainWithProof(Node lit, std::vector<TNode>& assumps, CDProof* curr);
+  void explainWithProof(Node lit, std::vector<TNode>& assumps, LazyCDProof* curr);
 };
 
 }  // namespace eq