Implement equality inference module for arithmetic terms. Optimization for entailment checks. Other minor infrastructure.

10 files changed, 683 insertions, 90 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 77c69c9ec..610bcb305 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -362,6 +362,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/quant_split.cpp \
 	theory/quantifiers/anti_skolem.h \
 	theory/quantifiers/anti_skolem.cpp \
+	theory/quantifiers/equality_infer.h \
+	theory/quantifiers/equality_infer.cpp \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
 	theory/arith/arithvar.h \
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
new file mode 100644
index 000000000..fc3a274ac
--- /dev/null
+++ b/src/theory/quantifiers/equality_infer.cpp
@@ -0,0 +1,235 @@
+/*********************                                                        */
+/*! \file equality_infer.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief  Method for inferring equalities between arithmetic equivalence classes, 
+ **         inspired by "A generalization of Shostak's method for combining decision procedures" Barrett et al. Figure 1.
+ **
+ **/
+
+#include "theory/quantifiers/equality_infer.h"
+#include "theory/quantifiers/quant_util.h"
+#include "context/context_mm.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ) {
+
+}
+
+EqualityInference::EqualityInference( context::Context* c ) : d_c( c ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ){
+  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+}
+
+EqualityInference::~EqualityInference(){
+  for( std::map< Node, EqcInfo * >::iterator it = d_eqci.begin(); it != d_eqci.end(); ++it ){
+    delete it->second;
+  }
+}
+
+void EqualityInference::eqNotifyNewClass(TNode t) {
+  if( t.getType().isReal() ){
+    Trace("eq-infer") << "Notify equivalence class : " << t << std::endl;
+    EqcInfo * eqci;
+    std::map< Node, EqcInfo * >::iterator itec = d_eqci.find( t );
+    if( itec==d_eqci.end() ){
+      eqci = new EqcInfo( d_c );
+      d_eqci[t] = eqci;
+    }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 );
+          }else{
+            children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) );
+          }
+        }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;
+        }
+      }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 );
+          }
+        }        
+      }
+    }else{
+      eqci->d_valid = false;
+    }
+  }
+}
+
+void EqualityInference::addToUseList( Node used, Node eqc ) {
+  NodeListMap::iterator ul_i = d_uselist.find( used );
+  NodeList* ul;
+  if( ul_i != d_uselist.end() ){
+    ul = (*ul_i).second;
+  }else{
+    ul = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
+    d_uselist.insertDataFromContextMemory( used, ul );
+  }
+  Trace("eq-infer-debug") << "      add to use list : " << used << " -> " << eqc << std::endl;
+  (*ul).push_back( eqc );
+}
+
+void EqualityInference::setEqcRep( Node t, Node r, 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 ) );
+    }
+  }
+}
+
+void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
+  Assert( !t1.isNull() );
+  Assert( !t2.isNull() );
+  std::map< Node, EqcInfo * >::iterator itv1 = d_eqci.find( t1 );
+  if( itv1!=d_eqci.end() ){
+    std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 );
+    if( itv2!=d_eqci.end() ){
+      Trace("eq-infer") << "Merge equivalence classes : " << t2 << " into " << t1 << std::endl;
+      Node tr1 = itv1->second->d_rep;
+      Node tr2 = itv2->second->d_rep;
+      itv2->second->d_valid = false;
+      Trace("eq-infer") << "Representatives : " << tr2 << " into " << tr1 << std::endl;
+      if( tr1!=tr2 ){
+        Node eq = tr1.eqNode( tr2 );
+        std::map< Node, Node > msum;
+        if( QuantArith::getMonomialSumLit( eq, msum ) ){
+          Node v_solve;
+          //solve for variables with no coefficient
+          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( !v_solve.isNull() ){
+            //solve for v_solve
+            Node veq;
+            if( QuantArith::isolate( v_solve, msum, veq, kind::EQUAL, true )==1 ){
+              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;
+              
+              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 );
+                }
+              }
+              
+              //go through all equivalence classes that may refer to v_solve
+              std::map< Node, bool > processed;
+              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];
+                  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 ){
+                      std::map< Node, Node > msum2;
+                      if( QuantArith::getMonomialSum( itt->second->d_rep.get(), msum2 ) ){
+                        std::map< Node, Node >::iterator itm = msum2.find( v_solve );
+                        if( itm!=msum2.end() ){
+                          //substitute in solved form
+                          std::map< Node, Node >::iterator itm2 = msum2.find( v_value );
+                          if( itm2 == msum2.end() ){
+                            msum2[v_value] = itm->second;
+                          }else{
+                            msum2[v_value] = NodeManager::currentNM()->mkNode( PLUS, itm2->second.isNull() ? d_one : itm2->second, 
+                                                                                    itm->second.isNull() ? d_one : itm->second );
+                          }
+                          msum2.erase( itm );
+                          Node rr = QuantArith::mkNode( msum2 );
+                          rr = Rewriter::rewrite( rr );
+                          Trace("eq-infer") << "......update " << itt->first << " => " << rr << std::endl;
+                          setEqcRep( itt->first, rr, itt->second );
+                          //update use list
+                          for( unsigned i=0; i<new_use.size(); i++ ){
+                            addToUseList( new_use[i], r );
+                          }
+                        }
+                      }else{
+                        itt->second->d_valid = false;
+                      }
+                    }
+                  }
+                }
+              }
+              Trace("eq-infer") << "...finished solved." << std::endl;
+            }
+          }
+        }
+      }
+    }else{
+      //no information to merge
+    }
+  }else{
+    //carry information (this might happen for non-linear t1 and linear t2?)
+    std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 );
+    if( itv2!=d_eqci.end() ){
+      d_eqci[t1] = d_eqci[t2];
+      d_eqci[t2] = NULL;
+    }
+  }
+}
+
+}
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
new file mode 100644
index 000000000..4a6943119
--- /dev/null
+++ b/src/theory/quantifiers/equality_infer.h
@@ -0,0 +1,77 @@
+/*********************                                                        */
+/*! \file equality_infer.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief additional inference for equalities
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef EQUALITY_INFER_H
+#define EQUALITY_INFER_H
+
+#include <ext/hash_set>
+#include <iostream>
+#include <map>
+#include <vector>
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "context/cdhashset.h"
+#include "theory/theory.h"
+
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class EqualityInference
+{
+  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
+  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
+  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDHashMap< Node, NodeList *, NodeHashFunction > NodeListMap;
+private:
+  context::Context * d_c;
+  Node d_one;
+  class EqcInfo {
+  public:
+    EqcInfo(context::Context* c);
+    ~EqcInfo(){}
+    context::CDO< Node > d_rep;
+    context::CDO< bool > d_valid;
+  };
+
+  /** information necessary for equivalence classes */
+  NodeMap d_elim_vars;
+  std::map< Node, EqcInfo * > d_eqci;
+  NodeMap d_rep_to_eqc;
+  /** set eqc rep */
+  void setEqcRep( Node t, Node r, EqcInfo * eqci );
+  /** use list */
+  NodeListMap d_uselist;
+  void addToUseList( Node used, Node eqc );
+public:
+  EqualityInference(context::Context* c);
+  virtual ~EqualityInference();
+  /** notification when equality engine is updated */
+  void eqNotifyNewClass(TNode t);
+  void eqNotifyMerge(TNode t1, TNode t2);
+  
+  NodeList d_pending_merges;
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index bf91f74c6..3d649f302 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -33,11 +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 ){
-    if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){
+  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( msum.find(Node::null())==msum.end() ){
+      msum[Node::null()] = n;
+      return true;
+    }
   }else{
     if( msum.find(n)==msum.end() ){
       msum[n] = Node::null();
@@ -63,10 +68,7 @@ bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) {
 bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
   if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){
     if( getMonomialSum( lit[0], msum ) ){
-      if( lit[1].isConst() ){
-        if( !lit[1].getConst<Rational>().isZero() ){
-          msum[Node::null()] = negate( lit[1] );
-        }
+      if( lit[1].isConst() && lit[1].getConst<Rational>().isZero() ){
         return true;
       }else{
         //subtract the other side
@@ -90,6 +92,29 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
   return false;
 }
 
+Node QuantArith::mkNode( std::map< Node, Node >& msum ) {
+  std::vector< Node > children;
+  for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+    Node m;
+    if( !it->first.isNull() ){
+      if( !it->second.isNull() ){
+        m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
+      }else{
+        m = it->first;
+      }
+    }else{
+      Assert( !it->second.isNull() );
+      m = it->second;
+    }
+    children.push_back(m);
+  }
+  return children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
+}
+
+// given (msum <k> 0), solve (veq_c * v <k> val) or (val <k> veq_c * v), where:
+// veq_c is either null (meaning 1), or positive.
+// return value -1: veq_c*v is LHS.
+
 int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) {
   std::map< Node, Node >::iterator itv = msum.find( v );
   if( itv!=msum.end() ){
@@ -155,6 +180,58 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Nod
   return ires;
 }
 
+/*
+int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
+  Assert( k==EQUAL || k==GEQ );
+  std::map< Node, Node >::iterator itv = msum.find( v );
+  if( itv!=msum.end() ){
+    Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>();
+    if( r.sgn()!=0 ){
+      veq_c = itv->second;
+      msum.erase( itv );
+      val = mkNode( msum );
+      msum[v] = veq_c;
+      if( !r.isOne() && !r.isNegativeOne() ){
+        if( v.getType().isInteger() ){
+          veq_c = NodeManager::currentNM()->mkConst( r.abs() );
+        }else{
+          val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) );
+          veq_c = Node::null();
+        }
+      }else{
+        veq_c = Node::null();
+      }
+      if( r.sgn()==1 ){
+        val = negate( val );
+      }
+      val = Rewriter::rewrite( val );
+      return ( r.sgn()==1 || k==EQUAL ) ? 1 : -1;
+    }
+  }
+  return 0;
+}
+
+int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) {
+  Node veq_c;
+  Node val;
+  //isolate v in the (in)equality
+  int ires = isolate( v, msum, veq_c, val, k );
+  if( ires!=0 ){
+    Node vc = v;
+    if( !veq_c.isNull() ){
+      if( doCoeff ){
+        vc = NodeManager::currentNM()->mkNode( MULT, veq_c, vc );
+      }else{
+        return 0;
+      }
+    }
+    bool inOrder = ires==1;
+    veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : val, inOrder ? val : vc );
+  }
+  return ires;
+}
+*/
+
 Node QuantArith::solveEqualityFor( Node lit, Node v ) {
   Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
   //first look directly at sides
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index b4cf54dfd..0327651d7 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -36,6 +36,7 @@ public:
   static bool getMonomial( Node n, std::map< Node, Node >& msum );
   static bool getMonomialSum( Node n, std::map< Node, Node >& msum );
   static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
+  static Node mkNode( std::map< Node, Node >& msum );
   //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed
   static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false );
   static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 0d7c9352c..a2ce9c368 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -151,7 +151,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
           Node op = getMatchOperator( n );
           d_op_map[op].push_back( n );
           added.insert( n );
-          
+
           if( options::eagerInstQuant() ){
             for( unsigned i=0; i<n.getNumChildren(); i++ ){
               if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
@@ -205,71 +205,123 @@ void TermDb::computeUfEqcTerms( TNode f ) {
   }
 }
 
-TNode TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep ) {
+//returns a term n' equivalent to n
+//  - if hasSubs = true, then n is consider under substitution subs
+//  - if mkNewTerms = true, then n' is either null, or a term in the master equality engine
+Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited ) {
+  std::map< TNode, Node >::iterator itv = visited.find( n );
+  if( itv != visited.end() ){
+    return itv->second;
+  }
+  Node ret;
   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
   eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
   if( ee->hasTerm( n ) ){
     Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
-    return ee->getRepresentative( n );
+    ret = ee->getRepresentative( n );
   }else if( n.getKind()==BOUND_VARIABLE ){
-    Assert( subs.find( n )!=subs.end() );
-    Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
-    if( subsRep ){
-      Assert( ee->hasTerm( subs[n] ) );
-      Assert( ee->getRepresentative( subs[n] )==subs[n] );
-      return subs[n];
-    }else{
-      return evaluateTerm( subs[n], subs, subsRep );
+    if( hasSubs ){
+      Assert( subs.find( n )!=subs.end() );
+      Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
+      if( subsRep ){
+        Assert( ee->hasTerm( subs[n] ) );
+        Assert( ee->getRepresentative( subs[n] )==subs[n] );
+        ret = subs[n];
+      }else{
+        ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited );
+      }
     }
+  }else if( n.getKind()==FORALL ){
+    ret = n;
   }else{
     if( n.hasOperator() ){
       TNode f = getMatchOperator( n );
-      if( !f.isNull() ){
-        std::vector< TNode > args;
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          TNode c = evaluateTerm( n[i], subs, subsRep );
-          if( c.isNull() ){
-            return TNode::null();
-          }
-          Trace("term-db-eval") << "Got child : " << c << std::endl;
+      std::vector< TNode > args;
+      bool ret_set = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited );
+        if( c.isNull() ){
+          ret = TNode::null();
+          ret_set = true;
+          break;
+        }
+        Trace("term-db-eval") << "Child " << i << " : " << c << std::endl;
+        //short-circuit and/or
+        if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){
+          ret = c;
+          ret_set = true;
+          break;
+        }else{
           args.push_back( c );
         }
-        Trace("term-db-eval") << "Get term from DB" << std::endl;
-        TNode nn = d_func_map_trie[f].existsTerm( args );
-        Trace("term-db-eval") << "Got term " << nn << std::endl;
-        if( !nn.isNull() ){
-          if( ee->hasTerm( nn ) ){
+      }
+      if( !ret_set ){
+        if( !f.isNull() ){
+          Trace("term-db-eval") << "Get term from DB" << std::endl;
+          TNode nn = d_func_map_trie[f].existsTerm( args );
+          Trace("term-db-eval") << "Got term " << nn << std::endl;
+          if( !nn.isNull() && ee->hasTerm( nn ) ){
             Trace("term-db-eval") << "return rep " << std::endl;
-            return ee->getRepresentative( nn );
-          }else{
-            //Assert( false );
+            ret = ee->getRepresentative( nn );
+            ret_set = true;
+          }
+        }
+        if( !ret_set ){
+          //a theory symbol or a new UF term
+          if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+            args.insert( args.begin(), n.getOperator() );
           }
+          ret = NodeManager::currentNM()->mkNode( n.getKind(), args );
+          ret = Rewriter::rewrite( ret );
         }
       }
     }
-    return TNode::null();
   }
+  Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << std::endl;
+  visited[n] = ret;
+  return ret;
 }
 
-TNode TermDb::evaluateTerm( TNode n ) {
+
+TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs ) {
+  Trace("term-db-eval") << "evaluate term : " << n << std::endl;
   eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
   if( ee->hasTerm( n ) ){
-    return ee->getRepresentative( n );
-  }else if( n.getKind()!=BOUND_VARIABLE ){
+    Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
+    return n;
+  }else if( n.getKind()==BOUND_VARIABLE ){
+    if( hasSubs ){
+      Assert( subs.find( n )!=subs.end() );
+      Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
+      if( subsRep ){
+        Assert( ee->hasTerm( subs[n] ) );
+        Assert( ee->getRepresentative( subs[n] )==subs[n] );
+        return subs[n];
+      }else{
+        return evaluateTerm2( subs[n], subs, subsRep, hasSubs );
+      }
+    }
+  }else{
     if( n.hasOperator() ){
       TNode f = getMatchOperator( n );
       if( !f.isNull() ){
         std::vector< TNode > args;
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          TNode c = evaluateTerm( n[i] );
+          TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs );
           if( c.isNull() ){
             return TNode::null();
           }
+          c = ee->getRepresentative( c );
+          Trace("term-db-eval") << "Got child : " << c << std::endl;
           args.push_back( c );
         }
+        Trace("term-db-eval") << "Get term from DB" << std::endl;
         TNode nn = d_func_map_trie[f].existsTerm( args );
+        Trace("term-db-eval") << "Got term " << nn << std::endl;
+        return nn;
         if( !nn.isNull() ){
           if( ee->hasTerm( nn ) ){
+            Trace("term-db-eval") << "return rep " << std::endl;
             return ee->getRepresentative( nn );
           }else{
             //Assert( false );
@@ -281,40 +333,53 @@ TNode TermDb::evaluateTerm( TNode n ) {
   return TNode::null();
 }
 
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) {
+Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms ) {
+  if( mkNewTerms ){
+    std::map< TNode, Node > visited;
+    return evaluateTerm2( n, subs, subsRep, true, visited );
+  }else{
+    return evaluateTerm2( n, subs, subsRep, true );
+  }
+}
+
+Node TermDb::evaluateTerm( TNode n, bool mkNewTerms ) {
+  std::map< TNode, TNode > subs;
+  if( mkNewTerms ){
+    std::map< TNode, Node > visited;
+    return evaluateTerm2( n, subs, false, false, visited );
+  }else{
+    return evaluateTerm2( n, subs, false, false );
+  }
+}
+
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol ) {
   Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
   Assert( n.getType().isBoolean() );
   if( n.getKind()==EQUAL ){
-    TNode n1 = evaluateTerm( n[0], subs, subsRep );
+    TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs );
     if( !n1.isNull() ){
-      TNode n2 = evaluateTerm( n[1], subs, subsRep );
+      TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs );
       if( !n2.isNull() ){
-        eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-        Assert( ee->hasTerm( n1 ) );
-        Assert( ee->hasTerm( n2 ) );
-        if( pol ){
-          return n1==n2 || ee->areEqual( n1, n2 );
+        if( n1==n2 ){
+          return pol;
         }else{
-          return n1!=n2 && ee->areDisequal( n1, n2, false );
+          eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+          Assert( ee->hasTerm( n1 ) );
+          Assert( ee->hasTerm( n2 ) );
+          if( pol ){
+            return ee->areEqual( n1, n2 );
+          }else{
+            return ee->areDisequal( n1, n2, false );
+          }
         }
       }
     }
-  }else if( n.getKind()==APPLY_UF ){
-    TNode n1 = evaluateTerm( n, subs, subsRep );
-    if( !n1.isNull() ){
-      eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-      Assert( ee->hasTerm( n1 ) );
-      TNode n2 = pol ? d_true : d_false;
-      if( ee->hasTerm( n2 ) ){
-        return ee->areEqual( n1, n2 );
-      }
-    }
   }else if( n.getKind()==NOT ){
-    return isEntailed( n[0], subs, subsRep, !pol );
+    return isEntailed( n[0], subs, subsRep, hasSubs, !pol );
   }else if( n.getKind()==OR || n.getKind()==AND ){
     bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( isEntailed( n[i], subs, subsRep, pol ) ){
+      if( isEntailed( n[i], subs, subsRep, hasSubs, pol ) ){
         if( simPol ){
           return true;
         }
@@ -327,16 +392,37 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
     return !simPol;
   }else if( n.getKind()==IFF || n.getKind()==ITE ){
     for( unsigned i=0; i<2; i++ ){
-      if( isEntailed( n[0], subs, subsRep, i==0 ) ){
+      if( isEntailed( n[0], subs, subsRep, hasSubs, i==0 ) ){
         unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
         bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
-        return isEntailed( n[ch], subs, subsRep, reqPol );
+        return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol );
+      }
+    }
+  }else if( n.getKind()==APPLY_UF ){
+    TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs );
+    if( !n1.isNull() ){
+      if( n1==d_true ){
+        return pol;
+      }else if( n1==d_false ){
+        return !pol;
+      }else{
+        eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+        return ee->getRepresentative( n1 ) == ( pol ? d_true : d_false );
       }
     }
   }
   return false;
 }
 
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) {
+  if( d_consistent_ee ){
+    return isEntailed( n, subs, subsRep, true, pol );
+  }else{
+    //don't check entailment wrt an inconsistent ee
+    return false;
+  }
+}
+
 bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   if( !useMode ){
     return d_has_map.find( n )!=d_has_map.end();
@@ -435,7 +521,7 @@ void TermDb::presolve() {
   }
 }
 
-void TermDb::reset( Theory::Effort effort ){
+bool TermDb::reset( Theory::Effort effort ){
   int nonCongruentCount = 0;
   int congruentCount = 0;
   int alreadyCongruentCount = 0;
@@ -444,6 +530,7 @@ void TermDb::reset( Theory::Effort effort ){
   d_arg_reps.clear();
   d_func_map_trie.clear();
   d_func_map_eqc_trie.clear();
+  d_consistent_ee = true;
 
   eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
   //compute has map
@@ -517,6 +604,26 @@ void TermDb::reset( Theory::Effort effort ){
             Trace("term-db-debug") << n << " is redundant." << std::endl;
             congruentCount++;
           }else{
+            if( at!=n && ee->areDisequal( at, n, false ) ){
+              std::vector< Node > lits;
+              lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) );
+              for( unsigned i=0; i<at.getNumChildren(); i++ ){
+                if( at[i]!=n[i] ){
+                  lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() );
+                }
+              }
+              Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
+              if( Trace.isOn("term-db-lemma") ){
+                Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
+                if( !d_quantEngine->getTheoryEngine()->needCheck() ){
+                  Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
+                }
+                Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
+              }
+              d_quantEngine->addLemma( lem );
+              d_consistent_ee = false;
+              return false;
+            }
             nonCongruentCount++;
             d_op_nonred_count[ it->first ]++;
           }
@@ -543,6 +650,7 @@ void TermDb::reset( Theory::Effort effort ){
       }
     }
   }
+  return true;
 }
 
 TermArgTrie * TermDb::getTermArgTrie( Node f ) {
@@ -1914,13 +2022,13 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){
           Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
           qa.d_quant_elim = true;
           //don't set owner, should happen naturally
-        } 
+        }
         if( avar.getAttribute(QuantElimPartialAttribute()) ){
           Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
           qa.d_quant_elim = true;
           qa.d_quant_elim_partial = true;
           //don't set owner, should happen naturally
-        } 
+        }
         if( avar.getKind()==REWRITE_RULE ){
           Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
           Assert( i==0 );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 6b8f9c783..62da8c347 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -174,8 +174,14 @@ private:
   std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
   /** select op map */
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
+  /** whether master equality engine is UF-inconsistent */
+  bool d_consistent_ee;
   /** set has term */
   void setHasTerm( Node n );
+  /** evaluate term */
+  TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs );
+  Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited );
+  bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol );
 public:
   TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
   ~TermDb(){}
