mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-10 10:57:15 +00:00
Code Activity

spacer: enable model completion in arith qe_project (#9776)

Browse source 
Variables to be projected may not be assigned in the model (e.g.
grounded auxiliary variables that are don't-cares). Enable model
completion in the arith `qe_project` so their evaluation yields concrete
numerals, matching the behavior of the native MBP arith projector.

Two call sites in `arith_project_util`
(`src/muz/spacer/spacer_qe_project.cpp`) now install a
`model::scoped_model_completion` before evaluating projected variables
against the model.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-08 19:35:49 -07:00 • committed by GitHub
parent 2ed4e90c75
commit aa872bd289
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz/spacer/spacer_qe_project.cpp
View file

@ -1148,6 +1148,7 @@ class arith_project_util {
expr_ref_vector const &lits) {
app_ref_vector new_vars(m);
expr_ref_vector result(lits);
model::scoped_model_completion _smc(mdl, true);
for (unsigned i = 0; i < vars.size(); ++i) {
app *v = vars.get(i);
m_var = alloc(contains_app, m, v);
@ -1183,6 +1184,12 @@ class arith_project_util {
expr_map &map) {
app_ref_vector new_vars(m);
// Variables to be projected may not be assigned in the model
// (e.g. grounded auxiliary variables that are don't-cares). Enable
// model completion so their evaluation yields concrete numerals,
// matching the behavior of the native MBP arith projector.
model::scoped_model_completion _smc(mdl, true);
// factor out mod terms by introducing new variables
TRACE(qe, tout << "before factoring out mod terms:" << "\n";
tout << mk_pp(fml, m) << "\n"; tout << "mdl:\n";