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

remove an option and cache expansion sizes

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-05-22 08:53:07 -07:00
parent 7d78467af2
commit ad278c5fdc
2 changed files with 15 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -419,40 +419,25 @@ struct solver::imp {
statistics &st = m_nla_core.lp_settings().stats().m_st;
// 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.
// 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
// constraint we hit therefore has the minimum expansion size
// among all falsified candidates. Cache the expansion size for
// each constraint up front so the comparator is O(1).
svector<lp::constraint_index> coi_constraints;
for (auto ci : m_coi.constraints())
coi_constraints.push_back(ci);
unsigned pick_mode = m_nla_core.params().arith_nl_nra_check_assignment_pick();
if (pick_mode == 1) {
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<unsigned> expansion_size_cache;
for (auto ci : coi_constraints)
expansion_size_cache.insert(ci, constraint_expansion_size(ci));
std::stable_sort(coi_constraints.begin(), coi_constraints.end(),
[&](lp::constraint_index a, lp::constraint_index b) {
return expansion_size_cache[a] < expansion_size_cache[b];
});
u_map<rational> sub_cache;
lp::constraint_index best = lp::null_ci;

1
src/params/smt_params_helper.pyg
View file

@ -63,7 +63,6 @@ def_module_params(module_name='smt',
('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'),
('arith.nl.nra_check_assignment', BOOL, True, 'call check_assignment in nra_solver to verify current assignment against nlsat constraints'),
('arith.nl.nra_check_assignment_max_fail', UINT, 7, 'maximum consecutive check_assignment failures before disabling it'),
('arith.nl.nra_check_assignment_pick', UINT, 0, 'falsified-literal selection in check_assignment: 0 - minimal degree (size) of the max variable (default), 1 - random'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),
('arith.nl.expensive_patching', BOOL, False, 'use the expensive of monomials'),
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),