@@ -213,7 +219,7 @@ public:
   /** presolve (called once per user check-sat) */
   void presolve();
   /** reset (calculate which terms are active) */
-  void reset( Theory::Effort effort );
+  bool reset( Theory::Effort effort );
   /** get match operator */
   Node getMatchOperator( Node n );
   /** get term arg index */
@@ -228,9 +234,9 @@ public:
   /** evaluate a term under a substitution.  Return representative in EE if possible.
    * subsRep is whether subs contains only representatives
    */
-  TNode evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep );
+  Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false );
   /** same as above, but without substitution */
-  TNode evaluateTerm( TNode n );
+  Node evaluateTerm( TNode n, bool mkNewTerms = false );
   /** is entailed (incomplete check) */
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
   /** has term */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1aeb6f517..86e15485a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -41,6 +41,7 @@
 #include "theory/quantifiers/trigger.h"
 #include "theory/quantifiers/quant_split.h"
 #include "theory/quantifiers/anti_skolem.h"
+#include "theory/quantifiers/equality_infer.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
@@ -97,7 +98,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
     d_presolve_cache(u),
     d_presolve_cache_wq(u),
     d_presolve_cache_wic(u){
-  d_eq_query = new EqualityQueryQuantifiersEngine( this );
+  d_eq_query = new EqualityQueryQuantifiersEngine( c, this );
   d_term_db = new quantifiers::TermDb( c, u, this );
   d_tr_trie = new inst::TriggerTrie;
   d_hasAddedLemma = false;
@@ -411,22 +412,31 @@ void QuantifiersEngine::check( Theory::Effort e ){
       return;
     }
 
-    Trace("quant-engine-debug2") << "Reset term db..." << std::endl;
-    d_eq_query->reset( e );
-    d_term_db->reset( e );
-    if( d_rel_dom ){
-      d_rel_dom->reset();
+    if( Trace.isOn("quant-engine-ee-pre") ){
+      Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
+      debugPrintEqualityEngine( "quant-engine-ee-pre" );
     }
-    d_model->reset_round();
+    Trace("quant-engine-debug2") << "Reset equality engine..." << std::endl;
+    d_eq_query->reset( e );
     
+    if( Trace.isOn("quant-engine-assert") ){
+      Trace("quant-engine-assert") << "Assertions : " << std::endl;
+      getTheoryEngine()->printAssertions("quant-engine-assert");
+    }
     if( Trace.isOn("quant-engine-ee") ){
       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
       debugPrintEqualityEngine( "quant-engine-ee" );
     }
-    if( Trace.isOn("quant-engine-assert") ){
-      Trace("quant-engine-assert") << "Assertions : " << std::endl;
-      getTheoryEngine()->printAssertions("quant-engine-assert");
+    
+    Trace("quant-engine-debug2") << "Reset term database..." << std::endl;
+    if( !d_term_db->reset( e ) ){
+      flushLemmas();
+      return;
     }
+    if( d_rel_dom ){
+      d_rel_dom->reset();
+    }
+    d_model->reset_round();
     
     for( unsigned i=0; i<d_modules.size(); i++ ){
       Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
@@ -549,6 +559,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
 }
 
+void QuantifiersEngine::notifyCombineTheories() {
+  //if allowing theory combination to happen at most once between instantiation rounds
+  //d_ierCounter = 1;
+  //d_ierCounterLastLc = -1;
+}
+
 bool QuantifiersEngine::reduceQuantifier( Node q ) {
   std::map< Node, bool >::iterator it = d_quants_red.find( q );
   if( it==d_quants_red.end() ){
@@ -703,6 +719,29 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
   }
 }
 
+void QuantifiersEngine::eqNotifyNewClass(TNode t) {
+  addTermToDatabase( t );
+  if( d_eq_query->getEqualityInference() ){
+    d_eq_query->getEqualityInference()->eqNotifyNewClass( t );
+  }
+}
+
+void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
+  if( d_eq_query->getEqualityInference() ){
+    d_eq_query->getEqualityInference()->eqNotifyMerge( t1, t2 );
+  }
+}
+
+void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) {
+
+}
+
+void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+  //if( d_qcf ){
+  //  d_qcf->assertDisequal( t1, t2 );
+  //}
+}
+
 void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
     Node n = m.get( i );
