mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-03 00:45:15 +00:00
Code Activity
20345 commits 77 branches 58 tags 200 MiB
Commit graph

247 commits

Author SHA1 Message Date
Copilot
36323f723b
Fix 13 compiler warnings: sign-comparison and unused parameters (#8215) 
* Initial plan

* Fix 13 compiler warnings: sign-comparison and unused parameters

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>
 2026-01-16 16:00:42 -08:00
Copilot
2436943794
Standardize for-loop increments to prefix form (++i) (#8199) 
* Initial plan

* Convert postfix to prefix increment in for loops

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix member variable increment conversion bug

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update API generator to produce prefix increments

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>
 2026-01-14 19:55:31 -08:00
Copilot
c5b28950d5
Remove redundant overridden default destructors (#8191) 
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-14 18:41:26 +00:00
Copilot
7377d28c30
Replace empty destructors with = default for compiler optimization (#8189) 
* Initial plan

* Replace empty destructors with = default

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>
 2026-01-13 10:50:10 -08:00
Copilot
daefb4ddfd
Fix unused parameter warnings in empty override functions by omitting parameter names (#8174) 
* Initial plan

* Fix unused parameter warnings in empty override functions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Omit parameter names in empty override functions instead of casting to void

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>
 2026-01-12 21:27:33 -08:00
Copilot
4d188f07e9
Replace custom util/optional with std::optional (#8162) 
* Initial plan

* Replace optional with std::optional in source files

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix array_map contains() and remove optional_benchmark test

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback - simplify array_map and test

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>
 2026-01-11 19:47:39 -08:00
Nikolaj Bjorner
662e4293a5 check cancelation in invariant checker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-23 09:09:55 -08:00
Nikolaj Bjorner
7395152632
factor out coi, use polynomial elaboration for nlsat solver (#8039) 
* factor out coi, use polynomial elaboration for nlsat solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unused functionality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-23 08:59:55 -08:00
Nikolaj Bjorner
6d19c045d8 fix infinite loop in update function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 15:47:33 -08:00
Lev Nachmanson
06ed96dbda add the "noexcept" keyword to value_score=(value_score&&) declaration 2025-10-20 11:53:34 -07:00
Nikolaj Bjorner
aaaa32b4a0 build fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-19 20:55:45 +02:00
Nikolaj Bjorner
c387b20ac6 move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
LeeYoungJoon
0a93ff515d
Centralize and document TRACE tags using X-macros (#7657) 
* 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).
 2025-05-28 14:31:25 +01:00
Nikolaj Bjorner
1510b3112e fix build warnings 2025-04-14 10:34:09 -07:00
Nikolaj Bjorner
80f00f191a fix #7572 and fix #7574 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-07 10:46:29 -08:00
Nikolaj Bjorner
28f3f8046e #7559 2025-02-18 20:50:06 -08:00
Nikolaj Bjorner
b27a2aa7fc remove calls to removed def constructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-16 10:13:00 -08:00
Nikolaj Bjorner
62126fd6e2 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-10 11:51:21 -08:00
Nikolaj Bjorner
d465bdbb87 include extensionality constraints for arrays 2025-01-31 11:06:40 -08:00
Clemens Eisenhofer
9557e7cacf
Minor (#7540) 2025-01-31 08:22:30 -08:00
Nikolaj Bjorner
eb825855fa increase the log level on callbacks with bit-indices that get set 2025-01-30 16:34:36 -08:00
Nikolaj Bjorner
c9ac4d6f75 pre-flatten use list before iterating over m_unsat 
select_max_same_sign accesses the use-list which may cause it to be flattened.
 2025-01-30 16:34:17 -08:00
Nikolaj Bjorner
e3566288a4 fixes based on benchmarking UFDTLIA/NIA/BV 2025-01-29 17:00:26 -08:00
Nikolaj Bjorner
f1e0950069 fix several crashes exposed by QF_UFDTNIA benchmark sets 2025-01-29 16:23:38 -08:00
Nikolaj Bjorner
bfe4673dac this check is not an invariant in the first place 
but nice to have.
 2025-01-29 16:23:18 -08:00
Nikolaj Bjorner
51357f6d06 Add selective filter on Ackerman axioms 2025-01-29 11:42:50 -08:00
Clemens Eisenhofer
c2a0919f79
Removed no progress case in seq-sls (#7537) 2025-01-29 09:43:57 -08:00
Nikolaj Bjorner
6d3cfb63da add eval1 functionality for replace_all 2025-01-29 04:36:55 -08:00
Nikolaj Bjorner
ab43d2dcf1 fix semantics of check-int64 div operation to align with smtlib semantics 2025-01-29 04:29:38 -08:00
Nikolaj Bjorner
30d72f79ac remove verbose output of overflow 2025-01-29 03:48:11 -08:00
Nikolaj Bjorner
3379155a63 add check for root literal assignment 2025-01-29 03:14:14 -08:00
Nikolaj Bjorner
fe5d17d515 handle exception internally, avoid passing rationals to integer operations 2025-01-28 20:09:59 -08:00
Nikolaj Bjorner
5b175c1bcd fix crashes in sls_datatype 2025-01-28 19:24:32 -08:00
Nikolaj Bjorner
fe713eb8e9 disable quadratic moves for non-integers as sqrt isn't currently defined for rationals 2025-01-28 16:53:12 -08:00
Nikolaj Bjorner
d8430810fe fix mixup between sync and sls managed variables 2025-01-28 16:35:50 -08:00
Nikolaj Bjorner
5c2a9d9936 fix pickup of new constraints 2025-01-28 15:04:13 -08:00
Nikolaj Bjorner
1676378be9 skip last power 2025-01-28 15:03:01 -08:00
Nikolaj Bjorner
8a7d971264 Update sls_bv_lookahead.h 2025-01-28 15:02:45 -08:00
Nikolaj Bjorner
2ebc647079 skip update stack items that are not Bool/bv 2025-01-28 15:02:33 -08:00
Nikolaj Bjorner
632e2b56e4 fix initialization of mod terms 2025-01-28 15:01:50 -08:00
Nikolaj Bjorner
a8279dd9d5 reset kv map consistently with egraph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 17:09:38 -08:00
Nikolaj Bjorner
72ae161307 compress store array before model-eval rewriter sees it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 16:55:07 -08:00
Nikolaj Bjorner
fe1622b592 sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 15:16:13 -08:00
Nikolaj Bjorner
63f9fdaf3e fix build 2025-01-27 10:52:21 -08:00
Nikolaj Bjorner
b6e7b80704 updates to handle bugs exposed by qf-abv for local search 
- ctx.is_true(e) - changed to work with expressions that are not literals, but come from top-level assertions
- set fixed in sls_bv_fixed to work with non-zero low order bits
- array plugin to deal with cases where e-graph is inconsistent after a merge.
 2025-01-27 10:35:29 -08:00
Nikolaj Bjorner
7ffed8613a fix bug with handling theory symbols of bit-vector type. Happens for data-type accessors. Reported by Clemens Eisenhofer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 08:22:33 -08:00
Nikolaj Bjorner
09e84e0448 fix crash when accessing bool-info vars, reported by Clemens Eisenhofer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-27 07:28:20 -08:00
Nikolaj Bjorner
5634dc5875 fix model construction bug: ignore non-relevant expressions when building model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-26 17:50:15 -08:00
Nikolaj Bjorner
d3bf25ce85 throttle value smt -> sls 2025-01-26 14:16:43 -08:00
Nikolaj Bjorner
d4100fc472 fixes to update propagation. 
rename update and update_args_value to
update_checked
update_unchecked

ensure upward propagation so that local values are consistent when entering lookahead solvers.
 2025-01-26 12:55:03 -08:00