Make the relevancy_propagator watch-list membership filter (m_is_watched)
runtime-toggleable via a new boolean parameter smt.relevancy.watch_filter
(default true). When false, get_watches() always probes m_watches, giving
the pre-filter behavior. This enables A/B performance comparison of the
same binary (filter on vs off) under the Ramon benchmark harness.
Behavior-preserving either way: verified identical results on QF_LIA with
the filter on and off.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
* Add adaptive growth knobs for Gröbner under arith.nl.grobner_adaptive
When enabled, the per-call growth budget (m_eqs_growth, m_expr_size_growth,
m_expr_degree_growth, m_max_simplified) is scaled by m_growth_boost:
- two consecutive productive runs bump the boost by 3/2 (cap 4x)
- a miss resets the streak and decays the boost toward 1.0x by 1/4 of excess
Default is off; the existing miss-frequency throttle (m_quota / m_delay_base)
is unchanged, so this only affects per-call power, not call frequency.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Update src/params/smt_params_helper.pyg
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Arie Gurfinkel <arie.gurfinkel@gmail.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
* Add dual-row shared-factor sandwich for NLA bound propagation
When enabled via arith.nl.monomial_sandwich (default off), monomial_bounds
finds LP term columns whose term has shape a_m * m + a_v * v with exactly
two variables — both factors of a binary monomial m = u*v. The term column's
bound bounds (a_m * m + a_v * v); substituting m = u*v gives v * (a_m*u + a_v),
and sign-aware interval division by v plus an affine shift yields a numeric
bound on u. The derived interval is fed to the existing propagate_value path
so the lemma channel and integer rounding logic are shared with the rest of
NLA's forward/backward propagation; no new emit code.
Catches conflicts of the form
α_v1 * v + α_m * m ≥ k1
α_v2 * v + α_m * m ≤ k2
that today require nlsat (when no single row alone yields infeasibility but
their conjunction tightly bounds u after factoring v).
Scope: binary monomials only (m.size()==2, no squares); cap of 16 term-columns
scanned per call; one lemma per (u,v) attempt to keep the lemma channel quiet.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Add arith.nl.order.binomial_sign flag (default true)
Granular gate for order_lemma_on_binomial_sign — the only order family that
embeds a model-snapshot literal (x ≷ val(x)) in the lemma body. Disabling it
keeps the always-good structural mon-ol family running while removing the
SAT-splitter shape that cascades under model perturbations (e.g., from
arith.nl.monomial_sandwich tightening factor bounds).
Default true preserves master behaviour; the flag is intended as an
experimental knob to measure how much of an observed cascade is specifically
attributable to the binomial-sign splitter vs. the structural cancellation
lemmas in the same module.
See ord-binom-opportunities.md for the full gap analysis and the
deterministic-replacement directions (sandwich, McCormick) that would let
this flag eventually default to false without regressing leaves where
ord-binom currently carries the proof.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Add sign-pinned binomial bound for NLA (Opportunity 1 from ord-binom doc)
When enabled via arith.nl.monomial_binomial_sign (default off), monomial_bounds
adds a third pass alongside propagate_down (existing) and propagate_shared_factor
(sandwich). For a binary monomial m = u*v in m_to_refine whose model value mv
disagrees with val(u)*val(v), and where v has a determined sign:
1. synthesize a one-sided interval for m.var() at mv (no deps; the snapshot
enters as a literal in the lemma body, not as an antecedent)
2. divide by v's interval (sign-aware via dep.div<with_deps>) to get a
deterministic interval for u
3. emit a propagate_value-style lemma whose body is
m.var() < mv (or > mv) ∨ u-bound
conditioned on v's bound witness
Targets the case ord-binom currently handles: factors have determined signs,
m.var() may have no LP bound. The clause is sound modulo the monomial
definition (same condition propagate_down, propagate_shared_factor, and
ord-binom already rely on).
A new throttle kind MONOMIAL_BINOMIAL_SIGN keyed on (m.var, u, v, direction)
prevents cascading: without it, each new val(m.var()) snapshot would re-emit
across model changes the same way ord-binom does.
Validated via smt.arith.validate=true: 0 soundness errors across the
32-leaf test corpus.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Add McCormick box-corner tangent points (Opportunity 2 from ord-binom doc)
When enabled via arith.nl.tangents.box_corners (default off, sub-flag of
arith.nl.tangents), tangent_imp::get_points selects m_a, m_b at the corners
of the bound box [x_lo, x_hi] × [y_lo, y_hi] instead of the model-centered
points val(x) ± delta. The selection follows the classical McCormick
under/over envelope:
- m_below=true (under-approximation):
m_a = (x_lo, y_lo), m_b = (x_hi, y_hi)
- m_below=false (over-approximation):
m_a = (x_lo, y_hi), m_b = (x_hi, y_lo)
The existing generate_plane already produces the McCormick linear form
xy ≷ pl.y·x + pl.x·y − pl.x·pl.y at any chosen point pl. push_point is
skipped in box-corner mode: corners are extremes, so doubling the offset
moves out of the box and would invalidate the McCormick property.
Falls back to the existing model-driven point selection when either factor
has an unbounded side or the box is degenerate (single-point in a
dimension).
Soundness — non-strict inequality at corners. The classical model-driven
flow uses pl strictly in the interior of the box, so generate_plane emits
xy > T (strict). At the box corners the tangent meets the surface along
the box's edges (xy = T when x = pl.x or y = pl.y), so the strict
inequality is violated by any model with x at the box boundary. A new
m_pl_strict_interior member, set false on a successful set_box_corners(),
switches generate_plane's emission to ≥/≤ (non-strict). The model-driven
path keeps strict — its push_point + plane_is_correct_cut chain already
guarantees pl is interior.
Validated via smt.arith.validate=true: 0 validate_conflict() failures
across the 32-leaf test corpus with box_corners=true.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* 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>
for equations x*y + z = 0,
with x, y, z integer, enforce that x divides z
It is (currently) enabled within Grobner completion
and applied partially to x a variable, z linear, and
only when |z| < |x|.
#7791 reports on using model values during lex optimization that break soft constraints.
This is an artifact of using optimization where optimal values can be arbitrarily close to a rational.
In a way it is by design, but we give the user now an option to control the starting point for epsilon when converting infinitesimals into rationals.
