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

6 files changed, 54 insertions, 14 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);
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index dda9c7a3e..696622cfe 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -121,6 +121,33 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
   }
 
   if(mk == kind::metakind::CONSTANT) {
+    if(k == kind::STORE_ALL) {
+      const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>();
+      ArrayType arrType = asa.getType();
+      TypeNode indexType = TypeNode::fromType(arrType.getIndexType());
+      Type constituentType = arrType.getConstituentType();
+      if(constituentType.isBoolean()) {
+        // we have store_all(true) or store_all(false)
+        // just turn it into store_all(1) or store_all(0)
+        Node newConst = nm->mkConst(BitVector(1u, asa.getExpr().getConst<bool>() ? 1u : 0u));
+        if(indexType.isBoolean()) {
+          // change index type to BV(1) also
+          indexType = nm->mkBitVectorType(1);
+        }
+        ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr());
+        Node n = nm->mkConst(asaRepl);
+        Debug("boolean-terms") << " returning new store_all: " << n << std::endl;
+        return n;
+      }
+      if(indexType.isBoolean()) {
+        // must change index type to BV(1)
+        indexType = nm->mkBitVectorType(1);
+        ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr());
+        Node n = nm->mkConst(asaRepl);
+        Debug("boolean-terms") << " returning new store_all: " << n << std::endl;
+        return n;
+      }
+    }
     return top;
   } else if(mk == kind::metakind::VARIABLE) {
     TypeNode t = top.getType();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fb8b78759..c82b7ca2c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -495,7 +495,7 @@ public:
     Assert(options::abstractValues());
     Node& val = d_abstractValues[n];
     if(val.isNull()) {
-      val = d_smt.d_nodeManager->mkConst(AbstractValue(d_abstractValues.size()));
+      val = d_smt.d_nodeManager->mkAbstractValue(n.getType());
       d_abstractValueMap.addSubstitution(val, n);
     }
     return val;
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 40f838623..baf498968 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -139,9 +139,9 @@ class AbstractValueTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
     // An UnknownTypeException means that this node has no type.  For now,
-    // only abstract values are like this.  Assigning them a type in all
-    // cases is difficult, since then the parser and the SmtEngine must be
-    // more tightly coupled.
+    // only abstract values are like this---and then, only if they are created
+    // by the user and don't actually correspond to one that the SmtEngine gave
+    // them previously.
     throw UnknownTypeException(n);
   }
 };/* class AbstractValueTypeRule */