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.

1 files changed, 9 insertions, 1 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));