fix #3180 fix #3181 #3184

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

src/ast/ast.cpp

@@ -1676,6 +1676,16 @@ void ast_manager::set_next_expr_id(unsigned id) {
 
 unsigned ast_manager::get_node_size(ast const * n) { return ::get_node_size(n); }
 
+std::ostream& ast_manager::display(std::ostream& out) const {
+    for (ast * a : m_ast_table) {
+        if (is_func_decl(a)) {
+            out << to_func_decl(a)->get_name() << " " << a->get_id() << "\n";
+        }
+    }
+    return out;
+}
+
+
 void ast_manager::register_plugin(symbol const & s, decl_plugin * plugin) {
     family_id id = m_family_manager.mk_family_id(s);
     SASSERT(is_format_manager() || s != symbol("format"));

src/ast/ast.h

@@ -1713,6 +1713,8 @@ public:
         return m_alloc.get_allocation_size();
     }
 
+    std::ostream& display(std::ostream& out) const;
+
 protected:
     ast * register_node_core(ast * n);
 

src/ast/ast_translation.cpp

@@ -168,7 +168,7 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
         new_fi.set_chainable(fi->is_chainable());
         new_fi.set_pairwise(fi->is_pairwise());
         new_fi.set_injective(fi->is_injective());
-/// TBD        new_fi.set_skolem(fi->is_skolem()); 
+        new_fi.set_skolem(fi->is_skolem()); 
         new_fi.set_idempotent(fi->is_idempotent());
 
         new_f = m_to_manager.mk_func_decl(f->get_name(),

src/model/model.cpp

@@ -166,9 +166,9 @@ model * model::translate(ast_translation & translator) const {
     model * res = alloc(model, translator.to());
 
     // Translate const interps
-    for (auto const& kv : m_interp) 
+    for (auto const& kv : m_interp) {
         res->register_decl(translator(kv.m_key), translator(kv.m_value));
-
+    }
     // Translate func interps
     for (auto const& kv : m_finterp) {
         func_interp * fi = kv.m_value;

src/qe/qsat.cpp

@@ -160,15 +160,12 @@ namespace qe {
         }
         model_evaluator eval(*mdl);
         eval.set_model_completion(true);
-        TRACE("qe", model_v2_pp(tout, *mdl););
+        TRACE("qe_assumptions", model_v2_pp(tout, *mdl););
 
         expr_ref val(m);
         for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) {
-            app* p = m_preds[level - 1][j].get();
+            app* p = m_preds[level - 1][j].get();            
-            TRACE("qe", tout << "process level: " << level - 1 << ": " << mk_pp(p, m) << "\n";);
+            eval(p, val);            
-            
-            eval(p, val);
-            
             if (m.is_false(val)) {
                 m_asms.push_back(m.mk_not(p));
             }
@@ -197,7 +194,7 @@ namespace qe {
                 }
             }
         }
-        TRACE("qe", tout << "level: " << level << "\n";
+        TRACE("qe_assumptions", tout << "level: " << level << "\n";
               model_v2_pp(tout, *mdl);
               display(tout, asms););
     }
@@ -291,7 +288,7 @@ namespace qe {
     }
 
     app_ref pred_abs::fresh_bool(char const* name) {
-        app_ref r(m.mk_fresh_const(name, m.mk_bool_sort()), m);
+        app_ref r(m.mk_fresh_const(name, m.mk_bool_sort(), true), m);
         m_fmc->hide(r);
         return r;
     }
@@ -576,7 +573,7 @@ namespace qe {
         void get_core(expr_ref_vector& core) {
             core.reset();
             m_solver->get_unsat_core(core);
-            TRACE("qe", m_solver->display(tout << "core: " << core << "\n") << "\n";);
+            TRACE("qe_core", m_solver->display(tout << "core: " << core << "\n") << "\n";);
         }
     };
 
@@ -659,6 +656,7 @@ namespace qe {
                         if (m_mode == qsat_sat) {
                             return l_true; 
                         }
+
                         if (m_model.get()) {
                             SASSERT(validate_assumptions(*m_model.get(), asms));
                             if (!project_qe(asms)) return l_undef;
@@ -1106,8 +1104,7 @@ namespace qe {
             for (expr* c : core) {
                 if (!mdl.is_true(c)) {
                     TRACE("qe", tout << "component of core is not true: " << mk_pp(c, m) << "\n";
-                          tout << mdl << "\n";
+                          tout << mdl << "\n";);
-                          );
                     if (mdl.is_false(c)) {
                         return false;
                     }
@@ -1292,7 +1289,6 @@ namespace qe {
             m_fa.assert_expr(m.mk_not(fml));
             TRACE("qe", tout << "ex: " << fml << "\n";);
             lbool is_sat = check_sat();
-            
             switch (is_sat) {
             case l_false:
                 in->reset();

src/smt/dyn_ack.cpp

@@ -25,12 +25,12 @@ namespace smt {
     /**
        \brief Justification for dynamic ackermann clause
     */
-    class dyn_ack_justification : public justification {
+    class dyn_ack_cc_justification : public justification {
         app *     m_app1;
         app *     m_app2;
     public:
-        dyn_ack_justification(app * n1, app * n2):
+        dyn_ack_cc_justification(app * n1, app * n2):
-            justification(false), // dyn_ack_justifications are not stored in regions.
+            justification(false), // dyn_ack_cc_justifications are not stored in regions.
             m_app1(n1), 
             m_app2(n2) {
             SASSERT(m_app1->get_num_args() == m_app2->get_num_args());
@@ -41,8 +41,7 @@ namespace smt {
 
         char const * get_name() const override { return "dyn-ack"; }
 
-        void get_antecedents(conflict_resolution & cr) override {
+        void get_antecedents(conflict_resolution & cr) override {}
-        }
 
         void display_debug_info(conflict_resolution & cr, std::ostream & out) override {
             ast_manager & m = cr.get_manager();
@@ -58,7 +57,7 @@ namespace smt {
            \remark if negate == true, then the hypothesis is actually (not (= lhs rhs))
         */
         proof * mk_hypothesis(ast_manager & m, app * eq, bool negate, expr * lhs, expr * rhs) {
-            SASSERT(m.is_eq(eq) || m.is_iff(eq));
+            SASSERT(m.is_eq(eq));
             SASSERT((eq->get_arg(0) == lhs && eq->get_arg(1) == rhs) ||
                     (eq->get_arg(0) == rhs && eq->get_arg(1) == lhs));
             app * h = negate ? m.mk_not(eq) : eq;
@@ -103,6 +102,29 @@ namespace smt {
 
     };
 
+    class dyn_ack_eq_justification : public justification {
+        app *     m_app1;
+        app *     m_app2;
+    public:
+        dyn_ack_eq_justification(app * n1, app * n2):
+            justification(false), // dyn_ack_cc_justifications are not stored in regions.
+            m_app1(n1), 
+            m_app2(n2) {
+        }
+        char const * get_name() const override { return "dyn-ack-eq"; }
+        void get_antecedents(conflict_resolution & cr) override {}
+        void display_debug_info(conflict_resolution & cr, std::ostream & out) override {
+            ast_manager & m = cr.get_manager();
+            out << "m_app1:\n" << mk_pp(m_app1, m) << "\n";
+            out << "m_app2:\n" << mk_pp(m_app2, m) << "\n";
+        }
+
+        proof * mk_proof(conflict_resolution & cr) override {
+            ast_manager & m   = cr.get_manager();
+            return m.mk_symmetry(m.mk_eq(m_app1, m_app2));
+        }
+    };
+
     dyn_ack_manager::dyn_ack_manager(context & ctx, dyn_ack_params & p):
         m_context(ctx),
         m(ctx.get_manager()),
@@ -180,15 +202,14 @@ namespace smt {
         if (n1->get_id() > n2->get_id())
             std::swap(n1,n2);
         TRACE("dyn_ack", 
-              tout << mk_pp(n1, m) << " = " << mk_pp(n2, m) 
+              tout << mk_pp(n1, m) << " = " << mk_pp(n2, m) << " = " << mk_pp(r, m) << "\n";);
-              << " = " << mk_pp(r, m) << "\n";);
         app_triple tr(n1, n2, r);
         if (m_triple.m_instantiated.contains(tr)) {
             return;
         }
         unsigned num_occs = 0;
         if (m_triple.m_app2num_occs.find(n1, n2, r, num_occs)) {
-            TRACE("dyn_ack", tout << mk_pp(n1, m) << "\n" << mk_pp(n2, m) 
+            TRACE("dyn_ack", tout << mk_pp(n1, m) << "\n" << mk_pp(n2, m) << "\n"
                   << mk_pp(r, m) << "\n" << "\nnum_occs: " << num_occs << "\n";);
             num_occs++;
         }
@@ -372,7 +393,7 @@ namespace smt {
 
         justification * js = nullptr;
         if (m.proofs_enabled())
-            js = alloc(dyn_ack_justification, n1, n2);
+            js = alloc(dyn_ack_cc_justification, n1, n2);
         clause * cls = m_context.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
             dealloc(del_eh);
@@ -418,10 +439,9 @@ namespace smt {
         lits.push_back(~mk_eq(n2, r));
         lits.push_back(mk_eq(n1, n2));
         clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this);
-
         justification * js = nullptr;
-        if (m.proofs_enabled())
+        if (m.proofs_enabled()) 
-            js = alloc(dyn_ack_justification, n1, n2);
+            js = alloc(dyn_ack_eq_justification, n1, n2);
         clause * cls = m_context.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
             dealloc(del_eh);

src/smt/smt_parallel.cpp

@@ -64,7 +64,7 @@ namespace smt {
             context& new_ctx = *pctxs.back();
             context::copy(ctx, new_ctx, true);
             new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed);
-            ast_translation tr(*new_m, m);
+            ast_translation tr(m, *new_m);
             pasms.push_back(tr(asms));
         }
 
@@ -202,11 +202,11 @@ namespace smt {
         switch (result) {
         case l_true: 
             pctx.get_model(mdl);
-            if (mdl) {
+            if (mdl) 
-                ctx.set_model(mdl->translate(tr));
+                ctx.set_model(mdl->translate(tr));            
-            }
             break;
         case l_false:
+            ctx.m_unsat_core.reset();
             for (expr* e : pctx.unsat_core()) 
                 ctx.m_unsat_core.push_back(tr(e));
             break;