From c2098b41d663af99654a3fba1ee33c1387682739 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 May 2025 03:24:45 -0700 Subject: [PATCH] Pr (#7654) * add prd Signed-off-by: Nikolaj Bjorner * missing text Signed-off-by: Nikolaj Bjorner * fix Signed-off-by: Nikolaj Bjorner * fix #7647 * fix #7647 - with respect to scope level * initial stab at randomizer Signed-off-by: Nikolaj Bjorner * Create prd.yml * missing text Signed-off-by: Nikolaj Bjorner * fix Signed-off-by: Nikolaj Bjorner * Update prd.yml * allows setting simplifier factory independently of whether solver has been allocated. Instances, such as #7484 can be solved faster by either having authors rewrite benchmarks or by using incremental pre-processing. You can add incremental pre-processing to the SMT solver by using the command ``` (set-simplifier (then simplify propagate-values solve-eqs elim-unconstrained simplify)) ``` This command can be invoked any time prior to push or adding assertions. The effect of the command is that it adds an incremental pre-processing pass to check-sat invocations that is potentially more powerful than the default pre-processing. The default pre-processing functionality is not touched mainly to avoid instability against functionality that is already built around its behavior. * remove experiment from pr --------- Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 5 ++++- src/cmd_context/cmd_context.h | 3 +++ src/cmd_context/simplifier_cmds.cpp | 3 ++- 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index ca13451b6..7c489ccc3 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1493,7 +1493,8 @@ void cmd_context::insert_aux_pdecl(pdecl * p) { m_aux_pdecls.push_back(p); } -void cmd_context::reset(bool finalize) { +void cmd_context::reset(bool finalize) { + m_simplifier_factory = nullptr; m_logic = symbol::null; m_check_sat_result = nullptr; m_numeral_as_real = false; @@ -2260,6 +2261,8 @@ void cmd_context::mk_solver() { m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled); m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic); m_solver = mk_slice_solver(m_solver.get()); + if (m_simplifier_factory) + m_solver = mk_simplifier_solver(m_solver.get(), &m_simplifier_factory); } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index c90d56237..5e5f30028 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -38,6 +38,7 @@ Notes: #include "solver/solver.h" #include "solver/check_logic.h" #include "solver/progress_callback.h" +#include "solver/simplifier_solver.h" #include "cmd_context/pdecl.h" #include "cmd_context/tactic_manager.h" #include "params/context_params.h" @@ -282,6 +283,7 @@ protected: std::vector m_assertion_strings; ptr_vector m_assertion_names; // named assertions are represented using boolean variables. scoped_ptr m_std_subst, m_rev_subst; + simplifier_factory m_simplifier_factory; struct scope { unsigned m_func_decls_stack_lim; @@ -429,6 +431,7 @@ public: void set_initial_value(expr* var, expr* value); void set_solver_factory(solver_factory * s); + void set_simplifier_factory(simplifier_factory& sf) { m_simplifier_factory = sf; } void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; } check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); } check_sat_state cs_state() const; diff --git a/src/cmd_context/simplifier_cmds.cpp b/src/cmd_context/simplifier_cmds.cpp index b2d96844a..291142b53 100644 --- a/src/cmd_context/simplifier_cmds.cpp +++ b/src/cmd_context/simplifier_cmds.cpp @@ -156,7 +156,8 @@ public: auto simplifier_factory = sexpr2simplifier(ctx, m_simplifier); ctx.init_manager(); auto* s = ctx.get_solver(); - if (!s) + ctx.set_simplifier_factory(simplifier_factory); + if (!s) return; if (s->get_num_assertions() > 0) throw cmd_exception("set-simplifier cannot be invoked if there are already assertions");