revisit as-array evaluation

Z3Prover · Sep 5, 2021 · 976c0a3 · 976c0a3
1 parent 38b82fa
commit 976c0a3
Showing 1 changed file with 42 additions and 30 deletions.
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
@@ -150,7 +150,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         auto st = reduce_app_core(f, num, args, result, result_pr);
         CTRACE("model_evaluator", st != BR_FAILED, 
-               tout << f->get_name() << "  ";
+               tout << st << " " << mk_pp(f, m) << "  ";
                for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " ";
                tout << "\n--> " << result << "\n";);
 
@@ -161,6 +161,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         result_pr = nullptr;
         family_id fid = f->get_family_id();
         bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
+        func_decl* g = nullptr;
         br_status st = BR_FAILED;
 #if 0
         struct pp {
@@ -171,6 +172,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         };
         pp _pp(f, result);
 #endif
+
+
         if (num == 0 && (fid == null_family_id || _is_uninterp || m_ar.is_as_array(f))) {
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
@@ -243,42 +246,51 @@ struct evaluator_cfg : public default_rewriter_cfg {
             result = args[0];
             st = BR_DONE;
         }
-        else if (evaluate(f, num, args, result)) {
-            st = BR_REWRITE1;
-        }
-        if (st == BR_FAILED && !m.is_builtin_family_id(fid)) {
-            st = evaluate_partial_theory_func(f, num, args, result, result_pr);
-        }
+        else if (evaluate(f, num, args, result)) 
+            st = BR_REWRITE1;        
+        if (st == BR_FAILED && !m.is_builtin_family_id(fid)) 
+            st = evaluate_partial_theory_func(f, num, args, result, result_pr);        
         if (st == BR_DONE && is_app(result)) {
             app* a = to_app(result);
-            if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
-                st = BR_REWRITE1;
-            }
-        }
-        if (st == BR_FAILED && num == 0 && m_ar.is_as_array(f) && m_model_completion) {
-            func_decl* g = nullptr;
-            VERIFY(m_ar.is_as_array(f, g));
-            expr* def = nullptr;
-            if (m_def_cache.find(g, def)) {
-                result = def;
-                TRACE("model_evaluator", tout << result << "\n";);
-                return BR_DONE;
-            }
-            func_interp * fi = m_model.get_func_interp(g);
-            if (fi && (result = fi->get_array_interp(g))) {
-                model_evaluator ev(m_model, m_params);
-                ev.set_model_completion(false);
-                result = ev(result);
-                m_pinned.push_back(result);
-                m_def_cache.insert(g, result);
-                TRACE("model_evaluator", tout << mk_pp(g, m) << " " << result << "\n";);
-                return BR_DONE;
-            }
+            if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result))
+                st = BR_REWRITE1;              
         }
 
+        if (st == BR_DONE && is_app(result) && expand_as_array(to_app(result)->get_decl(), result))
+            return BR_REWRITE_FULL;
+
+        if (st == BR_FAILED && expand_as_array(f, result))
+            return BR_REWRITE_FULL;        
         return st;
     }
 
+    bool expand_as_array(func_decl* f, expr_ref& result) {
+        if (!m_model_completion)
+            return false;
+        func_decl* g = nullptr;
+        if (!m_ar.is_as_array(f, g))
+            return false;
+        expr* def = nullptr;
+        if (m_def_cache.find(g, def)) {
+            result = def;
+            TRACE("model_evaluator", tout << result << "\n";);
+            return true;
+        }
+        expr_ref tmp(m);
+        func_interp* fi = m_model.get_func_interp(g);
+        if (fi && (tmp = fi->get_array_interp(g))) {
+            model_evaluator ev(m_model, m_params);
+            ev.set_model_completion(false);
+            result = ev(tmp);
+            m_pinned.push_back(result);
+            m_def_cache.insert(g, result);
+            TRACE("model_evaluator", tout << mk_pp(g, m) << " " << result << "\n";);
+            return true;
+        }
+
+        return false;
+    }
+
     void expand_stores(expr_ref& val) {
         TRACE("model_evaluator", tout << val << "\n";);
         vector<expr_ref_vector> stores;