Improve handling of constant array in Z3

1 files changed, 14 insertions, 8 deletions

diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index 6c0653e8..d03c4c89 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -101,6 +101,7 @@ Z3Builder::~Z3Builder() {
   // they aren associated with.
   clearConstructCache();
   _arr_hash.clear();
+  constant_array_assertions.clear();
   Z3_del_context(ctx);
   if (z3LogInteractionFile.length() > 0) {
     Z3_close_log();
@@ -400,16 +401,21 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
     array_expr = buildArray(unique_name.c_str(), root->getDomain(),
                             root->getRange());
 
-    if (root->isConstantArray()) {
-      // FIXME: Flush the concrete values into Z3. Ideally we would do this
-      // using assertions, which might be faster, but we need to fix the caching
-      // to work correctly in that case.
+    if (root->isConstantArray() && constant_array_assertions.count(root) == 0) {
+      std::vector<Z3ASTHandle> array_assertions;
       for (unsigned i = 0, e = root->size; i != e; ++i) {
-        Z3ASTHandle prev = array_expr;
-        array_expr = writeExpr(
-            prev, construct(ConstantExpr::alloc(i, root->getDomain()), 0),
-            construct(root->constantValues[i], 0));
+        // construct(= (select i root) root->value[i]) to be asserted in
+        // Z3Solver.cpp
+        int width_out;
+        Z3ASTHandle array_value =
+            construct(root->constantValues[i], &width_out);
+        assert(width_out == (int)root->getRange() &&
+               "Value doesn't match root range");
+        array_assertions.push_back(
+            eqExpr(readExpr(array_expr, bvConst32(root->getDomain(), i)),
+                   array_value));
       }
+      constant_array_assertions[root] = std::move(array_assertions);
     }
 
     _arr_hash.hashArrayExpr(root, array_expr);