fixed inequality checkDisequalities inefficiency

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index 6d2ed0cf683d856fe8546ee9bd4bc6d7d7b6ab79..499d362a96c72c0b52c1c71160927586ccd6d156 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -330,7 +330,7 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
   d_disequalities.push_back(reason);
 
   if (!isRegistered(a) || !isRegistered(b)) {
-    splitDisequality(reason);
+    //splitDisequality(reason);
     return true; 
   }
   TermId id_a = getTermId(a);
@@ -371,7 +371,7 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
       return addInequality(b, a, true, explanation);
     }
     // if none of the terms are constants just add the lemma 
-    splitDisequality(reason);
+    //splitDisequality(reason);
   } else {
     Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n"
                                     << "          " << b << " => " << val_b.toString(10) << "\n"; 
@@ -379,30 +379,13 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
   return true; 
 }
 
-void InequalityGraph::splitDisequality(TNode diseq) {
-  Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << diseq <<"\n"; 
-  Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
-  if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) {
-    d_disequalitiesToSplit.push_back(diseq); 
-  }
-}
-
-void InequalityGraph::getNewLemmas(std::vector<Node>& new_lemmas) {
-  for (unsigned i = d_diseqToSplitIndex; i < d_disequalitiesToSplit.size(); ++i)  {
-    TNode diseq = d_disequalitiesToSplit[i];
-    if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) {
-        TNode a = diseq[0][0];
-        TNode b = diseq[0][1];
-        Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
-        Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
-        Node eq = diseq[0]; 
-        Node lemma = utils::mkNode(kind::OR, a_lt_b, b_lt_a, eq);
-        new_lemmas.push_back(lemma);
-        d_disequalitiesAlreadySplit.insert(diseq); 
-    }
-    d_diseqToSplitIndex = d_diseqToSplitIndex + 1; 
-  }
-}
+// void InequalityGraph::splitDisequality(TNode diseq) {
+//   Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << diseq <<"\n"; 
+//   Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
+//   if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) {
+//     d_disequalitiesToSplit.push_back(diseq); 
+//   }
+// }
 
 void InequalityGraph::backtrack() {
   Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n"; 
@@ -425,7 +408,18 @@ void InequalityGraph::backtrack() {
   }
 }
 
-void InequalityGraph::checkDisequalities() {
+Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) {
+  Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
+  TNode a = diseq[0][0];
+  TNode b = diseq[0][1];
+  Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
+  Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
+  Node eq = diseq[0]; 
+  Node lemma = utils::mkNode(kind::OR, a_lt_b, b_lt_a, eq);
+  return lemma; 
+}
+
+void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) {
   for (CDQueue<TNode>::const_iterator it = d_disequalities.begin(); it != d_disequalities.end(); ++it) {
     if (d_disequalitiesAlreadySplit.find(*it) == d_disequalitiesAlreadySplit.end()) {
       // if we haven't already split on this disequality
@@ -433,8 +427,8 @@ void InequalityGraph::checkDisequalities() {
       TermId a_id = registerTerm(diseq[0][0]);
       TermId b_id = registerTerm(diseq[0][1]);
       if (getValue(a_id) == getValue(b_id)) {
-        // if the disequality is not satisified by the model 
-        d_disequalitiesToSplit.push_back(diseq); 
+        lemmas.push_back(makeDiseqSplitLemma(diseq));
+        d_disequalitiesAlreadySplit.insert(diseq);
       }
     }
   }

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 860302aa4d2a9c9098ecf79ecdd254e6eb7fec50..d402b1561a192f1a993722c1cf8928a93e8aecbd 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -190,7 +190,7 @@ class InequalityGraph : public context::ContextNotifyObj{
    * @param explanation 
    */
   void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation); 
-  void splitDisequality(TNode diseq); 
+  //  void splitDisequality(TNode diseq); 
 
   /**
      Disequality reasoning
@@ -198,11 +198,8 @@ class InequalityGraph : public context::ContextNotifyObj{
   
   /*** The currently asserted disequalities */
   context::CDQueue<TNode> d_disequalities;
-  context::CDQueue<TNode> d_disequalitiesToSplit; 
-  context::CDO<unsigned> d_diseqToSplitIndex; 
-  TNodeSet d_lemmasAdded;
-  TNodeSet d_disequalitiesAlreadySplit; 
-  
+  NodeSet d_disequalitiesAlreadySplit; 
+  Node makeDiseqSplitLemma(TNode diseq); 
   /** Backtracking mechanisms **/
   std::vector<std::pair<TermId, InequalityEdge> > d_undoStack;
   context::CDO<unsigned> d_undoStackIndex; 
@@ -225,8 +222,6 @@ public:
       d_signed(s),
       d_modelValues(c),
       d_disequalities(c),
-      d_disequalitiesToSplit(c),
-      d_diseqToSplitIndex(c, 0),
       d_disequalitiesAlreadySplit(),
       d_undoStack(),
       d_undoStackIndex(c)
@@ -254,18 +249,11 @@ public:
   bool addDisequality(TNode a, TNode b, TNode reason); 
   void getConflict(std::vector<TNode>& conflict);
   virtual ~InequalityGraph() throw(AssertionException) {}
-  /** 
-   * Get any new lemmas (resulting from disequalities splits) that need
-   * to be added. 
-   * 
-   * @param new_lemmas 
-   */
-  void getNewLemmas(std::vector<Node>& new_lemmas);
   /** 
    * Check that the currently asserted disequalities that have not been split on
    * are still true in the current model. 
    */
-  void checkDisequalities();
+  void checkDisequalities(std::vector<Node>& lemmas);
   /** 
    * Return true if a < b is entailed by the current set of assertions. 
    * 

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 5504dbc11e60fe23af09adb7a5dd362eeeb3ecc4..17ac8a2e5b3724f229802da05c1b49199b26bd71 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -83,13 +83,11 @@ bool InequalitySolver::check(Theory::Effort e) {
     return false; 
   }
 
-  // make sure all the disequalities we didn't split on are still satisifed
-  // and split on the ones that are not
-  d_inequalityGraph.checkDisequalities();
-  if (isComplete()) {
-    // if we are complete we want to send out any inequality lemmas 
+  if (isComplete() && Theory::fullEffort(e)) {
+    // make sure all the disequalities we didn't split on are still satisifed
+    // and split on the ones that are not
     std::vector<Node> lemmas;
-    d_inequalityGraph.getNewLemmas(lemmas); 
+    d_inequalityGraph.checkDisequalities(lemmas);
     for(unsigned i = 0; i < lemmas.size(); ++i) {
       d_bv->lemma(lemmas[i]); 
     }