mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-18 02:08:31 +00:00
Code Activity

add sketch for incremental algorithm

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-30 02:53:13 -07:00
parent 450412c854
commit ba28e85f04
5 changed files with 94 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_arith_value.cpp
View file

@ -163,4 +163,10 @@ namespace smt {
return th->final_check_eh();
}
lbool arith_value::check_lp_feasible(vector<std::pair<bool, expr_ref>>& 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);
}
};

2
src/smt/smt_arith_value.h
View file

@ -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<std::pair<bool, expr_ref>> &ineqs, literal_vector &lit_core,
enode_pair_vector &eq_core);
};
};

27
src/smt/theory_finite_set_size.cpp
View file

@ -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);

59
src/smt/theory_lra.cpp
View file

@ -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<std::pair<bool, expr_ref>> &ineqs, literal_vector& lit_core, enode_pair_vector& eq_core) {
lbool st = l_undef;
push_scope_eh(); // pushes an arithmetic scope
u_map<unsigned> 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<std::pair<bool, expr_ref>>& 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<smt::theory_lra::imp>;
template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);

5
src/smt/theory_lra.h
View file

@ -95,6 +95,11 @@ namespace smt {
bool get_upper(enode* n, rational& r, bool& is_strict);
void solve_for(vector<solution>& 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<std::pair<bool, expr_ref>> &ineqs, literal_vector& lit_core, enode_pair_vector& eq_core);
void updt_params() override;
void display(std::ostream & out) const override;