mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

sketch of internal propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-09-27 20:43:38 -07:00
parent 7207f0ff9c
commit 65e59e3ec4
1 changed files with 15 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/math/lp/monomial_bounds.cpp
View file

@ -298,19 +298,21 @@ namespace nla {
u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) { u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) {
u_dependency* dep = nullptr; u_dependency* dep = nullptr;
for (auto j : m.vars()) { auto update_dep = [&](unsigned j) {
if (k == 0) { dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j));
if (c().var_is_fixed_to_zero(j)) { dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j));
dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j)); return dep;
dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j)); };
return dep;
} if (k == 0) {
continue; for (auto j : m.vars())
} if (c().var_is_fixed_to_zero(j))
if (c().var_is_fixed(j)) { return update_dep(j);
dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j)); }
dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j)); else {
} for (auto j : m.vars())
if (c().var_is_fixed(j))
update_dep(j);
} }
return dep; return dep;
} }