Some UP bugfixes in the new core (#6673)

src/sat/sat_solver/inc_sat_solver.cpp

@@ -701,6 +701,10 @@ public:
         ensure_euf()->user_propagate_register_created(r);
     }
 
+    void user_propagate_register_decide(user_propagator::decide_eh_t& r) override {
+        ensure_euf()->user_propagate_register_decide(r);
+    }
+
 
 private:
 

src/sat/sat_solver/sat_smt_solver.cpp

@@ -568,6 +568,10 @@ public:
         ensure_euf()->user_propagate_register_created(r);
     }
 
+    void user_propagate_register_decide(user_propagator::decide_eh_t& r) override {
+        ensure_euf()->user_propagate_register_decide(r);
+    }
+
 private:
 
     void add_assumption(expr* a) {

src/sat/smt/euf_solver.cpp

@@ -349,6 +349,20 @@ namespace euf {
         si.uncache(literal(v, true));
     }
 
+    bool solver::decide(bool_var& var, lbool& phase) {
+        for (auto const& th : m_solvers)
+            if (th->decide(var, phase))
+                return true;
+        return false;
+    }
+
+    bool solver::get_case_split(bool_var& var, lbool& phase) {
+        for (auto const& th : m_solvers)
+            if (th->get_case_split(var, phase))
+                return true;
+        return false;
+    }
+
     void solver::asserted(literal l) {
         m_relevancy.asserted(l);
         if (!m_relevancy.is_relevant(l))

src/sat/smt/euf_solver.h

@@ -369,6 +369,8 @@ namespace euf {
         void add_explain(size_t* p) { m_explain.push_back(p); }
         void reset_explain() { m_explain.reset(); }
         void set_eliminated(bool_var v) override;
+        bool decide(bool_var& var, lbool& phase) override;
+        bool get_case_split(bool_var& var, lbool& phase) override;
         void asserted(literal l) override;
         sat::check_result check() override;
         void push() override;
@@ -540,6 +542,10 @@ namespace euf {
             check_for_user_propagator();
             m_user_propagator->register_created(ceh);
         }
+        void user_propagate_register_decide(user_propagator::decide_eh_t& ceh) {
+            check_for_user_propagator();
+            m_user_propagator->register_decide(ceh);
+        }
         void user_propagate_register_expr(expr* e) {
             check_for_user_propagator();
             m_user_propagator->add_expr(e);

src/sat/smt/user_solver.cpp

@@ -21,7 +21,7 @@ Author:
 namespace user_solver {
 
     solver::solver(euf::solver& ctx) :
-        th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user"))
+        th_euf_solver(ctx, symbol(user_propagator::plugin::name()), ctx.get_manager().mk_family_id(user_propagator::plugin::name()))
     {}
 
     solver::~solver() {
@@ -92,24 +92,24 @@ namespace user_solver {
         
         euf::enode* original_enode = bool_var2enode(var);
         
-        if (!is_attached_to_var(original_enode))
+        if (!original_enode || !is_attached_to_var(original_enode))
             return false;
         
         unsigned new_bit = 0; // ignored; currently no bv-support
-        expr* e = bool_var2expr(var);
+        expr* e = original_enode->get_expr();
         
         m_decide_eh(m_user_context, this, &e, &new_bit, &phase);
         
         euf::enode* new_enode = ctx.get_enode(e);
     
-        if (original_enode == new_enode)
+        if (original_enode == new_enode || new_enode->bool_var() == sat::null_bool_var)
             return false;
         
         var = new_enode->bool_var();
         return true;
     }
     
-    bool solver::get_case_split(sat::bool_var& var, lbool &phase){
+    bool solver::get_case_split(sat::bool_var& var, lbool& phase){
         if (!m_next_split_expr)
             return false;
         
@@ -123,9 +123,12 @@ namespace user_solver {
     void solver::asserted(sat::literal lit) {
         if (!m_fixed_eh)
             return;
-        force_push();
         auto* n = bool_var2enode(lit.var());
         euf::theory_var v = n->get_th_var(get_id());
+        if (!m_id2justification.get(v, sat::literal_vector()).empty())
+            // the core merged variables. We already issued the respective fixed callback for an equated variable
+            return;
+        force_push();
         sat::literal_vector lits;
         lits.push_back(lit);
         m_id2justification.setx(v, lits, sat::literal_vector());