T-entailment work, and QCF (quant conflict find) work that uses it.

This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

25 files changed, 2063 insertions, 127 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 2d306d464..e7cc9628e 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -354,6 +354,8 @@ libcvc4_la_SOURCES = \
 	theory/arith/fc_simplex.cpp \
 	theory/arith/soi_simplex.h \
 	theory/arith/soi_simplex.cpp \
+	theory/arith/infer_bounds.h \
+	theory/arith/infer_bounds.cpp \
 	theory/arith/approx_simplex.h \
 	theory/arith/approx_simplex.cpp \
 	theory/arith/attempt_solution_simplex.h \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 36f9866f4..6dd1f4465 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1192,7 +1192,7 @@ void SmtEngine::setDefaults() {
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
-  if( options::qcfMode.wasSetByUser() ){
+  if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
 
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 98aa43e71..f78893324 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -162,7 +162,7 @@ inline int deltaCoeff(Kind k){
  * - (NOT (GT left right))    -> LEQ
  * If none of these match, it returns UNDEFINED_KIND.
  */
- inline Kind oldSimplifiedKind(TNode literal){
+inline Kind oldSimplifiedKind(TNode literal){
   switch(literal.getKind()){
   case kind::LT:
   case kind::GT:
@@ -195,6 +195,19 @@ inline int deltaCoeff(Kind k){
   }
 }
 
+inline Kind negateKind(Kind k){
+  switch(k){
+  case kind::LT:       return kind::GEQ;
+  case kind::GT:       return kind::LEQ;
+  case kind::LEQ:      return kind::GT;
+  case kind::GEQ:      return kind::LT;
+  case kind::EQUAL:    return kind::DISTINCT;
+  case kind::DISTINCT: return kind::EQUAL;
+  default:
+    return kind::UNDEFINED_KIND;
+  }
+}
+
 inline Node negateConjunctionAsClause(TNode conjunction){
   Assert(conjunction.getKind() == kind::AND);
   NodeBuilder<> orBuilder(kind::OR);
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 7945b44c3..c2924f239 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -191,6 +191,11 @@ public:
     return !(*this <= other);
   }
 
+  int compare(const DeltaRational& other) const{
+    int cmpRes = c.cmp(other.c);
+    return (cmpRes != 0) ? cmpRes : (k.cmp(other.k));
+  }
+
   DeltaRational& operator=(const DeltaRational& other){
     c = other.c;
     k = other.k;
diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp
new file mode 100644
index 000000000..05a520d35
--- /dev/null
+++ b/src/theory/arith/infer_bounds.cpp
@@ -0,0 +1,319 @@
+/*********************                                                        */
+/*! \file infer_bounds.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/arith/infer_bounds.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+using namespace inferbounds;
+
+InferBoundAlgorithm::InferBoundAlgorithm()
+  : d_alg(None)
+{}
+
+InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
+  : d_alg(a)
+{
+  Assert(a != Simplex);
+}
+
+InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds)
+  : d_alg(Simplex)
+{}
+
+Algorithms InferBoundAlgorithm::getAlgorithm() const{
+  return d_alg;
+}
+
+const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{
+  Assert(getAlgorithm() == Simplex);
+  return d_simplexRounds;
+}
+
+
+InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
+  return InferBoundAlgorithm(Lookup);
+}
+
+InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
+  return InferBoundAlgorithm(RowSum);
+}
+
+InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
+  return InferBoundAlgorithm(rounds);
+}
+
+ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
+  : EntailmentCheckParameters(theory::THEORY_ARITH)
+  , d_algorithms()
+{}
+
+ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
+{}
+
+
+void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){
+  addAlgorithm(InferBoundAlgorithm::mkLookup());
+  addAlgorithm(InferBoundAlgorithm::mkRowSum());
+}
+
+void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){
+  d_algorithms.push_back(alg);
+}
+
+ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{
+  return d_algorithms.begin();
+}
+
+ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{
+  return d_algorithms.end();
+}
+
+
+// SimplexInferBoundsParameters::SimplexInferBoundsParameters()
+//   : d_parameter(1)
+//   , d_upperBound(true)
+//   , d_threshold()
+// {}
+
+// SimplexInferBoundsParameters::~SimplexInferBoundsParameters(){}
+
+
+
+// int SimplexInferBoundsParameters::getSimplexRoundParameter() const {
+//   return d_parameter;
+// }
+
+// bool SimplexInferBoundsParameters::findLowerBound() const {
+//   return ! findUpperBound();
+// }
+
+// bool SimplexInferBoundsParameters::findUpperBound() const {
+//   return d_upperBound;
+// }
+
+// void SimplexInferBoundsParameters::setThreshold(const DeltaRational& th){
+//   d_threshold = th;
+//   d_useThreshold = true;
+// }
+
+// bool SimplexInferBoundsParameters::useThreshold() const{
+//   return d_useThreshold;
+// }
+
+// const DeltaRational& SimplexInferBoundsParameters::getThreshold() const{
+//   return d_threshold;
+// }
+
+// SimplexInferBoundsParameters::SimplexInferBoundsParameters(int p, bool ub)
+//   : d_parameter(p)
+//   , d_upperBound(ub)
+//   , d_useThreshold(false)
+//   , d_threshold()
+// {}
+
+
+InferBoundsResult::InferBoundsResult()
+  : d_foundBound(false)
+  , d_budgetExhausted(false)
+  , d_boundIsProvenOpt(false)
+  , d_inconsistentState(false)
+  , d_reachedThreshold(false)
+  , d_value(false)
+  , d_term(Node::null())
+  , d_upperBound(true)
+  , d_explanation(Node::null())
+{}
+
+InferBoundsResult::InferBoundsResult(Node term, bool ub)
+  : d_foundBound(false)
+  , d_budgetExhausted(false)
+  , d_boundIsProvenOpt(false)
+  , d_inconsistentState(false)
+  , d_reachedThreshold(false)
+  , d_value(false)
+  , d_term(term)
+  , d_upperBound(ub)
+  , d_explanation(Node::null())
+{}
+
+bool InferBoundsResult::foundBound() const {
+  return d_foundBound;
+}
+bool InferBoundsResult::boundIsOptimal() const {
+  return d_boundIsProvenOpt;
+}
+bool InferBoundsResult::inconsistentState() const {
+  return d_inconsistentState;
+}
+
+bool InferBoundsResult::boundIsInteger() const{
+  return foundBound() && d_value.isIntegral();
+}
+
+bool InferBoundsResult::boundIsRational() const {
+  return foundBound() && d_value.infinitesimalIsZero();
+}
+
+Integer InferBoundsResult::valueAsInteger() const{
+  Assert(boundIsInteger());
+  return getValue().floor();
+}
+const Rational& InferBoundsResult::valueAsRational() const{
+  Assert(boundIsRational());
+  return getValue().getNoninfinitesimalPart();
+}
+
+const DeltaRational& InferBoundsResult::getValue() const{
+  return d_value;
+}
+
+Node InferBoundsResult::getTerm() const { return d_term; }
+
+Node InferBoundsResult::getLiteral() const{
+  const Rational& q = getValue().getNoninfinitesimalPart();
+  NodeManager* nm = NodeManager::currentNM();
+  Node qnode = nm->mkConst(q);
+
+  Kind k;
+  if(d_upperBound){
+    // x <= q + c*delta
+    Assert(getValue().infinitesimalSgn() <= 0);
+    k = boundIsRational() ? kind::LEQ : kind::LT;
+  }else{
+    // x >= q + c*delta
+    Assert(getValue().infinitesimalSgn() >= 0);
+    k = boundIsRational() ? kind::GEQ : kind::GT;
+  }
+  Node atom = nm->mkNode(k, getTerm(), qnode);
+  Node lit = Rewriter::rewrite(atom);
+  return lit;
+}
+
+/* If there is a bound, this is a node that explains the bound. */
+Node InferBoundsResult::getExplanation() const{
+  return d_explanation;
+}
+
+
+void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){
+  d_foundBound = true;
+  d_value = dr;
+  d_explanation = exp;
+}
+
+//bool InferBoundsResult::foundBound() const { return d_foundBound; }
+//bool InferBoundsResult::boundIsOptimal() const { return d_boundIsProvenOpt; }
+//bool InferBoundsResult::inconsistentState() const { return d_inconsistentState; }
+
+
+void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; }
+void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; }
+void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; }
+void InferBoundsResult::setInconsistent() { d_inconsistentState = true; }
+
+bool InferBoundsResult::thresholdWasReached() const{
+  return d_reachedThreshold;
+}
+bool InferBoundsResult::budgetIsExhausted() const{
+  return d_budgetExhausted;
+}
+
+std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){
+  os << "{InferBoundsResult " << std::endl;
+  os << "on " << ibr.getTerm() << ", ";
+  if(ibr.findUpperBound()){
+    os << "find upper bound, ";
+  }else{
+    os << "find lower bound, ";
+  }
+  if(ibr.foundBound()){
+    os << "found a bound: ";
+    if(ibr.boundIsInteger()){
+      os << ibr.valueAsInteger() << "(int), ";
+    }else if(ibr.boundIsRational()){
+      os << ibr.valueAsRational() << "(rat), ";
+    }else{
+      os << ibr.getValue() << "(extended), ";
+    }
+
+    os << "as term " << ibr.getLiteral() << ", ";
+    os << "explanation " << ibr.getExplanation() << ", ";
+  }else {
+    os << "did not find a bound, ";
+  }
+
+  if(ibr.boundIsOptimal()){
+    os << "(opt), ";
+  }
+
+  if(ibr.inconsistentState()){
+    os << "(inconsistent), ";
+  }
+  if(ibr.budgetIsExhausted()){
+    os << "(budget exhausted), ";
+  }
+  if(ibr.thresholdWasReached()){
+    os << "(reached threshold), ";
+  }
+  os << "}";
+  return os;
+}
+
+
+ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
+  : EntailmentCheckSideEffects(theory::THEORY_ARITH)
+  , d_simplexSideEffects (NULL)
+{}
+
+ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
+  if(d_simplexSideEffects != NULL){
+    delete d_simplexSideEffects;
+    d_simplexSideEffects = NULL;
+  }
+}
+
+InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){
+  if(d_simplexSideEffects == NULL){
+    d_simplexSideEffects = new InferBoundsResult;
+  }
+  return *d_simplexSideEffects;
+}
+
+namespace inferbounds { /* namespace arith */
+
+std::ostream& operator<<(std::ostream& os,  const Algorithms a){
+  switch(a){
+  case None:    os << "AlgNone"; break;
+  case Lookup:  os << "AlgLookup"; break;
+  case RowSum:  os << "AlgRowSum"; break;
+  case Simplex: os << "AlgSimplex"; break;
+  default:
+    Unhandled();
+  }
+
+  return os;
+}
+
+} /* namespace inferbounds */
+
+} /* namespace arith */
+} /* namespace theory */
+} /* namespace CVC4 */
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
new file mode 100644
index 000000000..55486080a
--- /dev/null
+++ b/src/theory/arith/infer_bounds.h
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \file infer_bounds.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "util/maybe.h"
+#include "util/integer.h"
+#include "util/rational.h"
+#include "expr/node.h"
+#include "theory/arith/delta_rational.h"
+#include "theory/theory.h"
+#include <ostream>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+namespace inferbounds {
+  enum Algorithms {None = 0, Lookup, RowSum, Simplex};
+  enum SimplexParamKind { Unbounded, NumVars, Direct};
+
+class InferBoundAlgorithm {
+private:
+  Algorithms d_alg;
+  Maybe<int> d_simplexRounds;
+  InferBoundAlgorithm(Algorithms a);
+  InferBoundAlgorithm(const Maybe<int>& simplexRounds);
+
+public:
+  InferBoundAlgorithm();
+
+  Algorithms getAlgorithm() const;
+  const Maybe<int>& getSimplexRounds() const;
+
+  static InferBoundAlgorithm mkLookup();
+  static InferBoundAlgorithm mkRowSum();
+  static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds);
+};
+
+std::ostream& operator<<(std::ostream& os, const Algorithms a);
+} /* namespace inferbounds */
+
+class ArithEntailmentCheckParameters : public EntailmentCheckParameters {
+private:
+  typedef std::vector<inferbounds::InferBoundAlgorithm> VecInferBoundAlg;
+  VecInferBoundAlg d_algorithms;
+
+public:
+  typedef VecInferBoundAlg::const_iterator const_iterator;
+
+  ArithEntailmentCheckParameters();
+  ~ArithEntailmentCheckParameters();
+
+  void addLookupRowSumAlgorithms();
+  void addAlgorithm(const inferbounds::InferBoundAlgorithm& alg);
+
+  const_iterator begin() const;
+  const_iterator end() const;
+};
+
+
+
+class InferBoundsResult {
+public:
+  InferBoundsResult();
+  InferBoundsResult(Node term, bool ub);
+
+  void setBound(const DeltaRational& dr, Node exp);
+  bool foundBound() const;
+
+  void setIsOptimal();
+  bool boundIsOptimal() const;
+
+  void setInconsistent();
+  bool inconsistentState() const;
+
+  const DeltaRational& getValue() const;
+  bool boundIsRational() const;
+  const Rational& valueAsRational() const;
+  bool boundIsInteger() const;
+  Integer valueAsInteger() const;
+
+  Node getTerm() const;
+  Node getLiteral() const;
+  void setTerm(Node t){ d_term = t; }
+
+  /* If there is a bound, this is a node that explains the bound. */
+  Node getExplanation() const;
+
+  bool budgetIsExhausted() const;
+  void setBudgetExhausted();
+
+  bool thresholdWasReached() const;
+  void setReachedThreshold();
+
+  bool findUpperBound() const { return d_upperBound; }
+
+  void setFindLowerBound() { d_upperBound = false; }
+  void setFindUpperBound() { d_upperBound = true; }
+private:
+  /* was a bound found */
+  bool d_foundBound;
+
+  /* was the budget exhausted */
+  bool d_budgetExhausted;
+
+  /* does the bound have to be optimal*/
+  bool d_boundIsProvenOpt;
+
+  /* was this started on an inconsistent state. */
+  bool d_inconsistentState;
+
+  /* reached the threshold. */
+  bool d_reachedThreshold;
+
+  /* the value of the bound */
+  DeltaRational d_value;
+
+  /* The input term. */
+  Node d_term;
+
+  /* Was the bound found an upper or lower bound.*/
+  bool d_upperBound;
+
+  /* Explanation of the bound. */
+  Node d_explanation;
+};
+
+std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr);
+
+class ArithEntailmentCheckSideEffects : public EntailmentCheckSideEffects{
+public:
+  ArithEntailmentCheckSideEffects();
+  ~ArithEntailmentCheckSideEffects();
+
+  InferBoundsResult& getSimplexSideEffects();
+
+private:
+  InferBoundsResult* d_simplexSideEffects;
+};
+
+
+} /* namespace arith */
+} /* namespace theory */
+} /* namespace CVC4 */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 960a5a066..74453d985 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
+#include "theory/arith/infer_bounds.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -100,6 +101,43 @@ Node TheoryArith::getModelValue(TNode var) {
   return d_internal->getModelValue( var );
 }
 
