mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 03:16:21 +00:00
Code Activity

nra_solver: visit COI constraints in order; stop at first falsified

Browse source 
Instead of evaluating every COI constraint to materialize the list of
falsified ones, decide the visit order up front so that the first
falsified constraint encountered is exactly the one we want:

* pick mode 0 (min substitution-expansion): structurally sort COI
  constraints by ascending expansion-size in the max variable
  (stable_sort, so ties keep insertion order). The first falsified
  found has the minimum expansion size among all falsified, without
  evaluating later constraints.

* pick mode 1 (random): Fisher-Yates shuffle the COI constraints.
  Restricted to the falsified subset, a uniform permutation yields a
  uniform first-element distribution, so the picked constraint is a
  uniformly random falsified one. Stops at the first falsified found.

The substituted-LRA evaluation is therefore performed only on the
prefix of the ordered list up to (and including) the picked constraint.
The sub_cache memoizes variable substitutions across that prefix.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-05-21 15:17:11 -07:00
parent ec72144c66
commit 7d78467af2
1 changed files with 40 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

70
src/math/lp/nra_solver.cpp
View file

@ -419,42 +419,52 @@ struct solver::imp {
statistics &st = m_nla_core.lp_settings().stats().m_st;
// Identify falsified COI constraints by evaluating each one at
// the LRA model after substituting monics and terms (this matches
// what mk_definition does when building NLSAT polynomials). We
// avoid materializing any NLSAT polynomial or clause for
// constraints that already hold.
u_map<rational> sub_cache;
svector<lp::constraint_index> falsified;
// Choose the falsified constraint to send to NLSAT according to
// arith.nl.nra_check_assignment_pick. In both modes we visit COI
// constraints in an order that lets us stop at the first
// falsified one rather than evaluating every constraint.
//
// 0 - sort COI constraints by ascending substitution-expansion
// size (a structural, model-independent measure that acts
// as a cheap LRA-side proxy for the lowest-degree-in-max-
// var heuristic of nlsat::solver::check(rvalues, clause)).
// The first falsified one we hit therefore has the minimum
// expansion size among all falsified candidates.
//
// 1 - Fisher-Yates shuffle the COI constraints and pick the
// first falsified one. Restricted to the falsified subset
// a uniform permutation induces a uniform first-element
// distribution, so the picked constraint is uniformly
// random among falsified.
svector<lp::constraint_index> coi_constraints;
for (auto ci : m_coi.constraints())
if (!lra_holds_substituted(ci, sub_cache))
falsified.push_back(ci);
coi_constraints.push_back(ci);
if (falsified.empty())
return l_undef;
// Pick the falsified constraint according to
// arith.nl.nra_check_assignment_pick:
// 0 - minimal substitution expansion (cheap LRA-side proxy
// for the lowest-degree-in-max-var heuristic that
// nlsat::solver::check(rvalues, clause) applies).
// 1 - uniformly random falsified constraint.
lp::constraint_index best = falsified[0];
unsigned pick_mode = m_nla_core.params().arith_nl_nra_check_assignment_pick();
if (pick_mode == 1) {
unsigned k = m_nla_core.random() % falsified.size();
best = falsified[k];
}
else {
unsigned best_score = constraint_expansion_size(best);
for (unsigned k = 1; k < falsified.size(); ++k) {
unsigned sc = constraint_expansion_size(falsified[k]);
if (sc < best_score) {
best_score = sc;
best = falsified[k];
}
for (unsigned i = coi_constraints.size(); i-- > 1; ) {
unsigned j = m_nla_core.random() % (i + 1);
std::swap(coi_constraints[i], coi_constraints[j]);
}
}
else {
std::stable_sort(coi_constraints.begin(), coi_constraints.end(),
[&](lp::constraint_index a, lp::constraint_index b) {
return constraint_expansion_size(a) < constraint_expansion_size(b);
});
}
u_map<rational> sub_cache;
lp::constraint_index best = lp::null_ci;
for (auto ci : coi_constraints) {
if (!lra_holds_substituted(ci, sub_cache)) {
best = ci;
break;
}
}
if (best == lp::null_ci)
return l_undef;
// Determine the LRA variables transitively referenced by the
// chosen constraint, then create only those NLSAT variables and