Partial merge of integers work; this is simple B&B and some pseudoboolean

infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

5 files changed, 67 insertions, 6 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5c3e4731b..0ac215f1e 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -509,9 +509,12 @@ public:
   /** Get the (singleton) type for integers. */
   inline TypeNode integerType();
 
-  /** Get the (singleton) type for booleans. */
+  /** Get the (singleton) type for reals. */
   inline TypeNode realType();
 
+  /** Get the (singleton) type for pseudobooleans. */
+  inline TypeNode pseudobooleanType();
+
   /** Get the (singleton) type for sorts. */
   inline TypeNode kindType();
 
@@ -772,6 +775,11 @@ inline TypeNode NodeManager::realType() {
   return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
 }
 
+/** Get the (singleton) type for pseudobooleans. */
+inline TypeNode NodeManager::pseudobooleanType() {
+  return TypeNode(mkTypeConst<TypeConstant>(PSEUDOBOOLEAN_TYPE));
+}
+
 /** Get the (singleton) type for sorts. */
 inline TypeNode NodeManager::kindType() {
   return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 077fc5ee2..e162065b0 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -202,6 +202,19 @@ Type::operator RealType() const throw(AssertionException) {
   return RealType(*this);
 }
 
+/** Is this the pseudoboolean type? */
+bool Type::isPseudoboolean() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isPseudoboolean();
+}
+
+/** Cast to a pseudoboolean type */
+Type::operator PseudobooleanType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isPseudoboolean());
+  return PseudobooleanType(*this);
+}
+
 /** Is this the bit-vector type? */
 bool Type::isBitVector() const {
   NodeManagerScope nms(d_nodeManager);
@@ -435,6 +448,11 @@ RealType::RealType(const Type& t) throw(AssertionException) :
   Assert(isReal());
 }
 
+PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) :
+  Type(t) {
+  Assert(isPseudoboolean());
+}
+
 BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
   Type(t) {
   Assert(isBitVector());
diff --git a/src/expr/type.h b/src/expr/type.h
index 14ca3baf3..a63ca6cf0 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -46,6 +46,7 @@ class NodeTemplate;
 class BooleanType;
 class IntegerType;
 class RealType;
+class PseudobooleanType;
 class BitVectorType;
 class ArrayType;
 class DatatypeType;
@@ -226,6 +227,18 @@ public:
   operator RealType() const throw(AssertionException);
 
   /**
+   * Is this the pseudoboolean type?
+   * @return true if the type is the pseudoboolean type
+   */
+  bool isPseudoboolean() const;
+
+  /**
+   * Cast this type to a pseudoboolean type
+   * @return the PseudobooleanType
+   */
+  operator PseudobooleanType() const throw(AssertionException);
+
+  /**
    * Is this the bit-vector type?
    * @return true if the type is a bit-vector type
    */
@@ -410,6 +423,17 @@ public:
 };/* class RealType */
 
 /**
+ * Singleton class encapsulating the pseudoboolean type.
+ */
+class CVC4_PUBLIC PseudobooleanType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  PseudobooleanType(const Type& type) throw(AssertionException);
+};/* class PseudobooleanType */
+
+/**
  * Class encapsulating a function type.
  */
 class CVC4_PUBLIC FunctionType : public Type {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index b9047307d..76a084204 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -73,18 +73,26 @@ Node TypeNode::mkGroundTerm() const {
 
 bool TypeNode::isBoolean() const {
   return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == BOOLEAN_TYPE;
+    ( getConst<TypeConstant>() == BOOLEAN_TYPE ||
+      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
 }
 
 bool TypeNode::isInteger() const {
   return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == INTEGER_TYPE;
+    ( getConst<TypeConstant>() == INTEGER_TYPE ||
+      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
 }
 
 bool TypeNode::isReal() const {
-  return getKind() == kind::TYPE_CONSTANT
-    && ( getConst<TypeConstant>() == REAL_TYPE ||
-         getConst<TypeConstant>() == INTEGER_TYPE );
+  return getKind() == kind::TYPE_CONSTANT &&
+    ( getConst<TypeConstant>() == REAL_TYPE ||
+      getConst<TypeConstant>() == INTEGER_TYPE ||
+      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
+}
+
+bool TypeNode::isPseudoboolean() const {
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE;
 }
 
 bool TypeNode::isArray() const {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0f4b122db..3f4e52d36 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -413,6 +413,9 @@ public:
   /** Is this the Real type? */
   bool isReal() const;
 
+  /** Is this the Pseudoboolean type? */
+  bool isPseudoboolean() const;
+
   /** Is this an array type? */
   bool isArray() const;