+
+std::pair<bool, Node> TheoryArith::entailmentCheck (TNode lit,
+                                                    const EntailmentCheckParameters* params,
+                                                    EntailmentCheckSideEffects* out)
+{
+  const ArithEntailmentCheckParameters* aparams = NULL;
+  if(params == NULL){
+    ArithEntailmentCheckParameters* def = new ArithEntailmentCheckParameters();
+    def->addLookupRowSumAlgorithms();
+    aparams = def;
+  }else{
+    AlwaysAssert(params->getTheoryId() == getId());
+    aparams = dynamic_cast<const ArithEntailmentCheckParameters*>(params);
+  }
+  Assert(aparams != NULL);
+
+  ArithEntailmentCheckSideEffects* ase = NULL;
+  if(out == NULL){
+    ase = new ArithEntailmentCheckSideEffects();
+  }else{
+    AlwaysAssert(out->getTheoryId() == getId());
+    ase = dynamic_cast<ArithEntailmentCheckSideEffects*>(out);
+  }
+  Assert(ase != NULL);
+
+  std::pair<bool, Node> res = d_internal->entailmentCheck(lit, *aparams, *ase);
+
+  if(params == NULL){
+    delete aparams;
+  }
+  if(out == NULL){
+    delete ase;
+  }
+
+  return res;
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index eaa9a98c6..56a8d9b60 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -21,6 +21,7 @@
 #include "expr/node.h"
 #include "theory/arith/theory_arith_private_forward.h"
 
+
 namespace CVC4 {
 namespace theory {
 
@@ -79,6 +80,12 @@ public:
   void addSharedTerm(TNode n);
 
   Node getModelValue(TNode var);
+
+
+  std::pair<bool, Node> entailmentCheck(TNode lit,
+                                        const EntailmentCheckParameters* params,
+                                        EntailmentCheckSideEffects* out);
+
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index b0e66b564..efc93e26f 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -121,16 +121,21 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_tableauResetDensity(1.6),
   d_tableauResetPeriod(10),
   d_conflicts(c),
+
   d_blackBoxConflict(c, Node::null()),
   d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseConflict(*this, d_conflictBuffer)),
   d_cmEnabled(c, true),
+
   d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
   d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
   d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
   d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
+
   d_pass1SDP(NULL),
   d_otherSDP(NULL),
   d_lastContextIntegerAttempted(c,-1),
+
+
   d_DELTA_ZERO(0),
   d_approxCuts(c),
   d_fullCheckCounter(0),
@@ -1822,10 +1827,6 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){
   Assert(!done());
   TNode assertion = get();
 
-  if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){
-    d_quantEngine->getBoundedIntegers()->assertNode(assertion);
-  }
-
   Kind simpleKind = Comparison::comparisonKind(assertion);
   ConstraintP constraint = d_constraintDatabase.lookup(assertion);
   if(constraint == NullConstraint){
@@ -4621,6 +4622,7 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
   return d_rowTracking[ridx];
 }
 
+
 Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) {
   NodeManager* nm = NodeManager::currentNM();
 
@@ -4684,6 +4686,900 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
 }
 
 
