Skip to content

Commit

Permalink
fix #3183 - change relevancy propagation to ensure that div/mod axiom…
Browse files Browse the repository at this point in the history 
…s are picked up

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner @levnach
NikolajBjorner authored and levnach committed Mar 24, 2020
1 parent 3b60146 commit d456402
Show file tree
Hide file tree
Showing 3 changed files with 58 additions and 103 deletions.
4 changes: 3 additions & 1 deletion src/smt/smt_theory.cpp
View file
Expand Up @@ -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) {
Expand All @@ -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) {
Expand Down
14 changes: 14 additions & 0 deletions src/smt/smt_theory.h
View file
Expand Up @@ -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:
/**
Expand Down Expand Up @@ -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.
Expand Down
143 changes: 41 additions & 102 deletions src/smt/theory_lra.cpp
View file
Expand Up @@ -1340,59 +1340,35 @@ class theory_lra::imp {

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 {
Expand All @@ -1404,64 +1380,29 @@ class theory_lra::imp {
// 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();
Expand All @@ -1484,10 +1425,10 @@ class theory_lra::imp {
}

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) {
Expand All @@ -1498,16 +1439,16 @@ class theory_lra::imp {
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);
}
}

void mk_axiom(literal l1, literal l2, literal l3) {
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);
}
}

Expand Down Expand Up @@ -1566,7 +1507,6 @@ class theory_lra::imp {

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();
}

Expand All @@ -1575,7 +1515,6 @@ class theory_lra::imp {
return m_variable_values[vi];

if (!lp().is_term(vi)) {
TRACE("arith", tout << "not a term v" << v << "\n";);
return rational::zero();
}

Expand Down Expand Up @@ -3801,7 +3740,7 @@ class theory_lra::imp {
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);
Expand Down

0 comments on commit d456402

Please sign in to comment.