@@ -1005,6 +1044,9 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
       Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
       return false;
     }
+    //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
+    //Trace("ajr-temp") << "Instantiation evaluates to : " << std::endl;
+    //Trace("ajr-temp") << "   " << eval << std::endl;
   }
 
   //check for duplication
@@ -1253,6 +1295,19 @@ 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 );
+  }else{
+    d_eq_inference = NULL;
+  }
+}
+
+EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
+  delete d_eq_inference;
+}
+
 void EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
   d_int_rep.clear();
   d_reset_count++;
@@ -1261,9 +1316,11 @@ void EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
 
 void EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
   if( options::inferArithTriggerEq() ){
+    eq::EqualityEngine* ee = getEngine();
+    //naive implementation
+    /*
     std::vector< Node > infer;
     std::vector< Node > infer_exp;
-    eq::EqualityEngine* ee = getEngine();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
     while( !eqcs_i.isFinished() ){
       TNode r = (*eqcs_i);
@@ -1309,6 +1366,18 @@ void EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
       Trace("quant-engine-ee-proc-debug") << "Asserting equality " << infer[i] << std::endl;
       ee->assertEquality( infer[i], true, infer_exp[i] );
     }
+    */
+    //updated implementation
+    while( d_eqi_counter.get()<d_eq_inference->d_pending_merges.size() ){
+      Node eq = d_eq_inference->d_pending_merges[d_eqi_counter.get()];
+      Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << 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;
+    }
     Assert( ee->consistent() );
   }
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 920c45c1a..afde8c996 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -102,6 +102,7 @@ namespace quantifiers {
   class InstStrategyCegqi;
   class QuantDSplit;
   class QuantAntiSkolem;
+  class EqualityInference;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -284,6 +285,8 @@ public:
   void presolve();
   /** check at level */
   void check( Theory::Effort e );
+  /** notify that theories were combined */
+  void notifyCombineTheories();
   /** register quantifier */
   bool registerQuantifier( Node f );
   /** register quantifier */
@@ -348,7 +351,12 @@ public:
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */
-  void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
+  void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );  
+  /** notification when master equality engine is updated */
+  void eqNotifyNewClass(TNode t);
+  void eqNotifyPreMerge(TNode t1, TNode t2);
+  void eqNotifyPostMerge(TNode t1, TNode t2);
+  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   /** get the master equality engine */
   eq::EqualityEngine* getMasterEqualityEngine() ;
   /** debug print equality engine */