+
+
+// InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const InferBoundsParameters& param){
+//   Node t = Rewriter::rewrite(term);
+//   Assert(Polynomial::isMember(t));
+//   Polynomial p = Polynomial::parsePolynomial(t);
+//   if(p.containsConstant()){
+//     Constant c = p.getHead().getConstant();
+//     if(p.isConstant()){
+//       InferBoundsResult res(t, param.findLowerBound());
+//       res.setBound((DeltaRational)c.getValue(), mkBoolNode(true));
+//       return res;
+//     }else{
+//       Polynomial tail = p.getTail();
+//       InferBoundsResult res = inferBound(tail.getNode(), param);
+//       if(res.foundBound()){
+//         DeltaRational newBound = res.getValue() + c.getValue();
+//         if(tail.isIntegral()){
+//           Integer asInt  = (param.findLowerBound()) ? newBound.ceiling() : newBound.floor();
+//           newBound = DeltaRational(asInt);
+//         }
+//         res.setBound(newBound, res.getExplanation());
+//       }
+//       return res;
+//     }
+//   }else if(param.findLowerBound()){
+//     InferBoundsParameters find_ub = param;
+//     find_ub.setFindUpperBound();
+//     if(param.useThreshold()){
+//       find_ub.setThreshold(- param.getThreshold() );
+//     }
+//     Polynomial negP = -p;
+//     InferBoundsResult res = inferBound(negP.getNode(), find_ub);
+//     res.setFindLowerBound();
+//     if(res.foundBound()){
+//       res.setTerm(p.getNode());
+//       res.setBound(-res.getValue(), res.getExplanation());
+//     }
+//     return res;
+//   }else{
+//     Assert(param.findUpperBound());
+//     // does not contain a constant
+//     switch(param.getEffort()){
+//     case InferBoundsParameters::Lookup:
+//       return inferUpperBoundLookup(t, param);
+//     case InferBoundsParameters::Simplex:
+//       return inferUpperBoundSimplex(t, param);
+//     case InferBoundsParameters::LookupAndSimplexOnFailure:
+//     case InferBoundsParameters::TryBoth:
+//       {
+//         InferBoundsResult lookup = inferUpperBoundLookup(t, param);
+//         if(lookup.foundBound()){
+//           if(param.getEffort() == InferBoundsParameters::LookupAndSimplexOnFailure ||
+//              lookup.boundIsOptimal()){
+//             return lookup;
+//           }
+//         }
+//         InferBoundsResult simplex = inferUpperBoundSimplex(t, param);
+//         if(lookup.foundBound() && simplex.foundBound()){
+//           return (lookup.getValue() <= simplex.getValue()) ? lookup : simplex;
+//         }else if(lookup.foundBound()){
+//           return lookup;
+//         }else{
+//           return simplex;
+//         }
+//       }
+//     default:
+//       Unreachable();
+//       return InferBoundsResult();
+//     }
+//   }
+// }
+
+
+std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
+  using namespace inferbounds;
+
+  // l k r
+  // diff : (l - r) k 0
+  Debug("arith::entailCheck") << "TheoryArithPrivate::entailmentCheck(" << lit << ")"<< endl;
+  Kind k;
+  int primDir;
+  Rational lm, rm, dm;
+  Node lp, rp, dp;
+  DeltaRational sep;
+  bool successful = decomposeLiteral(lit, k, primDir, lm, lp, rm, rp, dm, dp, sep);
+  if(!successful) { return make_pair(false, Node::null()); }
+
+  if(dp.getKind() == CONST_RATIONAL){
+    Node eval = Rewriter::rewrite(lit);
+    Assert(eval.getKind() == kind::CONST_BOOLEAN);
+    // if true, true is an acceptable explaination
+    // if false, the node is uninterpreted and eval can be forgotten
+    return make_pair(eval.getConst<bool>(), eval);
+  }
+  Assert(dm != Rational(0));
+  Assert(primDir == 1 || primDir == -1);
+
+  int negPrim = -primDir;
+
+  int secDir = (k == EQUAL || k == DISTINCT) ? negPrim: 0;
+  int negSecDir = (k == EQUAL || k == DISTINCT) ? primDir: 0;
+
+  // primDir*[lm*( lp )] k primDir*[ [rm*( rp )] + sep ]
+  // primDir*[lm*( lp ) - rm*( rp ) ] k primDir*sep
+  // primDir*[dm * dp] k primDir*sep
+
+  std::pair<Node, DeltaRational> bestPrimLeft, bestNegPrimRight, bestPrimDiff, tmp;
+  std::pair<Node, DeltaRational> bestSecLeft, bestNegSecRight, bestSecDiff;
+  bestPrimLeft.first = Node::null(); bestNegPrimRight.first = Node::null(); bestPrimDiff.first = Node::null();
+  bestSecLeft.first = Node::null(); bestNegSecRight.first = Node::null(); bestSecDiff.first = Node::null();
+
+
+
+  ArithEntailmentCheckParameters::const_iterator alg, alg_end;
+  for( alg = params.begin(), alg_end = params.end(); alg != alg_end; ++alg ){
+    const inferbounds::InferBoundAlgorithm& ibalg = *alg;
+
+    Debug("arith::entailCheck") << "entailmentCheck trying " << (inferbounds::Algorithms) ibalg.getAlgorithm() << endl;
+    switch(ibalg.getAlgorithm()){
+    case inferbounds::None:
+      break;
+    case inferbounds::Lookup:
+    case inferbounds::RowSum:
+      {
+        typedef void (TheoryArithPrivate::*EntailmentCheckFunc)(std::pair<Node, DeltaRational>&, int, TNode) const;
+
+        EntailmentCheckFunc ecfunc =
+          (ibalg.getAlgorithm() == inferbounds::Lookup)
+          ? (&TheoryArithPrivate::entailmentCheckBoundLookup)
+          : (&TheoryArithPrivate::entailmentCheckRowSum);
+
+        (*this.*ecfunc)(tmp, primDir * lm.sgn(), lp);
+        setToMin(primDir * lm.sgn(), bestPrimLeft, tmp);
+
+        (*this.*ecfunc)(tmp, negPrim * rm.sgn(), rp);
+        setToMin(negPrim * rm.sgn(), bestNegPrimRight, tmp);
+
+        (*this.*ecfunc)(tmp, secDir * lm.sgn(), lp);
+        setToMin(secDir * lm.sgn(), bestSecLeft, tmp);
+
+        (*this.*ecfunc)(tmp, negSecDir * rm.sgn(), rp);
+        setToMin(negSecDir * rm.sgn(), bestNegSecRight, tmp);
+
+        (*this.*ecfunc)(tmp, primDir * dm.sgn(), dp);
+        setToMin(primDir * dm.sgn(), bestPrimDiff, tmp);
+
+        (*this.*ecfunc)(tmp, secDir * dm.sgn(), dp);
+        setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
+      }
+      break;
+    case inferbounds::Simplex:
+      {
+        // primDir * diffm * diff < c or primDir * diffm * diff > c
+        tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
+        setToMin(primDir * dm.sgn(), bestPrimDiff, tmp);
+
+        tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
+        setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
+      }
+      break;
+    default:
+      Unhandled();
+    }
+
+    // turn bounds on prim * left and -prim * right into bounds on prim * diff
+    if(!bestPrimLeft.first.isNull() && !bestNegPrimRight.first.isNull()){
+      //  primDir*lm* lp <= primDir*lm*L
+      // -primDir*rm* rp <= -primDir*rm*R
+      // primDir*lm* lp -primDir*rm* rp <=  primDir*lm*L - primDir*rm*R
+      // primDir [lm* lp -rm* rp] <= primDir[lm*L - *rm*R]
+      // primDir [dm * dp] <= primDir[lm*L - *rm*R]
+      // primDir [dm * dp] <= primDir * dm * ([lm*L - *rm*R]/dm)
+      tmp.second = ((bestPrimLeft.second * lm) - (bestNegPrimRight.second * rm)) / dm;
+      tmp.first = (bestPrimLeft.first).andNode(bestNegPrimRight.first);
+      setToMin(primDir, bestPrimDiff, tmp);
+    }
+
+    // turn bounds on sec * left and sec * right into bounds on sec * diff
+    if(secDir != 0 && !bestSecLeft.first.isNull() && !bestNegSecRight.first.isNull()){
+      //  secDir*lm* lp <= secDir*lm*L
+      // -secDir*rm* rp <= -secDir*rm*R
+      // secDir*lm* lp -secDir*rm* rp <=  secDir*lm*L - secDir*rm*R
+      // secDir [lm* lp -rm* rp] <= secDir[lm*L - *rm*R]
+      // secDir [dm * dp] <= secDir[lm*L - *rm*R]
+      // secDir [dm * dp] <= secDir * dm * ([lm*L - *rm*R]/dm)
+      tmp.second = ((bestSecLeft.second * lm) - (bestNegSecRight.second * rm)) / dm;
+      tmp.first = (bestSecLeft.first).andNode(bestNegSecRight.first);
+      setToMin(secDir, bestSecDiff, tmp);
+    }
+
+    switch(k){
+    case LEQ:
+      if(!bestPrimDiff.first.isNull()){
+        DeltaRational d = (bestPrimDiff.second * dm);
+        if((primDir > 0 && d <= sep) || (primDir < 0 && d >= sep) ){
+          Debug("arith::entailCheck") << "entailmentCheck found "
+                                      << primDir << "*" << dm << "*(" << dp<<")"
+                                      << " <= " << primDir << "*" << dm << "*" << bestPrimDiff.second
+                                      << " <= " << primDir << "*" << sep << endl
+                                      << " by " << bestPrimDiff.first << endl;
+          Assert(bestPrimDiff.second * (Rational(primDir)* dm) <=  (sep * Rational(primDir)));
+          return make_pair(true, bestPrimDiff.first);
+        }
+      }
+      break;
+    case EQUAL:
+      if(!bestPrimDiff.first.isNull() && !bestSecDiff.first.isNull()){
+        // Is primDir [dm * dp] == primDir * sep entailed?
+        // Iff [dm * dp] == sep entailed?
+        // Iff dp == sep / dm entailed?
+        // Iff dp <= sep / dm and dp >= sep / dm entailed?
+
+        // primDir [dm * dp] <= primDir * dm * U
+        // secDir [dm * dp] <= secDir * dm * L
+
+        // Suppose primDir * dm > 0
+        // then secDir * dm < 0
+        //   dp >= (secDir * L) / secDir * dm
+        //   dp >= (primDir * L) / primDir * dm
+        //
+        //   dp <= U / dm
+        //   dp >= L / dm
+        //   dp == sep / dm entailed iff U == L == sep
+        // Suppose primDir * dm < 0
+        // then secDir * dm > 0
+        //   dp >= U / dm
+        //   dp <= L / dm
+        //   dp == sep / dm entailed iff U == L == sep
+        if(bestPrimDiff.second == bestSecDiff.second){
+          if(bestPrimDiff.second == sep){
+            return make_pair(true, (bestPrimDiff.first).andNode(bestSecDiff.first));
+          }
+        }
+      }
+      // intentionally fall through to DISTINCT case!
+      // entailments of negations are eager exit cases for EQUAL
+    case DISTINCT:
+      if(!bestPrimDiff.first.isNull()){
+        // primDir [dm * dp] <= primDir * dm * U < primDir * sep
+        if((primDir > 0 && (bestPrimDiff.second * dm  < sep)) ||
+           (primDir < 0 && (bestPrimDiff.second * dm  > sep))){
+          // entailment of negation
+          if(k == DISTINCT){
+            return make_pair(true, bestPrimDiff.first);
+          }else{
+            Assert(k == EQUAL);
+            return make_pair(false, Node::null());
+          }
+        }
+      }
+      if(!bestSecDiff.first.isNull()){
+        // If primDir [dm * dp] > primDir * sep, then this is not entailed.
+        // If primDir [dm * dp] >= primDir * dm * L > primDir * sep
+        // -primDir * dm * L < -primDir * sep
+        // secDir * dm * L < secDir * sep
+        if((secDir > 0 && (bestSecDiff.second * dm < sep)) ||
+           (secDir < 0 && (bestSecDiff.second * dm > sep))){
+          if(k == DISTINCT){
+            return make_pair(true, bestSecDiff.first);
+          }else{
+            Assert(k == EQUAL);
+            return make_pair(false, Node::null());
+          }
+        }
+      }
+
+      break;
+    default:
+      Unreachable();
+      break;
+    }
+  }
+  return make_pair(false, Node::null());
+}
+
+bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational& c){
+  Node t = Rewriter::rewrite(term);
+  if(!Polynomial::isMember(t)){
+    return false;
+  }
+#warning "DO NOT LET INTO TRUNK!"
+  ContainsTermITEVisitor ctv;
+  if(ctv.containsTermITE(t)){
+    return false;
+  }
+
+  Polynomial poly = Polynomial::parsePolynomial(t);
+  if(poly.isConstant()){
+    c = poly.getHead().getConstant().getValue();
+    p = mkRationalNode(Rational(0));
+    m = Rational(1);
+    return true;
+  }else if(poly.containsConstant()){
+    c = poly.getHead().getConstant().getValue();
+    poly = poly.getTail();
+  }else{
+    c = Rational(0);
+  }
+  Assert(!poly.isConstant());
+  Assert(!poly.containsConstant());
+
+  const bool intVars = poly.allIntegralVariables();
+
+  if(intVars){
+    m = Rational(1);
+    if(!poly.isIntegral()){
+      Integer denom = poly.denominatorLCM();
+      m /= denom;
+      poly = poly * denom;
+    }
+    Integer g = poly.gcd();
+    m *= g;
+    poly = poly * Rational(1,g);
+    Assert(poly.isIntegral());
+    Assert(poly.leadingCoefficientIsPositive());
+  }else{
+    Assert(!intVars);
+    m = poly.getHead().getConstant().getValue();
+    poly = poly * m.inverse();
+    Assert(poly.leadingCoefficientIsAbsOne());
+  }
+  p = poly.getNode();
+  return true;
+}
+
+void TheoryArithPrivate::setToMin(int sgn, std::pair<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e){
+  if(sgn != 0){
+    if(min.first.isNull() && !e.first.isNull()){
+      min = e;
+    }else if(!min.first.isNull() && !e.first.isNull()){
+      if(sgn > 0 && min.second > e.second){
+        min = e;
+      }else if(sgn < 0 &&  min.second < e.second){
+        min = e;
+      }
+    }
+  }
+}
+
+// std::pair<bool, Node> TheoryArithPrivate::entailmentUpperCheck(const Rational& lm, Node lp, const Rational& rm, Node rp, const DeltaRational& sep, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
+
+//   Rational negRM = -rm;
+//   Node diff = NodeManager::currentNM()->mkNode(MULT, mkRationalConstan(lm), lp) + (negRM * rp);
+
+//   Rational diffm;
+//   Node diffp;
+//   decompose(diff, diffm, diffNode);
+
+
+//   std::pair<Node, DeltaRational> bestUbLeft, bestLbRight, bestUbDiff, tmp;
+//   bestUbLeft = bestLbRight = bestUbDiff = make_pair(Node::Null(), DeltaRational());
+
+//   return make_pair(false, Node::null());
+// }
+
+/**
+ * Decomposes a literal into the form:
+ *   dir*[lm*( lp )] k dir*[ [rm*( rp )] + sep ]
+ *   dir*[dm* dp]  k dir *sep
+ *   dir is either 1 or -1
+ */
+bool TheoryArithPrivate::decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm,  Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep){
+  bool negated = (lit.getKind() == kind::NOT);
+  TNode atom = negated ? lit[0] : lit;
+
+  TNode left = atom[0];
+  TNode right = atom[1];
+
+  // left : lm*( lp ) + lc
+  // right: rm*( rp ) + rc
+  Rational lc, rc;
+  bool success = decomposeTerm(left, lm, lp, lc);
+  if(!success){ return false; }
+  success = decomposeTerm(right, rm, rp, rc);
+  if(!success){ return false; }
+
+  Node diff = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::MINUS, left, right));
+  Rational dc;
+  success = decomposeTerm(diff, dm, dp, dc);
+  Assert(success);
+
+  // reduce the kind of the to not include literals
+  // GT, NOT LEQ
+  // GEQ, NOT LT
+  // LT, NOT GEQ
+  // LEQ, NOT LT
+  Kind atomKind = atom.getKind();
+  Kind normKind = negated ? negateKind(atomKind) : atomKind;
+
+  if(normKind == GEQ || normKind == GT){
+    dir = -1;
+    normKind = (normKind == GEQ) ? LEQ : LT;
+  }else{
+    dir = 1;
+  }
+
+  Debug("arith::decomp") << "arith::decomp "
+                         << lit << "(" << normKind << "*" << dir << ")"<< endl
+                         << "  left:" << lc << " + " << lm << "*(" <<  lp << ") : " <<left << endl
+                         << "  right:" << rc << " + " << rm << "*(" <<  rp << ") : " << right << endl
+                         << "  diff: " << dc << " + " << dm << "*("<< dp <<"): " << diff << endl
+                         << "  sep: " << sep << endl;
+
+
+  // k in LT, LEQ, EQUAL, DISEQUAL
+  // [dir*lm*( lp ) + dir*lc] k [dir*rm*( rp ) + dir*rc]
+  Rational change = rc - lc;
+  Assert(change == (-dc));
+  // [dir*lm*( lp )] k [dir*rm*( rp ) + dir*(rc - lc)]
+  if(normKind == LT){
+    sep = DeltaRational(change, Rational(-1));
+    k = LEQ;
+  }else{
+    sep = DeltaRational(change);
+    k = normKind;
+  }
+  // k in LEQ, EQUAL, DISEQUAL
+  // dir*lm*( lp ) k [dir*rm*( rp )] + dir*(sep + d * delta)
+  return true;
+}
+
+/**
+ *  Precondition:
+ *   tp is a polynomial not containing an ite.
+ *   either tp is constant or contains no constants.
+ *  Post:
+ *    if tmp.first is not null, then
+ *      sgn * tp <= sgn * tmp.second
+ */
+void TheoryArithPrivate::entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const {
+  tmp.first = Node::null();
+  if(sgn == 0){ return; }
+
+  Assert(Polynomial::isMember(tp));
+  if(tp.getKind() == CONST_RATIONAL){
+    tmp.first = mkBoolNode(true);
+    tmp.second = DeltaRational(tp.getConst<Rational>());
+  }else if(d_partialModel.hasArithVar(tp)){
+    Assert(tp.getKind() != CONST_RATIONAL);
+    ArithVar v = d_partialModel.asArithVar(tp);
+    Assert(v != ARITHVAR_SENTINEL);
+    ConstraintP c = (sgn > 0)
+      ? d_partialModel.getUpperBoundConstraint(v)
+      : d_partialModel.getLowerBoundConstraint(v);
+    if(c != NullConstraint){
+      tmp.first = c->externalExplainByAssertions();
+      tmp.second = c->getValue();
+    }
+  }
+}
+
+void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const {
+  tmp.first = Node::null();
+  if(sgn == 0){ return; }
+  if(tp.getKind() != PLUS){ return; }
+  Assert(Polynomial::isMember(tp));
+
+  tmp.second = DeltaRational(0);
+  NodeBuilder<> nb(kind::AND);
+
+  Polynomial p = Polynomial::parsePolynomial(tp);
+  for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) {
+    Monomial m = *i;
+    Node x = m.getVarList().getNode();
+    if(d_partialModel.hasArithVar(x)){
+      ArithVar v = d_partialModel.asArithVar(x);
+      const Rational& coeff = m.getConstant().getValue();
+      int dir = sgn * coeff.sgn();
+      ConstraintP c = (dir > 0)
+        ? d_partialModel.getUpperBoundConstraint(v)
+        : d_partialModel.getLowerBoundConstraint(v);
+      if(c != NullConstraint){
+        tmp.second += c->getValue() * coeff;
+        c->externalExplainByAssertions(nb);
+      }else{
+        //failed
+        return;
+      }
+    }else{
+      // failed
+      return;
+    }
+  }
+  // success
+  tmp.first = nb;
+}
+
+std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){
+
+  if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){
+    return make_pair(Node::null(), DeltaRational());
+  }
+
+  Assert(d_qflraStatus == Result::SAT);
+  Assert(d_errorSet.noSignals());
+  Assert(param.getAlgorithm() == inferbounds::Simplex);
+
+  // TODO Move me into a new file
+
+  enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
+  ResultState finalState = Unset;
+
+  int maxRounds = param.getSimplexRounds().just()
+    ? param.getSimplexRounds().constValue()
+    : -1;
+
+  Maybe<DeltaRational> threshold;
+  // TODO: get this from the parameters
+
+  // setup term
+  Polynomial p = Polynomial::parsePolynomial(tp);
+  vector<ArithVar> variables;
+  vector<Rational> coefficients;
+  asVectors(p, coefficients, variables);
+  if(sgn < 0){
+    for(size_t i=0, N=coefficients.size(); i < N; ++i){
+      coefficients[i] = -coefficients[i];
+    }
+  }
+  // implicitly an upperbound
+  Node skolem = mkRealSkolem("tmpVar$$");
+  ArithVar optVar = requestArithVar(skolem, false, true);
+  d_tableau.addRow(optVar, coefficients, variables);
+  RowIndex ridx = d_tableau.basicToRowIndex(optVar);
+
+  DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
+  d_partialModel.setAssignment(optVar, newAssignment);
+  d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
+
+  // Setup simplex
+  d_partialModel.stopQueueingBoundCounts();
+  UpdateTrackingCallback utcb(&d_linEq);
+  d_partialModel.processBoundsQueue(utcb);
+  d_linEq.startTrackingBoundCounts();
+
+  // maximize optVar via primal Simplex
+  int rounds = 0;
+  while(finalState == Unset){
+    ++rounds;
+    if(maxRounds >= 0 && rounds > maxRounds){
+      finalState = ExhaustedRounds;
+      break;
+    }
+
+    // select entering by bland's rule
+    // TODO improve upon bland's
+    ArithVar entering = ARITHVAR_SENTINEL;
+    const Tableau::Entry* enteringEntry = NULL;
+    for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
+      const Tableau::Entry& entry = *ri;
+      ArithVar v = entry.getColVar();
+      if(v != optVar){
+        int sgn = entry.getCoefficient().sgn();
+        Assert(sgn != 0);
+        bool candidate = (sgn > 0)
+          ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
+          : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
+        if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
+          entering = v;
+          enteringEntry = &entry;
+        }
+      }
+    }
+    if(entering == ARITHVAR_SENTINEL){
+      finalState = Inferred;
+      break;
+    }
+    Assert(entering != ARITHVAR_SENTINEL);
+    Assert(enteringEntry != NULL);
+
+    int esgn = enteringEntry->getCoefficient().sgn();
+    Assert(esgn != 0);
+
+    // select leaving and ratio
+    ArithVar leaving = ARITHVAR_SENTINEL;
+    DeltaRational minRatio;
+    const Tableau::Entry* pivotEntry = NULL;
+
+    // Special case check the upper/lowerbound on entering
+    ConstraintP cOnEntering = (esgn > 0)
+      ? d_partialModel.getUpperBoundConstraint(entering)
+      : d_partialModel.getLowerBoundConstraint(entering);
+    if(cOnEntering != NullConstraint){
+      leaving = entering;
+      minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
+    }
+    for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
+      const Tableau::Entry& centry = *ci;
+      ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
+      int csgn = centry.getCoefficient().sgn();
+      int basicDir = csgn * esgn;
+
+      ConstraintP bound = (basicDir > 0)
+        ? d_partialModel.getUpperBoundConstraint(basic)
+        : d_partialModel.getLowerBoundConstraint(basic);
+      if(bound != NullConstraint){
+        DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
+        DeltaRational ratio = diff/(centry.getCoefficient());
+        bool selected = false;
+        if(leaving == ARITHVAR_SENTINEL){
+          selected = true;
+        }else{
+          int cmp = ratio.compare(minRatio);
+          if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
+            selected = (cmp != 0) ||
+              ((leaving != entering) && (basic < leaving));
+          }
+        }
+        if(selected){
+          leaving = basic;
+          minRatio = ratio;
+          pivotEntry = &centry;
+        }
+      }
+    }
+
+
+    if(leaving == ARITHVAR_SENTINEL){
+      finalState = NoBound;
+      break;
+    }else if(leaving == entering){
+      d_linEq.update(entering, minRatio);
+    }else{
+      DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
+      d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
+      // no conflicts clear signals
+      Assert(d_errorSet.noSignals());
+    }
+
+    if(threshold.just()){
+      if(d_partialModel.getAssignment(optVar) >= threshold.constValue()){
+        finalState = ReachedThreshold;
+        break;
+      }
+    }
+  };
+
+  result = InferBoundsResult(tp, sgn > 0);
+
+  // tear down term
+  switch(finalState){
+  case Inferred:
+    {
+      NodeBuilder<> nb(kind::AND);
+      for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
+        const Tableau::Entry& e =*ri;
+        ArithVar colVar = e.getColVar();
+        if(colVar != optVar){
+          const Rational& q = e.getCoefficient();
+          Assert(q.sgn() != 0);
+          ConstraintP c = (q.sgn() > 0)
+            ? d_partialModel.getUpperBoundConstraint(colVar)
+            : d_partialModel.getLowerBoundConstraint(colVar);
+          c->externalExplainByAssertions(nb);
+        }
+      }
+      Assert(nb.getNumChildren() >= 1);
+      Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
+      result.setBound(d_partialModel.getAssignment(optVar), exp);
+      result.setIsOptimal();
+      break;
+    }
+  case NoBound:
+    break;
+  case ReachedThreshold:
+    result.setReachedThreshold();
+    break;
+  case ExhaustedRounds:
+    result.setBudgetExhausted();
+    break;
+  case Unset:
+  default:
+    Unreachable();
+    break;
+  };
+
+  d_linEq.stopTrackingRowIndex(ridx);
+  d_tableau.removeBasicRow(optVar);
+  releaseArithVar(optVar);
+
+  d_linEq.stopTrackingBoundCounts();
+  d_partialModel.startQueueingBoundCounts();
+
+  if(result.foundBound()){
+    return make_pair(result.getExplanation(), result.getValue());
+  }else{
+    return make_pair(Node::null(), DeltaRational());
+  }
+}
+
+// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const inferbounds::InferBoundAlgorithm& param){
+//   Assert(param.findUpperBound());
+
+//   if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){
+//     InferBoundsResult inconsistent;
+//     inconsistent.setInconsistent();
+//     return inconsistent;
+//   }
+
+//   Assert(d_qflraStatus == Result::SAT);
+//   Assert(d_errorSet.noSignals());
+
+//   // TODO Move me into a new file
+
+//   enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
+//   ResultState finalState = Unset;
+
+//   int maxRounds = 0;
+//   switch(param.getParamKind()){
+//   case InferBoundsParameters::Unbounded:
+//     maxRounds = -1;
+//     break;
+//   case InferBoundsParameters::NumVars:
+//     maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter();
+//     break;
+//   case InferBoundsParameters::Direct:
+//     maxRounds = param.getSimplexRoundParameter();
+//     break;
+//   default: maxRounds = 0; break;
+//   }
+
+//   // setup term
+//   Polynomial p = Polynomial::parsePolynomial(t);
+//   vector<ArithVar> variables;
+//   vector<Rational> coefficients;
+//   asVectors(p, coefficients, variables);
+
+//   Node skolem = mkRealSkolem("tmpVar$$");
+//   ArithVar optVar = requestArithVar(skolem, false, true);
+//   d_tableau.addRow(optVar, coefficients, variables);
+//   RowIndex ridx = d_tableau.basicToRowIndex(optVar);
+
+//   DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
+//   d_partialModel.setAssignment(optVar, newAssignment);
+//   d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
+
+//   // Setup simplex
+//   d_partialModel.stopQueueingBoundCounts();
+//   UpdateTrackingCallback utcb(&d_linEq);
+//   d_partialModel.processBoundsQueue(utcb);
+//   d_linEq.startTrackingBoundCounts();
+
+//   // maximize optVar via primal Simplex
+//   int rounds = 0;
+//   while(finalState == Unset){
+//     ++rounds;
+//     if(maxRounds >= 0 && rounds > maxRounds){
+//       finalState = ExhaustedRounds;
+//       break;
+//     }
+
+//     // select entering by bland's rule
+//     // TODO improve upon bland's
+//     ArithVar entering = ARITHVAR_SENTINEL;
+//     const Tableau::Entry* enteringEntry = NULL;
+//     for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
+//       const Tableau::Entry& entry = *ri;
+//       ArithVar v = entry.getColVar();
+//       if(v != optVar){
+//         int sgn = entry.getCoefficient().sgn();
+//         Assert(sgn != 0);
+//         bool candidate = (sgn > 0)
+//           ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
+//           : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
+//         if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
+//           entering = v;
+//           enteringEntry = &entry;
+//         }
+//       }
+//     }
+//     if(entering == ARITHVAR_SENTINEL){
+//       finalState = Inferred;
+//       break;
+//     }
+//     Assert(entering != ARITHVAR_SENTINEL);
+//     Assert(enteringEntry != NULL);
+
+//     int esgn = enteringEntry->getCoefficient().sgn();
+//     Assert(esgn != 0);
+
+//     // select leaving and ratio
+//     ArithVar leaving = ARITHVAR_SENTINEL;
+//     DeltaRational minRatio;
+//     const Tableau::Entry* pivotEntry = NULL;
+
+//     // Special case check the upper/lowerbound on entering
+//     ConstraintP cOnEntering = (esgn > 0)
+//       ? d_partialModel.getUpperBoundConstraint(entering)
+//       : d_partialModel.getLowerBoundConstraint(entering);
+//     if(cOnEntering != NullConstraint){
+//       leaving = entering;
+//       minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
+//     }
+//     for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
+//       const Tableau::Entry& centry = *ci;
+//       ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
+//       int csgn = centry.getCoefficient().sgn();
+//       int basicDir = csgn * esgn;
+
+//       ConstraintP bound = (basicDir > 0)
+//         ? d_partialModel.getUpperBoundConstraint(basic)
+//         : d_partialModel.getLowerBoundConstraint(basic);
+//       if(bound != NullConstraint){
+//         DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
+//         DeltaRational ratio = diff/(centry.getCoefficient());
+//         bool selected = false;
+//         if(leaving == ARITHVAR_SENTINEL){
+//           selected = true;
+//         }else{
+//           int cmp = ratio.compare(minRatio);
+//           if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
+//             selected = (cmp != 0) ||
+//               ((leaving != entering) && (basic < leaving));
+//           }
+//         }
+//         if(selected){
+//           leaving = basic;
+//           minRatio = ratio;
+//           pivotEntry = &centry;
+//         }
+//       }
+//     }
+
+
+//     if(leaving == ARITHVAR_SENTINEL){
+//       finalState = NoBound;
+//       break;
+//     }else if(leaving == entering){
+//       d_linEq.update(entering, minRatio);
+//     }else{
+//       DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
+//       d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
+//       // no conflicts clear signals
+//       Assert(d_errorSet.noSignals());
+//     }
+
+//     if(param.useThreshold()){
+//       if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){
+//         finalState = ReachedThreshold;
+//         break;
+//       }
+//     }
+//   };
+
+//   InferBoundsResult result(t, param.findUpperBound());
+
+//   // tear down term
+//   switch(finalState){
+//   case Inferred:
+//     {
+//       NodeBuilder<> nb(kind::AND);
+//       for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
+//         const Tableau::Entry& e =*ri;
+//         ArithVar colVar = e.getColVar();
+//         if(colVar != optVar){
+//           const Rational& q = e.getCoefficient();
+//           Assert(q.sgn() != 0);
+//           ConstraintP c = (q.sgn() > 0)
+//             ? d_partialModel.getUpperBoundConstraint(colVar)
+//             : d_partialModel.getLowerBoundConstraint(colVar);
+//           c->externalExplainByAssertions(nb);
+//         }
+//       }
+//       Assert(nb.getNumChildren() >= 1);
+//       Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
+//       result.setBound(d_partialModel.getAssignment(optVar), exp);
+//       result.setIsOptimal();
+//       break;
+//     }
+//   case NoBound:
+//     break;
+//   case ReachedThreshold:
+//     result.setReachedThreshold();
+//     break;
+//   case ExhaustedRounds:
+//     result.setBudgetExhausted();
+//     break;
+//   case Unset:
+//   default:
+//     Unreachable();
+//     break;
+//   };
+
+//   d_linEq.stopTrackingRowIndex(ridx);
+//   d_tableau.removeBasicRow(optVar);
+//   releaseArithVar(optVar);
+
+//   d_linEq.stopTrackingBoundCounts();
+//   d_partialModel.startQueueingBoundCounts();
+
+//   return result;
+// }
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 68e839ef8..5e7943e5e 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -64,6 +64,7 @@
 
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
+#include "theory/arith/infer_bounds.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/matrix.h"
 
