From 9ecae4abad81ce2a222c18262f6e1683850a09b1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 10 Dec 2019 09:51:19 -1000 Subject: [PATCH] revert changes in smt directory Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 4 ++-- src/smt/smt_context.cpp | 4 +--- src/smt/smt_context.h | 1 - src/smt/smt_internalizer.cpp | 4 +--- src/smt/theory_lra.cpp | 30 ++++++++++-------------------- 5 files changed, 14 insertions(+), 29 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index dc5b97e93..d4c075b96 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -159,8 +159,8 @@ rational core::product_value(const unsigned_vector & m) const { } // return true iff the monic value is equal to the product of the values of the factors -bool core::check_monic(const monic& m) const { - SASSERT(m_lar_solver.get_column_value(m.var()).is_int()); +bool core::check_monic(const monic& m) const { + SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()); return product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var()); } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 3401df479..f9a6e59f0 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -75,7 +75,6 @@ namespace smt { m_phase_default(false), m_conflict(null_b_justification), m_not_l(null_literal), - m_empty_clause(false), m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)), m_unsat_proof(m), m_dyn_ack_manager(*this, p), @@ -2397,10 +2396,9 @@ namespace smt { m_unsat_proof = nullptr; } m_base_scopes.shrink(new_lvl); - m_empty_clause = false; } else { - m_conflict = m_empty_clause ? b_justification::mk_axiom() : null_b_justification; + m_conflict = null_b_justification; m_not_l = null_literal; } del_clauses(m_aux_clauses, s.m_aux_clauses_lim); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index ace0eaed0..0b78bc887 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -193,7 +193,6 @@ namespace smt { // levels survives to the base level. b_justification m_conflict; literal m_not_l; - bool m_empty_clause; scoped_ptr m_conflict_resolution; proof_ref m_unsat_proof; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 56eecbd15..efca6c042 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1346,15 +1346,13 @@ namespace smt { bool lemma = is_lemma(k); m_stats.m_num_mk_lits += num_lits; switch (num_lits) { - case 0: { + case 0: if (j && !j->in_region()) m_justifications.push_back(j); TRACE("mk_clause", tout << "empty clause... setting conflict\n";); set_conflict(j == nullptr ? b_justification::mk_axiom() : b_justification(j)); - m_empty_clause = true; SASSERT(inconsistent()); return nullptr; - } case 1: if (j && !j->in_region()) m_justifications.push_back(j); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 43fb7f67b..724e6da01 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -165,7 +165,6 @@ class theory_lra::imp { ast_manager& m; theory_arith_params& m_arith_params; arith_util a; - unsigned m_final_check_idx; arith_eq_adapter m_arith_eq_adapter; vector m_columns; @@ -943,8 +942,7 @@ public: imp(theory_lra& th, ast_manager& m, theory_arith_params& ap): th(th), m(m), m_arith_params(ap), - a(m), - m_final_check_idx(0), + a(m), m_arith_eq_adapter(th, ap, a), m_internalize_head(0), m_one_var(UINT_MAX), @@ -999,7 +997,7 @@ public: return true; } else { - TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";); + TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";); found_not_handled(atom); return true; } @@ -1653,16 +1651,13 @@ public: if (lp().get_status() != lp::lp_status::OPTIMAL) { is_sat = make_feasible(); } - final_check_status st = FC_DONE; - unsigned old_idx = m_final_check_idx; switch (is_sat) { case l_true: if (delayed_assume_eqs()) { return FC_CONTINUE; } - TRACE("arith", display(tout);); switch (check_lia()) { @@ -1686,7 +1681,7 @@ public: st = FC_GIVEUP; break; } - if (assume_eqs()) { + if (assume_eqs()) { return FC_CONTINUE; } if (m_not_handled != nullptr) { @@ -1696,7 +1691,7 @@ public: return st; case l_false: - set_conflict(); + get_infeasibility_explanation_and_set_conflict(); return FC_CONTINUE; case l_undef: TRACE("arith", tout << "check feasiable is undef\n";); @@ -1705,7 +1700,6 @@ public: UNREACHABLE(); break; } - TRACE("arith", tout << "default giveup\n";); return FC_GIVEUP; } @@ -2177,7 +2171,7 @@ public: for(const nla::lemma & l : lv) { m_lemma = l; //todo avoid the copy m_explanation = l.expl(); - m_stats.m_nla_explanations += static_cast(l.expl().size()); + m_stats.m_nla_explanations += l.expl().size(); false_case_of_check_nla(); } break; @@ -2776,14 +2770,10 @@ public: bool sign = ub->get_bound_kind() != lp_api::upper_t; lit2 = literal(ub->get_bv(), sign); } - if (ctx().get_assignment(lit2) == l_true) { - return; - } TRACE("arith", ctx().display_literal_verbose(tout, lit1); - ctx().display_literal_verbose(tout << " => ", lit2) << "\n"; - tout << ctx().get_assignment(lit2) << " " << ctx().get_assignment(lit1) << "\n"; - ); + ctx().display_literal_verbose(tout << " => ", lit2); + tout << "\n";); updt_unassigned_bounds(v, -1); ++m_stats.m_bound_propagations2; m_params.reset(); @@ -2983,15 +2973,15 @@ public: auto vi = register_theory_var_in_lar_solver(b.get_var()); rational bound = b.get_value(); lp::constraint_index ci; - TRACE("arith", tout << "v" << b.get_var() << ", vi = " << vi << "\n";); + TRACE("arith", tout << "v" << b.get_var() << ", vi = " << vi;); if (is_int && !is_true) { rational bound = b.get_value(false).get_rational(); ci = m_solver->add_var_bound(vi, k, bound); - TRACE("arith", tout << "bound = " << bound << ", ci = " << ci << "\n";); + TRACE("arith", tout << "\bbound = " << bound << ", ci = " << ci << "\n";); } else { ci = m_solver->add_var_bound(vi, k, b.get_value()); - TRACE("arith", tout << "bound = " << bound << ", ci = " << ci << "\n";); + TRACE("arith", tout << "\nbound = " << bound << ", ci = " << ci << "\n";); } add_ineq_constraint(ci, literal(bv, !is_true)); if (is_infeasible()) {