Improvements to equality inference module: add missing cases for solvable variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations. Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort.

6 files changed, 307 insertions, 88 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 04b6e6813..5f23a02e0 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -66,6 +66,8 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false
  consider ground terms within bodies of quantified formulas for matching
 option inferArithTriggerEq --infer-arith-trigger-eq bool :default false
  infer equalities for trigger terms based on solving arithmetic equalities
+option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false
+ record explanations for inferArithTriggerEq
  
 option smartTriggers --smart-triggers bool :default true
  enable smart triggers
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
index f1dbb32fa..e4dbb9c43 100644
--- a/src/theory/quantifiers/equality_infer.cpp
+++ b/src/theory/quantifiers/equality_infer.cpp
@@ -26,13 +26,17 @@ using namespace std;
 
 namespace CVC4 {
 
-EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_rep_exp(c) {
+EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_solved( c, false ), d_master(c)
+//, d_rep_exp(c), d_uselist(c) 
+{
 
 }
 
 EqualityInference::EqualityInference( context::Context* c, bool trackExp ) : 
-d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){
+d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), 
+d_rep_to_eqc( c ), d_rep_exp( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+  d_true = NodeManager::currentNM()->mkConst( true );
 }
 
 EqualityInference::~EqualityInference(){
@@ -41,6 +45,86 @@ EqualityInference::~EqualityInference(){
   }
 }
 
+void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) {
+  if( std::find( exp.begin(), exp.end(), e )==exp.end() ){
+    Trace("eq-infer-debug2") << "......add to explanation " << e << std::endl;
+    exp.push_back( e );
+  }
+}
+
+void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) {
+  NodeListMap::iterator re_i = d_rep_exp.find( eqc );
+  if( re_i!=d_rep_exp.end() ){
+    for( unsigned i=0; i<(*re_i).second->size(); i++ ){
+      addToExplanation( exp, (*(*re_i).second)[i] );
+    }
+  }
+  //for( unsigned i=0; i<d_eqci[n]->d_rep_exp.size(); i++ ){
+  //  addToExplanation( exp, d_eqci[n]->d_rep_exp[i] );
+  //}
+}
+
+void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) {
+  NodeListMap::iterator re_i = d_rep_exp.find( eqc );
+  NodeList* re;
+  if( re_i != d_rep_exp.end() ){
+    re = (*re_i).second;
+  }else{
+    re = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
+    d_rep_exp.insertDataFromContextMemory( eqc, re );
+  }
+  for( unsigned i=0; i<exp_to_add.size(); i++ ){
+    re->push_back( exp_to_add[i] );
+  }
+  //for( unsigned i=0; i<exp_to_add.size(); i++ ){
+  //  eqci->d_rep_exp.push_back( exp_to_add[i] );
+  //}
+}
+
+Node EqualityInference::getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m ) {
+  if( !eqc->d_master.get().isNull() ){
+    if( eqc->d_master.get()==t ){
+      if( !new_m.isNull() && t!=new_m ){
+        eqc->d_master = new_m;
+        updated = true;
+        return new_m;
+      }else{
+        return t;
+      }
+    }else{
+      Assert( d_eqci.find( eqc->d_master.get() )!=d_eqci.end() );
+      EqcInfo * eqc_m = d_eqci[eqc->d_master.get()];
+      Node m = getMaster( eqc->d_master.get(), eqc_m, updated, new_m );
+      eqc->d_master = m;
+      return m;
+    }
+  }else{
+    return Node::null();
+  }
+}
+
+//update the internal "master" representative of the equivalence class, return true if the merge was non-redundant
+bool EqualityInference::updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 ) {
+  bool updated = false;
+  Node m1 = getMaster( t1, eqc1, updated );
+  if( m1.isNull() ){
+    eqc1->d_master = t2;
+    if( eqc2->d_master.get().isNull() ){
+      eqc2->d_master = t2;
+    }
+    return true;
+  }else{
+    updated = false;
+    Node m2 = getMaster( t2, eqc2, updated, m1);
+    if( m2.isNull() ){
+      eqc2->d_master = m1;
+      return true;
+    }else{
+      return updated;
+    }
+  }
+}
+
 void EqualityInference::eqNotifyNewClass(TNode t) {
   if( t.getType().isReal() ){
     Trace("eq-infer") << "Notify equivalence class : " << t << std::endl;
@@ -52,56 +136,74 @@ void EqualityInference::eqNotifyNewClass(TNode t) {
     }else{
       eqci = itec->second;
     }
-    std::map< Node, Node > msum;
-    if( QuantArith::getMonomialSum( t, msum ) ){
-      eqci->d_valid = true;
-      bool changed = false;
-      std::vector< Node > children;
-      for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
-        Node n = it->first;
-        if( !n.isNull() ){
-          NodeMap::const_iterator itv = d_elim_vars.find( n );
-          if( itv!=d_elim_vars.end() ){
-            changed = true;
-            n = (*itv).second;
-          }
-          if( it->second.isNull() ){
-            children.push_back( n );
+    Assert( !eqci->d_valid.get() );
+    if( !eqci->d_solved.get() ){
+      //somewhat strange: t may not be in rewritten form    
+      Node r = Rewriter::rewrite( t );
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSum( r, msum ) ){
+        Trace("eq-infer-debug2") << "...process monomial sum, size = " << msum.size() << std::endl;
+        eqci->d_valid = true;
+        bool changed = false;
+        std::vector< Node > exp;
+        std::vector< Node > children;
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
+          Trace("eq-infer-debug2") << "...process child " << it->first << ", " << it->second << std::endl;
+          if( !it->first.isNull() ){
+            Node n = it->first;
+            BoolMap::const_iterator itv = d_elim_vars.find( n );
+            if( itv!=d_elim_vars.end() ){
+              changed = true;
+              Assert( d_eqci.find( n )!=d_eqci.end() );
+              Assert( n!=t );
+              Assert( d_eqci[n]->d_solved.get() );
+              Trace("eq-infer-debug2") << "......its solved form is " << d_eqci[n]->d_rep.get() << std::endl;
+              if( d_trackExplain ){
+                //track the explanation: justified by explanation for each substitution
+                addToExplanationEqc( exp, n );
+              }
+              n = d_eqci[n]->d_rep;
+              Assert( !n.isNull() );
+            }
+            if( it->second.isNull() ){
+              children.push_back( n );
+            }else{
+              children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) );
+            }
           }else{
-            children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) );
+            Assert( !it->second.isNull() );
+            children.push_back( it->second );
           }
-        }else{
-          children.push_back( it->second );
         }
-      }
-      Node r;
-      bool mvalid = true;
-      if( changed ){
-        r = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
-        r = Rewriter::rewrite( r );
-        msum.clear();
-        if( !QuantArith::getMonomialSum( r, msum ) ){
-          mvalid = false;
+        Trace("eq-infer-debug2") << "...children size = " << children.size() << std::endl;
+        bool mvalid = true;
+        if( changed ){
+          r = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
+          Trace("eq-infer-debug2") << "...pre-rewrite : " << r << std::endl;
+          r = Rewriter::rewrite( r );
+          msum.clear();
+          if( !QuantArith::getMonomialSum( r, msum ) ){
+            mvalid = false;
+          }
+        }
+        Trace("eq-infer") << "...value is " << r << std::endl;
+        setEqcRep( t, r, exp, eqci );
+        if( mvalid ){
+          for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+            if( !it->first.isNull() ){
+              addToUseList( it->first, t );
+            }
+          }        
         }
       }else{
-        r = t;
-      }
-      Trace("eq-infer") << "...value is " << r << std::endl;
-      setEqcRep( t, r, eqci );
-      if( mvalid ){
-        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-          if( !it->first.isNull() ){
-            addToUseList( it->first, t );
-          }
-        }        
+        eqci->d_valid = false;
       }