@@ -92,6 +93,13 @@ class BranchCutInfo;
 class TreeLog;
 class ApproximateStatistics;
 
+class ArithEntailmentCheckParameters;
+class ArithEntailmentCheckSideEffects;
+namespace inferbounds {
+  class InferBoundAlgorithm;
+}
+class InferBoundsResult;
+
 /**
  * Implementation of QF_LRA.
  * Based upon:
@@ -146,7 +154,42 @@ public:
   void releaseArithVar(ArithVar v);
   void signal(ArithVar v){ d_errorSet.signalVariable(v); }
 
+
 private:
+  // t does not contain constants
+  void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
+  void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
+
+  std::pair<Node, DeltaRational> entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out);
+
+  //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p);
+  //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p);
+  //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p);
+
+  /**
+   * Infers either a new upper/lower bound on term in the real relaxation.
+   * Either:
+   * - term is malformed (see below)
+   * - a maximum/minimum is found with the result being a pair
+   * -- <dr, exp> where
+   * -- term <?> dr is implies by exp
+   * -- <?> is <= if inferring an upper bound, >= otherwise
+   * -- exp is in terms of the assertions to the theory.
+   * - No upper or lower bound is inferrable in the real relaxation.
+   * -- Returns <0, Null()>
+   * - the maximum number of rounds was exhausted:
+   * -- Returns <v, term> where v is the current feasible value of term
+   * - Threshold reached:
+   * -- If theshold != NULL, and a feasible value is found to exceed threshold
+   * -- Simplex stops and returns <threshold, term>
+   */
+  //std::pair<DeltaRational, Node> inferBound(TNode term, bool lb, int maxRounds = -1, const DeltaRational* threshold = NULL);
+
+private:
+  static bool decomposeTerm(Node term, Rational& m, Node& p, Rational& c);
+  static bool decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm,  Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep);
+  static void setToMin(int sgn, std::pair<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e);
+
   /**
    * The map between arith variables to nodes.
    */
