merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/proto_model/proto_model.cpp

@@ -93,6 +93,7 @@ bool proto_model::is_select_of_model_value(expr* e) const {
 
 bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
     m_eval.set_model_completion(model_completion);
+    m_eval.set_expand_array_equalities(false);
     try {
         m_eval(e, result);
 #if 0

src/smt/smt_context.cpp

@@ -4136,6 +4136,7 @@ namespace smt {
         if (fcs == FC_DONE) {
             mk_proto_model(l_true);
             m_model = m_proto_model->mk_model();
+            add_rec_funs_to_model();            
         }
             
         return fcs == FC_DONE;
@@ -4188,8 +4189,51 @@ namespace smt {
         return m_last_search_failure; 
     }
 
+    void context::add_rec_funs_to_model() {
+        ast_manager& m = m_manager;
+        SASSERT(m_model);
+        for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
+            expr* e = m_asserted_formulas.get_formula(i);
+            if (is_quantifier(e)) {
+                quantifier* q = to_quantifier(e);
+                if (!m.is_rec_fun_def(q)) continue;
+                SASSERT(q->get_num_patterns() == 1);
+                expr* fn = to_app(q->get_pattern(0))->get_arg(0);
+                SASSERT(is_app(fn));
+                func_decl* f = to_app(fn)->get_decl();
+                expr* eq = q->get_expr();
+                expr_ref body(m);
+                if (is_fun_def(fn, q->get_expr(), body)) {
+                    func_interp* fi = alloc(func_interp, m, f->get_arity());
+                    fi->set_else(body);
+                    m_model->register_decl(f, fi);
+                }
+            }
+        }
+    }
+
+    bool context::is_fun_def(expr* f, expr* body, expr_ref& result) {
+        expr* t1, *t2, *t3;
+        if (m_manager.is_eq(body, t1, t2) || m_manager.is_iff(body, t1, t2)) {
+            if (t1 == f) return result = t2, true;
+            if (t2 == f) return result = t1, true;
+            return false;
+        }
+        if (m_manager.is_ite(body, t1, t2, t3)) {
+            expr_ref body1(m_manager), body2(m_manager);
+            if (is_fun_def(f, t2, body1) && is_fun_def(f, t3, body2)) {
+                // f is not free in t1
+                result = m_manager.mk_ite(t1, body1, body2);
+                return true;
+            }
+        }
+        return false;
+    }
+
+
 };
 
+
 #ifdef Z3DEBUG
 void pp(smt::context & c) {
     c.display(std::cout);

src/smt/smt_context.h

@@ -209,6 +209,7 @@ namespace smt {
             ~scoped_mk_model() {
                 if (m_ctx.m_proto_model.get() != 0) {
                     m_ctx.m_model = m_ctx.m_proto_model->mk_model();
+                    m_ctx.add_rec_funs_to_model();            
                     m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
                 }
             }
@@ -1163,6 +1164,10 @@ namespace smt {
 
         bool propagate();
 
+        void add_rec_funs_to_model();
+
+        bool is_fun_def(expr* f, expr* q, expr_ref& body);
+
     public:
         bool can_propagate() const;
 

src/smt/smt_model_checker.cpp

@@ -290,7 +290,7 @@ namespace smt {
 
         while (true) {
             lbool r = m_aux_context->check();
-            TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
+            TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);                
             if (r != l_true)
                 break; 
             model_ref cex;
@@ -300,7 +300,7 @@ namespace smt {
             }
             num_new_instances++;
             if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
-                TRACE("model_checker", tout << "Add blocking clause failed\n";);
+                TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";);
                 // add_blocking_clause failed... stop the search for new counter-examples...
                 break; 
             }
@@ -407,6 +407,7 @@ namespace smt {
                 found_relevant = true;
                 if (m.is_rec_fun_def(q)) {
                     if (!check_rec_fun(q)) {
+                        TRACE("model_checker", tout << "checking recursive function failed\n";);
                         num_failures++;
                     }
                 }
@@ -414,6 +415,7 @@ namespace smt {
                     if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
                         verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
                     }
+                    TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
                     num_failures++;
                 }
             }
@@ -452,6 +454,7 @@ namespace smt {
     }
 
     bool model_checker::has_new_instances() {
+        TRACE("model_checker", tout << "instances: " << m_new_instances.size() << "\n";);
         return !m_new_instances.empty();
     }
 

src/smt/smt_quantifier.h

@@ -165,6 +165,8 @@ namespace smt {
         virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;
 
+        
+
     };
 };