remove output

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Sep 18, 2024 · 1c163db · 1c163db
1 parent 0f89650
commit 1c163db
Show file tree

Hide file tree

Showing 6 changed files with 45 additions and 22 deletions.
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
@@ -51,6 +51,16 @@ namespace arith {
         }
     }
 
+    void solver::initialize_value(expr* var, expr* value) {
+        rational r;
+        if (!a.is_numeral(value, r)) {
+            IF_VERBOSE(5, verbose_stream() << "numeric constant expected in initialization " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+            return;
+        }
+        lp().move_lpvar_to_value(get_lpvar(mk_evar(var)), r);
+    }
+
+
     lpvar solver::get_one(bool is_int) {
         return add_const(1, is_int ? m_one_var : m_rone_var, is_int);
     }

diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
@@ -485,6 +485,8 @@ namespace arith {
 
         bool validate_conflict();
 
+
+
     public:
         solver(euf::solver& ctx, theory_id id);
         ~solver() override;
@@ -512,6 +514,7 @@ namespace arith {
         void internalize(expr* e) override;
         void eq_internalized(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode* n, sort* s) override {}
+        void initialize_value(expr* var, expr* value) override;
         bool is_shared(theory_var v) const override;
         lbool get_phase(bool_var v) override;
         bool include_func_interp(func_decl* f) const override;

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
@@ -195,6 +195,30 @@ namespace euf {
         m_reason_unknown.clear();
         for (auto* s : m_solvers)
             s->init_search();
+
+        for (auto const& [var, value] : m_initial_values) {
+            if (m.is_bool(var)) {
+                auto lit = expr2literal(var);
+                if (lit == sat::null_literal) {
+                    IF_VERBOSE(5, verbose_stream() << "no literal associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+                    continue;
+                }
+                if (m.is_true(value))
+                    s().set_phase(lit);
+                else if (m.is_false(value))
+                    s().set_phase(~lit);
+                else
+                    IF_VERBOSE(5, verbose_stream() << "malformed value " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");                
+                continue;
+            }
+            auto* th = m_id2solver.get(var->get_sort()->get_family_id(), nullptr);
+            if (!th) {
+                IF_VERBOSE(5, verbose_stream() << "no default initialization associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+                continue;
+            }
+            th->initialize_value(var, value);
+        }
+
     }
 
     bool solver::is_external(bool_var v) {
@@ -1257,27 +1281,10 @@ namespace euf {
     }
 
     void solver::user_propagate_initialize_value(expr* var, expr* value) {
-        if (m.is_bool(var)) {
-            auto lit = expr2literal(var);
-            if (lit == sat::null_literal) {
-                IF_VERBOSE(5, verbose_stream() << "no literal associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
-                return;
-            }
-            if (m.is_true(value))
-                s().set_phase(lit);
-            else if (m.is_false(value))
-                s().set_phase(~lit);
-            else
-                IF_VERBOSE(5, verbose_stream() << "malformed value " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");                
-            return;
-        }
-        auto* th = m_id2solver.get(var->get_sort()->get_family_id(), nullptr);
-        if (!th) {
-            IF_VERBOSE(5, verbose_stream() << "no default initialization associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
-            return;
-        }
-        // th->initialize_value(var, value);
-        IF_VERBOSE(5, verbose_stream() << "no default initialization associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+
+        m_initial_values.push_back({expr_ref(var, m), expr_ref(value, m)});
+        push(push_back_vector(m_initial_values));
+
     }
 
 

diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
@@ -189,6 +189,8 @@ namespace euf {
         euf::enode* mk_true();
         euf::enode* mk_false();
 
+        vector<std::pair<expr_ref, expr_ref>> m_initial_values;
+
         // replay
         typedef std::tuple<expr_ref, unsigned, sat::bool_var> reinit_t;
         vector<reinit_t>    m_reinit;

diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
@@ -152,6 +152,8 @@ namespace euf {
 
         virtual void finalize() {}
 
+        virtual void initialize_value(expr* v, expr* value) { IF_VERBOSE(5, verbose_stream() << "value initialzation is not supported for theory\n"); }
+
     };
 
     class th_proof_hint : public sat::proof_hint {

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -1422,7 +1422,6 @@ class theory_lra::imp {
         m_num_conflicts = 0;
         for (auto const& [v, r] : m_values)
             lp().move_lpvar_to_value(v, r);
-        display(verbose_stream() << "init search\n");
     }
 
     bool can_get_value(theory_var v) const {