From 9b609af8fc5e582280e0a8791b1c565239d21d3c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Apr 2020 16:19:54 -0700 Subject: [PATCH] fix #3924 Signed-off-by: Nikolaj Bjorner --- src/math/lp/lar_solver.cpp | 1 - src/math/lp/lp_types.h | 2 ++ src/sat/sat_config.cpp | 2 +- src/smt/theory_dense_diff_logic_def.h | 9 ++++++--- src/smt/theory_lra.cpp | 23 ++++++++++------------- 5 files changed, 19 insertions(+), 18 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 0d76ddf83..ee08ac88e 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -194,7 +194,6 @@ void lar_solver::calculate_implied_bounds_for_row(unsigned i, lp_bound_propagato unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const { if (!tv::is_term(j)) { unsigned ext_var_or_term = m_var_register.local_to_external(j); - TRACE("arith", tout << j << " " << ext_var_or_term << "\n";); j = !tv::is_term(ext_var_or_term) ? j : ext_var_or_term; } return j; diff --git a/src/math/lp/lp_types.h b/src/math/lp/lp_types.h index 41aeaa9cf..2cde01ec0 100644 --- a/src/math/lp/lp_types.h +++ b/src/math/lp/lp_types.h @@ -70,6 +70,8 @@ public: return strm.str(); } + bool is_null() const { return m_index == UINT_MAX; } + }; class column_index { diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 3b3bc43bf..258ab6850 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -244,7 +244,7 @@ namespace sat { throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected"); m_card_solver = p.cardinality_solver(); - m_xor_solver = p.xor_solver(); + m_xor_solver = false && p.xor_solver(); // hide this option until thoroughly tested sat_simplifier_params sp(_p); m_elim_vars = sp.elim_vars(); diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 678e87116..6b86e718c 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -210,7 +210,7 @@ namespace smt { } template - bool theory_dense_diff_logic::internalize_term(app * term) { + bool theory_dense_diff_logic::internalize_term(app * term) { if (memory::above_high_watermark()) { found_non_diff_logic_expr(term); // little hack... TODO: change to no_memory and return l_undef if SAT return false; @@ -225,6 +225,7 @@ namespace smt { template void theory_dense_diff_logic::internalize_eq_eh(app * atom, bool_var v) { + TRACE("ddl", tout << "eq-eh: " << mk_pp(atom, get_manager()) << "\n";); if (memory::above_high_watermark()) return; context & ctx = get_context(); @@ -243,8 +244,10 @@ namespace smt { enode * n1 = ctx.get_enode(lhs); enode * n2 = ctx.get_enode(rhs); if (n1->get_th_var(get_id()) != null_theory_var && - n2->get_th_var(get_id()) != null_theory_var) - m_arith_eq_adapter.mk_axioms(n1, n2); + n2->get_th_var(get_id()) != null_theory_var) { + m_arith_eq_adapter.mk_axioms(n1, n2); + return; + } } } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 30a365694..4e81115b5 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -789,10 +789,6 @@ class theory_lra::imp { return v; } - bool theory_var_is_registered_in_lar_solver(theory_var v) const { - return lp().external_is_used(v); - } - bool const has_int() const { return lp().has_int_var(); } lpvar register_theory_var_in_lar_solver(theory_var v) { @@ -957,9 +953,7 @@ class theory_lra::imp { theory_var internalize_linearized_def(app* term, scoped_internalize_state& st) { theory_var v = mk_var(term); - TRACE("arith", - tout << mk_bounded_pp(term, m) << " v" << v << "\n"; - tout << st.offset() << " " << st.coeffs().size() << " " << st.coeffs()[0] << "\n";); + TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << "\n";); if (is_unit_var(st) && v == st.vars()[0]) { return st.vars()[0]; @@ -1510,6 +1504,12 @@ public: return can_get_bound(v); } + void ensure_column(theory_var v) { + if (!lp().external_is_used(v)) { + register_theory_var_in_lar_solver(v); + } + } + mutable vector> m_todo_terms; lp::impq get_ivalue(theory_var v) const { @@ -1596,16 +1596,13 @@ public: svector vars; theory_var sz = static_cast(th.get_num_vars()); for (theory_var v = 0; v < sz; ++v) { - if (!can_get_ivalue(v)) { - continue; - } enode * n1 = get_enode(v); if (!th.is_relevant_and_shared(n1)) { continue; } + ensure_column(v); lp::column_index vj = lp().to_column_index(v); - if (vj.is_null()) - continue; + SASSERT(!vj.is_null()); theory_var other = m_model_eqs.insert_if_not_there(v); if (other == v) { continue; @@ -3830,7 +3827,7 @@ public: auto t = get_tv(v); if (!ctx().is_relevant(get_enode(v))) out << "irr: "; out << "v" << v << " "; - out << (t.is_term() ? "t":"j") << t.id(); + if (t.is_null()) out << "null"; else out << (t.is_term() ? "t":"j") << t.id(); if (can_get_value(v)) out << " = " << get_value(v); if (is_int(v)) out << ", int"; if (ctx().is_shared(get_enode(v))) out << ", shared";