From 080c9c68930ba62019c760fe331db8033c8034b9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Feb 2021 10:35:02 -0800
Subject: [PATCH] fixes to dt solver

---
 src/sat/smt/dt_solver.cpp | 36 +++++++++++++++++++++++-------------
 src/sat/smt/dt_solver.h   |  1 +
 src/sat/smt/euf_model.cpp |  5 ++---
 3 files changed, 26 insertions(+), 16 deletions(-)

diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index c7f062819..9bf80e5b0 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -99,15 +99,14 @@ namespace dt {
        \brief Assert the axiom (antecedent => lhs = rhs)
        antecedent may be null_literal
     */
-    void solver::assert_eq_axiom(enode* lhs, expr* rhs, literal antecedent) {
+    void solver::assert_eq_axiom(enode* n1, expr* e2, literal antecedent) {
+        expr* e1 = n1->get_expr();
         if (antecedent == sat::null_literal)
-            add_unit(eq_internalize(lhs->get_expr(), rhs));
-        else if (s().value(antecedent) == l_true) {
-            euf::th_propagation* jst = euf::th_propagation::mk(*this, antecedent);
-            ctx.propagate(lhs, e_internalize(rhs), jst);
-        }
-        else
-            add_clause(~antecedent, eq_internalize(lhs->get_expr(), rhs));
+            add_unit(eq_internalize(e1, e2));
+        else if (s().value(antecedent) == l_true) 
+            ctx.propagate(n1, e_internalize(e2), euf::th_propagation::mk(*this, antecedent));
+        else 
+            add_clause(~antecedent, eq_internalize(e1, e2));
     }
 
     /**
@@ -129,6 +128,10 @@ namespace dt {
             m_args.push_back(m.mk_app(d, e));
         expr_ref con(m.mk_app(c, m_args), m);
         assert_eq_axiom(n, con, antecedent);
+        enode* n2 = e_internalize(con);
+        theory_var v1 = n->get_th_var(get_id());
+        theory_var v2 = n2->get_th_var(get_id());
+        m_find.merge(v1, v2);
     }
 
     /**
@@ -239,7 +242,7 @@ namespace dt {
        \brief Create a new case split for v. That is, create the atom (is_mk v) and mark it as relevant.
        If first is true, it means that v does not have recognizer yet.
     */
-    void solver::mk_split(theory_var v) {
+    void solver::mk_split(theory_var v) {        
         m_stats.m_splits++;
 
         v = m_find.find(v);
@@ -258,10 +261,11 @@ namespace dt {
                                
         if (recognizer == nullptr)
             r = dt.get_constructor_is(non_rec_c);
-        else if (ctx.value(recognizer) != l_false)
+        else if (ctx.value(recognizer) != l_false) {
             // if is l_true, then we are done
             // otherwise wait for recognizer to be assigned.
             return;
+        }
         else {
             // look for a slot of d->m_recognizers that is 0, or it is not marked as relevant and is unassigned.
             unsigned idx = 0;
@@ -284,7 +288,8 @@ namespace dt {
         SASSERT(r != nullptr);
         app_ref r_app(m.mk_app(r, n->get_expr()), m);
         TRACE("dt", tout << "creating split: " << mk_pp(r_app, m) << "\n";);
-        mk_literal(r_app);
+        sat::literal lit = mk_literal(r_app);
+        s().set_phase(lit);
     }
 
     void solver::apply_sort_cnstr(enode* n, sort* s) {
@@ -695,8 +700,13 @@ namespace dt {
 
     void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
         theory_var v = n->get_th_var(get_id());
-        for (enode* arg : euf::enode_args(m_var_data[m_find.find(v)]->m_constructor))
-            dep.add(n, arg);
+        if (!is_datatype(n->get_expr()))
+            return;
+        euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
+        if (con->num_args() == 0)
+            dep.insert(n, nullptr);                
+        for (enode* arg : euf::enode_args(con))
+            dep.add(n, arg->get_root());
     }
 
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h
index 92300301f..07021057c 100644
--- a/src/sat/smt/dt_solver.h
+++ b/src/sat/smt/dt_solver.h
@@ -151,6 +151,7 @@ namespace dt {
         euf::theory_var mk_var(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override { return false; }
+        lbool get_phase(bool_var v) override { return l_true; }
 
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 9f95083c1..58748c9ca 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -103,16 +103,15 @@ namespace euf {
         TRACE("euf",
               for (auto const& d : deps.deps()) 
                   if (d.m_value) {
-                      tout << mk_bounded_pp(d.m_key->get_expr(), m) << ":\n";
+                      tout << bpp(d.m_key) << ":\n";
                       for (auto* n : *d.m_value)
-                          tout << "   " << mk_bounded_pp(n->get_expr(), m) << "\n";
+                          tout << "   " << bpp(n) << "\n";
                   }
               );
     }
 
     void solver::dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl) {
         for (enode* n : deps.top_sorted()) {
-            
             unsigned id = n->get_root_id();
             if (m_values.get(id, nullptr))
                 continue;