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

fix #3183 - change relevancy propagation to ensure that div/mod axioms are picked up

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-10 19:14:04 -07:00 • committed by Lev Nachmanson
parent 1e9013fe6d
commit 0207878f5f
3 changed files with 58 additions and 103 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_theory.cpp
View file

@ -141,6 +141,7 @@ namespace smt {
void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
ast_manager & m = get_manager();
app_ref _r(r, m);
std::ostream& out = m.trace_stream();
symbol const & family_name = m.get_family_name(get_family_id());
if (pattern_id == UINT_MAX) {
@ -158,7 +159,8 @@ namespace smt {
out << " #" << substituted->get_owner_id();
}
}
} else {
}
else {
SASSERT(axiom_id != UINT_MAX);
obj_hashtable<enode> already_visited;
for (auto n : used_enodes) {

14
src/smt/smt_theory.h
View file

@ -114,6 +114,15 @@ namespace smt {
}
};
struct if_trace_stream {
ast_manager& m;
if_trace_stream(ast_manager& m, std::function<void (void)>& fn): m(m) {
if (m.has_trace_stream()) {
fn();
}
}
};
protected:
/**
@ -418,6 +427,11 @@ namespace smt {
log_axiom_instantiation(r, UINT_MAX, 0, nullptr, UINT_MAX, used_enodes);
}
void log_axiom_unit(app* r) {
log_axiom_instantiation(r);
m_manager->trace_stream() << "[end-of-instance]\n";
}
public:
/**
\brief Assume eqs between variable that are equal with respect to the given table.

143
src/smt/theory_lra.cpp
View file

@ -1351,59 +1351,35 @@ public:
context& c = ctx();
if (!k.is_zero()) {
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(eq);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(mod_ge_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper));
th.log_axiom_instantiation(body);
mk_axiom(mk_literal(a.mk_le(mod, upper)));
{
std::function<void(void)> log = [&,this]() {
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper)));
};
if_trace_stream _ts(m, log);
}
expr_ref le(a.mk_le(mod, upper), m);
mk_axiom(mk_literal(le));
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (k.is_pos()) {
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(~p_ge_0, div_ge_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(~p_ge_0, div_ge_0);
mk_axiom(~p_le_0, div_le_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
std::function<void(void)> log = [&,this]() {
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
};
if_trace_stream _ts(m, log);
}
else {
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(~p_ge_0, div_le_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(~p_le_0, div_ge_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
std::function<void(void)> log = [&,this]() {
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
};
if_trace_stream _ts(m, log);
}
}
else {
@ -1415,64 +1391,29 @@ public:
// q >= 0 or (p mod q) < -q
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
literal q_le_0 = mk_literal(a.mk_le(q, zero));
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(q_ge_0, eq);
mk_axiom(q_le_0, eq);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(q_ge_0, mod_ge_0);
mk_axiom(q_le_0, mod_ge_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero));
th.log_axiom_instantiation(body);
}
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero));
th.log_axiom_instantiation(body);
}
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(q_le_0, ~p_ge_0, div_ge_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(q_le_0, ~p_le_0, div_le_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(q_ge_0, ~p_le_0, div_ge_0);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
mk_axiom(q_ge_0, ~p_le_0, div_ge_0);
std::function<void(void)> log = [&,this]() {
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)));
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
};
if_trace_stream _ts(m, log);
}
if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
unsigned _k = k.get_unsigned();
@ -1495,10 +1436,10 @@ public:
}
void mk_axiom(literal l) {
ctx().mk_th_axiom(get_id(), false_literal, l);
if (ctx().relevancy()) {
ctx().mark_as_relevant(l);
}
ctx().mk_th_axiom(get_id(), false_literal, l);
}
void mk_axiom(literal l1, literal l2) {
@ -1509,7 +1450,7 @@ public:
ctx().mk_th_axiom(get_id(), l1, l2);
if (ctx().relevancy()) {
ctx().mark_as_relevant(l1);
ctx().add_rel_watch(~l1, ctx().bool_var2expr(l2.var()));
ctx().mark_as_relevant(l2);
}
}
@ -1517,8 +1458,8 @@ public:
ctx().mk_th_axiom(get_id(), l1, l2, l3);
if (ctx().relevancy()) {
ctx().mark_as_relevant(l1);
ctx().add_rel_watch(~l1, ctx().bool_var2expr(l2.var()));
ctx().add_rel_watch(~l2, ctx().bool_var2expr(l3.var()));
ctx().mark_as_relevant(l2);
ctx().mark_as_relevant(l3);
}
}
@ -1577,7 +1518,6 @@ public:
rational get_value(theory_var v) const {
if (v == null_theory_var || !lp().external_is_used(v)) {
TRACE("arith", tout << "Variable v" << v << " not internalized\n";);
return rational::zero();
}
@ -1586,7 +1526,6 @@ public:
return m_variable_values[vi];
if (!lp().is_term(vi)) {
TRACE("arith", tout << "not a term v" << v << "\n";);
return rational::zero();
}
@ -3812,7 +3751,7 @@ public:
lp().print_terms(out);
// the tableau
auto pp = lp ::core_solver_pretty_printer<lp::mpq, lp::impq>(
lp().m_mpq_lar_core_solver.m_r_solver, out);
lp().m_mpq_lar_core_solver.m_r_solver, out);
pp.print();
for (unsigned j = 0; j < lp().number_of_vars(); j++) {
lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);