fix #2544

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/smt/smt_model_checker.cpp

@@ -80,14 +80,29 @@ namespace smt {
     }
 
     expr * model_checker::get_type_compatible_term(expr * val) {
-        for (expr* f : m_fresh_exprs) {
-            if (m.get_sort(f) == m.get_sort(val)) {
-                return f;
+        app* fresh_term;
+        if (is_app(val) && to_app(val)->get_num_args() > 0) {
+            ptr_buffer<expr> args;
+            for (expr* arg : *to_app(val)) {
+                args.push_back(get_type_compatible_term(arg));
             }
+            fresh_term = m.mk_app(to_app(val)->get_decl(), args.size(), args.c_ptr());
+        }
+        else {
+            expr * sk_term = get_term_from_ctx(val);
+            if (sk_term != nullptr) {
+                return sk_term;
+            }
+
+            for (expr* f : m_fresh_exprs) {
+                if (m.get_sort(f) == m.get_sort(val)) {
+                    return f;
+                }
+            }
+            fresh_term = m.mk_fresh_const("sk", m.get_sort(val));
         }
-        app* fresh_term = m.mk_fresh_const("sk", m.get_sort(val));
-        m_context->ensure_internalized(fresh_term);
         m_fresh_exprs.push_back(fresh_term);
+        m_context->ensure_internalized(fresh_term);
         return fresh_term;
     }
 
@@ -279,14 +294,14 @@ namespace smt {
         return false;
     }
 
-
     bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) {
         SASSERT(cex != nullptr);
         expr_ref_buffer diseqs(m);
         for (expr * sk : sks) {
             func_decl * sk_d = to_app(sk)->get_decl();
             expr_ref sk_value(cex->get_some_const_interp(sk_d), m);
             if (!sk_value) {
+                TRACE("model_checker", tout << "no constant interpretation for " << mk_pp(sk, m) << "\n";);
                 return false; // get_some_value failed... aborting add_blocking_clause
             }
             diseqs.push_back(m.mk_not(m.mk_eq(sk, sk_value)));

src/smt/theory_seq.cpp

@@ -390,7 +390,7 @@ final_check_status theory_seq::final_check_eh() {
     }
     if (branch_unit_variable()) {
         ++m_stats.m_branch_variable;
-        TRACEFIN("ranch_unit_variable");
+        TRACEFIN("branch_unit_variable");
         return FC_CONTINUE;
     }
     if (branch_binary_variable()) {
@@ -3321,7 +3321,7 @@ bool theory_seq::solve_nc(unsigned idx) {
     expr_ref c = canonize(n.contains(), deps);
     expr* a = nullptr, *b = nullptr;
 
-    CTRACE("seq", c != n.contains(), tout << n.contains() << " =>\n" << c << "\n";);
+    CTRACE("seq", c != n.contains(), tout << n.contains() << " =>\n" << c << "\n";);    
 
 
     if (m.is_true(c)) {

src/tactic/fd_solver/smtfd_solver.cpp

@@ -1045,6 +1045,17 @@ namespace smtfd {
         expr* abs(expr* e) { return m_context.get_abs().abs(e);  }
         expr_ref eval_abs(expr* t) { return (*m_model)(abs(t)); }
 
+
+        void restrict_to_universe(expr * sk, ptr_vector<expr> const & universe) {
+            SASSERT(!universe.empty());
+            expr_ref_vector eqs(m);
+            for (expr * e : universe) {
+                eqs.push_back(m.mk_eq(sk, e));
+            }
+            expr_ref fml = mk_or(eqs);
+            m_solver->assert_expr(fml);
+        }
+
         // !Ex P(x) => !P(t)
         // Ax P(x) => P(t)
         // l_true: new instance
@@ -1056,21 +1067,24 @@ namespace smtfd {
             if (!m_model->eval_expr(q->get_expr(), tmp, true)) {
                 return l_undef;
             }
+
+            m_solver->push();
             expr_ref_vector vars(m), vals(m);
             vars.resize(sz, nullptr);
             vals.resize(sz, nullptr);
             for (unsigned i = 0; i < sz; ++i) {
-                vars[sz - i - 1] = m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));    
-
-                // TBD: finite domain variables
+                sort* s = q->get_decl_sort(i);
+                vars[i] = m.mk_fresh_const(q->get_decl_name(i), s);    
+                if (m_model->has_uninterpreted_sort(s)) {
+                    restrict_to_universe(vars.get(i), m_model->get_universe(s));
+                }
             }
             var_subst subst(m);
             expr_ref body = subst(tmp, vars.size(), vars.c_ptr());
             if (is_forall(q)) {
                 body = m.mk_not(body);
             }
 
-            m_solver->push();
             m_solver->assert_expr(body);
             lbool r = m_solver->check_sat(0, nullptr);
             model_ref mdl;
@@ -1115,12 +1129,8 @@ namespace smtfd {
             return r;
         }
 
-        bool is_enforced(quantifier* q) {
-            return m_enforced.contains(q);
-        }
-
         lbool check_exists(quantifier* q) {
-            if (is_enforced(q)) {
+            if (m_enforced.contains(q)) {
                 return l_true;
             }
             expr_ref tmp(m);
@@ -1504,7 +1514,7 @@ namespace smtfd {
             lbool r;
             expr_ref_vector core(m);
             while (true) {
-                IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat " << m_stats.m_num_rounds << " " << m_stats.m_num_lemmas << ")\n");
+                IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat " << m_stats.m_num_rounds << " " << m_stats.m_num_lemmas << " " << m_stats.m_num_mbqi << ")\n");
                 m_stats.m_num_rounds++;
                 checkpoint();
 
@@ -1542,7 +1552,7 @@ namespace smtfd {
                 case l_undef:
                     break;
                 case l_false:
-                    m_max_conflicts = UINT_MAX;
+                    // m_max_conflicts = UINT_MAX;
                     break;
                 }
             }

src/util/ref_vector.h

@@ -249,7 +249,6 @@ class ref_vector : public ref_vector_core<T, ref_manager_wrapper<T, TManager> >
         }
 
         element_ref & operator=(T * n) {
-            SASSERT(n);
             m_manager.inc_ref(n);
             m_manager.dec_ref(m_ref);
             m_ref = n;