mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-07 16:31:55 +00:00
Code Activity

more imp notes and relevancy experiment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-22 12:44:50 +03:00
parent 0a0e925f27
commit db5a991257
5 changed files with 54 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/lp_params_helper.pyg
View file

@ -9,5 +9,6 @@ def_module_params(module_name='lp',
('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
('enable_relevancy', BOOL, False, 'enable relevancy propagation to filter emons (experiment)')
))

1
src/math/lp/lp_settings.cpp
View file

@ -44,4 +44,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
m_dio_calls_period = lp_p.dio_calls_period();
m_dio_run_gcd = lp_p.dio_run_gcd();
m_max_conflicts = p.max_conflicts();
m_enable_relevancy = lp.enable_relevancy();
}

1
src/math/lp/lp_settings.h
View file

@ -259,6 +259,7 @@ private:
unsigned m_dio_calls_period = 4;
bool m_dio_run_gcd = true;
public:
bool m_enable_relevancy = false;
unsigned dio_calls_period() const { return m_dio_calls_period; }
unsigned & dio_calls_period() { return m_dio_calls_period; }
bool print_external_var_name() const { return m_print_external_var_name; }

55
src/math/lp/nla_mul_saturate.cpp
View file

@ -31,10 +31,10 @@ namespace nla {
for (auto& con : lra.constraints().active()) {
for (auto v : m.vars()) {
for (auto [coeff, u] : con.coeffs()) {
if (u == v) {
// add new constraint
if (u == v)
// multiply by remaining vars
}
multiply_constraint(con, m, v);
// add new constraint
}
}
}
@ -55,8 +55,53 @@ namespace nla {
return r;
}
lp::lar_base_constraint* mul_saturate::multiply_constraint(lp::lar_base_constraint const& c, monic const& m, lpvar x) {
// multiply by remaining vars
void mul_saturate::multiply_constraint(lp::lar_base_constraint const& con, monic const& m, lpvar x) {
auto const& lhs = con.coeffs();
auto const& rhs = con.rhs();
auto k = con.kind();
auto sign = false;
svector<lpvar> vars;
bool first = true;
for (auto v : m.vars()) {
if (v != x || !first)
vars.push_back(v);
else
first = false;
}
vector<std::pair<rational, lpvar>> new_lhs;
rational new_rhs(rhs);
for (auto [coeff, v] : lhs) {
vars.push_back(v);
return nullptr;
auto new_m = c().emons().find_canonical(vars);
if (!new_m) {
bool is_int = lra.var_is_int(x); // assume all vars in monic have the same type, can be changed for MIP
lpvar new_monic_var = 0; // lra.add_var(is_int);
c().emons().add(new_monic_var, vars);
new_m = c().emons().find_canonical(vars);
SASSERT(new_m);
}
new_lhs.push_back({coeff, new_m->var()});
vars.pop_back();
}
if (rhs != 0) {
new_lhs.push_back({-rhs, m.var()});
new_rhs = 0;
}
// compute sign of vars
for (auto v : vars)
if (c().val(v).is_neg())
sign = !sign;
if (sign) {
switch (k) {
case lp::lconstraint_kind::LE: k = lp::lconstraint_kind::GE; break;
case lp::lconstraint_kind::LT: k = lp::lconstraint_kind::GT; break;
case lp::lconstraint_kind::GE: k = lp::lconstraint_kind::LE; break;
case lp::lconstraint_kind::GT: k = lp::lconstraint_kind::LT; break;
default: break;
}
}
// instead of adding a constraint here, add row to tableau based on the new_lhs, new_rhs, k.
}
}

2
src/math/lp/nla_mul_saturate.h
View file

@ -10,7 +10,7 @@ namespace nla {
class lar_solver;
class mul_saturate : common {
lp::lar_solver& lra;
lp::lar_base_constraint* multiply_constraint(lp::lar_base_constraint const& c, monic const& m, lpvar x);
void multiply_constraint(lp::lar_base_constraint const& c, monic const& m, lpvar x);
public:
mul_saturate(core* core);