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

6 files changed, 571 insertions, 67 deletions

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 */