mk_preamble_tactic in qflia_tactic.cpp constructed lia2card with a
throttled params_ref but did not wrap the call in using_params, so
when the preamble is invoked standalone the throttle is silently
clobbered by and_then's ambient param propagation: each child gets
updt_params(outer_p) called on it, re-reading lia2card.max_range
from the outer params (default 101) and discarding the constructor
override.
mk_qflia_tactic masks the bug because it wraps the whole chain in
using_params(..., main_p) where main_p also carries
lia2card.max_range=1. But QF_UFNIA goals reach mk_preamble_tactic
through the fall-through tail in mk_default_tactic
(default_tactic.cpp:52) without that outer wrap: is_qfnia_probe
rejects goals containing UF, so QF_UFNIA does not route through
mk_qfnia_tactic and instead lands on the unguarded preamble. Any
integer variable with concrete range hi-lo <= 101 then gets
hot-encoded into ~hi-lo indicator Booleans plus a sum-of-ITEs,
inflating SAT search and bloating each NLA refutation that touches
the partition.
Fix: wrap the call with using_params(mk_lia2card_tactic(m),
lia2card_p) so the throttle survives ambient propagation.
Verified on a Certora QF_UFNIA VC with a 0..98 integer: metrics now
match running with explicit tactic.lia2card.max_range=0 (mk-bool-var,
decisions, nlsat-restarts all within run-to-run noise of the
workaround), confirming the built-in throttle is finally effective.
This mirrors the pattern from commit 87e45accd ("Throttle lia2card
in QF_NIA preamble", #9362) which fixed the same bug in
mk_qfnia_preamble but did not propagate the fix to the QF_LIA
preamble. The original throttle parameters (max_range=1,
max_ite_nesting=1) were introduced by Nikolaj's commit 99cbfa715
("Add a sharp throttle to lia2card tactic to control overhead in
default tactic mode") in Feb 2025; that commit set the params at
construction time, which works under mk_qflia_tactic's outer
using_params wrap but not under standalone invocation.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
updates to nlsat polynomial simplification introduced checkpoints.
These can throw exceptions (if setting a timeout).
The code that uses this was not properly protected from exceptions to distinguish timeout based tactics from genuine exceptions that should terminate solving altogether.
see updates such as: 117da362f0
mk_qfnia_preamble invoked lia2card with no params, so the default
max_range=101 was in effect. Any integer variable with a concrete
range hi-lo <= 101 was expanded into that many fresh Booleans plus
a sum-of-ITEs, bloating SAT search alongside the nonlinear structure.
On an observed QF_UFNIA benchmark this drove a 0.2s problem to a 30s
timeout.
Mirror the throttle already applied in mk_preamble_tactic
(qflia_tactic.cpp, commit 99cbfa715): limit lia2card to 0-1 integer
variables and nesting depth 1. Wrap with using_params so the
override survives and_then's downstream updt_params calls (passing
the params to mk_lia2card_tactic alone is overwritten when and_then
re-propagates the ambient params to each child).
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Initial plan
* Add std::initializer_list overloads for BV and arith functions
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update call sites to use initializer_list format for BV and arith functions
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Refactor mk_and and mk_app to use std::span
- Made mk_and(unsigned num_args, expr * const * args) private
- Added new public mk_and(std::span<expr* const> args) method
- Added new public mk_app(family_id fid, decl_kind k, std::span<expr* const> args) method
- Updated all convenience overloads to use std::span version
- Updated all external call sites to use the new std::span API
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix remaining test files to use std::span API
- Updated src/test/sorting_network.cpp
- Updated src/test/ho_matcher.cpp with explicit cast to resolve ambiguity
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert overlapping changes superseded by PR #8286
Reverted 30 files to match the state from PR #8286 (commit ebc0688) which refactored mk_and/mk_or call sites to use vector overloads. This supersedes the std::span changes in those files.
Retained std::span changes in files unique to this PR:
- Core API changes (ast.h, ast.cpp)
- Files not affected by PR #8286 (api_context.cpp, ast_util.cpp, bool_rewriter.h, datatype_rewriter.cpp, dom_simplifier.cpp, factor_rewriter.cpp, pb2bv_rewriter.cpp, quant_hoist.cpp, spacer_cluster_util.cpp, sortmax.cpp, array_axioms.cpp, smtfd_solver.cpp, goal.cpp, ho_matcher.cpp, qe_arith.cpp, sorting_network.cpp)
- Special case in hnf.cpp where both PRs modified different lines
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Refactor mk_and and mk_or call sites to use overloaded methods
Changed 130 call sites across 64 files to use vector overloads directly instead of manually passing .size() and .data()/.c_ptr()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert mk_or changes for ptr_buffer/ptr_vector (no overload exists in ast_util.h)
* Fix compilation errors from mk_and/mk_or refactoring
Fixed type mismatches by:
- Removing m parameter for expr_ref_vector (ast_util.h has mk_and/mk_or(expr_ref_vector) overloads)
- Reverting changes for ref_buffer types (no overload exists in ast_util.h, only in ast.h for m.mk_and)
- Verified build succeeds and Z3 works correctly
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix test files to use correct mk_and/mk_or overloads
Changed test/doc.cpp and test/udoc_relation.cpp to use mk_and(expr_ref_vector) and mk_or(expr_ref_vector) without m parameter
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Update z3 codebase to use std::string_view (except z3++.h)
- Updated params.cpp/h to use string_view internally for parameter descriptions
- Updated trace.h/cpp to accept string_view for trace tag functions
- Updated hash.h/cpp to use string_view for string_hash function
- Updated all callers of string_hash to use string_view
- Properly handled nullptr to empty string_view conversions
- All tests passing
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add missing string_view includes to headers
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Migrate iterator-based for loops to range-based for loops in 11 files
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix compilation error in aig_exporter.cpp - use correct iterator API
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert changes to z3++.h as requested
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Add virtual translate method to solver_factory base class and all implementations
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add documentation for the translate method in solver_factory
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation
