mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

add branching on literals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-26 08:30:01 -07:00
parent caf314e569
commit e84d1e9d96
14 changed files with 181 additions and 93 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/dd/pdd_interval.h
View file

@ -126,8 +126,8 @@ public:
else {
get_interval<w_dep::without_deps>(p.lo(), lo_interval);
m_dep_intervals.sub(bound, lo_interval, hi_bound);
m_dep_intervals.div(hi_bound, p.hi().val(), hi_bound);
vectro<scoped_dep_interval> as;
m_dep_intervals.div(hi_bound, p.hi().val().to_mpq(), hi_bound);
vector<scoped_dep_interval> as;
m_var2intervals(p.var(), true, as);
// use hi_bound to adjust for variable bound.
}

10
src/math/grobner/pdd_simplifier.cpp
View file

@ -75,7 +75,7 @@ namespace dd {
}
}
catch (pdd_manager::mem_out) {
IF_VERBOSE(2, verbose_stream() << "simplifier memout\n");
IF_VERBOSE(3, verbose_stream() << "simplifier memout\n");
// done reduce
DEBUG_CODE(s.invariant(););
}
@ -89,7 +89,7 @@ namespace dd {
bool simplifier::simplify_linear_step(bool binary) {
TRACE("dd.solver", tout << "binary " << binary << "\n";);
IF_VERBOSE(2, verbose_stream() << "binary " << binary << "\n");
IF_VERBOSE(3, verbose_stream() << "binary " << binary << "\n");
equation_vector linear;
for (equation* e : s.m_to_simplify) {
pdd p = e->poly();
@ -184,7 +184,7 @@ namespace dd {
*/
bool simplifier::simplify_cc_step() {
TRACE("dd.solver", tout << "cc\n";);
IF_VERBOSE(2, verbose_stream() << "cc\n");
IF_VERBOSE(3, verbose_stream() << "cc\n");
u_map<equation*> los;
bool reduced = false;
unsigned j = 0;
@ -217,7 +217,7 @@ namespace dd {
*/
bool simplifier::simplify_leaf_step() {
TRACE("dd.solver", tout << "leaf\n";);
IF_VERBOSE(2, verbose_stream() << "leaf\n");
IF_VERBOSE(3, verbose_stream() << "leaf\n");
use_list_t use_list = get_use_list();
equation_vector leaves;
for (unsigned i = 0; i < s.m_to_simplify.size(); ++i) {
@ -262,7 +262,7 @@ namespace dd {
*/
bool simplifier::simplify_elim_pure_step() {
TRACE("dd.solver", tout << "pure\n";);
IF_VERBOSE(2, verbose_stream() << "pure\n");
IF_VERBOSE(3, verbose_stream() << "pure\n");
use_list_t use_list = get_use_list();
unsigned j = 0;
for (equation* e : s.m_to_simplify) {

9
src/math/grobner/pdd_solver.cpp
View file

@ -99,7 +99,7 @@ namespace dd {
while (!done() && step()) {
TRACE("dd.solver", display(tout););
DEBUG_CODE(invariant(););
IF_VERBOSE(3, display_statistics(verbose_stream()));
IF_VERBOSE(3, display_statistics(verbose_stream()));
}
DEBUG_CODE(invariant(););
}
@ -322,7 +322,7 @@ namespace dd {
SASSERT(curr->idx() != UINT_MAX);
pdd const& p = curr->poly();
if (curr->state() == to_simplify && p.var() == v) {
if (!eq || is_simpler(*curr, *eq))
if (!eq || is_simpler(*curr, *eq) || (curr->poly().is_linear() && !eq->poly().is_linear()))
eq = curr;
}
}
@ -412,6 +412,11 @@ namespace dd {
}
bool solver::done() {
TRACE("dd.solver",
tout << "simplify.size + process.size >= eqs_threshold " << m_to_simplify.size() << " + " << m_processed.size() << " >= " << m_config.m_eqs_threshold << "\n";
tout << "simplified >= max_simplified " << m_stats.simplified() << " >= " << m_config.m_max_simplified << "\n";
tout << "canceled " << canceled() << "\n";
tout << "compute_steps > max_steps " << m_stats.m_compute_steps << " > " << m_config.m_max_steps << "\n");
return
m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold ||
m_stats.simplified() >= m_config.m_max_simplified ||

4
src/math/lp/lar_solver.h
View file

@ -389,9 +389,9 @@ public:
m_term_register.local_to_external(idx) : m_var_register.local_to_external(idx);
}
bool column_corresponds_to_term(unsigned) const;
const lar_term & column_to_term(unsigned j) const {
const lar_term & column_index_to_term(unsigned j) const {
SASSERT(column_corresponds_to_term(j));
return get_term(column2tv(to_column_index(j)));
return get_term(column2tv(j));
}
inline unsigned row_count() const { return A_r().row_count(); }

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

@ -115,6 +115,7 @@ struct statistics {
unsigned m_hnf_cutter_calls;
unsigned m_hnf_cuts;
unsigned m_nla_calls;
unsigned m_nla_bounds;
unsigned m_horner_calls;
unsigned m_horner_conflicts;
unsigned m_cross_nested_forms;
@ -146,7 +147,7 @@ struct statistics {
st.update("arith-grobner-propagations", m_grobner_propagations);
st.update("arith-offset-eqs", m_offset_eqs);
st.update("arith-fixed-eqs", m_fixed_eqs);
st.update("arith-nla-bounds", m_nla_bounds);
}
};

85
src/math/lp/nla_core.cpp
View file

@ -643,11 +643,11 @@ void core::trace_print_monic_and_factorization(const monic& rm, const factorizat
bool core::var_has_positive_lower_bound(lpvar j) const {
return m_lar_solver.column_has_lower_bound(j) && m_lar_solver.get_lower_bound(j) > lp::zero_of_type<lp::impq>();
return has_lower_bound(j) && m_lar_solver.get_lower_bound(j) > lp::zero_of_type<lp::impq>();
}
bool core::var_has_negative_upper_bound(lpvar j) const {
return m_lar_solver.column_has_upper_bound(j) && m_lar_solver.get_upper_bound(j) < lp::zero_of_type<lp::impq>();
return has_upper_bound(j) && m_lar_solver.get_upper_bound(j) < lp::zero_of_type<lp::impq>();
}
bool core::var_is_separated_from_zero(lpvar j) const {
@ -811,6 +811,7 @@ void core::print_stats(std::ostream& out) {
void core::clear() {
m_lemma_vec->clear();
m_literal_vec->clear();
}
void core::init_search() {
@ -1501,11 +1502,53 @@ void core::check_bounded_divisions(vector<lemma>& l_vec) {
m_divisions.check_bounded_divisions();
}
lbool core::check(vector<lemma>& l_vec) {
bool core::can_add_bound(unsigned j, u_map<unsigned>& bounds) {
unsigned count = 1;
if (bounds.find(j, count))
++count;
bounds.insert(j, count);
struct decrement : public trail {
u_map<unsigned>& bounds;
unsigned j;
decrement(u_map<unsigned>& bounds, unsigned j):
bounds(bounds),
j(j)
{}
void undo() override {
--bounds[j];
}
};
trail().push(decrement(bounds, j));
return count < 3;
}
void core::add_bounds() {
unsigned r = random(), sz = m_to_refine.size();
for (unsigned k = 0; k < sz; k++) {
lpvar i = m_to_refine[(k + r) % sz];
auto const& m = m_emons[i];
for (lpvar j : m.vars()) {
//m_lar_solver.print_column_info(j, verbose_stream() << "check variable " << j << " ") << "\n";
if (var_is_free(j))
m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
else if (has_lower_bound(j) && can_add_bound(j, m_lower_bounds_added))
m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::LE, get_lower_bound(j)));
else if (has_upper_bound(j) && can_add_bound(j, m_upper_bounds_added))
m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::GE, get_upper_bound(j)));
else
continue;
++lp_settings().stats().m_nla_bounds;
return;
}
}
}
lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
lp_settings().stats().m_nla_calls++;
TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
m_lar_solver.get_rid_of_inf_eps();
m_lemma_vec = &l_vec;
m_literal_vec = &lits;
if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL ||
m_lar_solver.get_status() == lp::lp_status::FEASIBLE)) {
TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << m_lar_solver.get_status() << "\n";);
@ -1524,15 +1567,30 @@ lbool core::check(vector<lemma>& l_vec) {
bool run_horner = need_run_horner();
bool run_bounded_nlsat = should_run_bounded_nlsat();
if (l_vec.empty() && !done())
m_monomial_bounds();
auto no_effect = [&]() { return !done() && l_vec.empty() && lits.empty(); };
if (l_vec.empty() && !done() && run_horner)
m_horner.horner_lemmas();
if (l_vec.empty() && !done() && run_grobner)
m_grobner();
{
std::function<void(void)> check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); };
std::function<void(void)> check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); };
std::function<void(void)> check3 = [&]() { if (no_effect()) add_bounds(); };
std::pair<unsigned, std::function<void(void)>> checks[] =
{ {1, check1},
{1, check2},
{1, check3} };
check_weighted(3, checks);
if (!l_vec.empty() || !lits.empty())
return l_false;
}
if (l_vec.empty() && !done())
m_basics.basic_lemma(true);
@ -1542,14 +1600,6 @@ lbool core::check(vector<lemma>& l_vec) {
if (l_vec.empty() && !done())
m_divisions.check();
#if 0
if (l_vec.empty() && !done() && !run_horner)
m_horner.horner_lemmas();
if (l_vec.empty() && !done() && !run_grobner)
m_grobner();
#endif
if (!conflict_found() && !done() && run_bounded_nlsat)
ret = bounded_nlsat();
@ -1633,8 +1683,9 @@ bool core::no_lemmas_hold() const {
}
lbool core::test_check(vector<lemma>& l) {
vector<ineq> lits;
m_lar_solver.set_status(lp::lp_status::OPTIMAL);
return check(l);
return check(lits, l);
}
std::ostream& core::print_terms(std::ostream& out) const {

7
src/math/lp/nla_core.h
View file

@ -84,6 +84,7 @@ class core {
reslimit& m_reslim;
std::function<bool(lpvar)> m_relevant;
vector<lemma> * m_lemma_vec;
vector<ineq> * m_literal_vec = nullptr;
lp::u_set m_to_refine;
tangents m_tangents;
basics m_basics;
@ -111,6 +112,10 @@ class core {
void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
u_map<unsigned> m_lower_bounds_added, m_upper_bounds_added;
bool can_add_bound(unsigned j, u_map<unsigned>& bounds);
void add_bounds();
public:
// constructor
core(lp::lar_solver& s, reslimit&);
@ -381,7 +386,7 @@ public:
bool conflict_found() const;
lbool check(vector<lemma>& l_vec);
lbool check(vector<ineq>& ineqs, vector<lemma>& l_vec);
lbool check_power(lpvar r, lpvar x, lpvar y, vector<lemma>& l_vec);
void check_bounded_divisions(vector<lemma>&);

23
src/math/lp/nla_grobner.cpp
View file

@ -33,6 +33,9 @@ namespace nla {
}
void grobner::operator()() {
if (m_quota == 0) {
m_quota = 2*c().m_nla_settings.grobner_quota;
}
if (m_quota <= c().m_nla_settings.grobner_quota) {
++m_quota;
return;
@ -66,12 +69,12 @@ namespace nla {
}
m_quota -= 3;
// m_quota -= 3;
TRACE("grobner", tout << "saturated\n");
IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
IF_VERBOSE(3, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
#if 0
@ -93,7 +96,7 @@ namespace nla {
lp_settings().stats().m_grobner_conflicts++;
TRACE("grobner", m_solver.display(tout));
IF_VERBOSE(2, if (conflicts > 0) verbose_stream() << "grobner conflict\n");
IF_VERBOSE(3, if (conflicts > 0) verbose_stream() << "grobner conflict\n");
return conflicts > 0;
}
@ -184,8 +187,6 @@ namespace nla {
if (vars.empty() || !q.is_linear())
return false;
// IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n");
term t;
while (!q.is_val()) {
t.add_monomial(q.hi().val(), q.var());
@ -287,15 +288,15 @@ namespace nla {
lo_t.add_monomial(coeff, m.vars[0]);
}
else if (c().find_canonical_monic_of_vars(m.vars, j)) {
verbose_stream() << "canonical monic\n";
//verbose_stream() << "canonical monic\n";
lo_t.add_monomial(coeff, j);
}
else
return false;
}
c().m_intervals.display(verbose_stream(), i); verbose_stream() << "\n";
c().print_ineq(ineq(lo_t, lp::EQ, k), verbose_stream()) << "\n";
//c().m_intervals.display(verbose_stream(), i); verbose_stream() << "\n";
//c().print_ineq(ineq(lo_t, lp::EQ, k), verbose_stream()) << "\n";
new_lemma lemma(c(), "pdd-gcd");
add_dependencies(lemma, eq);
@ -306,7 +307,7 @@ namespace nla {
lemma &= e;
lemma |= ineq(lo_t, lp::EQ, k);
verbose_stream() << lemma << "\n";
//verbose_stream() << lemma << "\n";
return true;
}
@ -339,13 +340,13 @@ namespace nla {
}
}
catch (...) {
IF_VERBOSE(2, verbose_stream() << "pdd throw\n");
IF_VERBOSE(3, verbose_stream() << "pdd throw\n");
return;
}
TRACE("grobner", m_solver.display(tout));
#if 0
IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream()));
IF_VERBOSE(3, m_pdd_grobner.display(verbose_stream()));
dd::pdd_eval eval(m_pdd_manager);
eval.var2val() = [&](unsigned j){ return val(j); };
for (auto* e : m_pdd_grobner.equations()) {

2
src/math/lp/nla_intervals.cpp
View file

@ -276,7 +276,7 @@ void intervals::set_var_interval(lpvar v, interval& b) {
}
if (ls().column_corresponds_to_term(v)) {
auto const& lt = ls().column_to_term(v);
auto const& lt = ls().column_index_to_term(v);
scoped_dep_interval ti(m_dep_intervals), r(m_dep_intervals);
if (interval_from_lar_term<wd>(lt, ti)) {
m_dep_intervals.intersect<wd>(b, ti, r);

4
src/math/lp/nla_solver.cpp
View file

@ -45,8 +45,8 @@ namespace nla {
bool solver::need_check() { return m_core->has_relevant_monomial(); }
lbool solver::check(vector<lemma>& l) {
return m_core->check(l);
lbool solver::check(vector<ineq>& lits, vector<lemma>& lemmas) {
return m_core->check(lits, lemmas);
}
void solver::push(){

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

@ -38,7 +38,7 @@ namespace nla {
void push();
void pop(unsigned scopes);
bool need_check();
lbool check(vector<lemma>&);
lbool check(vector<ineq>& lits, vector<lemma>&);
lbool check_power(lpvar r, lpvar x, lpvar y, vector<lemma>&);
bool is_monic_var(lpvar) const;
bool influences_nl_var(lpvar) const;

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

@ -1414,30 +1414,40 @@ namespace arith {
m_lemma = l; //todo avoid the copy
m_explanation = l.expl();
literal_vector core;
for (auto const& ineq : m_lemma.ineqs()) {
bool is_lower = true, pos = true, is_eq = false;
switch (ineq.cmp()) {
case lp::LE: is_lower = false; pos = false; break;
case lp::LT: is_lower = true; pos = true; break;
case lp::GE: is_lower = true; pos = false; break;
case lp::GT: is_lower = false; pos = true; break;
case lp::EQ: is_eq = true; pos = false; break;
case lp::NE: is_eq = true; pos = true; break;
default: UNREACHABLE();
}
TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
// TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
// then term is used instead of ineq.m_term
sat::literal lit;
if (is_eq)
lit = mk_eq(ineq.term(), ineq.rs());
else
lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower));
core.push_back(pos ? lit : ~lit);
}
for (auto const& ineq : m_lemma.ineqs())
core.push_back(mk_ineq_literal(ineq));
set_conflict_or_lemma(core, false);
}
void solver::assume_literals() {
for (auto const& ineq : m_nla_literals)
s().set_phase(mk_ineq_literal(ineq));
}
sat::literal solver::mk_ineq_literal(nla::ineq const& ineq) {
bool is_lower = true, pos = true, is_eq = false;
switch (ineq.cmp()) {
case lp::LE: is_lower = false; pos = false; break;
case lp::LT: is_lower = true; pos = true; break;
case lp::GE: is_lower = true; pos = false; break;
case lp::GT: is_lower = false; pos = true; break;
case lp::EQ: is_eq = true; pos = false; break;
case lp::NE: is_eq = true; pos = true; break;
default: UNREACHABLE();
}
TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
// TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
// then term is used instead of ineq.m_term
sat::literal lit;
if (is_eq)
lit = mk_eq(ineq.term(), ineq.rs());
else
lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower));
return pos ? lit : ~lit;
}
lbool solver::check_nla() {
if (!m.inc()) {
TRACE("arith", tout << "canceled\n";);
@ -1450,9 +1460,10 @@ namespace arith {
return l_true;
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nla->check(m_nla_lemma_vector);
lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector);
switch (r) {
case l_false:
case l_false:
assume_literals();
for (const nla::lemma& l : m_nla_lemma_vector)
false_case_of_check_nla(l);
break;

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

@ -253,6 +253,7 @@ namespace arith {
// lemmas
lp::explanation m_explanation;
vector<nla::lemma> m_nla_lemma_vector;
vector<nla::ineq> m_nla_literals;
literal_vector m_core, m_core2;
svector<enode_pair> m_eqs;
vector<parameter> m_params;
@ -465,6 +466,8 @@ namespace arith {
void set_evidence(lp::constraint_index idx);
void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, euf::th_proof_hint const* pma);
void assume_literals();
sat::literal mk_ineq_literal(nla::ineq const& ineq);
void false_case_of_check_nla(const nla::lemma& l);
void dbg_finalize_model(model& mdl);

61
src/smt/theory_lra.cpp
View file

@ -2556,44 +2556,54 @@ public:
}
nla::lemma m_lemma;
literal mk_literal(nla::ineq const& ineq) {
bool is_lower = true, pos = true, is_eq = false;
switch (ineq.cmp()) {
case lp::LE: is_lower = false; pos = false; break;
case lp::LT: is_lower = true; pos = true; break;
case lp::GE: is_lower = true; pos = false; break;
case lp::GT: is_lower = false; pos = true; break;
case lp::EQ: is_eq = true; pos = false; break;
case lp::NE: is_eq = true; pos = true; break;
default: UNREACHABLE();
}
TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
app_ref atom(m);
// TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
// then term is used instead of ineq.m_term
if (is_eq)
atom = mk_eq(ineq.term(), ineq.rs());
else
// create term >= 0 (or term <= 0)
atom = mk_bound(ineq.term(), ineq.rs(), is_lower);
return literal(ctx().get_bool_var(atom), pos);
}
void false_case_of_check_nla(const nla::lemma & l) {
m_lemma = l; //todo avoid the copy
m_explanation = l.expl();
literal_vector core;
for (auto const& ineq : m_lemma.ineqs()) {
bool is_lower = true, pos = true, is_eq = false;
switch (ineq.cmp()) {
case lp::LE: is_lower = false; pos = false; break;
case lp::LT: is_lower = true; pos = true; break;
case lp::GE: is_lower = true; pos = false; break;
case lp::GT: is_lower = false; pos = true; break;
case lp::EQ: is_eq = true; pos = false; break;
case lp::NE: is_eq = true; pos = true; break;
default: UNREACHABLE();
}
TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
app_ref atom(m);
// TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
// then term is used instead of ineq.m_term
if (is_eq) {
atom = mk_eq(ineq.term(), ineq.rs());
}
else {
// create term >= 0 (or term <= 0)
atom = mk_bound(ineq.term(), ineq.rs(), is_lower);
}
literal lit(ctx().get_bool_var(atom), pos);
auto lit = mk_literal(ineq);
core.push_back(~lit);
}
set_conflict_or_lemma(core, false);
}
void assume_literal(nla::ineq const& i) {
auto lit = mk_literal(i);
ctx().set_true_first_flag(lit.var());
}
final_check_status check_nla_continue() {
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nla->check(m_nla_lemma_vector);
lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector);
for (const nla::ineq& i : m_nla_literals)
return (assume_literal(i), FC_CONTINUE);
switch (r) {
case l_false:
case l_false:
for (const nla::lemma & l : m_nla_lemma_vector)
false_case_of_check_nla(l);
return FC_CONTINUE;
@ -3751,6 +3761,7 @@ public:
lp::explanation m_explanation;
vector<nla::lemma> m_nla_lemma_vector;
vector<nla::ineq> m_nla_literals;
literal_vector m_core;
svector<enode_pair> m_eqs;
vector<parameter> m_params;