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

17972 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
b91cb3ab6c remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-12 20:33:46 -07:00
Nikolaj Bjorner
8e16acce19 add synth_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-12 20:31:15 -07:00
Nikolaj Bjorner
31677a0570 set synth solver check as last resort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-12 20:22:12 -07:00
Petra Hozzova
93833d1045 Suimplify conditions - wip 2023-08-11 16:37:52 -07:00
Nikolaj Bjorner
69a9701b5c compute normalize sketch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-11 15:47:05 -07:00
Nikolaj Bjorner
e2e377cfd7 use abstract datatype for synth objectives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-11 13:52:41 -07:00
Nikolaj Bjorner
75894a10c1 adding conditions and smallest depth expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-10 18:32:47 -07:00
Nikolaj Bjorner
2209d09cd9 format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-10 10:54:20 -07:00
Nikolaj Bjorner
f624890b04 add weighted repr extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-10 10:49:38 -07:00
Nikolaj Bjorner
0be3d016f6 updates with constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-09 18:35:05 -07:00
Nikolaj Bjorner
7db0df22e8 updates with constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-09 18:32:45 -07:00
Nikolaj Bjorner
942571d5a4 updates with constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-09 18:23:06 -07:00
Petra Hozzova
3fc8f7e5d0 Annotate spec as "constraint" - work in progress 2023-08-09 17:36:40 -07:00
Nikolaj Bjorner
a7e2b64545 remove dependency on spacer_util 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-09 16:33:50 -07:00
Nikolaj Bjorner
75c6d7b5a8 add comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-09 16:31:44 -07:00
Nikolaj Bjorner
52182098d0 add incremental 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-09 16:05:54 -07:00
Nikolaj Bjorner
97c8b9068f wip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-09 14:58:31 -07:00
Nikolaj Bjorner
b009697642 small fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-09 14:40:00 -07:00
Petra Hozzova
60ed472f88 Merge branch 'synth' of https://github.com/z3prover/z3 into synth 2023-08-09 14:20:49 -07:00
Petra Hozzova
272cb14b19 Store uncomputable symbols in synth_solver 2023-08-09 14:06:42 -07:00
Nikolaj Bjorner
0fb7055597 synth 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-08 20:39:53 -07:00
Nikolaj Bjorner
90780576f1 clean up header/cpp division 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-08 20:08:27 -07:00
Nikolaj Bjorner
f4a6c0df3e nits, add local functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-08 18:53:04 -07:00
Nikolaj Bjorner
3df12a641f nits, add local functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-08 16:12:36 -07:00
Nikolaj Bjorner
b7d2ba471e use namespace, add util with discriminators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-08 16:02:43 -07:00
Petra Hozzova
78b8072bb4 Implement internalize() for synth_solver 2023-08-08 15:51:41 -07:00
Nikolaj Bjorner
27dce71ea9 initial files to support theory-solver based synthesis 2023-08-08 09:24:34 -07:00
Lev Nachmanson
a7966dc436 remove an assert 2023-08-07 14:55:13 -10:00
Lev Nachmanson
858eebca82 more efficient column_is_fixed 2023-08-07 14:55:13 -10:00
Lev Nachmanson
0fbf8f92f5 delete remove_fixed_vars_from_base() from 
int_solver
 2023-08-07 14:55:13 -10:00
Nikolaj Bjorner
c3a373e225 format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-07 14:55:13 -10:00
Lev Nachmanson
0c98c755ba new equality propagation scheme, etc 2023-08-07 14:55:13 -10:00
Nikolaj Bjorner
125787c458 remove dead code 2023-08-07 11:22:34 -07:00
Hari Govind V K
dd0b0b47b8
fix #5925 (#6846) 2023-08-04 15:18:16 -07:00
Nikolaj Bjorner
84520d53ea remove out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-04 11:33:39 -07:00
Nikolaj Bjorner
b0055df4ab revert arithmetic final check to original order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-04 10:48:44 -07:00
Lev Nachmanson
f58b703ac5
u_set replaced by indexed_uint_set (#6841) 
* replace u_set by indexed_uint_set

* replace u_set by indexed_uint_set

* create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier

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

* update nightly to pull arm

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

* update nightly to pull arm

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

* fixing the build of lp_tst

* update nightly to pull arm

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

* replace u_set by indexed_uint_set

* replace u_set by indexed_uint_set

* fixing the build of lp_tst

* remove unnecessery call to contains() before
insert to indexed_uint_set

* formatting, no check for contains()
 in indexed_uint_set, always init m_touched_rows to nullptr

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-03 16:01:27 -07:00
Nikolaj Bjorner
4637339091 update model validate to include arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-03 15:51:29 -07:00
Nikolaj Bjorner
23da36126a update nightly to pull arm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-03 11:01:49 -07:00
Nikolaj Bjorner
3df6cd2c5f update nightly to pull arm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-03 10:26:12 -07:00
Nikolaj Bjorner
4bfe9a895a update nightly to pull arm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-03 10:04:23 -07:00
Nikolaj Bjorner
7b36563196 create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-03 09:48:07 -07:00
Nikolaj Bjorner
0478ab1498 update nightly script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-02 17:16:32 -07:00
Nikolaj Bjorner
8d48ff44c4 update nightly script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-02 17:10:23 -07:00
Nikolaj Bjorner
5b287bff09 nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-02 16:59:59 -07:00
NikolajBjorner
260cb337de try to instrument nightly with aarch compiler for arm64 
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
 2023-08-02 11:25:16 -07:00
NikolajBjorner
ea95f8086f try to instrument nightly with aarch compiler for arm64 
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
 2023-08-02 11:24:32 -07:00
Nikolaj Bjorner
09dd7688ce fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-02 11:19:41 -07:00
Nikolaj Bjorner
d33d8ac07a revert setting arm on linux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-02 10:55:03 -07:00
Nikolaj Bjorner
9b5727adde enable arm for non-osx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-02 10:51:52 -07:00