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, 38 insertions, 0 deletions

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