mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Fix elim_uncnstr disabled by manager-wide has_type_vars() flag

Browse source 
elim_uncnstr_tactic and the elim_unconstrained simplifier bailed out
whenever ast_manager::has_type_vars() was true. That flag is a coarse
manager-wide flag set as soon as any type variable is created, including
the type variables used to define the polymorphic signatures of builtin
plugins (e.g. finite_set), which never occur in the asserted formulas.

As a result, elim_uncnstr was disabled for ordinary (non-polymorphic)
goals as soon as such a plugin was initialized, causing a completeness
regression: unconstrained subterms that used to be eliminated now reach
the theory solvers. For seq/regex goals this surfaced as 'unknown'
(e.g. an unconstrained str.contains/str.replace_re term that made the
goal trivially sat was no longer eliminated, and theory_seq gives up on
str.replace_re).

Only bail out when the goal/formulas actually contain type-variable
typed terms, using polymorphism::util::has_type_vars, keeping the coarse
flag as a cheap pre-filter (matching existing usage in ast_translation
and ast_manager::has_type_var). This preserves the polymorphism
crash-protection while restoring elim_uncnstr for non-polymorphic goals.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-07 01:43:44 -07:00 • committed by GitHub
parent d9d3be959c
commit a3fbb7dcba
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 30 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -116,6 +116,7 @@ eliminate:
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/polymorphism_util.h"
#include "ast/simplifiers/elim_unconstrained.h"
elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
@ -425,8 +426,18 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
void elim_unconstrained::reduce() {
if (!m_config.m_enabled)
return;
if (m.has_type_vars())
return;
// has_type_vars() is a manager-wide flag that is set as soon as any type variable is
// created, including the ones used to define polymorphic signatures of builtin plugins
// (e.g. finite_set) that never occur in the asserted formulas. Only bail out when the
// formulas actually contain type-variable typed terms, which this simplifier cannot invert.
if (m.has_type_vars()) {
polymorphism::util u(m);
for (unsigned i : indices()) {
auto [f, p, d] = m_fmls[i]();
if (u.has_type_vars(f))
return;
}
}
generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
m_inverter.set_model_converter(mc.get());
m_created_compound = true;

18
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -27,6 +27,7 @@ Notes:
#include "ast/datatype_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/for_each_expr.h"
#include "ast/polymorphism_util.h"
#include "tactic/core/collect_occs.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h"
@ -936,6 +937,21 @@ class elim_uncnstr_tactic : public tactic {
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_nonvars, m_disabled, m_mc.get(), m_max_memory, m_max_steps);
}
// The manager-wide has_type_vars() flag is a coarse over-approximation: it becomes
// true as soon as any type variable is created, including the type variables used to
// define the polymorphic signatures of builtin plugins (e.g. finite_set). Those never
// occur in the actual goal, so relying on the global flag needlessly disables this
// tactic. Check whether the goal itself contains type-variable typed terms instead.
bool goal_has_type_vars(goal_ref const & g) {
if (!m().has_type_vars())
return false;
polymorphism::util u(m());
for (unsigned i = 0; i < g->size(); ++i)
if (u.has_type_vars(g->form(i)))
return true;
return false;
}
void run(goal_ref const & g, goal_ref_buffer & result) {
bool produce_proofs = g->proofs_enabled();
TRACE(goal, g->display(tout););
@ -945,7 +961,7 @@ class elim_uncnstr_tactic : public tactic {
collect_occs p;
p(*g, m_vars);
disable_quantified(g);
if (m_vars.empty() || recfun::util(m()).has_rec_defs() || m().has_type_vars()) {
if (m_vars.empty() || recfun::util(m()).has_rec_defs() || goal_has_type_vars(g)) {
result.push_back(g.get());
// did not increase depth since it didn't do anything.
return;