@@ -427,6 +470,10 @@ public:
 
   Node getModelValue(TNode var);
 
+
+  std::pair<bool, Node> entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out);
+
+
 private:
 
   /** The constant zero. */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index c8a08dad9..06858cf92 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -208,6 +208,7 @@ void InstantiationEngine::check( Theory::Effort e ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
       Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
     }
+    ++(d_statistics.d_instantiation_rounds);
     bool quantActive = false;
     Debug("quantifiers") << "quantifiers:  check:  asserted quantifiers size"
                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
@@ -438,7 +439,8 @@ InstantiationEngine::Statistics::Statistics():
   d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
   d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
   d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
-  d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0)
+  d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0),
+  d_instantiation_rounds("InstantiationEngine::Rounds", 0 )
 {
   StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
   StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
@@ -447,6 +449,7 @@ InstantiationEngine::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
+  StatisticsRegistry::registerStat(&d_instantiation_rounds);
 }
 
 InstantiationEngine::Statistics::~Statistics(){
@@ -457,4 +460,5 @@ InstantiationEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
+  StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
 }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 53777d362..a460f1164 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -149,6 +149,7 @@ public:
     IntStat d_instantiations_cbqi_arith;
     IntStat d_instantiations_cbqi_arith_minus;
     IntStat d_instantiations_cbqi_datatypes;
