From 1c163dbad2d2d9716a6a9eb7654a6a4387104ee3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Sep 2024 16:41:00 +0300 Subject: [PATCH] remove output Signed-off-by: Nikolaj Bjorner --- src/sat/smt/arith_internalize.cpp | 10 +++++++ src/sat/smt/arith_solver.h | 3 ++ src/sat/smt/euf_solver.cpp | 49 ++++++++++++++++++------------- src/sat/smt/euf_solver.h | 2 ++ src/sat/smt/sat_th.h | 2 ++ src/smt/theory_lra.cpp | 1 - 6 files changed, 45 insertions(+), 22 deletions(-) diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index a389d13b8..9c4e5c9be 100644 --- 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 index 755611474..f940af8b4 100644 --- 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 index 0a58d7d1d..b443d836e 100644 --- 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 index 8c436b942..650208183 100644 --- 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> m_initial_values; + // replay typedef std::tuple reinit_t; vector m_reinit; diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 373948014..24226eede 100644 --- 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 index 8f334276d..38291237d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1422,7 +1422,6 @@ public: 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 {