Calling factor_sqf_pp recursively on Hensel-lifted factors corrupts
shared mutable state in the polynomial manager, m_m2pos, m_som_buffer,
m_cheap_som_buffer, m_tmp1, etc., causing assertion violations:
- polynomial.cpp:473 id < m_m2pos.size()
- upolynomial.cpp:2624 sign_a == -sign_b
Use factor_1_sqf_pp/factor_2_sqf_pp for small degrees, push directly
for larger degrees. These don't conflict with the outer call's buffers.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Fix memory leaks: use scoped_numeral instead of raw numeral for
evaluation points, ensuring cleanup on exceptions
- Precompute lc_inv before the Hensel lifting loop instead of
recomputing each iteration
- Use scoped_numeral_vector for eval_vals for consistency with codebase
- Move eval_values and candidate_primes to static constexpr class-level
- Document limitations: single-prime Hensel lifting, contiguous factor
splits only, pseudo-division lc-power caveat
- Condense Bezout derivation comment to 4-line summary
- Fix README to say Hensel lifting instead of GCD recovery
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the stub factor_n_sqf_pp (TODO: invoke Dejan's procedure) with a
working implementation using bivariate Hensel lifting:
- Evaluate away extra variables to reduce to bivariate
- Factor the univariate specialization
- Lift univariate factors to bivariate via linear Hensel lifting in Zp[x]
- Verify lifted factors multiply to original over Z[x,y]
- For >2 variables, check bivariate factors divide the original polynomial
Tests: (x0+x1)(x0+2x1)(x0+3x1) now correctly factors into 3 linear factors.
All 89 unit tests pass in both release and debug builds.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Initial plan
* simplify extract_var_bound in qe_lite_tactic.cpp via operator normalization
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add defensive check for integer type in lhs
Added a defensive check for integer type in lhs before proceeding with inequality checks.
* Update qe_lite_tactic.cpp
* Fix utility function call for integer check
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Replace hardcoded -j3 with -j$(nproc) in ci.yml, nightly.yml, and
release.yml to utilize all available cores on GitHub Actions runners.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
update_lower_lex updates m_lower for subsequent objectives with saved
values from the current model. Reset m_lower[i] and m_upper[i] to
their initial values before optimizing each objective so earlier
objectives do not contaminate later ones.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Z3_ast_to_string returns a pointer to an internal buffer that is
overwritten on the next call. Store results in std::string immediately
to avoid reading a stale, garbled buffer.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
geometric_lex's update_lower_lex updates m_lower for all subsequent
objectives with saved values from the current model. In box mode this
contaminates later objectives' starting bounds, causing platform-dependent
results. Save and restore m_lower/m_upper across iterations so each
objective starts from a clean state.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
In box mode (opt.priority=box), each objective should be optimized
independently. Previously, box() called geometric_opt() which optimizes
all objectives together using a shared disjunction of bounds. This caused
adding/removing an objective to change the optimal values of other
objectives.
Fix: Rewrite box() to optimize each objective in its own push/pop scope
using geometric_lex, ensuring complete isolation between objectives.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
resultant vanishes during a nested isolate_roots call. The mathematical
invariant that the resultant cannot vanish again after recovery does not
hold in all cases, e.g. with certain nonlinear real arithmetic formulas.
The algebraic_exception propagates cleanly through the nlsat solver and
tactic layers which already catch z3_exception.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
After qe-light's equation solver (eq_der) eliminates variables from
linear equations, remaining bounded integer quantifiers may still have
non-unit coefficients that prevent Fourier-Motzkin elimination.
Add a bounded quantifier expansion step: when the remaining quantified
integer variables all have explicit finite bounds and the product of
domain sizes is <= 10000, expand the quantifier into a finite
disjunction. This turns e.g. exists y0 in [0,10), y1 in [0,15): P(x,y0,y1)
into P(x,0,0) | P(x,0,1) | ... | P(x,9,14), which is 150 disjuncts.
The SMT solver handles the resulting quantifier-free formula instantly,
whereas the previous QSAT/MBP approach timed out due to weak integer
projections from the (|a|-1)*(|b|-1) slack in Fourier-Motzkin resolution
with non-unit coefficients.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Always print each test's captured output, not just for failures.
This preserves backward compatibility:
- PASS appears on its own line per test, as before
- ASAN/UBSAN reports from any test appear in captured logs
- timeit output is preserved for all tests
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Parallel mode (/j) is now the default. Use /seq to force serial execution.
Child processes are invoked with /seq to prevent recursive parallelism.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Refactor src/test/main.cpp to support parallel test execution:
- Add /j[:N] flag to run tests in parallel using N jobs (default: number of cores)
- Use process-based parallelism: each test runs as a child process,
avoiding thread-safety issues with global state like enable_debug/enable_trace
- Output is captured per-test and printed atomically, so different tests never mix
- Provide summary with pass/fail counts, wall time, and failed test names
- Refactor test list into X-macros for single source of truth
- Fix pre-existing bug where serial /a mode ran each test argc times
Platform support:
- Unix (Linux/macOS/FreeBSD): popen/pclose with WEXITSTATUS
- Windows: _popen/_pclose
- Emscripten: parallel disabled (no threading support)
- Works with both SINGLE_THREAD and multi-threaded builds
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
m_fixed.insert(e) was placed before the check_long_strings guard,
causing check_fixed_length(false, false) to mark variables with
len > 20 as processed without actually decomposing them. The
subsequent check_fixed_length(false, true) then skipped them.
Move the insertion after the guard so variables are only marked
as fixed once they are actually decomposed.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The add_axiom optimization that skips adding clauses when a literal is
already true was unsound: the satisfying literal could be retracted by
backtracking, leaving the axiom clause missing. This caused the solver
to miss propagations, e.g., not propagating indexof(a,s) = -1 when
contains(a,s) becomes false after backtracking.
Fix: only skip the clause if the satisfying literal is assigned at
base level (scope 0), where it can never be retracted.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
In multi-threaded solving, IF_VERBOSE(0, ...) in found_non_diff_logic_expr
was always acquiring the global g_verbose_mux mutex (since verbosity >= 0 is
always true) while holding it for potentially expensive mk_pp() calls. This
caused catastrophic lock contention when multiple threads internalized atoms.
Change IF_VERBOSE(0, ...) to IF_VERBOSE(2, ...) in both theory_diff_logic_def.h
and theory_dense_diff_logic_def.h. The diagnostic message is still available at
verbosity level 2 (-v:2), but is no longer printed (or locked) at the default
verbosity level, eliminating the contention.
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
Test tst_box_mod_opt verifies that maximize (mod (- (* 232 a)) 256)
returns 248 when using box priority with multiple objectives.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
