diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp index 068f401a0..91863f0f7 100644 --- a/src/smt/smt_arith_value.cpp +++ b/src/smt/smt_arith_value.cpp @@ -163,4 +163,10 @@ namespace smt { return th->final_check_eh(); } + lbool arith_value::check_lp_feasible(vector>& ineqs, literal_vector& lit_core, + enode_pair_vector& eq_core) { + if (!m_thr) + return l_undef; + return m_thr->check_lp_feasible(ineqs, lit_core, eq_core); + } }; diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h index d802dcb18..536014460 100644 --- a/src/smt/smt_arith_value.h +++ b/src/smt/smt_arith_value.h @@ -48,5 +48,7 @@ namespace smt { expr_ref get_up(expr* e) const; expr_ref get_fixed(expr* e) const; final_check_status final_check(); + lbool check_lp_feasible(vector> &ineqs, literal_vector &lit_core, + enode_pair_vector &eq_core); }; }; diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp index 843d6251c..c91dfd587 100644 --- a/src/smt/theory_finite_set_size.cpp +++ b/src/smt/theory_finite_set_size.cpp @@ -285,11 +285,28 @@ namespace smt { * Associate tracking literal C_i with current assignment. * Assume C_i * Assert !C_0, .. , !C_{i-1}, C_i => /\_i |s_i| = sum_j n_ij and /\ n_j >= 0 - * Incremental algorithm with blocking clauses (sketch) - * If /\_i |s_i| = sum_j n_ij and /\ n_j >= 0 is unsat - * Then, instead of asserting sum constraint assert - * C_i <=> \/_j core_j - * where core_j come from covering of LRA conflict + * Incremental algorithm with blocking clauses + * Enumerate N assignments at a time. + * use smt_arith_value::check_lp_feasiable to check if current assignment is feasible. + * if it is, then yield the current assignment. Assume there is a filter that avoids future + * calls to find more models if the current model satisfies all cardinality terms. + * In other words, for every |s| the model produces a set with |s| elements, + * where |s| is the value assigned by the arithmetic solver. + * if it is not feasible, extract the infeasible core from call: + * - card_core: a set of cardinality atoms + * - lit_core: a set of literals asserted into the arithmetic solver + * - eq_core: a set of equations asserte into the arithmetic solver + * First take the card_core atoms and enumerate Boolean models for m_solver that + * satisfy the disjunction of those atoms. + * - Infeasibility of the current model meant that there was no linear assignment to + * the subset in card_core that satisfied lit_core & eq_core. So the query to extend the + * set of assignments is to fix this. + * If there is some model for the disjunction of card_core atoms, then + * add new slacks for the models an continue, possibly querying the arithmetic solver if the new set of + * linear relaxation to the subset is feasible. + * If there is no model to the disjunction of card_core atoms, then + * it means that size_core & lit_core & eq_core is unsat. + * where size_core is the unsat core for m_solver. */ lbool theory_finite_set_size::run_solver() { expr_ref_vector asms(m); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9af1c492f..50e2860e4 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1624,6 +1624,61 @@ public: return FC_DONE; return FC_GIVEUP; } + + /** + * Check if a set of equalities are lp feasible. + * push local scope + * internalize ineqs + * assert ineq constraints + * check lp feasibility + * extract core + * pop local scope + * return verdict + */ + + lbool check_lp_feasible(vector> &ineqs, literal_vector& lit_core, enode_pair_vector& eq_core) { + lbool st = l_undef; + push_scope_eh(); // pushes an arithmetic scope + u_map ci2index; + unsigned index = 0; + for (auto &[in_core, f] : ineqs) { + expr *x, *y; + rational r; + in_core = false; + if (m.is_eq(f, x, y) && a.is_numeral(y, r)) { + internalize_term(to_app(x)); + auto j = get_lpvar(th.get_th_var(x)); + auto ci = lp().add_var_bound(j, lp::EQ, r); + ci2index.insert(ci, index); + lp().activate(ci); + if (is_infeasible()) { + st = l_false; + break; + } + } + else { + NOT_IMPLEMENTED_YET(); + } + ++index; + } + if (st != l_false) { + st = make_feasible(); + SASSERT(st != l_false || is_infeasible()); + } + if (st == l_false) { + m_explanation.clear(); + lp().get_infeasibility_explanation(m_explanation); + for (auto ev : m_explanation) { + unsigned index; + if (ci2index.find(ev.ci(), index)) + ineqs[index].first = true; + else + set_evidence(ev.ci(), lit_core, eq_core); + } + } + pop_scope_eh(1); + return st; + } final_check_status final_check_eh() { if (propagate_core()) @@ -4369,6 +4424,10 @@ void theory_lra::validate_model(proto_model& mdl) { m_imp->validate_model(mdl); } +lbool theory_lra::check_lp_feasible(vector>& ineqs, literal_vector& lit_core, enode_pair_vector& eq_core) { + return m_imp->check_lp_feasible(ineqs, lit_core, eq_core); +} + } template class lp::lp_bound_propagator; template void lp::lar_solver::propagate_bounds_for_touched_rows(lp::lp_bound_propagator&); diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index 64d200506..3712fb78b 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -95,6 +95,11 @@ namespace smt { bool get_upper(enode* n, rational& r, bool& is_strict); void solve_for(vector& s) override; + // check if supplied set of linear constraints are LP feasible within current backtracking context + // identify core by setting Boolean flags to true for constraints used in the proof of infeasibility + // and return l_false if infeasible. + lbool check_lp_feasible(vector> &ineqs, literal_vector& lit_core, enode_pair_vector& eq_core); + void updt_params() override; void display(std::ostream & out) const override;