* Fix broken term_comparer in m_normalized_terms_to_columns lookup
The `m_normalized_terms_to_columns` map in `lar_solver` uses a
`term_comparer` that delegates to `lar_term::operator==`, which
intentionally returns `false` (with comment "take care not to create
identical terms"). This makes `fetch_normalized_term_column` unable to
find any term, rendering the Horner module's `interval_from_term`
bounds-recovery path dead code.
History: `lar_term::operator==` returning `false` has been present since
the original "merge LRA" commit (911b24784, 2018). The
`m_normalized_terms_to_columns` lookup was added later (dfe0e856,
c95f66e0, Aug 2019) as "toward fetching existing terms intervals from
lar_solver". The initial code had `lp_assert(find == end)` on
registration (always true with broken ==) and `lp_assert(find != end)`
on deregister (always false). The very next commit (207c1c50, one day
later) removed both asserts, replacing them with soft checks. The
`term_comparer` struct delegating to `operator==` was introduced during
a later PIMPL refactor (b375faa77).
Fix: Replace the `term_comparer` implementation with a structural
comparison that checks size and then verifies each coefficient-variable
pair via `coeffs().find_core()`. This is localized to the
`m_normalized_terms_to_columns` map and does not change
`lar_term::operator==`, preserving its intentional semantics elsewhere.
Validated: on a QF_UFNIA benchmark, `interval_from_term` lookups go
from 0/573 successful to 34/573 successful. Unit test added for the
`fetch_normalized_term_column` round-trip.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* Disable operator== for lar_term
The operator== for lar_term was never intended to be used.
This changes physically disables it to identify what happens to depend
on the operator.
* Work around missing lar_term==
Previous commit disabled lar_term==. This is the only use of the
operator that seems meaningful. Changed it to compare by references
instead.
Compiles, but not sure this is the best solution.
* replace with e
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Delete unused ineq::operator==
The operator is unused, so there is no need to figure what is
the best fix for it.
* Remove lp tests that use ineq::operator==
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix: address issues 1,2,4,5 and add Goal API to Go bindings
Issue 2 (Go): Add Substitute, SubstituteVars, SubstituteFuns to Expr
Issue 4 (Go): Add GetDecl, NumArgs, Arg to Expr for AST app introspection
Goal API (Go): Add IsInconsistent and ToDimacsString to Goal
ASTVector (Go): Add public Size, Get, String methods
ASTMap (Go): Add ASTMap type with full CRUD API in spacer.go
Issue 1 (Go): Add Spacer fixedpoint methods QueryFromLvl, GetGroundSatAnswer,
GetRulesAlongTrace, GetRuleNamesAlongTrace, AddInvariant, GetReachable
Issue 1 (Go): Add context-level QE functions ModelExtrapolate, QeLite,
QeModelProject, QeModelProjectSkolem, QeModelProjectWithWitness
Issue 5 (OCaml): Add substitute_funs to z3.ml and z3.mli
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/afa18588-47af-4720-8cea-55fe0544ae55
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* fix: add substitute_funs to Expr module sig in z3.ml
The internal sig...end block in z3.ml (the module type declaration for Expr)
was missing val substitute_funs, causing OCaml compiler error:
The value substitute_funs is required but not provided
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c6662702-46a3-4aa0-b225-d6b73c2a2505
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>
The is_mod handler in theory_lra called ensure_nla(), which
unnecessarily created the NLA solver for pure linear problems, causing
the optimizer to return a finite value instead of -infinity.
Fix: check `m_nla` instead of calling `ensure_nla()`, matching the
pattern used by the is_idiv handler. The mod division is only registered
when NLA is already active due to nonlinear terms.
Update mod_factor tests to use QF_NIA logic and assert the mul term
before the mod term so that internalize_mul triggers ensure_nla() before
mod internalization.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* mini_quip: port to Python 3 and fix several bugs
examples/python/mini_quip.py was Python 2 only and had several
latent bugs that prevented it from running on Python 3 or producing
correct results on benchmarks beyond horn1..5.
Python 3 / import fixes:
- Convert `print stmt` to `print(...)` calls (lines 457-458, 567,
710, 747, 765, 776).
- The bare `print("Test file: %s") % file` form was applying `%`
to the return value of print() (None); rewrite as
`print("Test file: %s" % file)`.
- Add `import sys` (used by sys.stdout.write/flush) and
`import copy` (used by QReach.state2cube via copy.deepcopy);
neither was previously imported.
- next()/prev() passed `zip(...)` directly to z3.substitute. In
Python 3 zip returns a one-shot generator; wrap with list() the
same way mini_ic3 already does.
Bug fixes:
- is_transition(): when an init rule's body is an And without any
Invariant predicate, is_body() returns (And(...), None). The
function then passed inv0=None to subst_vars and crashed inside
get_vars(). Add an explicit None check so the rule falls through
to is_init() (same fix as mini_ic3).
- generalize(): guard against an empty unsat core. Without the
guard, an empty core can be returned and become
cube2clause([])=Or([])=False, poisoning all frames (same class
of bug as in mini_ic3).
- check_reachable(): self.prev(cube) on an empty cube produced an
empty list which was then added to a solver as a no-op
constraint, so an empty cube would always look reachable. Only
add the constraint when cube is non-empty.
- quip_blocked() at f==0 for must goals contained
`assert is_sat == s.check()` where `is_sat` is undefined in that
scope; the intent is `assert sat == s.check()`.
- Inside the lemma-pushing loop in quip_blocked(), `is_sat == unsat`
was a comparison whose result was discarded; the intended
assignment is `is_sat = unsat`.
Verified on horn1..5 (unchanged behavior, all return same
SAFE/UNSAFE result and validate). Larger benchmarks (h_CRC,
h_FIFO, cache_coherence_three) now at least run without exceptions
(performance is a separate matter).
* mini_quip: guard against None from QReach.intersect in CEX trace loop
In quip_blocked, the must-goal CEX-tracing loop calls
self.reachable.intersect(self.prev(r)) and immediately uses
r.children() on the result. QReach.intersect can return None when
the model literals do not match any state in the partial reachable
set, which crashes with AttributeError: 'NoneType' object has no
attribute 'children'. Reproduces on data/h_FIFO.smt2.
Fix: save the model, and when intersect returns None fall back to
the raw self.project0(model) as the predecessor cube. This still
gives a concrete predecessor and lets the CEX trace make progress
instead of crashing.
* Refactor parallel search tree to use global node selection (SMTS-style) instead of DFS traversal.
Introduce effort-based prioritization, allow activation of any open node, and add controlled/gated
expansion to prevent over-partitioning and improve load balancing.
* clean up code
* ablations
* ablations2: effort
* ablations2: activation
* ablations3: more activations
* ablations4: visit all nodes before splitting
* throttle tree size min is based on workers not activated nodes
* ablate random throttling
* ablate nonlinear effort
* clean up code
* ablate throttle
* ablate where add_effort is
* reset
* clean up a function and add comment
---------
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
Two fixes in examples/python/mini_ic3.py:
1. generalize(): the polarity of the disjointness check was inverted,
and there was no guard against an empty unsat core. With an empty
core, And([])=True so check_disjoint(init, prev(True)) is always
False (init is sat), and the code returned the empty core. That
empty core then became cube2clause([])=Or([])=False, which got
added as a lemma to all frames. The frame became inconsistent and
is_valid() returned And(Or())=False as the "inductive invariant".
Fix: require len(core) > 0 AND check_disjoint(init, prev(core))
(without the spurious 'not'), so the core is only used when it
is genuinely disjoint from init.
2. is_transition(): when an init rule's body happens to be an And
without any Invariant predicate (e.g. (and (not A) (not B) ...)),
is_body() returns (And(...), None). is_transition then passed
inv0=None to subst_vars() which crashed inside get_vars(). Add an
explicit None check so the rule falls through to is_init().
Verified on horn1..5 (unchanged behavior), h_CRC and h_FIFO from the
blocksys benchmarks (now correctly return CEX matching z3 spacer),
and cache_coherence_three (no longer collapses to (and or)).