+    IntStat d_instantiation_rounds;
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index e733764f0..f4acfb926 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -126,6 +126,8 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default
  what effort to apply conflict find mechanism
 option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
  when to invoke conflict find mechanism for quantifiers
+option qcfTConstraint --qcf-tconstraint bool :read-write :default false
+ enable entailment checks for t-constraints in qcf algorithm
 
 option quantRewriteRules --rewrite-rules bool :default true
  use rewrite rules module
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index e27d438be..2f399be33 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -91,24 +91,44 @@ void QuantInfo::initialize( Node q, Node qn ) {
   d_mg = new MatchGen( this, qn );

 

   if( d_mg->isValid() ){

-    for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){

-      if( d_vars[j].getKind()!=BOUND_VARIABLE ){

-        bool beneathQuant = d_nbeneathQuant.find( d_vars[j] )==d_nbeneathQuant.end();

-        d_var_mg[j] = new MatchGen( this, d_vars[j], true, beneathQuant );

-        if( !d_var_mg[j]->isValid() ){

-          d_mg->setInvalid();

-          break;

-        }else{

-          std::vector< int > bvars;

-          d_var_mg[j]->determineVariableOrder( this, bvars );

-        }

+    /*

+    for( unsigned j=0; j<q[0].getNumChildren(); j++ ){

+      if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){

+        Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;

+        d_mg->setInvalid();

+        break;

       }

     }

-

+    */

     if( d_mg->isValid() ){

-      std::vector< int > bvars;

-      d_mg->determineVariableOrder( this, bvars );

+      for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){

+        if( d_vars[j].getKind()!=BOUND_VARIABLE ){

+          d_var_mg[j] = NULL;

+          bool is_tsym = false;

+          if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){

+            is_tsym = true;

+            d_tsym_vars.push_back( j );

+          }

+          if( !is_tsym || options::qcfTConstraint() ){

+            d_var_mg[j] = new MatchGen( this, d_vars[j], true );

+          }

+          if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){

+            Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;

+            d_mg->setInvalid();

+            break;

+          }else{

+            std::vector< int > bvars;

+            d_var_mg[j]->determineVariableOrder( this, bvars );

+          }

+        }

+      }

+      if( d_mg->isValid() ){

+        std::vector< int > bvars;

+        d_mg->determineVariableOrder( this, bvars );

+      }

     }

+  }else{

+    Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;

   }

   Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;

 }

@@ -131,20 +151,24 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
           for( unsigned i=1; i<=2; i++ ){

             flatten( n[i], beneathQuant );

           }

+          registerNode( n[0], false, pol, beneathQuant );

+        }else if( options::qcfTConstraint() ){

+          //a theory-specific predicate

+          for( unsigned i=0; i<n.getNumChildren(); i++ ){

+            flatten( n[i], beneathQuant );

+          }

         }

       }

-    }

-    if( isVar( n ) && !beneathQuant ){

-      d_nbeneathQuant[n] = true;

-    }

-    for( unsigned i=0; i<n.getNumChildren(); i++ ){

-      bool newHasPol;

-      bool newPol;

-      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );

-      //QcfNode * qcfc = new QcfNode( d_c );

-      //qcfc->d_parent = qcf;

-      //qcf->d_child[i] = qcfc;

-      registerNode( n[i], newHasPol, newPol, beneathQuant );

+    }else{

+      for( unsigned i=0; i<n.getNumChildren(); i++ ){

+        bool newHasPol;

+        bool newPol;

+        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );

+        //QcfNode * qcfc = new QcfNode( d_c );

+        //qcfc->d_parent = qcf;

+        //qcf->d_child[i] = qcfc;

+        registerNode( n[i], newHasPol, newPol, beneathQuant );

+      }

     }

   }

 }

@@ -152,6 +176,10 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
 void QuantInfo::flatten( Node n, bool beneathQuant ) {

   Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;

   if( n.hasBoundVar() ){

+    if( n.getKind()==BOUND_VARIABLE ){

+      d_inMatchConstraint[n] = true;

+    }

+    //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){

     if( d_var_num.find( n )==d_var_num.end() ){

       Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;

       d_var_num[n] = d_vars.size();

@@ -165,9 +193,6 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
           flatten( n[i], beneathQuant );

         }

       }

-      if( !beneathQuant ){

-        d_nbeneathQuant[n] = true;

-      }

     }else{

       Trace("qcf-qregister-debug2") << "...already processed" << std::endl;

     }

@@ -183,6 +208,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
     d_match_term[i] = TNode::null();

   }

   d_curr_var_deq.clear();

+  d_tconstraints.clear();

   //add built-in variable constraints

   for( unsigned r=0; r<2; r++ ){

     for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();

@@ -270,6 +296,8 @@ bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, boo
       }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){

         //they must actually be disequal if we are looking for conflicts

         if( !p->areDisequal( n, cv ) ){

+          //TODO : check for entailed disequal

+

           return false;

         }

       }

@@ -462,6 +490,53 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   return false;

 }

 

+bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {

+  if( !d_tconstraints.empty() ){

+    //check constraints

+    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){

+      //apply substitution to the tconstraint

+      Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(),

+                                        p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(),

+                                        terms.begin(), terms.end() );

+      cons = it->second ? cons : cons.negate();

+      if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){

+        return true;

+      }

+    }

+  }

+  return false;

+}

+

+bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {

+  Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;

+  Node rew = Rewriter::rewrite( lit );

+  if( rew==p->d_false ){

+    Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;

+    return false;

+  }else if( rew!=p->d_true ){

+    //if checking for conflicts, we must be sure that the constraint is entailed

+    if( chEnt ){

+      //check if it is entailed

+      Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;

+      std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );

+      ++(p->d_statistics.d_entailment_checks);

+      Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;

+      if( !et.first ){

+        Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;

+        return false;

+      }else{

+        return true;

+      }

+    }else{

+      Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;

+      return true;

+    }

+  }else{

+    Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;

+    return true;

+  }

+}

+

 bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {

   //assign values for variables that were unassigned (usually not necessary, but handles corner cases)

   bool doFail = false;

@@ -470,27 +545,124 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
     doFail = true;

     success = false;

   }else{

-    d_unassigned.clear();

-    d_unassigned_tn.clear();

-    std::vector< int > unassigned[2];

-    std::vector< TypeNode > unassigned_tn[2];

-    for( int i=0; i<getNumVars(); i++ ){

-      if( d_match[i].isNull() ){

-        int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;

-        unassigned[rindex].push_back( i );

-        unassigned_tn[rindex].push_back( getVar( i ).getType() );

-        assigned.push_back( i );

-      }

-    }

-    d_unassigned_nvar = unassigned[0].size();

-    for( unsigned i=0; i<2; i++ ){

-      d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );

-      d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );

+    //solve for interpreted symbol matches

+    //   this breaks the invariant that all introduced constraints are over existing terms

+    for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){

+      int index = d_tsym_vars[i];

+      TNode v = getCurrentValue( d_vars[index] );

+      int slv_v = -1;

+      if( v==d_vars[index] ){

+        slv_v = index;

+      }

+      Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;

+      if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){

+        Kind k = d_vars[index].getKind();

+        std::vector< TNode > children;

+        for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){

+          int vn = getVarNum( d_vars[index][j] );

+          if( vn!=-1 ){

+            TNode vv = getCurrentValue( d_vars[index][j] );

+            if( vv==d_vars[index][j] ){

+              //we will assign this

+              if( slv_v==-1 ){

+                Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;

+                slv_v = vn;

+                if( p->d_effort!=QuantConflictFind::effort_conflict ){

+                  break;

+                }

+              }else{

+                Node z = p->getZero( k );

+                if( !z.isNull() ){

+                  Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;

+                  assigned.push_back( vn );

+                  if( !setMatch( p, vn, z ) ){

+                    success = false;

+                    break;

+                  }

+                }

+              }

+            }else{

+              Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;

+              children.push_back( vv );

+            }

+          }else{

+            Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;

+            children.push_back( d_vars[index][j] );

+          }

+        }

+        if( success ){

+          if( slv_v!=-1 ){

+            Node lhs;

+            if( children.empty() ){

+              lhs = p->getZero( k );

+            }else if( children.size()==1 ){

+              lhs = children[0];

+            }else{

+              lhs = NodeManager::currentNM()->mkNode( k, children );

+            }

+            Node sum;

+            if( v==d_vars[index] ){

+              sum = lhs;

+            }else{

+              if( p->d_effort==QuantConflictFind::effort_conflict ){

+                Kind kn = k;

+                if( d_vars[index].getKind()==PLUS ){

+                  kn = MINUS;

+                }

+                if( kn!=k ){

+                  sum = NodeManager::currentNM()->mkNode( kn, v, lhs );

+                }

+              }

+            }

+            if( !sum.isNull() ){

+              assigned.push_back( slv_v );

+              Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;

+              if( !setMatch( p, slv_v, sum ) ){

+                success = false;

+              }

+              p->d_tempCache.push_back( sum );

+            }

+          }else{

+            //must show that constraint is met

+            Node sum = NodeManager::currentNM()->mkNode( k, children );

+            Node eq = sum.eqNode( v );

+            if( !entailmentTest( p, eq ) ){

+              success = false;

+            }

+            p->d_tempCache.push_back( sum );

+          }

+        }

+      }

+

+      if( !success ){

+        break;

+      }

+    }

+    if( success ){

+      //check what is left to assign

+      d_unassigned.clear();

+      d_unassigned_tn.clear();

+      std::vector< int > unassigned[2];

+      std::vector< TypeNode > unassigned_tn[2];

+      for( int i=0; i<getNumVars(); i++ ){

+        if( d_match[i].isNull() ){

+          int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;

+          unassigned[rindex].push_back( i );

+          unassigned_tn[rindex].push_back( getVar( i ).getType() );

+          assigned.push_back( i );

+        }

+      }

+      d_unassigned_nvar = unassigned[0].size();

+      for( unsigned i=0; i<2; i++ ){

+        d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );

+        d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );

+      }

+      d_una_eqc_count.clear();

+      d_una_index = 0;

     }

-    d_una_eqc_count.clear();

-    d_una_index = 0;

   }

