added model generation for bv subtheories and bv-inequality solver option

3 files changed, 59 insertions, 11 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5159f6b5a..eab41ee38 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -936,7 +936,7 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr
       ("export of types belonging to theory of DATATYPES kinds unsupported");
   }
   if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
-     n.getKind() != kind::SORT_TYPE) { 
+     n.getKind() != kind::SORT_TYPE) {
     throw ExportUnsupportedException
       ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
   }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 5f813dbe8..bd3827f47 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -713,6 +713,10 @@ public:
   operator Node();
   operator Node() const;
 
+  // similarly for TypeNode
+  operator TypeNode();
+  operator TypeNode() const;
+
   NodeBuilder<nchild_thresh>& operator&=(TNode);
   NodeBuilder<nchild_thresh>& operator|=(TNode);
   NodeBuilder<nchild_thresh>& operator+=(TNode);
@@ -902,6 +906,16 @@ NodeBuilder<nchild_thresh>::operator Node() const {
 }
 
 template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator TypeNode() {
+  return constructTypeNode();
+}
+
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator TypeNode() const {
+  return constructTypeNode();
+}
+
+template <unsigned nchild_thresh>
 expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   Assert(!isUsed(), "NodeBuilder is one-shot only; "
          "attempt to access it after conversion");
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 236f48017..7522b8110 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -94,15 +94,32 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
     if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
       return true;
     }
-    if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
-       getNumChildren() != t.getNumChildren()) {
+    if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
       return false;
     }
-    // children must be subtypes of t's, in order
-    for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
-      if(!(*i).isSubtypeOf(*j)) {
+    if(isTuple()) {
+      if(getNumChildren() != t.getNumChildren()) {
         return false;
       }
+      // children must be subtypes of t's, in order
+      for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
+        if(!(*i).isSubtypeOf(*j)) {
+          return false;
+        }
+      }
+    } else {
+      const Record& r1 = getConst<Record>();
+      const Record& r2 = t.getConst<Record>();
+      if(r1.getNumFields() != r2.getNumFields()) {
+        return false;
+      }
+      // r1's fields must be subtypes of r2's, in order
+      // names must match also
+      for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+        if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) {
+          return false;
+        }
+      }
     }
     return true;
   }
@@ -125,15 +142,32 @@ bool TypeNode::isComparableTo(TypeNode t) const {
          NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
         return true;
       }
-      if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
-         getNumChildren() != t.getNumChildren()) {
+      if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
         return false;
       }
-      // children must be comparable to t's, in order
-      for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
-        if(!(*i).isComparableTo(*j)) {
+      if(isTuple()) {
+        if(getNumChildren() != t.getNumChildren()) {
+          return false;
+        }
+        // children must be comparable to t's, in order
+        for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
+          if(!(*i).isComparableTo(*j)) {
+            return false;
+          }
+        }
+      } else {
+        const Record& r1 = getConst<Record>();
+        const Record& r2 = t.getConst<Record>();
+        if(r1.getNumFields() != r2.getNumFields()) {
           return false;
         }
+        // r1's fields must be comparable to r2's, in order
+        // names must match also
+        for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+          if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) {
+            return false;
+          }
+        }
       }
       return true;
     } else {