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.
* 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>
* Initial plan
* build verified: nseq_regex moved to smt/seq
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* rename nseq_regex/state/model to seq_regex/state/model in smt/seq; add Clemens Eisenhofer as co-author
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* seq_model: remove theory_nseq dependency; get family_id from seq_util
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add comments for regex enhancements in seq_model
Added comments regarding future improvements for regex handling.
* Add comments for large exponent handling
Add comments for handling large exponents in seq_model.cpp
* Revise comments for clarity on sort usage
Updated comments to reflect review suggestions regarding the use of the sort of 'n'.
* seq_state: remove sgraph dep; seq_model: use snode sort for is_empty; remove NSB review comments
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update seq_state.h
* Remove unnecessary include for smt_context.h
* move seq_model from smt/seq/ to smt/; fix seq_state.h add_str_mem typo
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>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.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.
- api_fpa.cpp: add RETURN_Z3(nullptr) after SET_ERROR_CODE in Z3_mk_fpa_sort to prevent fall-through to mk_float_sort with invalid params
- api_seq.cpp: add null check for str in Z3_mk_string; add null check for str when sz>0 in Z3_mk_lstring; add lo<=hi validation in Z3_mk_re_loop
- api_array.cpp: add explicit n==0 validation in Z3_mk_array_sort_n
- api_solver.cpp: rename local variable 'c' to avoid shadowing Z3_context param in Z3_solver_propagate_created/decide/on_binding; move init_solver call inside file-exists branches of Z3_solver_from_file
- api_ast.cpp: add null check for target in Z3_translate; add null check for _from/_to arrays when num_exprs>0 in Z3_substitute
- api_model.cpp: add CHECK_NON_NULL(m) in Z3_add_func_interp; add CHECK_NON_NULL(a) in Z3_model_get_const_interp; add null check for target in Z3_model_translate
- api_opt.cpp: add null check for weight string in Z3_optimize_assert_soft
- api_quant.cpp: add num_patterns==0 validation in Z3_mk_pattern
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
The optimizer's simplification pass did not expand products of sums
into sum-of-monomials form. This caused mathematically equivalent
expressions like (5-x)^2 vs (x-5)^2 to simplify into different
internal forms, where the former produced nested multiplies
(+ 5.0 (* -1.0 x)) that led to harder purification constraints
and solver timeouts.
Enabling som=true in the first simplification tactic normalizes
polynomial objectives into canonical monomial form, making the
optimizer robust to operand ordering.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Same as test_bnh_optimize but constructs f1 and f2 with reversed
parameter order in mk_add, mk_mul, mk_sub calls. Exposes optimizer
sensitivity to expression structure.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