-  if( !d_unassigned.empty() ){

+

+  if( !d_unassigned.empty() && ( success || doContinue ) ){

     Trace("qcf-check") << "Assign to unassigned..." << std::endl;

     do {

       if( doFail ){

@@ -571,6 +743,12 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
     }while( success && isMatchSpurious( p ) );

   }

   if( success ){

+    for( unsigned i=0; i<d_unassigned.size(); i++ ){

+      int ui = d_unassigned[i];

+      if( !d_match[ui].isNull() ){

+        Trace("qcf-check") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;

+      }

+    }

     return true;

   }else{

     for( unsigned i=0; i<assigned.size(); i++ ){

@@ -623,42 +801,21 @@ void QuantInfo::debugPrintMatch( const char * c ) {
     }

     Trace(c) <<  std::endl;

   }

+  if( !d_tconstraints.empty() ){

+    Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;

+    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){

+      Trace(c) << "   " << it->first << " -> " << it->second << std::endl;

+    }

+  }

 }

 

-//void QuantInfo::addFuncParent( int v, Node f, int arg ) {

-//  if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){

-//    d_f_parent[v][f].push_back( arg );

-//  }

-//}

-

-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){

-  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << ", beneathQuant = " << beneathQuant << std::endl;

+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){

+  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;

   std::vector< Node > qni_apps;

   d_qni_size = 0;

   if( isVar ){

     Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );

-    if( isHandledUfTerm( n ) ){

-      d_qni_var_num[0] = qi->getVarNum( n );

-      d_qni_size++;

-      d_type = typ_var;

-      d_type_not = false;

-      d_n = n;

-      //Node f = getOperator( n );

-      for( unsigned j=0; j<d_n.getNumChildren(); j++ ){

-        Node nn = d_n[j];

-        Trace("qcf-qregister-debug") << "  " << d_qni_size;

-        if( qi->isVar( nn ) ){

-          int v = qi->d_var_num[nn];

-          Trace("qcf-qregister-debug") << " is var #" << v << std::endl;

-          d_qni_var_num[d_qni_size] = v;

-          //qi->addFuncParent( v, f, j );

-        }else{

-          Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;

-          d_qni_gterm[d_qni_size] = nn;

-        }

-        d_qni_size++;

-      }

-    }else if( n.getKind()==ITE ){

+    if( n.getKind()==ITE ){

       d_type = typ_ite_var;

       d_type_not = false;

       d_n = n;

@@ -678,8 +835,26 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
         d_type = typ_invalid;

       }

     }else{

-      //for now, unknown term

-      d_type = typ_invalid;

+      d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;

+      d_qni_var_num[0] = qi->getVarNum( n );

+      d_qni_size++;

+      d_type_not = false;

+      d_n = n;

+      //Node f = getOperator( n );

+      for( unsigned j=0; j<d_n.getNumChildren(); j++ ){

+        Node nn = d_n[j];

+        Trace("qcf-qregister-debug") << "  " << d_qni_size;

+        if( qi->isVar( nn ) ){

+          int v = qi->d_var_num[nn];

+          Trace("qcf-qregister-debug") << " is var #" << v << std::endl;

+          d_qni_var_num[d_qni_size] = v;

+          //qi->addFuncParent( v, f, j );

+        }else{

+          Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;

+          d_qni_gterm[d_qni_size] = nn;

+        }

+        d_qni_size++;

+      }

     }

   }else{

     if( n.hasBoundVar() ){

@@ -693,10 +868,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
       if( isHandledBoolConnective( d_n ) ){

         //non-literals

         d_type = typ_formula;

-        bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL;

         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){

           if( d_n.getKind()!=FORALL || i==1 ){

-            d_children.push_back( MatchGen( qi, d_n[i], false, nBeneathQuant ) );

+            d_children.push_back( MatchGen( qi, d_n[i], false ) );

             if( !d_children[d_children.size()-1].isValid() ){

               setInvalid();

               break;

@@ -726,25 +900,28 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
       }else{

         d_type = typ_invalid;

         //literals

-        if( d_n.getKind()==EQUAL ){

-          for( unsigned i=0; i<2; i++ ){

+        if( isHandledUfTerm( d_n ) ){

+          Assert( qi->isVar( d_n ) );

+          d_type = typ_pred;

+        }else if( d_n.getKind()==BOUND_VARIABLE ){

+          Assert( d_n.getType().isBoolean() );

+          d_type = typ_bool_var;

+        }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){

+          for( unsigned i=0; i<d_n.getNumChildren(); i++ ){

             if( d_n[i].hasBoundVar() ){

               if( !qi->isVar( d_n[i] ) ){

                 Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;

               }

               Assert( qi->isVar( d_n[i] ) );

+              if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){

+                d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];

+              }

             }else{

               d_qni_gterm[i] = d_n[i];

             }

           }

-          d_type = typ_eq;

-        }else if( isHandledUfTerm( d_n ) ){

-          Assert( qi->isVar( d_n ) );

-          d_type = typ_pred;

-        }else if( d_n.getKind()==BOUND_VARIABLE ){

-          d_type = typ_bool_var;

-        }else{

-          Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl;

+          d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;

+          Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;

         }

       }

     }else{

@@ -900,7 +1077,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
 

   //set up processing matches

   if( d_type==typ_invalid ){

-    //do nothing : return success once?

+    //do nothing

   }else if( d_type==typ_ground ){

     if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){

       d_child_counter = 0;

@@ -933,6 +1110,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       d_qn.push_back( qni );

     }

     d_matched_basis = false;

+  }else if( d_type==typ_tsym || d_type==typ_tconstraint ){

+    for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){

+      int repVar = qi->getCurrentRepVar( it->second );

+      if( qi->d_match[repVar].isNull() ){

+        Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;

+        d_qni_bound[it->first] = repVar;

+      }

+    }

+    d_qn.push_back( NULL );

   }else if( d_type==typ_pred || d_type==typ_eq ){

     //add initial constraint

     Node nn[2];

@@ -1031,7 +1217,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
       d_wasSet = false;

       return false;

     }

-  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var ){

+  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){

     bool success = false;

     bool terminate = false;

     do {

@@ -1043,6 +1229,18 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
           d_binding = true;

           d_binding_it = d_qni_bound.begin();

           doReset = true;

+          //for tconstraint, add constraint

+          if( d_type==typ_tconstraint ){

+            std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );

+            if( it==qi->d_tconstraints.end() ){

+              qi->d_tconstraints[d_n] = d_tgt;

+              //store that we added this constraint

+              d_qni_bound_cons[0] = d_n;

+            }else if( d_tgt!=it->second ){

+              success = false;

+              terminate = true;

+            }

+          }

         }else{

           Debug("qcf-match-debug") << "     - Matching failed" << std::endl;

           success = false;

@@ -1128,6 +1326,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         }

         d_qni_bound.clear();

       }

+      if( d_type==typ_tconstraint ){

+        //remove constraint if applicable

+        if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){

+          qi->d_tconstraints.erase( d_n );

+          d_qni_bound_cons.clear();

+        }

+      }

       /*

       if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){

         d_matched_basis = true;

@@ -1869,7 +2074,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
     if( d_performCheck ){

       ++(d_statistics.d_inst_rounds);

       double clSet = 0;

+      int prevEt = 0;

       if( Trace.isOn("qcf-engine") ){

+        prevEt = d_statistics.d_entailment_checks.getData();

         clSet = double(clock())/double(CLOCKS_PER_SEC);

         Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;

       }

@@ -1980,31 +2187,37 @@ void QuantConflictFind::check( Theory::Effort level ) {
                   */

                   std::vector< Node > terms;

                   qi->getMatch( terms );

-                  if( Debug.isOn("qcf-check-inst") ){

-                    //if( e==effort_conflict ){

-                    Node inst = d_quantEngine->getInstantiation( q, terms );

-                    Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

-                    Assert( evaluate( inst )!=1 );

-                    Assert( evaluate( inst )==-1 || e>effort_conflict );

-                    //}

-                  }

-                  if( d_quantEngine->addInstantiation( q, terms ) ){

-                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;

-                    ++addedLemmas;

-                    if( e==effort_conflict ){

-                      d_quant_order.insert( d_quant_order.begin(), q );

-                      d_conflict.set( true );

-                      ++(d_statistics.d_conflict_inst);

-                      break;

-                    }else if( e==effort_prop_eq ){

-                      ++(d_statistics.d_prop_inst);

+                  if( !qi->isTConstraintSpurious( this, terms ) ){

+                    if( Debug.isOn("qcf-check-inst") ){

+                      //if( e==effort_conflict ){

+                      Node inst = d_quantEngine->getInstantiation( q, terms );

+                      Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

+                      Assert( evaluate( inst )!=1 );

+                      Assert( evaluate( inst )==-1 || e>effort_conflict );

+                      //}

+                    }

+                    if( d_quantEngine->addInstantiation( q, terms ) ){

+                      Trace("qcf-check") << "   ... Added instantiation" << std::endl;

+                      Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;

+                      qi->debugPrintMatch("qcf-inst");

+                      Trace("qcf-inst") << std::endl;

+                      ++addedLemmas;

+                      if( e==effort_conflict ){

+                        d_quant_order.insert( d_quant_order.begin(), q );

+                        d_conflict.set( true );

+                        ++(d_statistics.d_conflict_inst);

+                        break;

+                      }else if( e==effort_prop_eq ){

+                        ++(d_statistics.d_prop_inst);

+                      }

+                    }else{

+                      Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

+                      //Assert( false );

                     }

-                  }else{

-                    Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

-                    //Assert( false );

                   }

                   //clean up assigned

                   qi->revertMatch( assigned );

+                  d_tempCache.clear();

                 }else{

                   Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

                 }

@@ -2030,6 +2243,8 @@ void QuantConflictFind::check( Theory::Effort level ) {
           Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;

         }

         Trace("qcf-engine") << std::endl;

+        int currEt = d_statistics.d_entailment_checks.getData();

+        Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;

       }

     }

     Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;

@@ -2275,17 +2490,35 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 QuantConflictFind::Statistics::Statistics():

   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),

   d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),

-  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )

+  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),

+  d_entailment_checks("QuantConflictFind::Entailment_Checks",0)

 {

   StatisticsRegistry::registerStat(&d_inst_rounds);

   StatisticsRegistry::registerStat(&d_conflict_inst);

   StatisticsRegistry::registerStat(&d_prop_inst);

+  StatisticsRegistry::registerStat(&d_entailment_checks);

 }

 

 QuantConflictFind::Statistics::~Statistics(){

   StatisticsRegistry::unregisterStat(&d_inst_rounds);

   StatisticsRegistry::unregisterStat(&d_conflict_inst);

   StatisticsRegistry::unregisterStat(&d_prop_inst);

+  StatisticsRegistry::unregisterStat(&d_entailment_checks);

 }

 

+TNode QuantConflictFind::getZero( Kind k ) {

+  std::map< Kind, Node >::iterator it = d_zero.find( k );

+  if( it==d_zero.end() ){

+    Node nn;

+    if( k==PLUS ){

+      nn = NodeManager::currentNM()->mkConst( Rational(0) );

+    }

+    d_zero[k] = nn;

+    return nn;

+  }else{

+    return it->second;

+  }

+}

+

+

 }

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 71e967653..64ece7ed0 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -84,11 +84,13 @@ public:
     typ_var,

     typ_ite_var,

     typ_bool_var,

+    typ_tconstraint,

+    typ_tsym,

   };

   void debugPrintType( const char * c, short typ, bool isTrace = false );

 public:

   MatchGen() : d_type( typ_invalid ){}

-  MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false );

+  MatchGen( QuantInfo * qi, Node n, bool isVar = false );

   bool d_tgt;

   bool d_tgt_orig;

   bool d_wasSet;

