Bug fix: m_axioms and m_axiom_set were not restored on pop_scope,
causing axioms from a previous push/pop context to leak into
subsequent contexts with the same variable names, producing
non-termination in incremental solving (push/check-sat/pop sequences).
Fix: track m_axioms_size_at_push on the trail stack and truncate
m_axioms + remove corresponding m_axiom_set entries on pop.
Optimization: propagate_ground_split directly sets variable values when
one side is a pure ground string and all variables have known lengths.
Optimization: explicit len(z) = len(head) - len(var) axioms for
Skolem terms in var-vs-var splits to help arithmetic termination.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
When one side of an equation is a pure ground string and the other side
has variables with fully known lengths, directly propagate each variable's
value as a substring without going through character-by-character splitting.
E.g. x·y = "abcdef" with len(x)=2, len(y)=4 immediately gives x="ab", y="cdef".
Also reverted the add_theory_aware_branching_info change (caused cross-context
phase pollution across push/pop). Kept force_phase in branch_eq.
Known issue: T08 (x·y = y·x, x≠y, len>0) hangs when run after T01+T06 in the
same Z3 session due to phase-cache pollution across push/pop for the same variable
names. Works correctly in isolation and with distinct variable names.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
- split_variable: var-vs-var now uses length-guided branching via SAT
instead of incorrect circular mk_tail(var,1) split. With known lengths,
deterministically splits: unify if equal, mk_post(head,len_var) if var<head,
mk_post(var,len_head) if var>head. With unknown lengths, branches via
arithmetic SAT literal (|var| ≤ |head|).
- final_check_eh: process pending axioms then fall through to solve_eqs in
the same round. This ensures force_phase is set on branching variables
before the SAT solver makes any phase decisions. propagate_length_eqs and
check_zero_length no longer short-circuit with FC_CONTINUE.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Fix two bugs that caused false unsat results in the nseq string solver
when word equations were combined with length constraints:
1. propagate_length_eqs was creating fresh mk_concat terms not in the
SMT context, so ctx.e_internalized() always failed and the arithmetic
solver never learned len(x)+len(y)+len(z)=6 from x·y·z="abcdef".
Fix: new build_length_sum helper collapses concrete lengths to integer
numerals; propagate_length_eqs adds the sum equality as a theory axiom
that the arithmetic solver can immediately use.
2. branch_eq was branching variables as empty even when lower_bound > 0
was already known from arithmetic constraints (e.g. len(x)=2).
Fix: skip the empty branch when lower_bound(len_e, lo) && lo > 0.
3. Moved propagate_length_eqs before solve_eqs in final_check_eh so
arithmetic bounds are available to guide branching decisions.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
- New nseq_nielsen.h/cpp in src/ast/rewriter/: self-contained Nielsen
transformation engine for word equations
- simplify(): strip common prefix/suffix, empty elimination, variable
stripping, single-var assignment detection
- split(): case analysis for var vs constant, var vs var
- is_conflict(): mismatch detection (different constants, one side
has constants while other is empty)
- Wire Nielsen into theory_nseq:
- solve_eqs()/solve_eq(): process word equations using Nielsen
transformations with e-graph canonization
- branch_eq()/branch_var_prefix(): binary empty/non-empty decisions
and prefix enumeration (no fresh variable creation)
- canonize(): rewrite equation sides using current e-graph equivalences
- all_eqs_solved(): check if all equations are satisfied
- mk_value(): basic model generation (walk e-class for string constants)
- Passes basic tests: simple equalities, concat equations, unsat detection
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Phase 1 of the theory_nseq implementation: a stub theory solver for
strings based on Nielsen transformations and lazy regex membership.
- New files: theory_nseq.h/cpp with all required theory virtual methods
- Add 'nseq' to smt.string_solver parameter validation and documentation
- Wire into smt_setup.cpp dispatch (setup_QF_S, setup_seq_str, setup_nseq)
- Currently returns FC_GIVEUP for non-trivial string constraints
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The arith rewriter now recognizes that x * (x + 1) >= 0 for all
integers, since no integer lies strictly between -1 and 0.
Two changes:
1. is_non_negative: detect products where unpaired factors are
consecutive integer expressions (differ by exactly 1), handling
both +1 and -1 offsets and n-ary additions
2. is_separated: return true for (>= non_negative_mul 0), restricted
to multiplication expressions to avoid disrupting other theories
Also adds regression tests for the new simplification.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add (set-option :model_validate true) to each SMT-LIB2 spec in
src/test/fpa.cpp, and add ENSURE checks that the output does not
contain the string "invalid".
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Adds src/test/fpa.cpp with test_fp_to_real_denormal() exercising the
bug reported in the issue: denormal floating-point values in
(_ FloatingPoint 2 24) were getting wrong fp.to_real values because
mk_to_real was not subtracting the normalization shift lz from the
exponent.
Tests verify:
- The specific denormal from the bug report is NOT > 1.0
- Two other denormals have correct real values (0.5 and 0.125)
- A normal value is correctly identified as > 1.0
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
