mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

enable parameter updates after solver initialization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-28 12:49:29 -07:00
parent a4bcd74ba5
commit 8ba9d8c16a
4 changed files with 23 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.cpp
View file

@ -120,6 +120,10 @@ namespace smt {
if (!m_setup.already_configured()) { if (!m_setup.already_configured()) {
m_fparams.updt_params(p); m_fparams.updt_params(p);
} }
for (auto th : m_theory_set)
if (th)
th->updt_params();
} }
unsigned context::relevancy_lvl() const { unsigned context::relevancy_lvl() const {

2
src/smt/smt_theory.h
View file

@ -417,6 +417,8 @@ namespace smt {
smt_params const& get_fparams() const; smt_params const& get_fparams() const;
virtual void updt_params() {}
enode * get_enode(theory_var v) const { enode * get_enode(theory_var v) const {
SASSERT(v < static_cast<int>(m_var2enode.size())); SASSERT(v < static_cast<int>(m_var2enode.size()));
return m_var2enode[v]; return m_var2enode[v];

23
src/smt/theory_lra.cpp
View file

@ -870,16 +870,12 @@ public:
get_zero(true); get_zero(true);
get_zero(false); get_zero(false);
lp().updt_params(ctx().get_params()); lp().updt_params(ctx().get_params());
lp().settings().set_resource_limit(m_resource_limit); lp().settings().set_resource_limit(m_resource_limit);
lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode(); lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode(); // propagation_mode() is state dependent.
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); // suffice to set once
// todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts lp().settings().set_run_gcd_test(ctx().get_fparams().m_arith_gcd_test); // this is not exposed to the user yet.
unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
lp().set_cut_strategy(branch_cut_ratio);
lp().settings().set_run_gcd_test(ctx().get_fparams().m_arith_gcd_test);
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
m_lia = alloc(lp::int_solver, *m_solver.get()); m_lia = alloc(lp::int_solver, *m_solver.get());
} }
@ -4199,6 +4195,13 @@ public:
m_bound_predicate = nullptr; m_bound_predicate = nullptr;
} }
void updt_params() {
if (m_solver)
m_solver->updt_params(ctx().get_params());
if (m_nla)
m_nla->updt_params(ctx().get_params());
}
void validate_model(proto_model& mdl) { void validate_model(proto_model& mdl) {
@ -4359,6 +4362,10 @@ void theory_lra::setup() {
m_imp->setup(); m_imp->setup();
} }
void theory_lra::updt_params() {
m_imp->updt_params();
}
void theory_lra::validate_model(proto_model& mdl) { void theory_lra::validate_model(proto_model& mdl) {
m_imp->validate_model(mdl); m_imp->validate_model(mdl);
} }

2
src/smt/theory_lra.h
View file

@ -94,6 +94,8 @@ namespace smt {
bool get_lower(enode* n, rational& r, bool& is_strict); bool get_lower(enode* n, rational& r, bool& is_strict);
bool get_upper(enode* n, rational& r, bool& is_strict); bool get_upper(enode* n, rational& r, bool& is_strict);
void solve_for(vector<solution>& s) override; void solve_for(vector<solution>& s) override;
void updt_params() override;
void display(std::ostream & out) const override; void display(std::ostream & out) const override;