@@ -128,7 +130,8 @@ public:
   ~QuantInfo() { delete d_mg; }

   std::vector< TNode > d_vars;

   std::map< TNode, int > d_var_num;

-  std::map< TNode, bool > d_nbeneathQuant;

+  std::vector< int > d_tsym_vars;

+  std::map< TNode, bool > d_inMatchConstraint;

   std::map< int, std::vector< Node > > d_var_constraint[2];

   int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }

   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }

@@ -146,6 +149,7 @@ public:
   std::vector< TNode > d_match;

   std::vector< TNode > d_match_term;

   std::map< int, std::map< TNode, int > > d_curr_var_deq;

+  std::map< Node, bool > d_tconstraints;

   int getCurrentRepVar( int v );

   TNode getCurrentValue( TNode n );

   TNode getCurrentExpValue( TNode n );

@@ -154,6 +158,8 @@ public:
   int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );

   bool setMatch( QuantConflictFind * p, int v, TNode n );

   bool isMatchSpurious( QuantConflictFind * p );

+  bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );

+  bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );

   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );

   void revertMatch( std::vector< int >& assigned );

   void debugPrintMatch( const char * c );

@@ -174,6 +180,9 @@ private:
   context::CDO< bool > d_conflict;

   bool d_performCheck;

   std::vector< Node > d_quant_order;

+  std::map< Kind, Node > d_zero;

+  //for storing nodes created during t-constraint solving (prevents memory leaks)

+  std::vector< Node > d_tempCache;

 private:

   std::map< Node, Node > d_op_node;

   int d_fid_count;

@@ -182,6 +191,7 @@ private:
 public:  //for ground terms

   Node d_true;

   Node d_false;

+  TNode getZero( Kind k );

 private:

   Node evaluateTerm( Node n );

   int evaluate( Node n, bool pref = false, bool hasPref = false );

@@ -271,6 +281,7 @@ public:
     IntStat d_inst_rounds;

     IntStat d_conflict_inst;

     IntStat d_prop_inst;

+    IntStat d_entailment_checks;

     Statistics();

     ~Statistics();

   };

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 41108bc2a..757a76baa 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -207,7 +207,7 @@ public:
   Node getSkolemizedBody( Node f );
 
 //miscellaneous
-private:
+public:
   /** map from universal quantifiers to the list of variables */
   std::map< Node, std::vector< Node > > d_vars;
   /** free variable for instantiation constant type */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index c52ee936a..f65e48ec2 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -228,6 +228,32 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstituti
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
+std::pair<bool, Node> Theory::entailmentCheck(TNode lit,
+                                              const EntailmentCheckParameters* params,
+                                              EntailmentCheckSideEffects* out){
+  return make_pair(false, Node::null());
+}
+
+EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
+  : d_tid(tid) {
+}
+
+EntailmentCheckParameters::~EntailmentCheckParameters(){}
+
+TheoryId EntailmentCheckParameters::getTheoryId() const {
+  return d_tid;
+}
+
+EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
+  : d_tid(tid)
+{}
+
+TheoryId EntailmentCheckSideEffects::getTheoryId() const {
+  return d_tid;
+}
+
+EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
+}
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index c86aa17de..972abe3d8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -52,6 +52,9 @@ class QuantifiersEngine;
 class TheoryModel;
 class SubstitutionMap;
 
+class EntailmentCheckParameters;
+class EntailmentCheckSideEffects;
+
 namespace rrinst {
   class CandidateGenerator;
 }/* CVC4::theory::rrinst namespace */
@@ -808,6 +811,63 @@ public:
    * in a queriable form.  As this is
    */
   std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
+
+  /**
+   * This allows the theory to be queried for whether a literal, lit, is
+   * entailed by the theory.  This returns a pair of a Boolean and a node E.
+   *
+   * If the Boolean is true, then E is a formula that entails lit and E is propositionally
+   * entailed by the assertions to the theory.
+   *
+   * If the Boolean is false, it is "unknown" if lit is entailed and E may be
+   * any node.
+   *
+   * The literal lit is either an atom a or (not a), which must belong to the theory:
+   *   There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
+   *
+   * There are NO assumptions that a or the subterms of a have been
+   * preprocessed in any form.  This includes ppRewrite, rewriting,
+   * preregistering, registering, definition expansion or ITE removal!
+   *
+   * Theories are free to limit the amount of effort they use and so may
+   * always opt to return "unknown".  Both "unknown" and "not entailed",
+   * may return for E a non-boolean Node (e.g. Node::null()).  (There is no explicit output
+   * for the negation of lit is entailed.)
+   *
+   * If lit is theory valid, the return result may be the Boolean constant
+   * true for E.
+   *
+   * If lit is entailed by multiple assertions on the theory's getFact()
+   * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
+   * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
+   *
+   * If lit is entailed by a single assertion on the theory's getFact()
+   * queue, say a, this may return E=a.
+   *
+   * The theory may always return false!
+   *
+   * The search is controlled by the parameter params.  For default behavior,
+   * this may be left NULL.
+   *
+   * Theories that want parameters extend the virtual EntailmentCheckParameters
+   * class.  Users ask the theory for an appropriate subclass from the theory
+   * and configure that.  How this is implemented is on a per theory basis.
+   *
+   * The search may provide additional output to guide the user of
+   * this function.  This output is stored in a EntailmentCheckSideEffects*
+   * output parameter.  The implementation of this is theory specific.  For
+   * no output, this is NULL.
+   *
+   * Theories may not touch their output stream during an entailment check.
+   *
+   * @param  lit     a literal belonging to the theory.
+   * @param  params  the control parameters for the entailment check.
+   * @param  out     a theory specific output object of the entailment search.
+   * @return         a pair <b,E> s.t. if b is true, then a formula E such that
+   * E |= lit in the theory.
+   */
+  virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
+
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
@@ -852,6 +912,26 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta
   return out;
 }
 
+class EntailmentCheckParameters {
+private:
+  TheoryId d_tid;
+protected:
+  EntailmentCheckParameters(TheoryId tid);
+public:
+  TheoryId getTheoryId() const;
+  virtual ~EntailmentCheckParameters();
+};/* class EntailmentCheckParameters */
+
+class EntailmentCheckSideEffects {
+private:
+  TheoryId d_tid;
+protected:
+  EntailmentCheckSideEffects(TheoryId tid);
+public:
+  TheoryId getTheoryId() const;
+  virtual ~EntailmentCheckSideEffects();
+};/* class EntailmentCheckSideEffects */
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 33ff18126..18968e897 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1658,3 +1658,15 @@ void TheoryEngine::checkTheoryAssertionsWithModel() {
     }
   }
 }
+
+std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* seffects) {
+  TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
+  theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
+  theory::Theory* th = theoryOf(tid);
+
+  Assert(th != NULL);
+  Assert(params == NULL || tid == params->getTheoryId());
+  Assert(seffects == NULL || tid == seffects->getTheoryId());
+
+  return th->entailmentCheck(lit, params, seffects);
+}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 9a987c9d7..8bc67616f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -83,6 +83,9 @@ namespace theory {
   namespace eq {
     class EqualityEngine;
   }
+
+  class EntailmentCheckParameters;
+  class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
 class DecisionEngine;
 class RemoveITE;
@@ -755,6 +758,12 @@ public:
    */
   Node getModelValue(TNode var);
 
+  /**
+   * Forwards an entailmentCheck according to the given theoryOfMode mode.
+   * See theory.h for documentation on entailmentCheck().
+   */
+  std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
+
 private:
 
   /** Default visitor for pre-registration */
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 383f27688..bd23b48c9 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -57,3 +57,26 @@ void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, uns
     throw std::invalid_argument(ss.str());
   }
 }
+
+bool Integer::fitsSignedInt() const {
+  // TODO improve performance
+  return d_value <= std::numeric_limits<signed int>::max() &&
+    d_value >= std::numeric_limits<signed int>::min();
+}
+
+bool Integer::fitsUnsignedInt() const {
+  // TODO improve performance
+  return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::max();
+}
+
+signed int Integer::getSignedInt() const {
+  // ensure there isn't overflow
+  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
+  return cln::cl_I_to_int(d_value);
+}
+
+unsigned int Integer::getUnsignedInt() const {
+  // ensure there isn't overflow
+  CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+  return cln::cl_I_to_uint(d_value);
+}
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 05d820dbc..8b56c4b19 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -415,6 +415,16 @@ public:
     return d_value == -1;
   }
 
+  /** fits the C "signed int" primitive */
+  bool fitsSignedInt() const;
+
+  /** fits the C "unsigned int" primitive */
+  bool fitsUnsignedInt() const;
+
+  int getSignedInt() const;
+
+  unsigned int getUnsignedInt() const;
+
   long getLong() const {
     // ensure there isn't overflow
     CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index f2a888340..bb6166523 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -36,3 +36,32 @@ Integer::Integer(const char* s, unsigned base)
 Integer::Integer(const std::string& s, unsigned base)
   : d_value(s, base)
 {}
+
+
+bool Integer::fitsSignedInt() const {
+  return d_value.fits_sint_p();
+}
+
+bool Integer::fitsUnsignedInt() const {
+  return d_value.fits_uint_p();
+}
+
+signed int Integer::getSignedInt() const {
+  // ensure there isn't overflow
+  CheckArgument(d_value <= std::numeric_limits<int>::max(), this,
+                "Overflow detected in Integer::getSignedInt()");
+  CheckArgument(d_value >= std::numeric_limits<int>::min(), this,
+                "Overflow detected in Integer::getSignedInt()");
+  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
+  return (signed int) d_value.get_si();
+}
+
+unsigned int Integer::getUnsignedInt() const {
+  // ensure there isn't overflow
+  CheckArgument(d_value <= std::numeric_limits<unsigned int>::max(), this,
+                "Overflow detected in Integer::getUnsignedInt()");
+  CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this,
+                "Overflow detected in Integer::getUnsignedInt()");
+  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+  return (unsigned int) d_value.get_ui();
+}
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index a39de7996..68d335aec 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -22,6 +22,7 @@
 
 #include <string>
 #include <iostream>
+#include <limits>
 
 #include "util/gmp_util.h"
 #include "util/exception.h"
@@ -417,7 +418,13 @@ public:
     return d_value.get_str(base);
   }
 
-  //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
+  bool fitsSignedInt() const;
+
+  bool fitsUnsignedInt() const;
+
+  signed int getSignedInt() const;
+
+  unsigned int getUnsignedInt() const;
 
   long getLong() const {
     long si = d_value.get_si();
diff --git a/src/util/maybe.h b/src/util/maybe.h
index e90953e0b..b1c81f76e 100644
--- a/src/util/maybe.h
+++ b/src/util/maybe.h
@@ -75,6 +75,7 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){
   if(m.nothing()){
     out << "Nothing";
   }else{
+    out << "Just ";
     out << m.constValue();
   }
   out << "}";