From f6cbe3a016c1ce016a0db4272864ca9a3d67ceba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 30 Jul 2020 10:22:04 -0700
Subject: [PATCH] propagate on variables
---
src/smt/theory_lra.cpp | 90 +++++++++++++++---------------------------
1 file changed, 31 insertions(+), 59 deletions(-)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index cd8abd346..c410a0604 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -564,6 +564,9 @@ class theory_lra::imp {
if (is_app(n)) {
internalize_args(to_app(n));
}
+ if (m.is_ite(n)) {
+ if (!ctx().relevancy()) mk_ite_axiom(n);
+ }
theory_var v = mk_var(n);
coeffs[vars.size()] = coeffs[index];
vars.push_back(v);
@@ -1109,7 +1112,7 @@ public:
if (vi == lp::null_lpvar) {
return l_undef;
}
- return m_solver->compare_values(vi, k, b->get_value()) ? l_true : l_false;
+ return lp().compare_values(vi, k, b->get_value()) ? l_true : l_false;
}
void new_eq_eh(theory_var v1, theory_var v2) {
@@ -1193,6 +1196,8 @@ public:
mk_to_int_axiom(n);
else if (a.is_is_int(n))
mk_is_int_axiom(n);
+ else if (m.is_ite(n))
+ mk_ite_axiom(n);
}
// n < 0 || rem(a, n) = mod(a, n)
@@ -1252,6 +1257,16 @@ public:
}
}
+ void mk_ite_axiom(expr* n) {
+ return;
+ expr* c = nullptr, *t = nullptr, *e = nullptr;
+ VERIFY(m.is_ite(n, c, t, e));
+ literal e1 = th.mk_eq(n, t, false);
+ literal e2 = th.mk_eq(n, e, false);
+ scoped_trace_stream sts(th, e1, e2);
+ mk_axiom(e1, e2);
+ }
+
// is_int(x) <=> to_real(to_int(x)) = x
void mk_is_int_axiom(app* n) {
expr* x = nullptr;
@@ -1273,10 +1288,9 @@ public:
/// abs(r) > r >= 0
void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r) {
app_ref term(m);
- term = a.mk_sub(get_enode(u)->get_owner(),
- a.mk_add(get_enode(v)->get_owner(),
- a.mk_mul(a.mk_numeral(r, true),
- get_enode(w)->get_owner())));
+ term = a.mk_mul(a.mk_numeral(r, true), get_enode(w)->get_owner());
+ term = a.mk_add(get_enode(v)->get_owner(), term);
+ term = a.mk_sub(get_enode(u)->get_owner(), term);
theory_var z = internalize_def(term);
lpvar zi = register_theory_var_in_lar_solver(z);
lpvar vi = register_theory_var_in_lar_solver(v);
@@ -1353,37 +1367,6 @@ public:
};
if_trace_stream _ts(m, log);
}
-
-#if 0
- // creates more literals than useful.
- literal div_ge_0 = mk_literal(a.mk_ge(div, zero));
- literal div_le_0 = mk_literal(a.mk_le(div, zero));
- literal p_ge_0 = mk_literal(a.mk_ge(p, zero));
- literal p_le_0 = mk_literal(a.mk_le(p, zero));
-
- if (k.is_pos()) {
- mk_axiom(~p_ge_0, div_ge_0);
- mk_axiom(~p_le_0, div_le_0);
- mk_axiom(p_ge_0, ~div_ge_0);
- mk_axiom(p_le_0, ~div_le_0);
- 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 {
- mk_axiom(~p_ge_0, div_le_0);
- mk_axiom(~p_le_0, div_ge_0);
- mk_axiom(p_ge_0, ~div_le_0);
- mk_axiom(p_le_0, ~div_ge_0);
- 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);
- }
-#endif
}
else {
@@ -1717,7 +1700,7 @@ public:
final_check_status final_check_eh() {
reset_variable_values();
- IF_VERBOSE(12, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
+ IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
lbool is_sat = l_true;
SASSERT(lp().ax_is_correct());
if (lp().get_status() != lp::lp_status::OPTIMAL) {
@@ -2326,22 +2309,6 @@ public:
// }
// }
- bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) {
- theory_var v = lp().local_to_external(vi);
- if (v == null_theory_var) {
- return false;
- }
- if (m_bounds.size() <= static_cast<unsigned>(v) || m_unassigned_bounds[v] == 0) {
- return false;
- }
- for (lp_api::bound* b : m_bounds[v]) {
- if (ctx().get_assignment(b->get_bv()) == l_undef &&
- null_literal != is_bound_implied(kind, bval, *b)) {
- return true;
- }
- }
- return false;
- }
void consume(rational const& v, lp::constraint_index j) {
set_evidence(j, m_core, m_eqs);
@@ -2795,7 +2762,7 @@ public:
literal lit1(bv, !is_true);
literal lit2 = null_literal;
bool find_glb = (is_true == (k == lp_api::lower_t));
- TRACE("arith", tout << "find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
+ TRACE("arith", tout << "v" << v << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
if (find_glb) {
rational glb;
lp_api::bound* lb = nullptr;
@@ -2968,7 +2935,7 @@ public:
theory_var v = b.get_var();
auto ti = get_tv(v);
SASSERT(ti.is_term());
- lp::lar_term const& term = m_solver->get_term(ti);
+ lp::lar_term const& term = lp().get_term(ti);
for (auto const mono : term) {
auto wi = lp().column2tv(mono.column());
lp::constraint_index ci;
@@ -3013,8 +2980,9 @@ public:
}
void assert_bound(bool_var bv, bool is_true, lp_api::bound& b) {
+ TRACE("arith", tout << b << "\n";);
lp::constraint_index ci = b.get_constraint(is_true);
- m_solver->activate(ci);
+ lp().activate(ci);
if (is_infeasible()) {
return;
}
@@ -3029,6 +2997,10 @@ public:
if (propagate_eqs() && value.is_rational()) {
propagate_eqs(b.tv(), ci, k, b, value.get_rational());
}
+#if 0
+ if (propagation_mode() != BP_NONE)
+ lp().mark_rows_for_bound_prop(b.tv().id());
+#endif
}
lp_api::bound* mk_var_bound(bool_var bv, theory_var v, lp_api::bound_kind bk, rational const& bound) {
@@ -3043,13 +3015,13 @@ public:
lp::lconstraint_kind kT = bound2constraint_kind(v_is_int, bk, true);
lp::lconstraint_kind kF = bound2constraint_kind(v_is_int, bk, false);
- cT = m_solver->mk_var_bound(vi, kT, bound);
+ cT = lp().mk_var_bound(vi, kT, bound);
if (v_is_int) {
rational boundF = (bk == lp_api::lower_t) ? bound - 1 : bound + 1;
- cF = m_solver->mk_var_bound(vi, kF, boundF);
+ cF = lp().mk_var_bound(vi, kF, boundF);
}
else {
- cF = m_solver->mk_var_bound(vi, kF, bound);
+ cF = lp().mk_var_bound(vi, kF, bound);
}
add_ineq_constraint(cT, literal(bv, false));
add_ineq_constraint(cF, literal(bv, true));