Fix the way abstract values are typed; fixes some compliance issues.

Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).

(this commit was certified error- and warning-free by the test-and-commit script.)

3 files changed, 23 insertions, 10 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index e68873176..f6aa1920d 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1303,14 +1303,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
     kind::MetaKind mk = n.getMetaKind();
     if( mk != kind::metakind::VARIABLE
         && mk != kind::metakind::CONSTANT ) {
-      try {
-        d_nm->getType(n, true);
-      } catch(UnknownTypeException&) {
-        // Ignore the error; this expression doesn't have a type,
-        // because it has an abstract value in it.  If the user
-        // depends on the type of this expression, he should get an
-        // exception, but so far he's only constructed it.
-      }
+      d_nm->getType(n, true);
     }
   }
 }
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index f040c7c72..59d23c6ea 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -86,7 +86,8 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_attrManager(ctxt),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
-  d_inReclaimZombies(false) {
+  d_inReclaimZombies(false),
+  d_abstractValueCount(0) {
   init();
 }
 
@@ -99,7 +100,8 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_attrManager(ctxt),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
-  d_inReclaimZombies(false) {
+  d_inReclaimZombies(false),
+  d_abstractValueCount(0) {
   init();
 }
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 2cda23f2d..e94795f0e 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -171,6 +171,14 @@ class NodeManager {
   std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
 
   /**
+   * Keep a count of all abstract values produced by this NodeManager.
+   * Abstract values have a type attribute, so if multiple SmtEngines
+   * are attached to this NodeManager, we don't want their abstract
+   * values to overlap.
+   */
+  unsigned d_abstractValueCount;
+
+  /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
    * NodeValue.  In particular, "non-inlined" constants are permitted
@@ -455,6 +463,9 @@ public:
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
 
+  /** Make a new abstract value with the given type. */
+  Node mkAbstractValue(const TypeNode& type);
+
   /**
    * Create a constant of type T.  It will have the appropriate
    * CONST_* kind defined for T.
@@ -1557,6 +1568,13 @@ inline Node NodeManager::mkInstConstant(const TypeNode& type) {
   return n;
 }
 
+inline Node NodeManager::mkAbstractValue(const TypeNode& type) {
+  Node n = mkConst(AbstractValue(++d_abstractValueCount));
+  n.setAttribute(TypeAttr(), type);
+  n.setAttribute(TypeCheckedAttr(), true);
+  return n;
+}
+
 template <class T>
 Node NodeManager::mkConst(const T& val) {
   return mkConstInternal<Node, T>(val);