@@ -394,6 +402,9 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
 private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
+  /** quantifiers equality inference */
+  quantifiers::EqualityInference * d_eq_inference;
+  context::CDO< unsigned > d_eqi_counter;
   /** internal representatives */
   std::map< TypeNode, std::map< Node, Node > > d_int_rep;
   /** rep score */
@@ -408,8 +419,8 @@ private:
   /** get score */
   int getRepScore( Node n, Node f, int index, TypeNode v_tn );
 public:
-  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
-  ~EqualityQueryQuantifiersEngine(){}
+  EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
+  virtual ~EqualityQueryQuantifiersEngine();
   /** reset */
   void reset( Theory::Effort e );
   /** general queries about equality */
@@ -426,6 +437,8 @@ public:
   Node getInternalRepresentative( Node a, Node f, int index );
   /** flatten representatives */
   void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
+  /** get quantifiers equality inference */
+  quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; }
 }; /* EqualityQueryQuantifiersEngine */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 045af0864..c539315af 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -78,24 +78,26 @@ void TheoryEngine::finishInit() {
 }
 
 void TheoryEngine::eqNotifyNewClass(TNode t){
-  if( d_logicInfo.isQuantified() ){
-    d_quantEngine->addTermToDatabase( t );
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->eqNotifyNewClass( t );
   }
 }
 
 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->eqNotifyPreMerge( t1, t2 );
+  }
 }
 
 void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
-
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->eqNotifyPostMerge( t1, t2 );
+  }
 }
 
 void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
-  if( d_logicInfo.isQuantified() ){
-    if( options::quantConflictFind() ){
-      d_quantEngine->getConflictFind()->assertDisequal( t1, t2 );
-    }
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->eqNotifyDisequal( t1, t2, reason );
   }
 }
 
@@ -405,6 +407,9 @@ void TheoryEngine::check(Theory::Effort effort) {
         // Do the combination
         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
         combineTheories();
+        if(d_logicInfo.isQuantified()){
+          d_quantEngine->notifyCombineTheories();
+        }
       }
     }
 
@@ -419,7 +424,7 @@ void TheoryEngine::check(Theory::Effort effort) {
         // must build model at this point
         d_curr_model_builder->buildModel(d_curr_model, true);
       }
-    Trace("theory::assertions-model") << endl;
+      Trace("theory::assertions-model") << endl;
       if (Trace.isOn("theory::assertions-model")) {
         printAssertions("theory::assertions-model");
       }