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.)

1 files changed, 18 insertions, 0 deletions

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);