Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

7 files changed, 592 insertions, 5 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index a029bc97b..b1e8855c7 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -36,7 +36,9 @@ libarith_la_SOURCES = \
 	theory_arith.h \
 	theory_arith.cpp \
 	dio_solver.h \
-	dio_solver.cpp
+	dio_solver.cpp \
+	theory_arith_instantiator.h \
+	theory_arith_instantiator.cpp
 
 EXTRA_DIST = \
 	kinds
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 5f49ab3ab..63a370f9a 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -73,7 +73,12 @@ private:
         d_acm.propagate(t1.eqNode(t2));
       }
     }
-   };
+
+    void eqNotifyNewClass(TNode t) { }
+    void eqNotifyPreMerge(TNode t1, TNode t2) { }
+    void eqNotifyPostMerge(TNode t1, TNode t2) { }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+  };
   ArithCongruenceNotify d_notify;
 
   context::CDList<Node> d_keepAlive;
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 8ffe68376..c06cbc140 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -6,6 +6,7 @@
 
 theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h"
 typechecker "theory/arith/theory_arith_type_rules.h"
+instantiator ::CVC4::theory::arith::InstantiatorTheoryArith "theory/arith/theory_arith_instantiator.h"
 
 properties stable-infinite
 properties check propagate staticLearning presolve notifyRestart
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ac9796986..9ff9ceeb9 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -53,8 +53,8 @@ namespace arith {
 const uint32_t RESET_START = 2;
 
 
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_ARITH, c, u, out, valuation, logicInfo),
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
+  Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
   d_hasDoneWorkSinceCut(false),
   d_learner(d_pbSubstitutions),
   d_setupLiteralCallback(this),
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ebc131b60..1f0120387 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -53,12 +53,15 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class InstantiatorTheoryArith;
+
 /**
  * Implementation of QF_LRA.
  * Based upon:
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArith : public Theory {
+  friend class InstantiatorTheoryArith;
 private:
   bool rowImplication(ArithVar v, bool upperBound, const DeltaRational& r);
 
@@ -269,7 +272,7 @@ private:
   DeltaRational getDeltaValue(TNode n);
 
 public:
-  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   virtual ~TheoryArith();
 
   /**
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
new file mode 100644
index 000000000..48c8a30ee
--- /dev/null
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -0,0 +1,448 @@
+/*********************                                                        */
+/*! \file instantiator_arith_instantiator.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of instantiator_arith_instantiator class
+ **/
+
+#include "theory/arith/theory_arith_instantiator.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+#define ARITH_INSTANTIATOR_USE_DELTA
+#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
+#define ARITH_INSTANTIATOR_STRONG_DELTA_LEMMA
+
+#define USE_ARITH_INSTANTIATION
+
+InstStrategySimplex::InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) :
+    InstStrategy( ie ), d_th( th ), d_counter( 0 ){
+  d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
+}
+
+void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
+  d_counter++;
+}
+
+int InstStrategySimplex::process( Node f, Theory::Effort effort, int e, int instLimit ){
+  if( e<2 ){
+    return STATUS_UNFINISHED;
+  }else if( e==2 ){
+    //Notice() << f << std::endl;
+    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
+    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
+    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_th->d_instRows[f].size() << std::endl;
+    for( int j=0; j<(int)d_th->d_instRows[f].size(); j++ ){
+      ArithVar x = d_th->d_instRows[f][j];
+      if( !d_th->d_ceTableaux[x].empty() ){
+        Debug("quant-arith-simplex") << "Check row " << x << std::endl;
+        //instantiation row will be A*e + B*t = beta,
+        // where e is a vector of terms , and t is vector of ground terms.
+        // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+        // We will construct the term ( beta - B*t)/coeff to use for e_i.
+        InstMatch m;
+        //By default, choose the first instantiation constant to be e_i.
+        Node var = d_th->d_ceTableaux[x].begin()->first;
+        if( var.getType().isInteger() ){
+          std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin();
+          //try to find coefficent that is +/- 1
+          while( !var.isNull() && !d_th->d_ceTableaux[x][var].isNull() && d_th->d_ceTableaux[x][var]!=d_negOne ){
+            ++it;
+            if( it==d_th->d_ceTableaux[x].end() ){
+              var = Node::null();
+            }else{
+              var = it->first;
+            }
+          }
+          //otherwise, try one that divides all ground term coefficients? DO_THIS
+        }
+        if( !var.isNull() ){
+          Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+          d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, m, var );
+        }else{
+          Debug("quant-arith-simplex") << "Could not find var." << std::endl;
+        }
+        ////choose a new variable based on alternation strategy
+        //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
+        //Node var;
+        //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
+        //  if( index==0 ){
+        //    var = it->first;
+        //    break;
+        //  }
+        //  index--;
+        //}
+        //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
+      }
+    }
+  }
+  return STATUS_UNKNOWN;
+}
+
+//void InstStrategySimplexUfMatch::resetInstantiationRound(){
+//
+//}
+//
+//int InstStrategySimplexUfMatch::process( Node f, int effort, int instLimit ){
+//  if( effort<2 ){
+//    return STATUS_UNFINISHED;
+//  }else if( effort==2 ){
+//    for( int j=0; j<(int)d_th->d_instRows[f].size(); j++ ){
+//      ArithVar x = d_th->d_instRows[f][j];
+//      if( !d_th->d_ceTableaux[x].empty() && !d_th->d_tableaux_ce_term[x].empty() ){
+//        if( d_tableaux_ce_term_trigger.find( x )==d_tableaux_ce_term_trigger.end() ){
+//          std::vector< Node > terms;
+//          for( std::map< Node, Node >::iterator it = d_th->d_tableaux_ce_term[x].begin(); it != d_th->d_tableaux_ce_term[x].end(); ++it ){
+//            terms.push_back( it->first );
+//          }
+//          d_tableaux_ce_term_trigger[x] = new Trigger( d_quantEngine, f, terms );
+//        }else{
+//          d_tableaux_ce_term_trigger[x]->resetInstantiationRound();
+//        }
+//        Node term;
+//        bool addedLemma = false;
+//        while( d_tableaux_ce_term_trigger[x]->getNextMatch() && !addedLemma ){
+//          InstMatch* m = d_tableaux_ce_term_trigger[x]->getCurrent();
+//          if( m->isComplete( f ) ){
+//            if( d_quantEngine->addInstantiation( f, m, true ) ){
+//              ++(d_th->d_statistics.d_instantiations_match_pure);
+//              ++(d_th->d_statistics.d_instantiations);
+//              addedLemma = true;
+//            }
+//          }else{
+//            NodeBuilder<> plus_term(kind::PLUS);
+//            plus_term << d_th->d_tableaux_term[x];
+//            //Debug("quant-arith") << "Produced this match for ce_term_tableaux: " << std::endl;
+//            //m->debugPrint("quant-arith");
+//            //Debug("quant-arith") << std::endl;
+//            std::vector< Node > vars;
+//            std::vector< Node > matches;
+//            for( int i=0; i<d_quantEngine->getNumInstantiationConstants( f ); i++ ){
+//              Node ic = d_quantEngine->getInstantiationConstant( f, i );
+//              if( m->d_map[ ic ]!=Node::null() ){
+//                vars.push_back( ic );
+//                matches.push_back( m->d_map[ ic ] );
+//              }
+//            }
+//            Node var;
+//            //otherwise try to find a variable that is not specified in m
+//            for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
+//              if( m->d_map[ it->first ]!=Node::null() ){
+//                plus_term << NodeManager::currentNM()->mkNode( MULT, it->second, d_th->getTableauxValue( m->d_map[ it->first ] ) );
+//              }else if( var==Node::null() ){
+//                var = it->first;
+//              }
+//            }
+//            for( std::map< Node, Node >::iterator it = d_th->d_tableaux_ce_term[x].begin(); it != d_th->d_tableaux_ce_term[x].end(); ++it ){
+//              Node n = it->first;
+//              //substitute in matches
+//              n = n.substitute( vars.begin(), vars.end(), matches.begin(), matches.end() );
+//              plus_term << NodeManager::currentNM()->mkNode( MULT, it->second, d_th->getTableauxValue( n ) );
+//            }
+//            term = plus_term.getNumChildren()==1 ? plus_term.getChild( 0 ) : plus_term;
+//            if( var!=Node::null() ){
+//              if( d_th->doInstantiation( f, term, x, m, var ) ){
+//                addedLemma = true;
+//                ++(d_th->d_statistics.d_instantiations_match_var);
+//              }
+//            }else{
+//              if( d_quantEngine->addInstantiation( f, m, true ) ){
+//                addedLemma = true;
+//                ++(d_th->d_statistics.d_instantiations_match_no_var);
+//                ++(d_th->d_statistics.d_instantiations);
+//              }
+//            }
+//          }
+//        }
+//      }
+//    }
+//  }
+//  return STATUS_UNKNOWN;
+//}
+
+InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
+Instantiator( c, ie, th ){
+  if( Options::current()->cbqi ){
+    addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) );
+  }
+}
+
+void InstantiatorTheoryArith::preRegisterTerm( Node t ){
+
+}
+
+void InstantiatorTheoryArith::assertNode( Node assertion ){
+  Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
+  d_quantEngine->addTermToDatabase( assertion );
+  if( Options::current()->cbqi ){
+    if( assertion.hasAttribute(InstConstantAttribute()) ){
+      setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
+      setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+    }
+  }
+}
+
+void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){
+  if( Options::current()->cbqi ){
+    Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
+    d_instRows.clear();
+    d_tableaux_term.clear();
+    d_tableaux.clear();
+    d_ceTableaux.clear();
+    //search for instantiation rows in simplex tableaux
+    ArithVarToNodeMap avtnm = ((TheoryArith*)getTheory())->d_arithvarNodeMap.getArithVarToNodeMap();
+    for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
+      ArithVar x = (*it).first;
+      if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
+        Node n = (*it).second;
+        Node f;
+        NodeBuilder<> t(kind::PLUS);
+        if( n.getKind()==PLUS ){
+          for( int i=0; i<(int)n.getNumChildren(); i++ ){
+            addTermToRow( x, n[i], f, t );
+          }
+        }else{
+          addTermToRow( x, n, f, t );
+        }
+        if( f!=Node::null() ){
+          d_instRows[f].push_back( x );
+          //this theory has constraints from f
+          Debug("quant-arith") << "Has constraints from " << f << std::endl;
+          setHasConstraintsFrom( f );
+          //set tableaux term
+          if( t.getNumChildren()==0 ){
+            d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
+          }else if( t.getNumChildren()==1 ){
+            d_tableaux_term[x] = t.getChild( 0 );
+          }else{
+            d_tableaux_term[x] = t;
+          }
+        }
+      }
+    }
+    //print debug
+    debugPrint( "quant-arith-debug" );
+  }
+}
+
+int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e, int instLimit ){
+  Debug("quant-arith") << "Arith: Try to solve (" << effort << ") for " << f << "... " << std::endl;
+  return InstStrategy::STATUS_UNKNOWN;
+}
+
+void InstantiatorTheoryArith::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
+  if( n.getKind()==MULT ){
+    if( n[1].hasAttribute(InstConstantAttribute()) ){
+      f = n[1].getAttribute(InstConstantAttribute());
+      if( n[1].getKind()==INST_CONSTANT ){
+        d_ceTableaux[x][ n[1] ] = n[0];
+      }else{
+        d_tableaux_ce_term[x][ n[1] ] = n[0];
+      }
+    }else{
+      d_tableaux[x][ n[1] ] = n[0];
+      t << n;
+    }
+  }else{
+    if( n.hasAttribute(InstConstantAttribute()) ){
+      f = n.getAttribute(InstConstantAttribute());
+      if( n.getKind()==INST_CONSTANT ){
+        d_ceTableaux[x][ n ] = Node::null();
+      }else{
+        d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
+      }
+    }else{
+      d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
+      t << n;
+    }
+  }
+}
+
+void InstantiatorTheoryArith::debugPrint( const char* c ){
+  ArithVarToNodeMap avtnm = ((TheoryArith*)getTheory())->d_arithvarNodeMap.getArithVarToNodeMap();
+  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
+    ArithVar x = (*it).first;
+    Node n = (*it).second;
+    //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
+      Debug(c) << x << " : " << n << ", bounds = ";
+      if( ((TheoryArith*)getTheory())->d_partialModel.hasLowerBound( x ) ){
+        Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getLowerBound( x );
+      }else{
+        Debug(c) << "-infty";
+      }
+      Debug(c) << " <= ";
+      Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getAssignment( x );
+      Debug(c) << " <= ";
+      if( ((TheoryArith*)getTheory())->d_partialModel.hasUpperBound( x ) ){
+        Debug(c) << ((TheoryArith*)getTheory())->d_partialModel.getUpperBound( x );
+      }else{
+        Debug(c) << "+infty";
+      }
+      Debug(c) << std::endl;
+      //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;
+      //Debug(c) << "   ";
+      //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
+      //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
+      //}
+      //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
+      //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
+      //}
+      //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
+      //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
+      //}
+      //Debug(c) << std::endl;
+    //}
+  }
+  Debug(c) << std::endl;
+
+  for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){
+    Node f = d_quantEngine->getQuantifier( q );
+    Debug(c) << f << std::endl;
+    Debug(c) << "   Inst constants: ";
+    for( int i=0; i<(int)d_quantEngine->getNumInstantiationConstants( f ); i++ ){
+      if( i>0 ){
+        Debug( c ) << ", ";
+      }
+      Debug( c ) << d_quantEngine->getInstantiationConstant( f, i );
+    }
+    Debug(c) << std::endl;
+    Debug(c) << "   Instantiation rows: ";
+    for( int i=0; i<(int)d_instRows[f].size(); i++ ){
+      if( i>0 ){
+        Debug(c) << ", ";
+      }
+      Debug(c) << d_instRows[f][i];
+    }
+    Debug(c) << std::endl;
+  }
+}
+
+//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
+// where var is an instantiation constant from f,
+// t[e] is a vector of terms containing instantiation constants from f,
+// and term is a ground term (c1*t1 + ... + cn*tn).
+// We construct the term ( beta - term )/coeff to use as an instantiation for var.
+bool InstantiatorTheoryArith::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
+  //first try +delta
+  if( doInstantiation2( f, term, x, m, var ) ){
+    ++(d_statistics.d_instantiations);
+    return true;
+  }else{
+#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
+    //otherwise try -delta
+    if( doInstantiation2( f, term, x, m, var, true ) ){
+      ++(d_statistics.d_instantiations_minus);
+      ++(d_statistics.d_instantiations);
+      return true;
+    }else{
+      return false;
+    }
+#else
+    return false;
+#endif
+  }
+}
+
+bool InstantiatorTheoryArith::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
+  // make term ( beta - term )/coeff
+  Node beta = getTableauxValue( x, minus_delta );
+  Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
+  if( !d_ceTableaux[x][var].isNull() ){
+    if( var.getType().isInteger() ){
+      Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
+      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );
+    }else{
+      Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );
+      instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
+    }
+  }
+  instVal = Rewriter::rewrite( instVal );
+  //use as instantiation value for var
+  m.d_map[ var ] = instVal;
+  Debug("quant-arith") << "Add instantiation " << m << std::endl;
+  return d_quantEngine->addInstantiation( f, m, true );
+}
+
+Node InstantiatorTheoryArith::getTableauxValue( Node n, bool minus_delta ){
+  if( ((TheoryArith*)getTheory())->d_arithvarNodeMap.hasArithVar(n) ){
+    ArithVar v = ((TheoryArith*)getTheory())->d_arithvarNodeMap.asArithVar( n );
+    return getTableauxValue( v, minus_delta );
+  }else{
+    return NodeManager::currentNM()->mkConst( Rational(0) );
+  }
+}
+
+Node InstantiatorTheoryArith::getTableauxValue( ArithVar v, bool minus_delta ){
+  DeltaRational drv = ((TheoryArith*)getTheory())->d_partialModel.getAssignment( v );
+  Node val = NodeManager::currentNM()->mkConst( drv.getNoninfinitesimalPart() );
+#ifdef ARITH_INSTANTIATOR_USE_DELTA
+  //the tableaux value for v may contain an infinitesemal part: getDelta( val ) will return a fresh variable "delta"
+  //  (one for each sort) for which the lemma ( delta > 0 ) is asserted.
+  if( drv.getInfinitesimalPart()!=0 ){
+    Node delta = NodeManager::currentNM()->mkNode( MULT, getDelta( val ),
+                                                    NodeManager::currentNM()->mkConst( drv.getInfinitesimalPart() ) );
+    // add (or subtract) this delta component from the value of v
+    val = NodeManager::currentNM()->mkNode( minus_delta ? MINUS : PLUS, val, delta );
+  }
+#endif
+  return val;
+}
+
+Node InstantiatorTheoryArith::getDelta( Node n ){
+  std::map< TypeNode, Node >::iterator it = d_deltas.find( n.getType() );
+  if( it==d_deltas.end() ){
+    std::ostringstream os;
+    os << "delta_" << d_deltas.size();
+    Node delta = NodeManager::currentNM()->mkVar( os.str(), n.getType() );
+    d_deltas[ n.getType() ] = delta;
+    Node gt = NodeManager::currentNM()->mkNode( GT, delta, NodeManager::currentNM()->mkConst( Rational(0) ) );
+    //add split
+#ifdef ARITH_INSTANTIATOR_STRONG_DELTA_LEMMA
+    d_quantEngine->addLemma( gt );
+#else
+    gt = Rewriter::rewrite( gt );
+    d_quantEngine->addSplit( gt, true, true );
+#endif
+    return delta;
+  }
+  return it->second;
+}
+
+InstantiatorTheoryArith::Statistics::Statistics():
+  d_instantiations("InstantiatorTheoryArith::Instantiations_Total", 0),
+  d_instantiations_minus("InstantiatorTheoryArith::Instantiations_minus_delta", 0),
+  d_instantiations_match_pure("InstantiatorTheoryArith::Instantiations_via_pure_matching", 0),
+  d_instantiations_match_var("InstantiatorTheoryArith::Instantiations_via_matching_var", 0),
+  d_instantiations_match_no_var("InstantiatorTheoryArith::Instantiations_via_matching_no_var", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations);
+  StatisticsRegistry::registerStat(&d_instantiations_minus);
+  StatisticsRegistry::registerStat(&d_instantiations_match_pure);
+  StatisticsRegistry::registerStat(&d_instantiations_match_var);
+  StatisticsRegistry::registerStat(&d_instantiations_match_no_var);
+}
+
+InstantiatorTheoryArith::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations);
+  StatisticsRegistry::unregisterStat(&d_instantiations_minus);
+  StatisticsRegistry::unregisterStat(&d_instantiations_match_pure);
+  StatisticsRegistry::unregisterStat(&d_instantiations_match_var);
+  StatisticsRegistry::unregisterStat(&d_instantiations_match_no_var);
+}
diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h
new file mode 100644
index 000000000..524d16859
--- /dev/null
+++ b/src/theory/arith/theory_arith_instantiator.h
@@ -0,0 +1,128 @@
+/*********************                                                        */
+/*! \file instantiator_arith_instantiator.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief instantiator_arith_instantiator
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INSTANTIATOR_ARITH_H
+#define __CVC4__INSTANTIATOR_ARITH_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/arith/arithvar_node_map.h"
+
+#include "util/stats.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class InstantiatorTheoryArith;
+
+class InstStrategySimplex : public InstStrategy{
+private:
+  /** InstantiatorTheoryUf class */
+  InstantiatorTheoryArith* d_th;
+  /** */
+  int d_counter;
+  /** negative one */
+  Node d_negOne;
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e, int instLimit );
+public:
+  InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie );
+  ~InstStrategySimplex(){}
+  /** identify */
+  std::string identify() const { return std::string("Simplex"); }
+};
+//
+//class InstStrategySimplexUfMatch : public InstStrategy{
+//private:
+//  /** InstantiatorTheoryUf class */
+//  InstantiatorTheoryArith* d_th;
+//  /** trigger for instantiation rows */
+//  std::map< ArithVar, Trigger* > d_tableaux_ce_term_trigger;
+//public:
+//  InstStrategySimplexUfMatch( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) : 
+//      InstStrategy( ie ), d_th( th ){}
+//  ~InstStrategySimplexUfMatch(){}
+//  void resetInstantiationRound();
+//  int process( Node f, Theory::Effort effort, int e, int instLimit );
+//  /** identify */
+//  std::string identify() const { return std::string("SimplexUfMatch"); }
+//};
+
+class InstantiatorTheoryArith : public Instantiator{
+  friend class QuantifiersEngine;
+  friend class InstStrategySimplex;
+  friend class InstStrategySimplexUfMatch;
+private:
+  /** delta */
+  std::map< TypeNode, Node > d_deltas;
+  /** for each quantifier, simplex rows */
+  std::map< Node, std::vector< ArithVar > > d_instRows;
+  /** tableaux */
+  std::map< ArithVar, Node > d_tableaux_term;
+  std::map< ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
+  std::map< ArithVar, std::map< Node, Node > > d_tableaux;
+  /** ce tableaux */
+  std::map< ArithVar, std::map< Node, Node > > d_ceTableaux;
+  /** get value */
+  Node getTableauxValue( Node n, bool minus_delta = false );
+  Node getTableauxValue( ArithVar v, bool minus_delta = false );
+  /** do instantiation */
+  bool doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var );
+  bool doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
+public:
+  InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th);
+  ~InstantiatorTheoryArith() {}
+
+  /** assertNode function, assertion is asserted to theory */
+  void assertNode( Node assertion );
+  /** Pre-register a term.  Done one time for a Node, ever. */
+  void preRegisterTerm( Node t );
+  /** identify */
+  std::string identify() const { return std::string("InstantiatorTheoryArith"); }
+  /** print debug */
+  void debugPrint( const char* c );
+private:
+  /**  reset instantiation */
+  void processResetInstantiationRound( Theory::Effort effort );
+  /** process at effort */
+  int process( Node f, Theory::Effort effort, int e, int instLimit );
+  /** add term to row */
+  void addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t );
+  /** get delta for node */
+  Node getDelta( Node n );
+
+  class Statistics {
+  public:
+    IntStat d_instantiations;
+    IntStat d_instantiations_minus;
+    IntStat d_instantiations_match_pure;
+    IntStat d_instantiations_match_var;
+    IntStat d_instantiations_match_no_var;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
+};/* class InstantiatiorTheoryArith  */
+
+}
+}
+}
+
+#endif
\ No newline at end of file