#5324

src/sat/smt/euf_solver.cpp

@@ -332,10 +332,10 @@ namespace euf {
                 propagated1 = true;
             }
 
-            for (auto* s : m_solvers) {
-                if (s->unit_propagate())
+            for (unsigned i = 0; i < m_solvers.size(); ++i) 
+                if (m_solvers[i]->unit_propagate())
                     propagated1 = true;
-            }
+
             if (!propagated1)
                 break;
             propagated = true;             

src/sat/smt/fpa_solver.cpp

@@ -122,6 +122,50 @@ namespace fpa {
             n = mk_enode(e, false);
         SASSERT(!n->is_attached_to(get_id()));
         mk_var(n);
+        TRACE("fp", tout << "post: " << mk_bounded_pp(e, m) << "\n";);
+        m_nodes.push_back(std::tuple(n, sign, root));
+        ctx.push(push_back_trail(m_nodes));
+        return true;
+    }
+
+    void solver::apply_sort_cnstr(enode* n, sort* s) {
+        TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_expr(), m) << "\n";);
+        SASSERT(s->get_family_id() == get_id());
+        SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
+        SASSERT(m_fpa_util.is_float(n->get_expr()) || m_fpa_util.is_rm(n->get_expr()));
+        SASSERT(n->get_decl()->get_range() == s);
+
+        if (is_attached_to_var(n))
+            return;
+        attach_new_th_var(n);
+
+        expr* owner = n->get_expr();
+
+        if (m_fpa_util.is_rm(s) && !m_fpa_util.is_bv2rm(owner)) {
+            // For every RM term, we need to make sure that it's
+            // associated bit-vector is within the valid range.
+            expr_ref valid(m), limit(m);
+            limit = m_bv_util.mk_numeral(4, 3);
+            valid = m_bv_util.mk_ule(m_converter.wrap(owner), limit);
+            add_unit(mk_literal(valid));
+        }
+        activate(owner);
+    }
+
+    bool solver::unit_propagate() {
+
+        if (m_nodes.size() <= m_nodes_qhead)
+            return false;
+        ctx.push(value_trail<unsigned>(m_nodes_qhead));
+        for (; m_nodes_qhead < m_nodes.size(); ++m_nodes_qhead) 
+            unit_propagate(m_nodes[m_nodes_qhead]);
+        return true;
+    }
+
+    void solver::unit_propagate(std::tuple<enode*, bool, bool> const& t) {
+        auto [n, sign, root] = t;
+        expr* e = n->get_expr();
+        app* a = to_app(e);
         if (m.is_bool(e)) {
             sat::literal atom(ctx.get_si().add_bool_var(e), false);
             atom = ctx.attach_lit(atom, e);
@@ -151,31 +195,7 @@ namespace fpa {
                 break;
             }
         }
-        return true;
-    }
 
-    void solver::apply_sort_cnstr(enode* n, sort* s) {
-        TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_expr(), m) << "\n";);
-        SASSERT(s->get_family_id() == get_id());
-        SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
-        SASSERT(m_fpa_util.is_float(n->get_expr()) || m_fpa_util.is_rm(n->get_expr()));
-        SASSERT(n->get_decl()->get_range() == s);
-
-        if (is_attached_to_var(n))
-            return;
-        attach_new_th_var(n);
-
-        expr* owner = n->get_expr();
-
-        if (m_fpa_util.is_rm(s) && !m_fpa_util.is_bv2rm(owner)) {
-            // For every RM term, we need to make sure that it's
-            // associated bit-vector is within the valid range.
-            expr_ref valid(m), limit(m);
-            limit = m_bv_util.mk_numeral(4, 3);
-            valid = m_bv_util.mk_ule(m_converter.wrap(owner), limit);
-            add_unit(mk_literal(valid));
-        }
-        activate(owner);
     }
 
     void solver::activate(expr* n) {

src/sat/smt/fpa_solver.h

@@ -36,6 +36,8 @@ namespace fpa {
         bv_util                 & m_bv_util;
         arith_util              & m_arith_util;
         obj_map<expr, expr*>      m_conversions;
+        svector<std::tuple<enode*, bool, bool>> m_nodes;
+        unsigned                  m_nodes_qhead = 0;
 
         bool visit(expr* e) override;
         bool visited(expr* e) override;
@@ -45,6 +47,7 @@ namespace fpa {
         sat::literal_vector mk_side_conditions();
         void attach_new_th_var(enode* n);
         void activate(expr* e);
+        void unit_propagate(std::tuple<enode*, bool, bool> const& t);
         void ensure_equality_relation(theory_var x, theory_var y);      
 
     public:
@@ -67,7 +70,7 @@ namespace fpa {
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         void finalize_model(model& mdl) override;
 
-        bool unit_propagate() override { return false; }
+        bool unit_propagate() override;
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); }
         sat::check_result check() override { return sat::check_result::CR_DONE; }
 

src/sat/tactic/goal2sat.cpp

@@ -744,7 +744,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     };
 
     void process(expr* n, bool is_root, bool redundant) {
-        TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 3) 
+        TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 2) 
             << " root: " << is_root 
             << " result-stack: " << m_result_stack.size() 
             << " frame-stack: " << m_frame_stack.size() << "\n";);
@@ -784,7 +784,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 m_frame_stack[fsz - 1].m_idx++;
                 if (!visit(arg, false, false))
                     goto loop;
-                TRACE("goal2sat_bug", tout << "visit " << mk_bounded_pp(t, m, 2) << " result stack: " << m_result_stack.size() << "\n";);
+                TRACE("goal2sat_bug", tout << "visit " << mk_bounded_pp(arg, m, 2) << " result stack: " << m_result_stack.size() << "\n";);
             }
             TRACE("goal2sat_bug", tout << "converting\n";
                   tout << mk_bounded_pp(t, m, 2) << " root: " << root << " sign: " << sign << "\n";