mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 06:45:25 +00:00
Code Activity
19852 commits 49 branches 51 tags 174 MiB
Commit graph

19852 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
2d1a42d53f fixes to ho-matcher 2025-07-05 16:24:45 -07:00
Nikolaj Bjorner
3ccf7a695b make concurrent collect_statistics in a timeout thread safe 2025-07-04 18:58:29 -07:00