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

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;