mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' into nl_branches

Browse source
This commit is contained in:
Lev Nachmanson 2023-08-21 16:15:20 -07:00 • committed by GitHub
commit 9aeaed8f53
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
52 changed files with 735 additions and 590 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_anf_simplifier.cpp
View file

@ -42,7 +42,8 @@ namespace sat {
void anf_simplifier::operator()() {
dd::pdd_manager m(20, dd::pdd_manager::semantics::mod2_e);
pdd_solver solver(s.rlimit(), m);
u_dependency_manager dm;
pdd_solver solver(s.rlimit(), dm, m);
report _report(*this);
configure_solver(solver);
clauses2anf(solver);

6
src/sat/smt/arith_axioms.cpp
View file

@ -524,7 +524,7 @@ namespace arith {
return all_divs_valid;
}
void solver::fixed_var_eh(theory_var v, lp::constraint_index ci1, lp::constraint_index ci2, rational const& bound) {
void solver::fixed_var_eh(theory_var v, u_dependency* dep, rational const& bound) {
theory_var w = euf::null_theory_var;
enode* x = var2enode(v);
if (bound.is_zero())
@ -540,8 +540,8 @@ namespace arith {
return;
reset_evidence();
m_explanation.clear();
consume(rational::one(), ci1);
consume(rational::one(), ci2);
for (auto ci : lp().flatten(dep))
consume(rational::one(), ci);
++m_stats.m_fixed_eqs;
auto* hint = explain_implied_eq(m_explanation, x, y);
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y, hint);

46
src/sat/smt/arith_solver.cpp
View file

@ -402,12 +402,13 @@ namespace arith {
}
void solver::propagate_eqs(lp::tv t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) {
lp::constraint_index ci2;
if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t.index(), ci2, value)) {
fixed_var_eh(b.get_var(), ci1, ci2, value);
u_dependency* dep;
auto& dm = lp().dep_manager();
if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t.index(), dep, value)) {
fixed_var_eh(b.get_var(), dm.mk_join(dm.mk_leaf(ci1), dep), value);
}
else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t.index(), ci2, value)) {
fixed_var_eh(b.get_var(), ci1, ci2, value);
else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t.index(), dep, value)) {
fixed_var_eh(b.get_var(), dm.mk_join(dm.mk_leaf(ci1), dep), value);
}
}
@ -433,11 +434,12 @@ namespace arith {
// m_solver already tracks bounds on proper variables, but not on terms.
bool is_strict = false;
rational b;
u_dependency* dep = nullptr;
if (is_lower) {
return lp().has_lower_bound(tv.id(), ci, b, is_strict) && !is_strict && b == v;
return lp().has_lower_bound(tv.id(), dep, b, is_strict) && !is_strict && b == v;
}
else {
return lp().has_upper_bound(tv.id(), ci, b, is_strict) && !is_strict && b == v;
return lp().has_upper_bound(tv.id(), dep, b, is_strict) && !is_strict && b == v;
}
}
}
@ -692,7 +694,7 @@ namespace arith {
void solver::report_equality_of_fixed_vars(unsigned vi1, unsigned vi2) {
rational bound;
lp::constraint_index ci1, ci2, ci3, ci4;
u_dependency* ci1 = nullptr, *ci2 = nullptr, *ci3 = nullptr, *ci4 = nullptr;
theory_var v1 = lp().local_to_external(vi1);
theory_var v2 = lp().local_to_external(vi2);
TRACE("arith", tout << "fixed: " << mk_pp(var2expr(v1), m) << " " << mk_pp(var2expr(v2), m) << "\n";);
@ -714,10 +716,10 @@ namespace arith {
++m_stats.m_fixed_eqs;
reset_evidence();
m_explanation.clear();
consume(rational::one(), ci1);
consume(rational::one(), ci2);
consume(rational::one(), ci3);
consume(rational::one(), ci4);
auto& dm = lp().dep_manager();
auto* d = dm.mk_join(dm.mk_join(ci1, ci2), dm.mk_join(ci3, ci4));
for (auto ci : lp().flatten(d))
consume(rational::one(), ci);
enode* x = var2enode(v1);
enode* y = var2enode(v2);
auto* ex = explain_implied_eq(m_explanation, x, y);
@ -729,26 +731,28 @@ namespace arith {
return x == y || var2enode(x)->get_root() == var2enode(y)->get_root();
}
bool solver::has_upper_bound(lpvar vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, false); }
bool solver::has_upper_bound(lpvar vi, u_dependency*& ci, rational const& bound) { return has_bound(vi, ci, bound, false); }
bool solver::has_lower_bound(lpvar vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
bool solver::has_lower_bound(lpvar vi, u_dependency*& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
bool solver::has_bound(lpvar vi, lp::constraint_index& ci, rational const& bound, bool is_lower) {
bool solver::has_bound(lpvar vi, u_dependency*& dep, rational const& bound, bool is_lower) {
if (lp::tv::is_term(vi)) {
theory_var v = lp().local_to_external(vi);
rational val;
TRACE("arith", tout << lp().get_variable_name(vi) << " " << v << "\n";);
if (v != euf::null_theory_var && a.is_numeral(var2expr(v), val) && bound == val) {
ci = UINT_MAX;
dep = nullptr;
return bound == val;
}
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
lpvar ti = lp::tv::unmask_term(vi);
if (vec.size() > ti) {
constraint_bound& b = vec[ti];
ci = b.first;
return ci != UINT_MAX && bound == b.second;
auto& [ci, coeff] = vec[ti];
if (ci == UINT_MAX)
return false;
dep = lp().dep_manager().mk_leaf(ci);
return bound == coeff;
}
else {
return false;
@ -758,10 +762,10 @@ namespace arith {
bool is_strict = false;
rational b;
if (is_lower) {
return lp().has_lower_bound(vi, ci, b, is_strict) && b == bound && !is_strict;
return lp().has_lower_bound(vi, dep, b, is_strict) && b == bound && !is_strict;
}
else {
return lp().has_upper_bound(vi, ci, b, is_strict) && b == bound && !is_strict;
return lp().has_upper_bound(vi, dep, b, is_strict) && b == bound && !is_strict;
}
}
}

8
src/sat/smt/arith_solver.h
View file

@ -360,7 +360,7 @@ namespace arith {
void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r);
api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound);
lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true);
void fixed_var_eh(theory_var v1, lp::constraint_index ci1, lp::constraint_index ci2, rational const& bound);
void fixed_var_eh(theory_var v1, u_dependency* dep, rational const& bound);
bool set_upper_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); }
bool set_lower_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); }
bool set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower);
@ -413,9 +413,9 @@ namespace arith {
nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const;
bool has_bound(lpvar vi, lp::constraint_index& ci, rational const& bound, bool is_lower);
bool has_lower_bound(lpvar vi, lp::constraint_index& ci, rational const& bound);
bool has_upper_bound(lpvar vi, lp::constraint_index& ci, rational const& bound);
bool has_bound(lpvar vi, u_dependency*& ci, rational const& bound, bool is_lower);
bool has_lower_bound(lpvar vi, u_dependency*& ci, rational const& bound);
bool has_upper_bound(lpvar vi, u_dependency*& ci, rational const& bound);
/*
* Facility to put a small box around integer variables used in branch and bounds.