* Initial plan
* Refactor mk_and and mk_app to use std::span
- Made mk_and(unsigned num_args, expr * const * args) private
- Added new public mk_and(std::span<expr* const> args) method
- Added new public mk_app(family_id fid, decl_kind k, std::span<expr* const> args) method
- Updated all convenience overloads to use std::span version
- Updated all external call sites to use the new std::span API
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix remaining test files to use std::span API
- Updated src/test/sorting_network.cpp
- Updated src/test/ho_matcher.cpp with explicit cast to resolve ambiguity
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert overlapping changes superseded by PR #8286
Reverted 30 files to match the state from PR #8286 (commit ebc0688) which refactored mk_and/mk_or call sites to use vector overloads. This supersedes the std::span changes in those files.
Retained std::span changes in files unique to this PR:
- Core API changes (ast.h, ast.cpp)
- Files not affected by PR #8286 (api_context.cpp, ast_util.cpp, bool_rewriter.h, datatype_rewriter.cpp, dom_simplifier.cpp, factor_rewriter.cpp, pb2bv_rewriter.cpp, quant_hoist.cpp, spacer_cluster_util.cpp, sortmax.cpp, array_axioms.cpp, smtfd_solver.cpp, goal.cpp, ho_matcher.cpp, qe_arith.cpp, sorting_network.cpp)
- Special case in hnf.cpp where both PRs modified different lines
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>
* Initial plan
* Refactor mk_and and mk_or call sites to use overloaded methods
Changed 130 call sites across 64 files to use vector overloads directly instead of manually passing .size() and .data()/.c_ptr()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert mk_or changes for ptr_buffer/ptr_vector (no overload exists in ast_util.h)
* Fix compilation errors from mk_and/mk_or refactoring
Fixed type mismatches by:
- Removing m parameter for expr_ref_vector (ast_util.h has mk_and/mk_or(expr_ref_vector) overloads)
- Reverting changes for ref_buffer types (no overload exists in ast_util.h, only in ast.h for m.mk_and)
- Verified build succeeds and Z3 works correctly
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix test files to use correct mk_and/mk_or overloads
Changed test/doc.cpp and test/udoc_relation.cpp to use mk_and(expr_ref_vector) and mk_or(expr_ref_vector) without m parameter
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>
* Initial plan
* Update z3 codebase to use std::string_view (except z3++.h)
- Updated params.cpp/h to use string_view internally for parameter descriptions
- Updated trace.h/cpp to accept string_view for trace tag functions
- Updated hash.h/cpp to use string_view for string_hash function
- Updated all callers of string_hash to use string_view
- Properly handled nullptr to empty string_view conversions
- All tests passing
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add missing string_view includes to headers
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>
* Initial plan
* Migrate iterator-based for loops to range-based for loops in 11 files
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix compilation error in aig_exporter.cpp - use correct iterator API
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert changes to z3++.h as requested
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>
* Initial plan
* Add virtual translate method to solver_factory base class and all implementations
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add documentation for the translate method in solver_factory
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>
Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation
This allows using z3 for limited E-saturation simplification.
The tactic rewrites all assertions using the E-graph induced by the equalities and instantiated equality axioms.
It does allow solving with conditionals, although this is a first inefficient cut.
The following is a sample use case that rewrites to false.
```
(declare-fun prime () Int)
(declare-fun add (Int Int) Int)
(declare-fun mul (Int Int) Int)
(declare-fun ^ (Int Int) Int)
(declare-fun sub (Int Int) Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun base () Int)
(declare-fun S () (Seq Int))
(declare-fun hash ((Seq Int) Int Int Int Int) Int)
(assert (let ((a!1 (mul (seq.nth S i) (^ base (sub (sub j i) 1)))))
(let ((a!2 (mod (add (hash S base prime (add i 1) j) a!1) prime)))
(not (= (hash S base prime i j) a!2)))))
(assert (forall ((x Int))
(! (= (mod (mod x prime) prime) (mod x prime))
:pattern ((mod (mod x prime) prime)))))
(assert (forall ((x Int) (y Int))
(! (= (mod (mul x y) prime) (mod (mul (mod x prime) y) prime))
:pattern ((mod (mul x y) prime))
:pattern ((mod (mul (mod x prime) y) prime)))))
(assert (forall ((x Int) (y Int))
(! (= (mod (mul x y) prime) (mod (mul x (mod y prime)) prime))
:pattern ((mod (mul x y) prime))
:pattern ((mod (mul x (mod y prime)) prime)))))
(assert (forall ((x Int) (y Int))
(! (= (mod (add x y) prime) (mod (add x (mod y prime)) prime))
:pattern ((mod (add x y) prime))
:pattern ((mod (add x (mod y prime)) prime)))))
(assert (forall ((x Int) (y Int))
(! (= (mod (add x y) prime) (mod (add (mod x prime) y) prime))
:pattern ((mod (add x y) prime))
:pattern ((mod (add (mod x prime) y) prime)))))
(assert (forall ((x Int) (y Int))
(! (= (mul x (^ x y)) (^ x (add y 1))) :pattern ((mul x (^ x y))))))
(assert (forall ((x Int) (y Int)) (! (= (mul x y) (mul y x)) :pattern ((mul x y)))))
(assert (forall ((x Int) (y Int)) (! (= (add x y) (add y x)) :pattern ((add x y)))))
(assert (forall ((x Int) (y Int)) (! (= (mul x y) (mul y x)) :pattern ((mul x y)))))
(assert (forall ((x Int) (y Int) (z Int))
(! (= (add x (add y z)) (add (add x y) z))
:pattern ((add x (add y z)))
:pattern ((add (add x y) z)))))
(assert (forall ((x Int) (y Int) (z Int))
(! (= (mul x (mul y z)) (mul (mul x y) z))
:pattern ((mul x (mul y z)))
:pattern ((mul (mul x y) z)))))
(assert (forall ((x Int) (y Int) (z Int))
(! (= (sub (sub x y) z) (sub (sub x z) y)) :pattern ((sub (sub x y) z)))))
(assert (forall ((x Int) (y Int) (z Int))
(! (= (mul x (add y z)) (add (mul x y) (mul x z)))
:pattern ((mul x (add y z))))))
(assert (forall ((x Int)) (! (= (sub (add x 1) 1) x) :pattern ((add x 1)))))
(assert (forall ((x Int)) (! (= (add (sub x 1) 1) x) :pattern ((sub x 1)))))
(assert (let ((a!1 (^ base (sub (sub (sub j 1) i) 1))))
(let ((a!2 (mod (add (hash S base prime (add i 1) (sub j 1))
(mul (seq.nth S i) a!1))
prime)))
(= (hash S base prime i (sub j 1)) a!2))))
(assert (let ((a!1 (add (seq.nth S (- j 1)) (mul base (hash S base prime i (sub j 1))))))
(= (hash S base prime i j) (mod a!1 prime))))
(assert (let ((a!1 (add (seq.nth S (- j 1))
(mul base (hash S base prime (add i 1) (sub j 1))))))
(= (hash S base prime (add i 1) j) (mod a!1 prime))))
(apply euf-completion)
```
To use conditional rewriting you can
```
(assert (not (= 0 prime)))
```
and update axioms using modulus with prime to be of the form:
```
(=> (not (= 0 prime)) <original-body of quantifier>)
```
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros
* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md
* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled
* trace: improve trace tag handling system with hierarchical tagging
- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
(class names and descriptions to be refined in a future update)
* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals
* trace : add cstring header
* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py
* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.
* trace : Add TODO comment for future implementation of tag_class activation
* trace : Disable code related to tag_class until implementation is ready (#7663).
lia2card was added to qfuflia tactic based on a user scenario, but it overshot: lia2card is by default harmful. It is here tamed to only convert binary variables and throttle on nested ite terms
Add API solve_for(vars).
It takes a list of variables and returns a triangular solved form for the variables.
Currently for arithmetic. The solved form is a list with elements of the form (var, term, guard).
Variables solved in the tail of the list do not occur before in the list.
For example it can return a solution [(x, z, True), (y, x + z, True)] because first x was solved to be z,
then y was solved to be x + z which is the same as 2z.
Add congruent_explain that retuns an explanation for congruent terms.
Terms congruent in the final state after calling SimpleSolver().check() can be queried for
an explanation, i.e., a list of literals that collectively entail the equality under congruence closure.
The literals are asserted in the final state of search.
Adjust smt_context cancellation for the smt.qi.max_instantiations parameter.
It gets checked when qi-queue elements are consumed.
Prior it was checked on insertion time, which didn't allow for processing as many
instantations as there were in the queue. Moreover, it would not cancel the solver.
So it would keep adding instantations to the queue when it was full / depleted the
configuration limit.
The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM.
Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers.
The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time.
We characterize it as based on polling.
