Introduce exclusion intervals alongside the existing path-based condition
tracking in simplify_ite_rec. The intervals track which character values
are still possible at each point in the ITE tree, enabling simplification
of nested range conditions that the per-entry path approach cannot handle.
Key additions:
- intervals_t type and push_intervals() to maintain live character ranges
- eval_range_cond() checks AND-of-char_le conditions against intervals
- intersect_intervals/exclude_interval utilities from seq_rewriter pattern
- Negated AND handling: ¬(lo<=x ∧ x<=hi) excludes [lo,hi] from intervals
The interval check runs before the existing eval_path_cond logic, catching
cases like: if(0<=x<=10, t, if(1<=x<=8, t2, e2)) → if(0<=x<=10, t, e2)
where the inner range [1,8] is fully contained in the excluded outer range.
Fixes remaining regression timeouts on 5728 P2 and 5731 P4.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Simplify trivial range bounds in derive_range: when lo=0, omit
the lo<=x condition; when hi=max_char, omit the x<=hi condition.
Full charset ranges return epsilon directly.
- Add char_le(0,x)=true and char_le(x,max)=true to eval_cond for
always-valid bounds.
- Add range implication logic to simplify_ite_rec: when path has
negated/positive char_le constraints, detect implied or contradicted
char_le conditions (e.g., ¬(x<=127) implies 128<=x).
- Add is_subset(a, .+) check: non-nullable regexes are subsets of .+
- In update_state_graph, skip recursive exploration of nullable targets
to avoid state explosion.
These fixes resolve timeouts on 5724 (all problems), 5721 P1, and 5693.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add top-level cache (m_top_cache) to ensure stable AST node identity
across repeated derivative calls, preventing state graph divergence
- Add get_head_tail helper for derive_to_re with str.is_unit/str.is_concat
- Add ITE hoisting in mk_union/mk_inter to keep ITEs at top level
- Add De Morgan rule in mk_complement: ~(A∪B) → ~A ∩ ~B
- Add ~ε → .+ simplification in mk_complement
- Add prefix factoring: a·x ∪ a·y = a·(x∪y) and a·x ∩ a·y = a·(x∩y)
- Add r* ∩ .+ = r+ special case in mk_inter
- Enhance is_subset with union/intersection distributivity and complement
- Remove De Morgan from mk_inter to prevent infinite recursion loop
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add lightweight structural is_subset for union/inter simplification
- Use m.is_value instead of is_const_char for swap checks
- Move eval_cond to beginning of simplify_ite_rec
- Use path.shrink(sz) instead of copying extended_path
- Fix normalize_reverse stuck case to return mk_reverse(r)
- Expose subsumes() in public API
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Cache now indexes by (ele, r) pair using obj_pair_map
- Remove eval() function; operator()(ele, r) handles all cases
- Rewrite simplify_ite_rec with path vector of signed conditions
- Add range-based simplification: (lo <= x, false) + (x <= hi, false)
eliminates ite(x = v, t, e) when v is outside [lo, hi]
- Add is_itos case in derive_to_re: guards on n >= 0, digit range,
and first character match
- Port is_reverse normalization (previous commit)
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Instead of treating reverse(r) as stuck (returning symbolic mk_derivative),
normalize it by pushing reverse inward through the regex structure, then
compute the derivative of the normalized result. Mirrors mk_re_reverse logic.
Handles: concat, union, intersection, diff, ite, opt, complement, star,
plus, loop, to_re (string literals, units, concats), and symmetric cases.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Implement a new seq::derive class (seq_derive.h/cpp) that computes
symbolic derivatives of regular expressions using ITE-trees, based on
the RE# approach (Varatalu, Veanes, Ernits - POPL 2025).
Key features:
- Two-argument operator()(ele, r): computes derivative of regex r w.r.t.
element ele (concrete character or de Bruijn variable for symbolic mode)
- ACI canonicalization (flatten, stable_sort, dedup) for union/intersection
- ITE-tree combinators for binary/unary operations
- Info-based nullability with recursive fallback
- Complement absorption rules
- Depth-bounded recursion to prevent stack overflow
Integration with seq_rewriter:
- mk_derivative(ele, r) and mk_derivative(r) now delegate to m_derive
- Removed dead mk_derivative_rec function
- Added ITE hoisting in mk_re_star, mk_re_concat, mk_re_union0,
mk_re_inter0, mk_re_complement
- Added depth limiting in Antimirov derivative helpers
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This simplifies the recent `choice` axiom path in the SMT array solver
for consistency with the SAT-side implementation. The change is purely
structural: align local naming with the quantifier body it represents,
inline a single-use literal, and remove stray whitespace in the array
decl header.
- **Choice axiom cleanup**
- Rename the local implication term in
`theory_array_full::instantiate_choice_axiom` from `ax` to `body`
- Match the naming already used in
`sat/smt/array_axioms.cpp::assert_choice_axiom`
- **Single-use literal inlining**
- Replace the temporary `literal l = mk_literal(q); assert_axiom(l);`
with a direct call
- Reduce noise without changing behavior
- **Header whitespace cleanup**
- Remove trailing whitespace in `src/ast/array_decl_plugin.h`
```c++
expr_ref body(m.mk_implies(px, pc), m);
expr_ref q(m.mk_forall(1, &x_sort, &x_name, body), m);
ctx.get_rewriter()(q);
assert_axiom(mk_literal(q));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
- only the internalizer performs closure conversion
- theory_array treats propagation of lambdas similar to stores
- ho_matcher treats top-level flex patterns as first-order
- pattern-inference fix to handle quantifiers (lambdas) in patterns that are computed
This change wires SMT-LIB Hilbert choice parsing to a concrete
array-theory operator and ensures both array backends enforce the
expected semantic axiom. Previously, `(choice ((x T)) phi)` parsed as
NYI and had no solver-side instantiation path.
- **Parser: lower `choice_k` into array `OP_CHOICE`**
- `pop_quant_frame(choice_k)` now builds `(choice p)` instead of
throwing.
- Added parser include/use of array utilities to construct the term
directly from the generated lambda predicate.
- **Array decl plugin: add `OP_CHOICE` typing + surface syntax**
- Added declaration support for `choice` with signature:
- `(Array T Bool) -> T` (encoded as `('a -> Bool) -> 'a` in HO view).
- Added recognizer/util helpers (`is_choice`, `mk_choice`) and exposed
`"choice"` in op names.
- **SMT array theory (`theory_array_full`): instantiate choice axiom**
- Added instantiation for each encountered `choice(p)`:
- `forall x . p(x) => p(choice(p))`
- Integrated into internalization/relevancy paths and statistics.
- **SAT/SMT array backend (`sat/smt/array_*`): instantiate choice
axiom**
- Added new axiom record kind for choice, internalization hook,
assertion routine, and diagnostics/stat tracking.
- Uses the same quantified implication schema as above.
- **Regression coverage**
- Extended SMT2 parser regression with an HO `choice` example to ensure
parser/eval pipeline accepts and processes choice terms.
Example of the now-supported input:
```smt2
(set-logic HO_ALL)
(declare-sort U 0)
(declare-fun P () (-> U Bool))
(assert (exists ((x U)) (P x)))
(assert (= witness (choice ((x U)) (P x))))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Z3 could return `sat` for an unsatisfiable QF_ABV formula equating two
store chains over distinct constant arrays. The rewrite path for array
equalities was missing a necessary base-value constraint in
finite-domain cases where stores cannot cover all indices.
- **Root cause**
- In `array_rewriter::mk_eq_core`, equality rewriting for nested stores
over const-array bases did not enforce equality of the underlying const
values when the index domain size exceeds the number of updated indices.
- **Rewriter fix**
- Added a sound rewrite branch for:
- `store* ((as const ...) v)` vs `store* ((as const ...) w)`
- When `|domain| > (#stores_lhs + #stores_rhs)`, rewrite now includes:
- select equalities for touched indices (existing behavior)
- **and** base-value equality `v = w` (new requirement)
- This prevents spurious models where only updated indices are
constrained.
- **Regression coverage**
- Added a focused regression in `src/test/mod_factor.cpp` that asserts
`unsat` for a minimized constant-array/store-chain BV case with
`(distinct x y)` and one store per side.
```cpp
(assert (distinct x y))
(assert (= (store A0 i0 e0) (store A1 i1 e1)))
(check-sat) ; expected: unsat
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
`sat.smt=true` could return `sat` with an invalid model for QF_UFBV
formulas combining Bool-valued UFs and BV range constraints. The failure
came from broken model-trail reconstruction in `elim_unconstrained`,
where `ADD` entries were effectively turned into identity substitutions.
- **Root-cause fix: restore model-trail substitution composition**
- In `elim_unconstrained::update_model_trail`,
`generic_model_converter::ADD` entries now use `entry.m_def` (rewritten
through accumulated substitutions) instead of creating self-referential
const-to-const mappings.
- This re-enables correct back-substitution for eliminated unconstrained
terms during witness reconstruction.
- **Regression coverage: QF_UFBV + `sat.smt=true` + model validation**
- Added a focused unit test in `src/test/simplifier.cpp` for:
- Bool-valued UF predicate over BV vars
- split BV range constraints (`bvuge` / `bvult`)
- `:sat.smt true` and `:model_validate true`
- The test asserts the solver returns `sat` without emitting an
invalid-model error.
```cpp
// before (effectively no-op back-mapping)
new_def = m.mk_const(entry.m_f);
sub->insert(new_def, new_def, nullptr, nullptr);
// after (compose and apply recorded definition)
new_def = entry.m_def;
(*rp)(new_def);
sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Recent GCC builds report two warning classes in core codepaths: a
possible uninitialized read in `bound_propagator::relevant_bound`, and
repeated `-Warray-bounds` diagnostics in `mpz_manager::get_sign_cell`
when materializing small integers into a reserved `mpz_cell`.
- **Warning cleanup in bound propagation**
- Initialize `interval_size` at declaration in
`src/ast/simplifiers/bound_propagator.cpp` so the compiler can prove
safety across templated `LOWER/UPPER` instantiations using `std::clamp`.
- Preserves existing control flow and refinement heuristics (`bounded`
remains the gate for interval-based logic).
- **Warning cleanup in mpz small-value cell materialization**
- In `src/util/mpz.h`, replace direct writes through `cell->m_digits[0]`
with writes via a derived digits pointer
(`reinterpret_cast<digit_t*>(cell + 1)`), avoiding zero-length
trailing-array indexing diagnostics.
- Keeps memory layout and semantics unchanged for the stack-reserved
`sign_cell` buffer.
- **Representative change**
```cpp
cell = reserve;
cell->m_size = 1;
digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
cell_digits[0] = a.value() < 0 ? -a.value() : a.value();
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
`fpa2bv_converter::mk_to_real` computed `2^(1/|exp|)` instead of
`1/(2^|exp|)` for floats with negative exponents, causing the NRA solver
to reach contradictory conclusions and return spurious `unsat` for
satisfiable QF_FPLRA formulas.
## Root Cause
After the loop that evaluates `exp2 = |unbiased_exp|` as an integer, the
code took `1/exp2` (reciprocal of the integer) before calling
`mk_power`, yielding `2^(1/3)` instead of `2^(-3) = 1/8` for a float
with exponent -3:
```cpp
// Buggy
one_div_exp2 = mk_div(one, exp2); // 1/|exp|, not 1/2^|exp|
exp2 = mk_ite(exp_is_neg, one_div_exp2, exp2);
two_exp2 = mk_power(two, exp2); // 2^(1/3) ≠ 1/8 for exp=-3
```
## Fix
Compute the power of 2 first, then invert it:
```cpp
// Fixed
two_exp2 = mk_power(two, exp2); // 2^|exp|
one_div_two_exp2 = mk_div(one, two_exp2); // 1/(2^|exp|)
two_exp2 = mk_ite(exp_is_neg, one_div_two_exp2, two_exp2); // correct 2^exp
```
## Impact
- **QF_FPLRA**: `to_fp(RTZ, r)` with a symbolic real `r` constrained to
an interval containing a float's exact rational value now correctly
returns `sat`.
- **fp.to_real**: Fixes incorrect real-valued encoding for all floats
with negative exponents, including denormals (which adjust the exponent
by subtracting leading-zero count).
A regression test covering the reported case is added to
`src/test/fpa.cpp`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Compute term generations based on minimal match
* Tidy up get_*_f_app
* Update euf_mam to the minimum generation number among matches
* Update euf_mam.cpp
* Move the UNREACHABLE() test to smt_mam.cpp
* Enforce stickiness of max-generation
* Add current generation tracking to bind structure
* Fix build error
---------
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
