* 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>
- Relax restore_x() to handle backup/current size mismatches: when
backup is shorter (new columns added), call
move_non_basic_columns_to_bounds() to find a feasible solution.
- Fix 100x performance regression in nonlinear optimization: save LP
optimum before check_nla and return it as bound regardless of NLA
result, so opt_solver::check_bound() can validate via full re-solve
with accumulated NLA lemmas.
- Refactor theory_lra::maximize() into three helpers: max_with_lp(),
max_with_nl(), and max_result().
- Add mk_gt(theory_var, impq const&) overload for building blockers
from saved LP optimum values.
- Add BNH multi-objective optimization test (7/7 sat in <1s vs 1/7
in 30s before fix).
- Add restore_x test for backup size mismatch handling.
Fixes#8890
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
