Equality engine interface

6 files changed, 49 insertions, 32 deletions

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 102e8b27d..3eaf2c17d 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -42,6 +42,11 @@ void InferProofCons::notifyFact(const InferInfo& ii)
 {
   Trace("strings-ipc-debug")
       << "InferProofCons::notifyFact: " << ii << std::endl;
+  if (d_lazyFactMap.find(ii.d_conc)!=d_lazyFactMap.end())
+  {
+    Trace("strings-ipc-debug") << "...duplicate!" << std::endl;
+    return;
+  }
   std::shared_ptr<InferInfo> iic = std::make_shared<InferInfo>(ii);
   d_lazyFactMap.insert(ii.d_conc, iic);
 }
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index f64aba521..33f4c8f67 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -348,11 +348,13 @@ void InferenceManager::doPendingFacts()
       preProcessFact(fact);
       if (!d_recExplain)
       {
-        // notify fact
-        d_ipc->notifyFact(ii);
         // assert to equality engine using proof generator interface for
         // assertFact.
-        d_pfee->assertFact(fact, cexp, d_ipc.get());
+        if (d_pfee->assertFact(fact, cexp, d_ipc.get()))
+        {
+          // notify fact if the above call asserted a new fact
+          d_ipc->notifyFact(ii);
+        }
       }
       else
       {
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 00ddcbf68..56f081151 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -459,8 +459,14 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, un
 void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) {
   Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
   Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead";
-  assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid);
+  TNode b = polarity ? d_true : d_false;
+  if (hasTerm(t) && areEqual(t,b))
+  {
+    return false;
+  }
+  assertEqualityInternal(t, b, reason, pid);
   propagate();
+  return true;
 }
 
 void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) {
@@ -468,7 +474,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig
   if (polarity) {
     // If two terms are already equal, don't assert anything
     if (hasTerm(eq[0]) && hasTerm(eq[1]) && areEqual(eq[0], eq[1])) {
-      return;
+      return false;
     }
     // Add equality between terms
     assertEqualityInternal(eq[0], eq[1], reason, pid);
@@ -476,7 +482,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig
   } else {
     // If two terms are already dis-equal, don't assert anything
     if (hasTerm(eq[0]) && hasTerm(eq[1]) && areDisequal(eq[0], eq[1], false)) {
-      return;
+      return false;
     }
 
     // notify the theory
@@ -490,7 +496,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig
     propagate();
 
     if (d_done) {
-      return;
+      return true;
     }
 
     // If both have constant representatives, we don't notify anyone
@@ -499,7 +505,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig
     EqualityNodeId aClassId = getEqualityNode(a).getFind();
     EqualityNodeId bClassId = getEqualityNode(b).getFind();
     if (d_isConstant[aClassId] && d_isConstant[bClassId]) {
-      return;
+      return true;
     }
 
     // If we are adding a disequality, notify of the shared term representatives
@@ -551,6 +557,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsig
       }
     }
   }
+  return true;
 }
 
 TNode EqualityEngine::getRepresentative(TNode t) const {
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 366a986db..5d6801c7b 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -809,8 +809,9 @@ public:
    * @param polarity true if asserting the predicate, false if
    *                 asserting the negated predicate
    * @param reason the reason to keep for building explanations
+   * @return true if a new fact was asserted, false if this call was a no-op.
    */
-  void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
+  bool assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Adds an equality eq with the given polarity to the database.
@@ -819,8 +820,9 @@ public:
    * @param polarity true if asserting the equality, false if
    *                 asserting the negated equality
    * @param reason the reason to keep for building explanations
+   * @return true if a new fact was asserted, false if this call was a no-op.
    */
-  void assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
+  bool assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Returns the current representative of the term t.
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index b2bf09219..6838c9568 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -54,13 +54,9 @@ bool ProofEqEngine::assertAssume(TNode lit)
   // explanation. Notice we do not reference count atom/lit.
   if (atom.getKind() == EQUAL)
   {
-    d_ee.assertEquality(atom, polarity, lit);
+    return d_ee.assertEquality(atom, polarity, lit);
   }
-  else
-  {
-    d_ee.assertPredicate(atom, polarity, lit);
-  }
-  return true;
+  return d_ee.assertPredicate(atom, polarity, lit);
 }
 
 bool ProofEqEngine::assertFact(Node lit,
@@ -82,8 +78,7 @@ bool ProofEqEngine::assertFact(Node lit,
 
   // second, assert it to the equality engine
   Node reason = mkAnd(exp);
-  assertFactInternal(atom, polarity, reason);
-  return true;
+  return assertFactInternal(atom, polarity, reason);
 }
 
 bool ProofEqEngine::assertFact(Node lit,
@@ -107,8 +102,7 @@ bool ProofEqEngine::assertFact(Node lit,
   bool polarity = lit.getKind() != NOT;
 
   // second, assert it to the equality engine
-  assertFactInternal(atom, polarity, exp);
-  return true;
+  return assertFactInternal(atom, polarity, exp);
 }
 
 bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
@@ -125,8 +119,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
   bool polarity = lit.getKind() != NOT;
 
   // second, assert it to the equality engine
-  assertFactInternal(atom, polarity, exp);
-  return true;
+  return assertFactInternal(atom, polarity, exp);
 }
 
 bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
@@ -141,8 +134,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
   Node atom = lit.getKind() == NOT ? lit[0] : lit;
   bool polarity = lit.getKind() != NOT;
   // second, assert it to the equality engine
-  assertFactInternal(atom, polarity, exp);
-  return true;
+  return assertFactInternal(atom, polarity, exp);
 }
 
 TrustNode ProofEqEngine::assertConflict(Node lit)
@@ -464,7 +456,11 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
       std::stringstream ss;
       pfConc->printDebug(ss);
       ss << std::endl << "Free assumption: " << a << std::endl;
-      AlwaysAssert(false) << "Generated a non-closed proof: " << ss.str()
+      for (const Node& aprint : ac)
+      {
+        ss << "- assumption: " << aprint << std::endl;
+      }
+      AlwaysAssert(false) << "Generated a proof that is not closed by the scope: " << ss.str()
                           << std::endl;
     }
     if (acu.size() < ac.size())
@@ -563,21 +559,26 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
   return TrustNode::null();
 }
 
-void ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason)
+bool ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason)
 {
   Trace("pfee-debug") << "pfee::assertFactInternal: " << atom << " " << polarity
                       << " " << reason << std::endl;
+  bool ret;
   if (atom.getKind() == EQUAL)
   {
-    d_ee.assertEquality(atom, polarity, reason);
+    ret = d_ee.assertEquality(atom, polarity, reason);
   }
   else
   {
-    d_ee.assertPredicate(atom, polarity, reason);
+    ret = d_ee.assertPredicate(atom, polarity, reason);
+  }
+  if (ret)
+  {
+    // must reference count the new atom and explanation
+    d_keep.insert(atom);
+    d_keep.insert(reason);
   }
-  // must reference count the new atom and explanation
-  d_keep.insert(atom);
-  d_keep.insert(reason);
+  return ret;
 }
 
 bool ProofEqEngine::addProofStep(Node lit,
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 983aec708..9c18eeb25 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -164,7 +164,7 @@ class ProofEqEngine : public EagerProofGenerator
                     const std::vector<Node>& exp,
                     const std::vector<Node>& args);
   /** Assert internal */
-  void assertFactInternal(TNode pred, bool polarity, TNode reason);
+  bool assertFactInternal(TNode pred, bool polarity, TNode reason);
   /** assert lemma internal */
   TrustNode assertLemmaInternal(Node conc,
                                 const std::vector<Node>& exp,