From a3f35b6830fb9639a3e1d0dc23250e91973cb244 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Sep 2024 17:48:03 +0300 Subject: [PATCH] Add command to set initial value hints for solver in various components --- src/cmd_context/basic_cmds.cpp | 20 +++++++++++++++++++ src/cmd_context/cmd_context.h | 2 ++ src/nlsat/tactic/nlsat_tactic.cpp | 3 +++ src/opt/opt_context.h | 4 ++-- src/qe/nlqsat.cpp | 2 ++ src/qe/qsat.cpp | 4 +++- src/sat/tactic/sat_tactic.cpp | 5 +++++ src/smt/theory_bv.cpp | 20 +++++++++++++++++++ src/smt/theory_bv.h | 1 + src/smt/theory_lra.cpp | 6 +----- src/solver/combined_solver.cpp | 1 + src/solver/solver2tactic.cpp | 5 +++++ src/tactic/.#tactic.cpp | 1 + .../fd_solver/bounded_int2bv_solver.cpp | 3 +++ src/tactic/tactic.cpp | 1 + src/tactic/tactic.h | 1 + src/tactic/tactical.cpp | 11 ++++++++++ 17 files changed, 82 insertions(+), 8 deletions(-) create mode 100644 src/tactic/.#tactic.cpp diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index c93e4432f30..cf661df4980 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -318,6 +318,25 @@ UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, else ctx.regular_stream() << arg << std::endl;); +class set_initial_value_cmd : public cmd { + expr* m_var = nullptr, *m_value = nullptr; +public: + set_initial_value_cmd(): cmd("set-initial-value") {} + char const* get_usage() const override { return " "; } + char const* get_descr(cmd_context& ctx) const { return "set an initial value for search as a hint to the solver"; } + unsigned get_arity() const { return 2; } + void prepare(cmd_context& ctx) { m_var = m_value = nullptr; } + cmd_arg_kind next_arg_kind(cmd_context& ctx) const { return CPK_EXPR; } + void set_next_arg(cmd_context& ctx, expr* e) { if (m_var) m_value = e; else m_var = e; } + void execute(cmd_context& ctx) { + SASSERT(m_var && m_value); + if (ctx.get_opt()) + ctx.get_opt()->initialize_value(m_var, m_value); + else if (ctx.get_solver()) + ctx.get_solver()->user_propagate_initialize_value(m_var, m_value); + } +}; + class set_get_option_cmd : public cmd { protected: symbol m_true; @@ -893,6 +912,7 @@ void install_basic_cmds(cmd_context & ctx) { ctx.insert(alloc(get_option_cmd)); ctx.insert(alloc(get_info_cmd)); ctx.insert(alloc(set_info_cmd)); + ctx.insert(alloc(set_initial_value_cmd)); ctx.insert(alloc(get_consequences_cmd)); ctx.insert(alloc(builtin_cmd, "assert", "", "assert term.")); ctx.insert(alloc(builtin_cmd, "check-sat", "*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true.")); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index c07d888c7e4..fc3c9f310d4 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -173,6 +173,8 @@ class opt_wrapper : public check_sat_result { virtual void set_logic(symbol const& s) = 0; virtual void get_box_model(model_ref& mdl, unsigned index) = 0; virtual void updt_params(params_ref const& p) = 0; + virtual void initialize_value(expr* var, expr* value) = 0; + }; class ast_context_params : public context_params { diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 9426de78ee7..11c80de2abb 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -262,6 +262,9 @@ class nlsat_tactic : public tactic { void reset_statistics() override { m_stats.reset(); } + + void user_propagate_initialize_value(expr* var, expr* value) override { } + }; tactic * mk_nlsat_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 845fd39689a..991fe16e6ea 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -277,8 +277,8 @@ namespace opt { void add_offset(unsigned id, rational const& o) override; - void initialize_value(expr* var, expr* value); - + void initialize_value(expr* var, expr* value) override; + void register_on_model(on_model_t& ctx, std::function& on_model) { m_on_model_ctx = ctx; m_on_model_eh = on_model; diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 37cf62c615b..9fd1d4e0ec0 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -848,6 +848,8 @@ namespace qe { void collect_param_descrs(param_descrs & r) override { } + void user_propagate_initialize_value(expr* var, expr* value) override { } + void operator()(/* in */ goal_ref const & in, /* out */ goal_ref_buffer & result) override { diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index dc0613c59d8..0ff054a8940 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1377,7 +1377,9 @@ namespace qe { tactic * translate(ast_manager & m) override { return alloc(qsat, m, m_params, m_mode); - } + } + + void user_propagate_initialize_value(expr* var, expr* value) override { } lbool maximize(expr_ref_vector const& fmls, app* t, model_ref& mdl, opt::inf_eps& value) { expr_ref_vector defs(m); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 562fa431eda..223222f9aa1 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -246,6 +246,11 @@ class sat_tactic : public tactic { m_stats.reset(); } + void user_propagate_initialize_value(expr* var, expr* value) override { + + } + + protected: }; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 55d3a1d6245..cf110298f3b 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1789,6 +1789,26 @@ namespace smt { return false; } + void theory_bv::initialize_value(expr* var, expr* value) { + rational val; + unsigned sz; + if (!m_util.is_numeral(value, val, sz)) { + IF_VERBOSE(5, verbose_stream() << "value should be a bit-vector " << mk_pp(value, m) << "\n"); + return; + } + if (!is_app(var)) + return; + enode* n = mk_enode(to_app(var)); + auto v = get_var(n); + unsigned idx = 0; + for (auto lit : m_bits[v]) { + auto & b = ctx.get_bdata(lit.var()); + b.m_phase_available = true; + b.m_phase = val.get_bit(idx); + ++idx; + } + } + void theory_bv::init_model(model_generator & mg) { m_factory = alloc(bv_factory, m); mg.register_factory(m_factory); diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 10cf005e343..72775c1d353 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -251,6 +251,7 @@ namespace smt { bool merge_zero_one_bits(theory_var r1, theory_var r2); bool can_propagate() override { return m_prop_diseqs_qhead < m_prop_diseqs.size(); } void propagate() override; + void initialize_value(expr* var, expr* value) override; // ----------------------------------- // diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 38291237d97..6de623bb780 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -154,7 +154,6 @@ class theory_lra::imp { svector m_asserted_atoms; ptr_vector m_not_handled; ptr_vector m_underspecified; - vector> m_values; vector > m_use_list; // bounds where variables are used. // attributes for incremental version: @@ -998,8 +997,7 @@ class theory_lra::imp { IF_VERBOSE(5, verbose_stream() << "numeric constant expected in initialization " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n"); return; } - ctx().push_trail(push_back_vector(m_values)); - m_values.push_back({get_lpvar(var), r}); + lp().move_lpvar_to_value(get_lpvar(var), r); } void new_eq_eh(theory_var v1, theory_var v2) { @@ -1420,8 +1418,6 @@ class theory_lra::imp { void init_search_eh() { m_arith_eq_adapter.init_search_eh(); m_num_conflicts = 0; - for (auto const& [v, r] : m_values) - lp().move_lpvar_to_value(v, r); } bool can_get_value(theory_var v) const { diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 051dfd4eb9d..34d31ec84de 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -396,6 +396,7 @@ class combined_solver : public solver { } void user_propagate_initialize_value(expr* var, expr* value) override { + m_solver1->user_propagate_initialize_value(var, value); m_solver2->user_propagate_initialize_value(var, value); } diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index b8e3dd37a6e..add55c62846 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -189,6 +189,11 @@ class solver2tactic : public tactic { } char const* name() const override { return "solver2tactic"; } + + + void user_propagate_initialize_value(expr* var, expr* value) override { + m_solver->user_propagate_initialize_value(var, value); + } }; tactic* mk_solver2tactic(solver* s) { return alloc(solver2tactic, s); } diff --git a/src/tactic/.#tactic.cpp b/src/tactic/.#tactic.cpp new file mode 100644 index 00000000000..12fd8329bc4 --- /dev/null +++ b/src/tactic/.#tactic.cpp @@ -0,0 +1 @@ +nbjorner@LAPTOP-04AEAFKH.32880:1726092166 \ No newline at end of file diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index 317286e1e83..45b444fe9b2 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -375,6 +375,9 @@ class bounded_int2bv_solver : public solver_na2as { return m_assertions.get(idx); } } + + void user_propagate_initialize_value(expr* var, expr* value) override { + } }; solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s) { diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index f7dcfb3ea02..e4e7b246aef 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -151,6 +151,7 @@ class fail_if_undecided_tactic : public skip_tactic { throw tactic_exception("undecided"); skip_tactic::operator()(in, result); } + void user_propagate_initialize_value(expr* var, expr* value) override { } }; tactic * mk_fail_if_undecided_tactic() { diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index e62f93ecf06..c6927642476 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -129,6 +129,7 @@ class skip_tactic : public tactic { tactic * translate(ast_manager & m) override { return this; } char const* name() const override { return "skip"; } void collect_statistics(statistics& st) const override {} + void user_propagate_initialize_value(expr* var, expr* value) override { } }; tactic * mk_skip_tactic(); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 626380913f6..db0a6d44d76 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -382,6 +382,12 @@ class or_else_tactical : public nary_tactical { } tactic * translate(ast_manager & m) override { return translate_core(m); } + + void user_propagate_initialize_value(expr* var, expr* value) override { + for (auto t : m_ts) + t->user_propagate_initialize_value(var, value); + } + }; tactic * or_else(unsigned num, tactic * const * ts) { @@ -1163,6 +1169,11 @@ class cond_tactical : public binary_tactical { tactic * new_t2 = m_t2->translate(m); return alloc(cond_tactical, m_p.get(), new_t1, new_t2); } + + void user_propagate_initialize_value(expr* var, expr* value) override { + m_t1->user_propagate_initialize_value(var, value); + m_t2->user_propagate_initialize_value(var, value); + } }; tactic * cond(probe * p, tactic * t1, tactic * t2) {