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>

1 files changed, 319 insertions, 0 deletions

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