mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-28 16:29:50 +00:00
Code Activity
20059 commits 55 branches 53 tags 187 MiB
Commit graph

3481 commits

Author SHA1 Message Date
Lev Nachmanson
641741f3a8 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:30:58 -07:00
Lev Nachmanson
8af9a20e01 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:26:40 -07:00
Lev Nachmanson
6a9520bdc2 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:21:09 -07:00
Lev Nachmanson
8ccf4cd8f7 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:19:24 -07:00
Lev Nachmanson
40b980079b parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:14:02 -07:00
Lev Nachmanson
a41549eee6 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:06:43 -07:00
Lev Nachmanson
2b3068d85f parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 09:17:12 -07:00
Lev Nachmanson
3a2bbf4802 param eval order 2025-10-07 09:13:21 -07:00
Lev Nachmanson
6e52b9584c param eval 2025-10-07 09:04:24 -07:00
Lev Nachmanson
93ff8c76db parameter evaluation order 2025-10-07 08:53:49 -07:00
Lev Nachmanson
00f1e6af7e parameter eval order 2025-10-07 08:40:24 -07:00
Lev Nachmanson
c154b9df90 param order evaluation 2025-10-07 08:34:56 -07:00
Lev Nachmanson
77c70bf812 param order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 15:52:09 -07:00
Lev Nachmanson
63bb367a10 param order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 15:52:09 -07:00
Lev Nachmanson
5a9663247b fix the order of parameter evaluation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Lev Nachmanson
5ae858f66b fixing the order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Lev Nachmanson
aa5645b54b fixing the order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Nikolaj Bjorner
ce53e06e29
Par (#7945) 
* port parallel

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

* updates

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

* update smt-parallel

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

* cleanup

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

* neat

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

* configuration parameter renaming

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

* config parameters

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

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-21 10:11:04 +03:00
Lev Nachmanson
c43cb18e63 better rewriting 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-09-18 08:08:32 -07:00
Lev Nachmanson
37904b9e85 fix the parameter evaluation order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-09-18 07:52:13 -07:00
Lev Nachmanson
9b88aaf134 determine parameter evaluation order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-09-16 16:32:46 -07:00
Nikolaj Bjorner
3c897b450f add rewrite rules for update-field under accessors and recognizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 06:14:42 -07:00
Nikolaj Bjorner
d701702735 remove model converter operator on expr_ref& 2025-09-07 16:42:20 -07:00
Nikolaj Bjorner
7005d04755 propagate mod over ite even if it hurts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-02 18:39:29 -07:00
Nikolaj Bjorner
a382ddbd8a add rewrite for mod over negation, refine axioms for grobner quotients 2025-09-02 18:26:22 -07:00
Nikolaj Bjorner
debe04350c fix #7796 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-18 09:30:03 -07:00
Nikolaj Bjorner
7ff0b246e8 fix #7792 
add missing revert operations
 2025-08-17 17:08:27 -07:00
Nikolaj Bjorner
4082e4e56a update on euf 2025-08-17 16:51:00 -07:00
Copilot
a467d8c004
Fix compilation warning: add missing is_passive_eq case to switch statement (#7785) 
* Initial plan

* Fix compilation warning: add missing is_passive_eq case to switch statement

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-15 09:50:45 -07:00
Nikolaj Bjorner
6df8b39718 Update seq_rewriter.cpp 2025-08-14 14:40:26 -07:00
Nikolaj Bjorner
237891c901 updates to euf completion 2025-08-13 10:24:46 -07:00
Nikolaj Bjorner
fcd3a70c92 remove theory_str and classes that are only used by it 2025-08-07 21:05:12 -07:00
Nikolaj Bjorner
d4a4dd6cc7 add arithemtic saturation 2025-08-06 21:11:54 -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
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
e3139d4e03 #7750 
add pre-processing simplification
 2025-07-27 13:38:36 -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
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
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