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>
Push/pop isolation in maximize_objectives1 (added for #7677) can corrupt
LP column values between objectives. For non-linear objectives like mod,
the LP maximize call may return stale values after a preceding
objective's push/pop cycle.
Fix: save the baseline model before the push/pop loop and use it as a
floor for each objective's value. Extract two helpers:
- maximize_objective_isolated: push/pop + save/restore per objective
- update_from_baseline_model: adopt baseline model value when it is better
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When the LP optimizer returns the same blocker expression in successive
iterations of geometric_lex (e.g., due to nonlinear constraints like
mod/to_int preventing the LP from exploring the full feasible region),
the loop now falls back to using the model-based lower bound to push
harder instead of breaking immediately.
This fixes the case where minimize(3*a) incorrectly returned -162
while minimize(a) correctly returned -infinity with the same constraints.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When the LP optimizer returns the same blocker expression in successive
iterations of geometric_lex (e.g., due to nonlinear constraints like
mod/to_int preventing the LP from exploring the full feasible region),
the loop now falls back to using the model-based lower bound to push
harder instead of breaking immediately.
This fixes the case where minimize(3*a) incorrectly returned -162
while minimize(a) correctly returned -infinity with the same constraints.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
New methods:
- Expr.getNumeralDouble(): retrieve any numeral as a double
- IntNum.getUint(): extract numeral as unsigned 32-bit value
- IntNum.getUint64(): extract numeral as unsigned 64-bit value
- RatNum.getSmall(): numerator/denominator as int64 pair
- RatNum.getRationalInt64(): numerator/denominator (returns null on overflow)
Each is a thin wrapper around the existing Native binding.
Added examples to JavaExample.java covering all new methods.
gh CLI is not available inside AWF so the agent could not download
artifacts. Switch to GitHub MCP actions toolset for artifact URLs
and add helper scripts for download and parsing.
* outline of signature for assignment based conflict generation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* outline of interface contract
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove confusing construction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add material in nra-solver to interface
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add marshaling from nlsat lemmas into core solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add call to check-assignment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Nl2lin (#7795)
* add linearized projection in nlsat
* implement nlsat check for given assignment
* add some comments
* fixup loop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debug nl2lin
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Nl2lin (#7827)
* fix linear projection
* fix linear projection
* use an explicit cell description in check_assignment
* clean up (#7844)
* Simplify no effect checks in nla_core.cpp
Move up linear nlsat call to replace bounded nlsat.
* t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* detangle mess
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove the too early return
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* do not set use_nra_model to true
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* remove a comment
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* add a hook to add new multiplication definitions in nla_core
* add internalization routine that uses macro-expanded polynomial representation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add internalization routine that uses macro-expanded polynomial representation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixup backtranslation to not use roots
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* call setup_assignment_solver instead of setup_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debug the setup, still not working
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* updated clang format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* simplify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* create polynomials with integer coefficients, use the hook to create new monomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* integrating changes from master related to work with polynomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* add forgotten files
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Update nlsat_explain.cpp
Remove a duplicate call
* fix
* move linear cell construction to levelwise
* fix
* fix
* Port throttle and soundness fixes from master
- Fix soundness: pop incomplete lemma from m_lemmas on add_lemma failure
- Gracefully handle root atoms in add_lemma
- Throttle check_assignment with failure counter (decrement on success)
- Add arith.nl.nra_check_assignment parameter
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Add arith.nl.nra_check_assignment_max_fail parameter
Replace hardcoded failure threshold with configurable parameter (default 10).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Add cha_abort_on_fail parameter to control failure counter decrement
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* abort nla check_assignment after a set number of allowed failures
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Add missing AST query methods to Java API (#8977)
* add Expr.isGround() to Java API
Expose Z3_is_ground as a public method on Expr. Returns true when the
expression contains no free variables.
* add Expr.isLambda() to Java API
Expose Z3_is_lambda as a public method on Expr. Returns true when the
expression is a lambda quantifier.
* add AST.getDepth() to Java API
Expose Z3_get_depth as a public method on AST. Returns the maximum
number of nodes on any path from root to leaf.
* add ArraySort.getArity() to Java API
Expose Z3_get_array_arity as a public method on ArraySort. Returns
the number of dimensions of a multi-dimensional array sort.
* add DatatypeSort.isRecursive() to Java API
Expose Z3_is_recursive_datatype_sort as a public method on
DatatypeSort. Returns true when the datatype refers to itself.
* add FPExpr.isNumeral() to Java API
Expose Z3_fpa_is_numeral as a public method on FPExpr. Returns true
when the expression is a concrete floating-point value.
* add isGroundExample test to JavaExample
Test Expr.isGround() on constants, variables, and compound
expressions.
* add astDepthExample test to JavaExample
Test AST.getDepth() on leaf nodes and nested expressions to verify
the depth computation.
* add arrayArityExample test to JavaExample
Test ArraySort.getArity() on single-domain and multi-domain array
sorts.
* add recursiveDatatypeExample test to JavaExample
Test DatatypeSort.isRecursive() on a recursive list datatype and a
non-recursive pair datatype.
* add fpNumeralExample test to JavaExample
Test FPExpr.isNumeral() on a floating point constant and a symbolic
variable.
* add isLambdaExample test to JavaExample
Test Expr.isLambda() on a lambda expression and a plain variable.
* change the default number of failures in check_assignment to 7
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Fix high and medium priority API coherence issues (Go, Java, C++, TypeScript) (#8983)
* Initial plan
* Add missing API functions to Go, Java, C++, and TypeScript bindings
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>
* qf-s-benchmark: debug build + seq tracing + seq-fast/nseq-slow trace analysis (#8988)
* Initial plan
* Update qf-s-benchmark: debug build, seq tracing, trace analysis
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>
* disable linear approximation by default to check the merge
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* set check_assignment to true
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix restore_x by recalulating new column values
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix restore_x by recalulating new column values
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix a memory leak
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com>
Co-authored-by: Valentin Promies <valentin.promies@rwth-aachen.de>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Angelica Moreira <48168649+angelica-moreira@users.noreply.github.com>
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* add Expr.isGround() to Java API
Expose Z3_is_ground as a public method on Expr. Returns true when the
expression contains no free variables.
* add Expr.isLambda() to Java API
Expose Z3_is_lambda as a public method on Expr. Returns true when the
expression is a lambda quantifier.
* add AST.getDepth() to Java API
Expose Z3_get_depth as a public method on AST. Returns the maximum
number of nodes on any path from root to leaf.
* add ArraySort.getArity() to Java API
Expose Z3_get_array_arity as a public method on ArraySort. Returns
the number of dimensions of a multi-dimensional array sort.
* add DatatypeSort.isRecursive() to Java API
Expose Z3_is_recursive_datatype_sort as a public method on
DatatypeSort. Returns true when the datatype refers to itself.
* add FPExpr.isNumeral() to Java API
Expose Z3_fpa_is_numeral as a public method on FPExpr. Returns true
when the expression is a concrete floating-point value.
* add isGroundExample test to JavaExample
Test Expr.isGround() on constants, variables, and compound
expressions.
* add astDepthExample test to JavaExample
Test AST.getDepth() on leaf nodes and nested expressions to verify
the depth computation.
* add arrayArityExample test to JavaExample
Test ArraySort.getArity() on single-domain and multi-domain array
sorts.
* add recursiveDatatypeExample test to JavaExample
Test DatatypeSort.isRecursive() on a recursive list datatype and a
non-recursive pair datatype.
* add fpNumeralExample test to JavaExample
Test FPExpr.isNumeral() on a floating point constant and a symbolic
variable.
* add isLambdaExample test to JavaExample
Test Expr.isLambda() on a lambda expression and a plain variable.
