fix bugs in elim-unconstr2 and fix bugs in intblast_solver

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

src/ast/converters/expr_inverter.cpp

@@ -400,6 +400,7 @@ class bv_expr_inverter : public iexpr_inverter {
     }
 
     bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
+//        return false;
         if (num == 0)
             return false;
         if (!uncnstr(num, args))

src/ast/simplifiers/elim_unconstrained.cpp

@@ -66,7 +66,6 @@ bool elim_unconstrained::is_var_lt(int v1, int v2) const {
 }
 
 void elim_unconstrained::eliminate() {
-
     while (!m_heap.empty()) {
         expr_ref r(m);
         int v = m_heap.erase_min();
@@ -86,7 +85,12 @@ void elim_unconstrained::eliminate() {
             n.m_refcount = 0;
             continue;
         }
+        if (m_heap.contains(root(e))) {
+            IF_VERBOSE(11, verbose_stream() << "already in heap " << mk_bounded_pp(e, m) << "\n");
+            continue;
+        }
         app* t = to_app(e);
+        TRACE("elim_unconstrained", tout << "eliminating " << mk_pp(t, m) << "\n";);
         unsigned sz = m_args.size();
         for (expr* arg : *to_app(t))
             m_args.push_back(reconstruct_term(get_node(arg)));
@@ -99,6 +103,7 @@ void elim_unconstrained::eliminate() {
             proof * pr  = m.mk_apply_def(s, r, pr1);
             m_trail.push_back(pr);
         }
+        expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m);
         n.m_refcount = 0;
         m_args.shrink(sz);
         if (!inverted) {
@@ -106,6 +111,8 @@ void elim_unconstrained::eliminate() {
             continue;
         }
 
+        IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n");
+        
         TRACE("elim_unconstrained", tout << mk_pp(t, m) << " -> " << r << "\n");
         SASSERT(r->get_sort() == t->get_sort());
         m_stats.m_num_eliminated++;
@@ -119,7 +126,8 @@ void elim_unconstrained::eliminate() {
         get_node(e).m_term = r;
         get_node(e).m_proof = pr;
         get_node(e).m_refcount++;
-        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << "\n");
+        get_node(e).m_dirty = false;
+        IF_VERBOSE(11, verbose_stream() << "set " << &get_node(e) << " " << root(e) << " " << mk_bounded_pp(e, m) << " := " << mk_bounded_pp(r, m) << "\n");
         SASSERT(!m_heap.contains(root(e)));
         if (is_uninterp_const(r))
             m_heap.insert(root(e));
@@ -283,13 +291,22 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
     expr* t = n0.m_term;
     if (!n0.m_dirty)
         return expr_ref(t, m);
+    if (!is_node(t))
+        return expr_ref(t, m);
     ptr_vector<expr> todo;
     todo.push_back(t);
     while (!todo.empty()) {
         t = todo.back();
+        if (!is_node(t)) {
+            UNREACHABLE();
+        }
         node& n = get_node(t);
         unsigned sz0 = todo.size();
         if (is_app(t)) {     
+            if (n.m_term != t) {
+                todo.pop_back();
+                continue;
+            }
             for (expr* arg : *to_app(t)) 
                 if (get_node(arg).m_dirty || !get_node(arg).m_term)
                     todo.push_back(arg);
@@ -300,7 +317,6 @@ 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)) {
@@ -410,7 +426,7 @@ void elim_unconstrained::reduce() {
     generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
     m_inverter.set_model_converter(mc.get());
     m_created_compound = true;
-    for (unsigned rounds = 0; m_created_compound && rounds < 3; ++rounds) {
+    for (unsigned rounds = 0; m_created_compound && rounds < 1; ++rounds) {
         m_created_compound = false;
         init_nodes();
         eliminate();

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -182,11 +182,11 @@ std::ostream& model_reconstruction_trail::display(std::ostream& out) const {
             out << "hide " << t->m_decl->get_name() << "\n";
         else if (t->is_def()) {
             for (auto const& [f, def, dep] : t->m_defs)
-                out << f->get_name() << " <- " << mk_pp(def, m) << "\n";
+                out << "def: " << f->get_name() << " <- " << mk_pp(def, m) << "\n";
         }            
         else {
             for (auto const& [v, def] : t->m_subst->sub())
-                out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n";            
+                out << "sub: " << mk_pp(v, m) << " -> " << mk_pp(def, m) << "\n";
         }
         for (auto const& d : t->m_removed)
             out << "rm: " << d << "\n";

src/sat/smt/intblast_solver.cpp

@@ -347,6 +347,8 @@ namespace intblast {
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     continue;
+                if (sib->get_arg(0)->get_sort() != n->get_arg(0)->get_sort())
+                    continue;
                 auto a = eq_internalize(n, sib);
                 auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
                 ctx.mark_relevant(a);
@@ -957,7 +959,6 @@ namespace intblast {
             rational r;
             VERIFY(av.get_value(b2i->get_expr(), r));
             value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr()));
-            verbose_stream() << ctx.bpp(n) << " := " << value << "\n";
         }
         values.set(n->get_root_id(), value);
         TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
@@ -981,12 +982,11 @@ namespace intblast {
                     continue;
                 verbose_stream() << "value mismatch : " << mk_bounded_pp(e, m) << " := " << val1 << "\n";
                 verbose_stream() << mk_bounded_pp(f, m) << " := " << r2 << "\n";
-                for (expr* arg : *to_app(e)) {
+                for (expr* arg : *to_app(e)) 
                     verbose_stream() << mk_bounded_pp(arg, m) << " := " << mdl(arg) << "\n";
             }
         }
     }
-    }
 
     sat::literal_vector const& solver::unsat_core() {
         return m_core;