From ca5666cabdda8b90581add3dbaad7c170c12c2fc Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 6 Nov 2018 11:04:49 -0800 Subject: [PATCH] add diagnostics for registering vars in lar_solver Signed-off-by: Lev --- src/smt/theory_lra.cpp | 45 ++++++++++++++++++++++++++++---------- src/util/lp/lar_solver.cpp | 4 ++++ src/util/lp/lar_solver.h | 2 ++ 3 files changed, 40 insertions(+), 11 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 30ded0549..2910eade3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -630,12 +630,13 @@ class theory_lra::imp { if (!ctx().e_internalized(n)) { ctx().internalize(n, false); } - vars.push_back(get_var_index(mk_var(n))); + vars.push_back(register_theory_var_in_lar_solver(mk_var(n))); } } - TRACE("arith", tout << "v" << v << "(" << get_var_index(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";); + SASSERT(theory_var_is_registered_in_lar_solver(v)); + TRACE("arith", tout << "v" << v << "(" << register_theory_var_in_lar_solver(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";); if (!_has_var) { - m_switcher.add_monomial(get_var_index(v), vars.size(), vars.c_ptr()); + m_switcher.add_monomial(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr()); } } @@ -713,8 +714,12 @@ class theory_lra::imp { SASSERT(null_theory_var != v); return v; } - - lp::var_index get_var_index(theory_var v) { + + bool theory_var_is_registered_in_lar_solver(theory_var v) const { + return m_solver->external_is_used(v); + } + + lp::var_index register_theory_var_in_lar_solver(theory_var v) { lp::var_index result = UINT_MAX; if (m_theory_var2var_index.size() > static_cast(v)) { result = m_theory_var2var_index[v]; @@ -749,7 +754,7 @@ class theory_lra::imp { theory_var var = vars[i]; rational const& r = m_columns[var]; if (!r.is_zero()) { - m_left_side.push_back(std::make_pair(r, get_var_index(var))); + m_left_side.push_back(std::make_pair(r, register_theory_var_in_lar_solver(var))); m_columns[var].reset(); } } @@ -798,7 +803,7 @@ class theory_lra::imp { st.coeffs().push_back(rational::one()); st.coeffs().push_back(rational::minus_one()); theory_var z = internalize_linearized_def(term, st); - lp::var_index vi = get_var_index(z); + lp::var_index vi = register_theory_var_in_lar_solver(z); add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero())); add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero())); TRACE("arith", @@ -1205,6 +1210,24 @@ public: if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } + // create axiom for + // u = v + r*w, + /// 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()))); + theory_var z = internalize_def(term); + lp::var_index vi = register_theory_var_in_lar_solver(z); + add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero())); + add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero())); + add_def_constraint(m_solver->add_var_bound(register_theory_var_in_lar_solver(v), lp::GE, rational::zero())); + add_def_constraint(m_solver->add_var_bound(register_theory_var_in_lar_solver(v), lp::LT, abs(r))); + TRACE("arith", m_solver->print_constraints(tout << term << "\n");); + } + void mk_idiv_mod_axioms(expr * p, expr * q) { if (a.is_zero(q)) { return; @@ -2755,7 +2778,7 @@ public: void add_use_lists(lp_api::bound* b) { theory_var v = b->get_var(); - lp::var_index vi = get_var_index(v); + lp::var_index vi = register_theory_var_in_lar_solver(v); if (!m_solver->is_term(vi)) { return; } @@ -2936,7 +2959,7 @@ public: else { ++m_stats.m_assert_upper; } - auto vi = get_var_index(b.get_var()); + auto vi = register_theory_var_in_lar_solver(b.get_var()); rational bound = b.get_value(); lp::constraint_index ci; if (is_int && !is_true) { @@ -3090,8 +3113,8 @@ public: value_sort_pair key(bound, is_int(v1)); if (m_fixed_var_table.find(key, v2)) { if (static_cast(v2) < th.get_num_vars() && !is_equal(v1, v2)) { - auto vi1 = get_var_index(v1); - auto vi2 = get_var_index(v2); + auto vi1 = register_theory_var_in_lar_solver(v1); + auto vi2 = register_theory_var_in_lar_solver(v2); lp::constraint_index ci1, ci2, ci3, ci4; TRACE("arith", tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << has_lower_bound(vi2, ci3, bound) << "\n";); if (has_lower_bound(vi2, ci3, bound) && has_upper_bound(vi2, ci4, bound)) { diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 5ddd4d8e6..401c17450 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1614,6 +1614,10 @@ void lar_solver::register_new_ext_var_index(unsigned ext_v, bool is_int) { m_var_register.add_var(ext_v, is_int); } +bool lar_solver::external_is_used(unsigned v) const { + return m_var_register.external_is_used(v); +} + void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) { register_new_ext_var_index(ext_j, is_int); m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 6000d414c..2ac1ddf5d 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -163,6 +163,8 @@ public: void register_new_ext_var_index(unsigned ext_v, bool is_int); + bool external_is_used(unsigned) const; + bool term_is_int(const lar_term * t) const; bool var_is_int(var_index v) const;