implement #953: print the initial contents of non-local memory when d…

…isplaying counterexamples

ir/memory.cpp

@@ -2371,6 +2371,40 @@ Memory Memory::mkIf(const expr &cond, Memory &&then, Memory &&els) {
     os << "\t" name ": " << v;  \
   } while(0)
 
+void Memory::print_array(ostream &os, const expr &a, unsigned indent) const {
+  expr idx, val, a2, cond, then, els;
+  if (a.isConstArray(val)) {
+    os << "else: " << Byte(*this, std::move(val)) << '\n';
+  }
+  else if (a.isStore(a2, idx, val)) {
+    os << idx << ": " << Byte(*this, std::move(val)) << '\n';
+    print_array(os, a2);
+  }
+  else if (a.isLambda(val)) {
+    print_array(os, val.subst({expr::mkVar("idx", a.lambdaIdxType())}));
+  }
+  else if (a.isBV() && a.isConst() && a.bits() == Byte::bitsByte()) {
+    os << Byte(*this, expr(a)) << '\n';
+  }
+  else if (a.isIf(cond, then, els)) {
+    auto print_spaces = [&](unsigned limit) {
+      for (unsigned i = 0; i < limit; ++i) {
+        os << "  ";
+      }
+    };
+    os << "if " << cond << '\n';
+    print_spaces(indent + 1);
+    print_array(os, then, indent + 1);
+    print_spaces(indent);
+    os << "else\n";
+    print_spaces(indent + 1);
+    print_array(os, els, indent + 1);
+  }
+  else {
+    os << a << '\n';
+  }
+}
+
 void Memory::print(ostream &os, const Model &m) const {
   if (memory_unused())
     return;
@@ -2390,6 +2424,12 @@ void Memory::print(ostream &os, const Model &m) const {
       if (!local && is_constglb(bid))
         os << "\tconst";
       os << '\n';
+
+      if (!local && bid < numNonlocals()) {
+        os << "Contents:\n";
+        print_array(os, m[mk_block_val_array(bid)].simplify());
+        os << '\n';
+      }
     }
   };
 

ir/memory.h

@@ -355,6 +355,10 @@ class Memory {
   friend std::ostream& operator<<(std::ostream &os, const Memory &m);
 
   friend class Pointer;
+
+private:
+  void print_array(std::ostream &os, const smt::expr &a,
+                   unsigned indent = 0) const;
 };
 
 }

smt/expr.cpp

@@ -540,6 +540,21 @@ bool expr::isLoad(expr &array, expr &idx) const {
   return isBinOp(array, idx, Z3_OP_SELECT);
 }
 
+bool expr::isLambda(expr &body) const {
+  C();
+  if (Z3_is_lambda(ctx(), ast())) {
+    assert(Z3_get_quantifier_num_bound(ctx(), ast()) == 1);
+    body = Z3_get_quantifier_body(ctx(), ast());
+    return true;
+  }
+  return false;
+}
+expr expr::lambdaIdxType() const {
+  C();
+  assert(Z3_get_quantifier_num_bound(ctx(), ast()) == 1);
+  return ::mkVar("sort", Z3_get_quantifier_bound_sort(ctx(), ast(), 0));
+}
+
 bool expr::isFPAdd(expr &rounding, expr &lhs, expr &rhs) const {
   return isTernaryOp(rounding, lhs, rhs, Z3_OP_FPA_ADD);
 }
@@ -1998,11 +2013,8 @@ expr expr::load(const expr &idx) const {
 
   } else if (isConstArray(val)) {
     return val;
-
-  } else if (Z3_is_lambda(ctx(), ast())) {
-    assert(Z3_get_quantifier_num_bound(ctx(), ast()) == 1);
-    expr body = Z3_get_quantifier_body(ctx(), ast());
-    return body.subst({ idx }).foldTopLevel();
+  } else if (isLambda(val)) {
+    return val.subst({ idx }).foldTopLevel();
   }
 
   return Z3_mk_select(ctx(), ast(), idx());

smt/expr.h

@@ -143,6 +143,8 @@ class expr {
   bool isConstArray(expr &val) const;
   bool isStore(expr &array, expr &idx, expr &val) const;
   bool isLoad(expr &array, expr &idx) const;
+  bool isLambda(expr &body) const;
+  expr lambdaIdxType() const;
 
   bool isFPAdd(expr &rounding, expr &lhs, expr &rhs) const;
   bool isFPSub(expr &rounding, expr &lhs, expr &rhs) const;