diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 70e0a0a28..c6cf24048 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -72,7 +72,7 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) { template bool horner::lemmas_on_row(const T& row) { cross_nested cn( - [this](const nex* n) { return m_intervals->check_cross_nested_expr(n, m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals->dep_manager()) : nullptr); }, + [this](const nex* n) { return m_intervals->check_nex(n, m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals->dep_manager()) : nullptr); }, [this](unsigned j) { return c().var_is_fixed(j); }, [this]() { return c().random(); }, m_nex_creator); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 610077f11..d201ed949 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -453,7 +453,7 @@ void nla_grobner::process_simplified_target(equation* target, ptr_buffercheck_cross_nested_expr(target->expr(), target->dep())) { + if(m_intervals->check_nex(target->expr(), target->dep())) { TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n"; tout << "vars = \n"; for (lpvar j : get_vars_of_expr(target->expr())) { diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index acce58f65..16e610918 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -244,19 +244,19 @@ intervals::interv intervals::interval_of_mul(const nex_mul* e) { return a; } - -bool intervals::check_cross_nested_expr(const nex* n, ci_dependency* initial_deps) { - TRACE("nla_intervals", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";); +// return true iff the interval of n is does not contain 0 +bool intervals::check_nex(const nex* n, ci_dependency* initial_deps) { + TRACE("nla_grobner", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";); m_core->lp_settings().stats().m_cross_nested_forms++; auto i = interval_of_expr(n, 1); - TRACE("nla_intervals", tout << "callback n = " << *n << "\ni="; display(tout, i) << "\n";); + TRACE("nla_grobner", tout << "callback n = " << *n << "\ni="; display(tout, i) << "\n";); if (!separated_from_zero(i)) { reset(); return false; } auto interv_wd = interval_of_expr_with_deps(n, 1); - TRACE("nla_intervals", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n";); + TRACE("nla_grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n";); check_interval_for_conflict_on_zero(interv_wd, initial_deps); reset(); // clean the memory allocated by the interval bound dependencies return true; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index c9e1d1d01..0e3325a69 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -452,7 +452,7 @@ public: return false; } void reset() { m_alloc.reset(); } - bool check_cross_nested_expr(const nex*, ci_dependency*); + bool check_nex(const nex*, ci_dependency*); interval interval_of_expr_with_deps(const nex* e, unsigned power); interval interval_of_expr(const nex* e, unsigned power); interval interval_of_sum(const nex_sum*); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f9a6e59f0..3401df479 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -75,6 +75,7 @@ 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), @@ -2396,9 +2397,10 @@ namespace smt { m_unsat_proof = nullptr; } m_base_scopes.shrink(new_lvl); + m_empty_clause = false; } else { - m_conflict = null_b_justification; + m_conflict = m_empty_clause ? b_justification::mk_axiom() : 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 0b78bc887..ace0eaed0 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -193,6 +193,7 @@ 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/theory_lra.cpp b/src/smt/theory_lra.cpp index 94801b099..43fb7f67b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -165,6 +165,7 @@ 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; @@ -942,7 +943,8 @@ public: imp(theory_lra& th, ast_manager& m, theory_arith_params& ap): th(th), m(m), m_arith_params(ap), - a(m), + a(m), + m_final_check_idx(0), m_arith_eq_adapter(th, ap, a), m_internalize_head(0), m_one_var(UINT_MAX), @@ -997,7 +999,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; } @@ -1651,13 +1653,16 @@ 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()) { @@ -1681,18 +1686,17 @@ public: st = FC_GIVEUP; break; } + if (assume_eqs()) { + return FC_CONTINUE; + } if (m_not_handled != nullptr) { TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";); st = FC_GIVEUP; } - - if (assume_eqs()) { - return FC_CONTINUE; - } return st; case l_false: - get_infeasibility_explanation_and_set_conflict(); + set_conflict(); return FC_CONTINUE; case l_undef: TRACE("arith", tout << "check feasiable is undef\n";); @@ -1701,6 +1705,7 @@ public: UNREACHABLE(); break; } + TRACE("arith", tout << "default giveup\n";); return FC_GIVEUP; } @@ -2172,7 +2177,7 @@ public: for(const nla::lemma & l : lv) { m_lemma = l; //todo avoid the copy m_explanation = l.expl(); - m_stats.m_nla_explanations += l.expl().size(); + m_stats.m_nla_explanations += static_cast(l.expl().size()); false_case_of_check_nla(); } break; @@ -2771,10 +2776,14 @@ 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); - tout << "\n";); + ctx().display_literal_verbose(tout << " => ", lit2) << "\n"; + tout << ctx().get_assignment(lit2) << " " << ctx().get_assignment(lit1) << "\n"; + ); updt_unassigned_bounds(v, -1); ++m_stats.m_bound_propagations2; m_params.reset(); @@ -2974,15 +2983,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;); + TRACE("arith", tout << "v" << b.get_var() << ", vi = " << vi << "\n";); 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 << "\bbound = " << bound << ", ci = " << ci << "\n";); + TRACE("arith", tout << "bound = " << bound << ", ci = " << ci << "\n";); } else { ci = m_solver->add_var_bound(vi, k, b.get_value()); - TRACE("arith", tout << "\nbound = " << bound << ", ci = " << ci << "\n";); + TRACE("arith", tout << "bound = " << bound << ", ci = " << ci << "\n";); } add_ineq_constraint(ci, literal(bv, !is_true)); if (is_infeasible()) {