bug fixes to new core, elim_predicates and elim_unconstrained

src/ast/simplifiers/elim_unconstrained.cpp

@@ -52,9 +52,9 @@ monotonicity or reflexivity rules.
 #include "ast/simplifiers/elim_unconstrained.h"
 
 elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
-    dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m) {
+    dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m), m_args(m) {
     std::function<bool(expr*)> is_var = [&](expr* e) {
-        return is_uninterp_const(e) && !m_fmls.frozen(e) && get_node(e).m_refcount <= 1;
+        return is_uninterp_const(e) && !m_fmls.frozen(e) && is_node(e) && get_node(e).m_refcount <= 1;
     };
     m_inverter.set_is_var(is_var);
 }
@@ -114,7 +114,7 @@ void elim_unconstrained::eliminate() {
         gc(e);
         invalidate_parents(e);
         freeze_rec(r);
-
+        
         m_root.setx(r->get_id(), e->get_id(), UINT_MAX);
         get_node(e).m_term = r;
         get_node(e).m_proof = pr;
@@ -291,7 +291,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
         unsigned sz0 = todo.size();
         if (is_app(t)) {            
             for (expr* arg : *to_app(t)) 
-                if (get_node(arg).m_dirty)
+                if (get_node(arg).m_dirty || !get_node(arg).m_term)
                     todo.push_back(arg);
             if (todo.size() != sz0)
                 continue;
@@ -300,18 +300,20 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
             for (expr* arg : *to_app(t)) 
                 m_args.push_back(get_node(arg).m_term);            
             n.m_term = m.mk_app(to_app(t)->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz);
+
             m_args.shrink(sz);
         }
         else if (is_quantifier(t)) {
             expr* body = to_quantifier(t)->get_expr();
             node& n2 = get_node(body);
-            if (n2.m_dirty) {
+            if (n2.m_dirty || !n2.m_term) {
                 todo.push_back(body);
                 continue;
             }
             n.m_term = m.update_quantifier(to_quantifier(t), n2.m_term);            
         }
         m_trail.push_back(n.m_term);
+        m_root.setx(n.m_term->get_id(), n.m_term->get_id(), UINT_MAX);
         todo.pop_back();
         n.m_dirty = false;
     }

src/ast/simplifiers/elim_unconstrained.h

@@ -46,13 +46,15 @@ class elim_unconstrained : public dependent_expr_simplifier {
     var_lt                   m_lt;
     heap<var_lt>             m_heap;
     expr_ref_vector          m_trail;
-    ptr_vector<expr>         m_args;
+    expr_ref_vector          m_args;
     stats                    m_stats;
     unsigned_vector          m_root;
     bool                     m_created_compound = false;
     bool                     m_enable_proofs = false;
 
     bool is_var_lt(int v1, int v2) const;
+    bool is_node(unsigned n) const { return m_nodes.size() > n; }
+    bool is_node(expr* t) const { return is_node(t->get_id()); }
     node& get_node(unsigned n) { return m_nodes[n]; }
     node const& get_node(unsigned n) const { return m_nodes[n]; }
     node& get_node(expr* t) { return m_nodes[root(t)]; }

src/ast/simplifiers/eliminate_predicates.cpp

@@ -174,7 +174,7 @@ bool eliminate_predicates::can_be_quasi_macro_head(expr* _head, unsigned num_bou
 // then replace (f x y z) by (if (= z (+ x y)) s (f' x y z))
 //
 
-void eliminate_predicates::insert_quasi_macro(app* head, expr* body, clause const& cl) {
+void eliminate_predicates::insert_quasi_macro(app* head, expr* body, clause& cl) {
     expr_ref _body(body, m);
     uint_set indices;
     expr_ref_vector args(m), eqs(m);
@@ -208,7 +208,7 @@ void eliminate_predicates::insert_quasi_macro(app* head, expr* body, clause cons
 
     lhs = m.mk_app(f, args);
     rhs = m.mk_ite(mk_and(eqs), body, m.mk_app(f1, args));
-    insert_macro(lhs, rhs, cl.m_dep);
+    insert_macro(lhs, rhs, cl);
 }
 
 
@@ -311,6 +311,12 @@ bool eliminate_predicates::is_macro_safe(expr* e) {
     return true;
 }
 
+void eliminate_predicates::insert_macro(app* head, expr* def, clause& cl) {
+    insert_macro(head, def, cl.m_dep);
+    TRACE("elim_predicates", tout << "remove " << cl << "\n");
+    cl.m_alive = false;
+}
+
 void eliminate_predicates::insert_macro(app* head, expr* def, expr_dependency* dep) {
     unsigned num = head->get_num_args();
     ptr_buffer<expr> vars, subst_args;
@@ -335,7 +341,7 @@ void eliminate_predicates::insert_macro(app* head, expr* def, expr_dependency* d
     auto* info = alloc(macro_def, _head, _def, _dep);
     m_macros.insert(head->get_decl(), info);
     m_fmls.model_trail().push(head->get_decl(), _def, _dep, {}); // augment with definition for head
-    m_is_macro.mark(head->get_decl(), true);
+    m_is_macro.mark(head->get_decl(), true);    
     TRACE("elim_predicates", tout << "insert " << _head << " " << _def << "\n");
     ++m_stats.m_num_macros;
 }
@@ -368,26 +374,22 @@ void eliminate_predicates::try_find_macro(clause& cl) {
     // (= (f x) t)
     if (cl.is_unit() && !cl.sign(0) && m.is_eq(cl.atom(0), x, y)) {
         if (can_be_def(x, y)) {
-            insert_macro(to_app(x), y, cl.m_dep);
-            cl.m_alive = false;
+            insert_macro(to_app(x), y, cl);
             return;
         }
         if (can_be_def(y, x)) {
-            insert_macro(to_app(y), x, cl.m_dep);
-            cl.m_alive = false;
+            insert_macro(to_app(y), x, cl);
             return;
         }
     }
     // not (= (p x) t) -> (p x) = (not t)
     if (cl.is_unit() && cl.sign(0) && m.is_iff(cl.atom(0), x, y)) {
         if (can_be_def(x, y)) {
-            insert_macro(to_app(x), m.mk_not(y), cl.m_dep);
-            cl.m_alive = false;
+            insert_macro(to_app(x), m.mk_not(y), cl);
             return;
         }
         if (can_be_def(y, x)) {
-            insert_macro(to_app(y), m.mk_not(x), cl.m_dep);
-            cl.m_alive = false;
+            insert_macro(to_app(y), m.mk_not(x), cl);
             return;
         }
     }
@@ -414,8 +416,7 @@ void eliminate_predicates::try_find_macro(clause& cl) {
         m_fmls.model_trail().hide(fn); // hide definition of fn
         k = m.mk_app(fn, f->get_num_args(), f->get_args());        
         def = m.mk_ite(cond, t, k);
-        insert_macro(f, def, cl.m_dep);
-        cl.m_alive = false;
+        insert_macro(f, def, cl);
         fml = m.mk_not(m.mk_eq(k, t));
         clause* new_cl = init_clause(fml, cl.m_dep, UINT_MAX);
         add_use_list(*new_cl);
@@ -532,8 +533,7 @@ void eliminate_predicates::try_find_macro(clause& cl) {
                 expr_ref y1 = subtract(y, to_app(x), i);
                 if (inv) 
                     y1 = uminus(y1);                
-                insert_macro(to_app(arg), y1, cl.m_dep);
-                cl.m_alive = false;
+                insert_macro(to_app(arg), y1, cl);
                 return true;
             }
         next:
@@ -737,6 +737,7 @@ void eliminate_predicates::update_model(func_decl* p) {
     }
 
     rewrite(def);
+    TRACE("elim_predicates", tout << "insert " << p->get_name() << " " << def << "\n");
     m_fmls.model_trail().push(p, def, dep, deleted);
 }
 

src/ast/simplifiers/eliminate_predicates.h

@@ -111,9 +111,10 @@ class eliminate_predicates : public dependent_expr_simplifier {
     bool try_find_binary_definition(func_decl* p, app_ref& head, expr_ref& def, expr_dependency_ref& dep);
     void try_resolve_definition(func_decl* p);
     void insert_macro(app* head, expr* def, expr_dependency* dep);
+    void insert_macro(app* head, expr* def, clause& cl);
     expr_ref bind_free_variables_in_def(clause& cl, app* head, expr* def);
     bool can_be_macro_head(expr* head, unsigned num_bound);
-    void insert_quasi_macro(app* head, expr* body, clause const& cl);
+    void insert_quasi_macro(app* head, expr* body, clause& cl);
     bool can_be_quasi_macro_head(expr* head, unsigned num_bound);
     bool is_macro_safe(expr* e);
     void try_find_macro(clause& cl);

src/model/model_core.cpp

@@ -81,7 +81,7 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
 }
 
 func_interp* model_core::update_func_interp(func_decl* d, func_interp* fi) {
-    TRACE("model", tout << "register " << d->get_name() << "\n";);
+    TRACE("model_verbose", tout << "register " << d->get_name() << "\n";);
 
     SASSERT(d->get_arity() > 0);
     SASSERT(&fi->m() == &m);

src/sat/smt/euf_model.cpp

@@ -67,7 +67,7 @@ namespace euf {
         m_qmodel = mdl;
     }
 
-    void solver::update_model(model_ref& mdl) {
+    void solver::update_model(model_ref& mdl, bool validate) {
         TRACE("model", tout << "create model\n";);
         if (m_qmodel) {
             mdl = m_qmodel;
@@ -87,7 +87,8 @@ namespace euf {
         for (auto* mb : m_solvers)
             mb->finalize_model(*mdl);
         TRACE("model", tout << "created model " << *mdl << "\n";);
-        validate_model(*mdl);
+        if (validate)
+            validate_model(*mdl);
     }
 
     bool solver::include_func_interp(func_decl* f) {

src/sat/smt/euf_solver.cpp

@@ -478,8 +478,13 @@ namespace euf {
             m_ackerman->cg_conflict_eh(a, b);
         switch (s().value(lit)) {
         case l_true:
-            if (n->merge_tf() && !m.is_value(n->get_root()->get_expr())) 
-                m_egraph.merge(n, ante, to_ptr(lit));
+            if (!n->merge_tf())
+                break;
+            if (m.is_value(n->get_root()->get_expr()))
+                break;
+            if (!ante)
+                ante = mk_true();
+            m_egraph.merge(n, ante, to_ptr(lit));
             break;
         case l_undef:
         case l_false:

src/sat/smt/euf_solver.h

@@ -495,7 +495,7 @@ namespace euf {
 
         // model construction
         void save_model(model_ref& mdl);
-        void update_model(model_ref& mdl);
+        void update_model(model_ref& mdl, bool validate);
         obj_map<expr, enode*> const& values2root();
         void model_updated(model_ref& mdl);
         expr* node2value(enode* n) const;

src/sat/smt/q_mbi.cpp

@@ -635,7 +635,7 @@ namespace q {
         if (m_model)
             return;
         m_model = alloc(model, m);
-        ctx.update_model(m_model);
+        ctx.update_model(m_model, false);
     }
 
     void mbqi::init_solver() {

src/sat/tactic/goal2sat.cpp

@@ -987,7 +987,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     void update_model(model_ref& mdl) {
         auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
         if (ext)
-            ext->update_model(mdl);
+            ext->update_model(mdl, true);
     }
 
     void user_push() {