-    }else{
-      eqci->d_valid = false;
     }
   }
 }
 
 void EqualityInference::addToUseList( Node used, Node eqc ) {
+#if 1
   NodeListMap::iterator ul_i = d_uselist.find( used );
   NodeList* ul;
   if( ul_i != d_uselist.end() ){
@@ -111,26 +213,53 @@ void EqualityInference::addToUseList( Node used, Node eqc ) {
     d_uselist.insertDataFromContextMemory( used, ul );
   }
   Trace("eq-infer-debug") << "      add to use list : " << used << " -> " << eqc << std::endl;
-  (*ul).push_back( eqc );
+  (*ul).push_back( eqc );  
+#else
+  std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used );
+  EqcInfo * eqci_used;
+  if( itu==d_eqci.end() ){
+    eqci_used = new EqcInfo( d_c );
+    d_eqci[used] = eqci_used;
+  }else{
+    eqci_used = itu->second;
+  }
+  Trace("eq-infer-debug") << "      add to use list : " << used << " -> " << eqc << std::endl;
+  eqci_used->d_uselist.push_back( eqc );
+#endif
 }
 
-void EqualityInference::setEqcRep( Node t, Node r, EqcInfo * eqci ) {
+void EqualityInference::setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ) {
   eqci->d_rep = r;
-  NodeMap::const_iterator itr = d_rep_to_eqc.find( r );
-  if( itr==d_rep_to_eqc.end() ){
-    d_rep_to_eqc[r] = t;
-  }else{
-    //merge two equivalence classes
-    Node t2 = (*itr).second;
-    //check if it is valid
-    std::map< Node, EqcInfo * >::iterator itc = d_eqci.find( t2 );
-    if( itc!=d_eqci.end() && itc->second->d_valid ){
-      Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl;
-      Trace("eq-infer") << "  since they both normalize to : " << r << std::endl;
-      d_pending_merges.push_back( t.eqNode( t2 ) );
-      if( d_trackExplain ){
-        //TODO
-        d_pending_merge_exp.push_back( t.eqNode( t2 ) );
+  if( d_trackExplain ){
+    addToExplanationEqc( t, exp_to_add );
+  }
+  //if this is an active equivalence class
+  if( eqci->d_valid.get() ){
+    Trace("eq-infer-debug") << "Set eqc rep " << t << " -> " << r << std::endl;
+    NodeMap::const_iterator itr = d_rep_to_eqc.find( r );
+    if( itr==d_rep_to_eqc.end() ){
+      d_rep_to_eqc[r] = t;
+    }else{
+      //merge two equivalence classes
+      Node t2 = (*itr).second;
+      //check if it is valid
+      std::map< Node, EqcInfo * >::iterator itc = d_eqci.find( t2 );
+      if( itc!=d_eqci.end() && itc->second->d_valid.get() ){
+        //if we haven't already determined they should be merged
+        if( updateMaster( t, t2, eqci, itc->second ) ){
+          Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl;
+          Trace("eq-infer") << "  since they both normalize to : " << r << std::endl;
+          d_pending_merges.push_back( t.eqNode( t2 ) );
+          if( d_trackExplain ){
+            std::vector< Node > exp;
+            for( unsigned j=0; j<2; j++ ){
+              addToExplanationEqc( exp, j==0 ? t : t2 );
+            }
+            Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( AND, exp ) );
+            Trace("eq-infer") << "  explanation : " << exp_n << std::endl;
+            d_pending_merge_exp.push_back( exp_n );
+          }
+        }
       }
     }
   }
@@ -154,13 +283,30 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
         if( QuantArith::getMonomialSumLit( eq, msum ) ){
           Node v_solve;
           //solve for variables with no coefficient
+          if( Trace.isOn("eq-infer-debug2") ){
+            Trace("eq-infer-debug2") << "Monomial sum : " << std::endl;
+            for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
+              Trace("eq-infer-debug2") << "  " << it->first << " * " << it->second << std::endl;
+            }
+          }
           for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
             Node n = it->first;
-            if( !n.isNull() && it->second.isNull() ){
-              v_solve = n;
-              break;
+            if( !n.isNull() ){
+              bool canSolve = false;
+              if( it->second.isNull() ){
+                canSolve = true;
+              }else{
+                //Assert( it->second.isConst() );
+                Rational r = it->second.getConst<Rational>(); 
+                canSolve = r.isOne() || r.isNegativeOne();
+              }
+              if( canSolve ){
+                v_solve = n;
+                break;
+              }
             }
           }
+          Trace("eq-infer-debug") << "solve for variable : " << v_solve << std::endl;
           if( !v_solve.isNull() ){
             //solve for v_solve
             Node veq;
@@ -168,28 +314,61 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
               Node v_value = veq[1];
               Trace("eq-infer") << "...solved " << v_solve << " == " << v_value << std::endl;
               Assert( d_elim_vars.find( v_solve )==d_elim_vars.end() );
-              d_elim_vars[v_solve] = v_value;
-              
+              d_elim_vars[v_solve] = true;
+              //store value in eqc info
+              EqcInfo * eqci_solved;
+              std::map< Node, EqcInfo * >::iterator itec = d_eqci.find( v_solve );
+              if( itec==d_eqci.end() ){
+                eqci_solved = new EqcInfo( d_c );
+                d_eqci[v_solve] =  eqci_solved;
+              }else{
+                eqci_solved = itec->second;
+              }
+              eqci_solved->d_solved = true;
+              eqci_solved->d_rep = v_value;
+              //track the explanation
+              std::vector< Node > exp;
+              if( d_trackExplain ){
+                //explanation is t1 = t2 + their explanations
+                exp.push_back( t1.eqNode( t2 ) );
+                for( unsigned i=0; i<2; i++ ){
+                  addToExplanationEqc( exp, i==0 ? t1 : t2 );
+                }
+                if( Trace.isOn("eq-infer-debug") ){
+                  Trace("eq-infer-debug") << "      explanation for solving " << v_solve << " is ";
+                  for( unsigned i=0; i<exp.size(); i++ ){
+                    Trace("eq-infer-debug") << exp[i] << " ";
+                  }
+                  Trace("eq-infer-debug") << std::endl;
+                }
+                addToExplanationEqc( v_solve, exp );
+              }
+             
               std::vector< Node > new_use;
               for( std::map< Node, Node >::iterator itmm = msum.begin(); itmm != msum.end(); ++itmm ){
                 Node n = itmm->first;
                 if( !n.isNull() && n!=v_solve ){
                   new_use.push_back( n );
+                  addToUseList( n, v_solve );
                 }
               }
               
               //go through all equivalence classes that may refer to v_solve
               std::map< Node, bool > processed;
+              processed[v_solve] = true;
               NodeListMap::iterator ul_i = d_uselist.find( v_solve );
               if( ul_i != d_uselist.end() ){
                 NodeList* ul = (*ul_i).second;
                 Trace("eq-infer-debug") << "      use list size = " << ul->size() << std::endl;
                 for( unsigned j=0; j<ul->size(); j++ ){
                   Node r = (*ul)[j];
+                //Trace("eq-infer-debug") << "      use list size = " << eqci_solved->d_uselist.size() << std::endl;
+                //for( unsigned j=0; j<eqci_solved->d_uselist.size(); j++ ){
+                //  Node r = eqci_solved->d_uselist[j];
                   if( processed.find( r )==processed.end() ){
                     processed[r] = true;
                     std::map< Node, EqcInfo * >::iterator itt = d_eqci.find( r );
-                    if( itt!=d_eqci.end() && itt->second->d_valid ){
+                    if( itt!=d_eqci.end() && ( itt->second->d_valid || itt->second->d_solved ) ){
                       std::map< Node, Node > msum2;
                       if( QuantArith::getMonomialSum( itt->second->d_rep.get(), msum2 ) ){
                         std::map< Node, Node >::iterator itm = msum2.find( v_solve );
@@ -206,7 +385,7 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
                           Node rr = QuantArith::mkNode( msum2 );
                           rr = Rewriter::rewrite( rr );
                           Trace("eq-infer") << "......update " << itt->first << " => " << rr << std::endl;
-                          setEqcRep( itt->first, rr, itt->second );
+                          setEqcRep( itt->first, rr, exp, itt->second );
                           //update use list
                           for( unsigned i=0; i<new_use.size(); i++ ){
                             addToUseList( new_use[i], r );
@@ -238,8 +417,11 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
 }
 
 Node EqualityInference::getPendingMergeExplanation( unsigned i ) { 
-  Assert( d_trackExplain );
-  return d_pending_merge_exp[i]; 
+  if( d_trackExplain ){
+    return d_pending_merge_exp[i]; 
+  }else{
+    return d_pending_merges[i];
+  }
 }  
 
 }
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 2c01c9a80..8c728054e 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -43,30 +43,46 @@ class EqualityInference
 private:
   context::Context * d_c;
   Node d_one;
+  Node d_true;
   class EqcInfo {
   public:
     EqcInfo(context::Context* c);
     ~EqcInfo(){}
     context::CDO< Node > d_rep;
+    //whether the eqc of this info is a representative and d_rep can been computed successfully
     context::CDO< bool > d_valid;
-    //explanation for why d_rep is how it is
-    NodeList d_rep_exp;
+    //whether the eqc of this info is a solved variable
+    context::CDO< bool > d_solved;
+    //master equivalence class (a union find)
+    context::CDO< Node > d_master;
+    //a vector of equalities t1=t2 for which eqNotifyMerge(t1,t2) was called that explains d_rep
+    //NodeList d_rep_exp;
+    //the list of other eqc where this variable may be appear
+    //NodeList d_uselist;
   };
 
   /** track explanations */
   bool d_trackExplain;
   /** information necessary for equivalence classes */
-  NodeMap d_elim_vars;
+  BoolMap d_elim_vars;
   std::map< Node, EqcInfo * > d_eqci;
   NodeMap d_rep_to_eqc;
+  NodeListMap d_rep_exp;
   /** set eqc rep */
-  void setEqcRep( Node t, Node r, EqcInfo * eqci );
+  void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci );
   /** use list */
   NodeListMap d_uselist;
   void addToUseList( Node used, Node eqc );
   /** pending merges */
   NodeList d_pending_merges;
   NodeList d_pending_merge_exp;
+  /** add to explanation */
+  void addToExplanation( std::vector< Node >& exp, Node e );
+  void addToExplanationEqc( std::vector< Node >& exp, Node eqc );
+  void addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add );
+  /** for setting master/slave */
+  Node getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m = Node::null() );
+  bool updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 );
 public:
   //second argument is whether explanations should be tracked
   EqualityInference(context::Context* c, bool trackExp = false);
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index eb92b0f70..5344c0e88 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -33,16 +33,16 @@ bool QuantArith::getMonomial( Node n, Node& c, Node& v ){
   }
 }
 bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) {
-  if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
-    if( msum.find(n[1])==msum.end() ){
-      msum[n[1]] = n[0];
-      return true;
-    }
-  }else if( n.isConst() ){
+  if( n.isConst() ){
     if( msum.find(Node::null())==msum.end() ){
       msum[Node::null()] = n;
       return true;
     }
+  }else if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
+    if( msum.find(n[1])==msum.end() ){
+      msum[n[1]] = n[0];
+      return true;
+    }
   }else{
     if( msum.find(n)==msum.end() ){
       msum[n] = Node::null();
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 01229a171..9e26abfd7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -417,7 +417,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
       debugPrintEqualityEngine( "quant-engine-ee-pre" );
     }
     Trace("quant-engine-debug2") << "Reset equality engine..." << std::endl;
-    d_eq_query->reset( e );
+    if( !d_eq_query->reset( e ) ){
+      flushLemmas();
+      return;
+    }
     
     if( Trace.isOn("quant-engine-assert") ){
       Trace("quant-engine-assert") << "Assertions : " << std::endl;
@@ -1298,7 +1301,7 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
 
 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
   if( options::inferArithTriggerEq() ){
-    d_eq_inference = new quantifiers::EqualityInference( c );
+    d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
   }else{
     d_eq_inference = NULL;
   }
@@ -1308,28 +1311,44 @@ EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
   delete d_eq_inference;
 }
 
-void EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
+bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
   d_int_rep.clear();
   d_reset_count++;
-  processInferences( e );
+  return processInferences( e );
 }
 
-void EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
+bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
   if( options::inferArithTriggerEq() ){
     eq::EqualityEngine* ee = getEngine();
     //updated implementation
     while( d_eqi_counter.get()<d_eq_inference->getNumPendingMerges() ){
       Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() );
+      Node eq_exp = d_eq_inference->getPendingMergeExplanation( d_eqi_counter.get() );
       Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
+      Trace("quant-engine-ee-proc") << "      explanation : " << eq_exp << std::endl;
       Assert( ee->hasTerm( eq[0] ) );
       Assert( ee->hasTerm( eq[1] ) );
-      Assert( !ee->areDisequal( eq[0], eq[1], false ) );
-      //just use itself as an explanation for now (should never be used, since equality engine should be consistent)
-      ee->assertEquality( eq, true, eq );
-      d_eqi_counter = d_eqi_counter.get() + 1;
+      if( ee->areDisequal( eq[0], eq[1], false ) ){
+        Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
+        if( Trace.isOn("term-db-lemma") ){
+          Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
+          if( !d_qe->getTheoryEngine()->needCheck() ){
+            Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
+            //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
+            Assert( false );
+          }
+          Trace("term-db-lemma") << "  add split on : " << eq << std::endl;
+        }
+        d_qe->addSplit( eq );
+        return false;
+      }else{
+        ee->assertEquality( eq, true, eq_exp );
+        d_eqi_counter = d_eqi_counter.get() + 1;
+      }
     }
     Assert( ee->consistent() );
   }
+  return true;
 }
 
 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index afde8c996..06b1c312b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -413,7 +413,7 @@ private:
   int d_reset_count;
 
   /** processInferences : will merge equivalence classes in master equality engine, if possible */
-  void processInferences( Theory::Effort e );
+  bool processInferences( Theory::Effort e );
   /** node contains */
   Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
@@ -422,7 +422,7 @@ public:
   EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
   virtual ~EqualityQueryQuantifiersEngine();
   /** reset */
-  void reset( Theory::Effort e );
+  bool reset( Theory::Effort e );
   /** general queries about equality */
   bool hasTerm( Node a );
   Node getRepresentative( Node a );