mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity
20054 commits 49 branches 53 tags 182 MiB
Commit graph

20054 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
d57dd6ef73 use jboolean in Native interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-07 13:11:11 -07:00
Nikolaj Bjorner
fa3d341b18 add on_binding callbacks across APIs 
update release notes,
add to Java, .Net, C++
 2025-08-07 12:55:50 -07:00
Lev Nachmanson
30830aae75 rename a Python file 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
f5016b4433 remove a printout 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
3eda3867d3 precalc parameters to define the eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
eeb1c18aa4 more untangle params 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
efa63db691 debug under defined calls 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
d218e87f76 add python file 
Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local>
 2025-08-07 08:33:04 -07:00
Nikolaj Bjorner
31a30370ac add Z3_solver_propagate_on_binding to ml callback declarations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-07 05:53:59 -07:00
Nikolaj Bjorner
aad511d40b missing new closure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-06 21:22:23 -07:00
Nikolaj Bjorner
b33f444545 add an option to register callback on quantifier instantiation 
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
 2025-08-06 21:11:55 -07:00
Nikolaj Bjorner
d4a4dd6cc7 add arithemtic saturation 2025-08-06 21:11:54 -07:00
Nuno Lopes
b1ab695eb6
fix #7603: race condition in Ctrl-C handling (#7755) 
* fix #7603: race condition in Ctrl-C handling

* fix race in cancel_eh

* fix build
 2025-08-06 14:27:28 -07:00
Copilot
7a8ba4b474
Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) 
* Initial plan

* Add datatype type definitions to types.ts (work in progress)

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

* Complete datatype type definitions with working TypeScript compilation

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

* Implement core datatype functionality with TypeScript compilation success

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

* Complete datatype implementation with full Context integration and tests

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>
 2025-08-04 20:58:42 -07:00
Nikolaj Bjorner
d66fabe462 Update smt_parallel.cpp 
Drop non-relevant units from shared structures.
 2025-08-03 14:17:00 -07:00
Nikolaj Bjorner
b9b3e0d337 Update euf_completion.cpp 
try out restricting scope of equalities added by instantation
 2025-08-03 14:17:00 -07:00
Nikolaj Bjorner
d8fafd8731 Update euf_ac_plugin.cpp 
include reduction rules in forward simplification
 2025-08-03 14:17:00 -07:00
Nuno Lopes
f23b053fb9 remove a bunch of string copies 2025-08-03 10:41:38 +01:00
Nuno Lopes
97aa46add3 remove default constructor 2025-08-03 09:52:53 +01:00
Nikolaj Bjorner
89cc9bd333 disable pre-processing during cubing 2025-07-31 20:58:58 -07:00
Nikolaj Bjorner
2d876d5af1 allow for internalize implies 2025-07-31 20:48:15 -07:00
Nikolaj Bjorner
f77123c13c enable passive, add check for bloom up-to-date 2025-07-27 17:18:23 -07:00
Nikolaj Bjorner
67695b4cd6 updates to ac-plugin 
fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.
 2025-07-27 13:38:37 -07:00
Nikolaj Bjorner
07613942da Add parameter validation for selected API functions 2025-07-27 13:38:37 -07:00
Nikolaj Bjorner
e3139d4e03 #7750 
add pre-processing simplification
 2025-07-27 13:38:36 -07:00
humnrdble
eb24488c3e
FreshConst is_sort (#7748) 2025-07-27 03:19:43 -07:00
Nikolaj Bjorner
ad2934f8cf fix unsound len(substr) axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-26 15:38:25 -07:00
Nikolaj Bjorner
1f8b08108c #7739 optimization 
add simplification rule for at(x, offset) = ""

Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions.
The example highlights some opportunities for simplification, noteworthy at(..) = "".
The example is solved in both versions after adding this simplification.
 2025-07-26 14:02:34 -07:00
Nikolaj Bjorner
8e1a528796 ensure atomic constraints are processed by arithmetic solver 2025-07-26 12:52:48 -07:00
Nikolaj Bjorner
0528c86905 fix #7745 
axioms for len(substr(...)) escaped due to nested rewriting
 2025-07-26 12:30:42 -07:00
Nikolaj Bjorner
95be0cf9ba remove verbose output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-25 20:22:52 -07:00
Nikolaj Bjorner
e54928679f add option to selectively disable variable solving for only ground expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-25 19:15:20 -07:00
Nikolaj Bjorner
1a488bb67a indentation 2025-07-25 11:00:30 -07:00
Nikolaj Bjorner
01633f7ce2 respect smt configuration parameter in elim_unconstrained simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-24 16:22:08 -07:00
Nikolaj Bjorner
a6c51df144 ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-24 14:54:15 -07:00
Nikolaj Bjorner
a2f17420ff moving to active/passive division 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-23 15:22:16 -07:00
Nikolaj Bjorner
44cd38c9ff
Update msvc-static-build.yml 2025-07-23 10:32:56 -07:00
Nikolaj Bjorner
fc51067207 compile warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-21 16:20:08 -07:00
Nikolaj Bjorner
1d1a01c6cc update logging 2025-07-21 16:14:14 -07:00
Nikolaj Bjorner
dbcbc6c3ac revamp ac plugin and plugin propagation 2025-07-21 07:35:06 -07:00
Nikolaj Bjorner
b983524afc add diagnostics instrumentation to mam 2025-07-12 17:52:06 -07:00
Nikolaj Bjorner
383f4db14c update pretty printer to show lambdas 2025-07-12 17:51:37 -07:00
Nikolaj Bjorner
47a2376172 bugfix to ac-plugin 
use list for "shared" should be indices into an array of shared expressions, not the monomial index.
 2025-07-12 17:51:19 -07:00
Nikolaj Bjorner
fd5455422e fix #7725 - proofs are only possible if context was created with proofs enabled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-07-12 09:14:23 +02:00
LeeYoungJoon
e575919657
debug : Add support for selecting LLDB via invoke on macOS (#7726) 2025-07-12 09:02:09 +02:00
Nikolaj Bjorner
0995928f6e wip - throttle AC completion, enable congruences over bound bodies 
- AC completion which is exposed as an option to the new congruence closure core used roots of E-Graph which gets ordering of monomials out of sync.
- Added injective function handling to AC completion
- Move to model where all equations, also unit to unit are in completion
- throw in first level bound bodies into the E-graph to enable canonization on them.
 2025-07-11 12:48:27 +02:00
Nikolaj Bjorner
35b1d09425 working on ho-matcher 2025-07-08 04:50:43 +02:00
Nikolaj Bjorner
195f3c9110 update build dependencies 2025-07-07 16:50:35 +02:00
Nikolaj Bjorner
0c5b0c3724 turn on ho-matcher for completion 2025-07-07 14:08:51 +02:00
Nikolaj Bjorner
1b3c3c2716 initial pattern abstraction and move matching to src 2025-07-06 00:53:46 -07:00