mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity
17990 commits 23 branches 48 tags 156 MiB
Commit graph

17990 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 8568ab5a64 formulate setting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-31 13:20:25 -07:00
Nikolaj Bjorner 8f2ffb3b04 fix implication order of projection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-21 09:15:27 -07:00
Nikolaj Bjorner b85a60de5c update notes on computing guards and realizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-20 17:40:04 -07:00
Nikolaj Bjorner e2ec07b732 update notes on computing guards and realizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-20 11:53:09 -07:00
Nikolaj Bjorner c7902113ab add notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-19 14:31:29 -07:00
Nikolaj Bjorner 4bf8e23f9e build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-15 16:20:31 -07:00
Nikolaj Bjorner 49c8dff707 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-15 15:47:43 -07:00
Nikolaj Bjorner c73b2b68fa rename to for case sensitivity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-15 13:11:46 -07:00
Nikolaj Bjorner fafff0272a missing make file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-15 13:08:47 -07:00
Nikolaj Bjorner 51aeb93ff3 remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-15 13:07:46 -07:00
Nikolaj Bjorner 8192f36c50 refactor dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-15 13:06:22 -07:00
Nikolaj Bjorner 1bd73d4635 initial stab at mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-15 11:12:55 -07:00
Nikolaj Bjorner 4d48dba1e3 init 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-14 22:38:29 -07:00
Nikolaj Bjorner 6733a8a5dd prepare for arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-14 22:21:43 -07:00
Nikolaj Bjorner 2481e6b910 with const 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-14 21:57:53 -07:00
Nikolaj Bjorner b21845cf72 uninterp, take 2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-14 16:07:11 -07:00
Nikolaj Bjorner 6e45057a64 synth uninterpreted, take 1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-14 15:36:58 -07:00
Nikolaj Bjorner 5e9131042a re-order when synth is invoked compared to q-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-14 12:17:37 -07:00
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