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>

5 files changed, 71 insertions, 1 deletions

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 << "}";