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

simplify a few of the several axiom trace commands

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-07-26 18:02:16 -07:00
parent c7704ef9af
commit ae502bc2c4
2 changed files with 29 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_theory.h
View file

@ -126,6 +126,15 @@ namespace smt {
} }
} }
scoped_trace_stream(theory& th, literal lit1, literal lit2): m(th.get_manager()) {
if (m.has_trace_stream()) {
literal_vector lits;
lits.push_back(lit1);
lits.push_back(lit2);
th.log_axiom_instantiation(lits);
}
}
scoped_trace_stream(theory& th, std::function<literal(void)>& fn): m(th.get_manager()) { scoped_trace_stream(theory& th, std::function<literal(void)>& fn): m(th.get_manager()) {
if (m.has_trace_stream()) { if (m.has_trace_stream()) {
literal_vector ls; literal_vector ls;

49
src/smt/theory_lra.cpp
View file

@ -1206,14 +1206,14 @@ public:
literal dgez = mk_literal(degz_expr); literal dgez = mk_literal(degz_expr);
literal pos = th.mk_eq(rem, mod, false); literal pos = th.mk_eq(rem, mod, false);
literal neg = th.mk_eq(rem, mmod, false); literal neg = th.mk_eq(rem, mmod, false);
if (m.has_trace_stream()) { {
app_ref body(m); scoped_trace_stream ts(th, ~dgez, pos);
body = m.mk_ite(degz_expr, ctx().bool_var2expr(pos.var()), ctx().bool_var2expr(neg.var())); mk_axiom(~dgez, pos);
th.log_axiom_instantiation(body); }
{
scoped_trace_stream ts(th, dgez, neg);
mk_axiom( dgez, neg);
} }
mk_axiom(~dgez, pos);
mk_axiom( dgez, neg);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
} }
// q = 0 or q * (p div q) = p // q = 0 or q * (p div q) = p
@ -1221,13 +1221,8 @@ public:
if (a.is_zero(q)) return; if (a.is_zero(q)) return;
literal eqz = th.mk_eq(q, a.mk_real(0), false); literal eqz = th.mk_eq(q, a.mk_real(0), false);
literal eq = th.mk_eq(a.mk_mul(q, a.mk_div(p, q)), p, false); literal eq = th.mk_eq(a.mk_mul(q, a.mk_div(p, q)), p, false);
if (m.has_trace_stream()) { scoped_trace_stream ts(th, eqz, eq);
app_ref body(m);
body = m.mk_implies(m.mk_not(ctx().bool_var2expr(eqz.var())), ctx().bool_var2expr(eq.var()));
th.log_axiom_instantiation(body);
}
mk_axiom(eqz, eq); mk_axiom(eqz, eq);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
} }
// to_int (to_real x) = x // to_int (to_real x) = x
@ -1236,28 +1231,24 @@ public:
expr* x = nullptr, *y = nullptr; expr* x = nullptr, *y = nullptr;
VERIFY (a.is_to_int(n, x)); VERIFY (a.is_to_int(n, x));
if (a.is_to_real(x, y)) { if (a.is_to_real(x, y)) {
if (m.has_trace_stream()) { literal eq = th.mk_eq(y, n, false);
app_ref body(m); scoped_trace_stream ts(th, eq);
body = m.mk_eq(n, y); mk_axiom(eq);
th.log_axiom_instantiation(body);
}
mk_axiom(th.mk_eq(y, n, false));
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
} }
else { else {
expr_ref to_r(a.mk_to_real(n), m); expr_ref to_r(a.mk_to_real(n), m);
expr_ref lo(a.mk_le(a.mk_sub(to_r, x), a.mk_real(0)), m); expr_ref lo(a.mk_le(a.mk_sub(to_r, x), a.mk_real(0)), m);
expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m); expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m);
if (m.has_trace_stream()) th.log_axiom_instantiation(lo); literal llo = mk_literal(lo);
mk_axiom(mk_literal(lo)); literal lhi = mk_literal(hi);
if (m.has_trace_stream()) { {
m.trace_stream() << "[end-of-instance]\n"; scoped_trace_stream ts(th, llo);
expr_ref body(m); mk_axiom(llo);
body = m.mk_not(hi); }
th.log_axiom_instantiation(body); {
scoped_trace_stream ts(th, lhi);
mk_axiom(~lhi);
} }
mk_axiom(~mk_literal(hi));
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
} }
} }