mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity
15915 commits 24 branches 48 tags 158 MiB
Commit graph

107 commits

Author SHA1 Message Date
Nikolaj Bjorner
f0e9363e78 fix bug in smt_tactic_core for translating user-ids 2021-12-05 11:13:27 -08:00
Nikolaj Bjorner
c845b22c15 fix translation for equality propagation 2021-12-04 11:55:36 -08:00
Nikolaj Bjorner
1b0ac4940b prevent stale user-propagators from being used on the same tactic after it was applied. 2021-12-04 11:51:00 -08:00
Nikolaj Bjorner
da765355e8 don't rely on cleanup 2021-12-04 11:48:41 -08:00
Nikolaj Bjorner
3d528c8ef6 typo 2021-12-04 11:19:49 -08:00
Nikolaj Bjorner
eae567ac3d indirection for user ids 2021-12-04 11:04:32 -08:00
Nikolaj Bjorner
68b072e7f1 only use setup_and_check if there is no user propagator set. 2021-12-04 09:22:25 -08:00
Nikolaj Bjorner
0077ddf33c try delay init for user propagator in smt_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 09:45:07 -08:00
Nikolaj Bjorner
bfd61fec00 enable user propagation on tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-02 08:28:52 -08:00
Nikolaj Bjorner
9031b5b949 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-18 11:46:46 -07:00
Nikolaj Bjorner
30974968af fix #5256 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-17 17:41:34 -07:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
0ce1c34d81 fix #5065 - regression solving str.from_int equations now that it isn't injective any longer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-02 12:59:48 -08:00
Nikolaj Bjorner
3ae4c6e9de refactor get_sort 2021-02-02 04:45:54 -08:00
Nikolaj Bjorner
f519c58ace Add groovy R.U.Stan option to retrieve models even when they don't exist #4924 
Usage:
z3 4924.smt2 smt.candidate_models=true
 2020-12-30 14:38:41 -08:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
cbf089e10d fix #4448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 19:41:25 -07:00
Nikolaj Bjorner
ae2f0ca85b fix #4448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 19:40:26 -07:00
Nikolaj Bjorner
3fc001baea simplifications noticed by trying #4147 
The change masks possible bugs in smt.threads and arrays.
 2020-04-29 12:07:01 -07:00
Nikolaj Bjorner
426e4cc75c fix #3557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 16:37:59 -07:00
Nikolaj Bjorner
b686bb61fe fix #3673 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 18:18:44 -07:00
Nikolaj Bjorner
06a64669a2 heap issue of #3655 ? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:52:32 -07:00
Nikolaj Bjorner
5c2a381eb0 fix #3654 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:46:37 -07:00
Nikolaj Bjorner
e160320e8a fix #3659 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:31:12 -07:00
Nikolaj Bjorner
f98e6a62fe fix #3648 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 03:49:48 -07:00
Nikolaj Bjorner
fe267803d1 fix #3634 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 20:33:42 -07:00
Nikolaj Bjorner
a1f68a619d fix #3612 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 15:09:12 -07:00
Nikolaj Bjorner
8a961a5ce9 fix #3554 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 15:02:55 -07:00
Nikolaj Bjorner
ba4765f16f debugging #3511 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner
51e459d02b fix #3294 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 10:46:03 -07:00
Nikolaj Bjorner
d229efabfc na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-09 17:12:34 +01:00
Nikolaj Bjorner
bbcfd79bf6 fix #3129 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-09 08:13:05 +01:00
Lev Nachmanson
26eb23c05b move lp_params to smt_params_helper 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-10 11:25:54 -08:00
Nikolaj Bjorner
b0a28160f7 fix #2921 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 10:35:06 -08:00
Lev Nachmanson
33cbd29ed0 mv util/lp to math/lp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner
78a1736bd2 prepare symbols to be more abstract, update mbi, delay initialize some modules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:02:08 -08:00
Nikolaj Bjorner
b479c34c0b fix #2751 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-29 10:18:55 -08:00
Nikolaj Bjorner
b8734273c8 pydoc regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-22 17:49:46 -08:00
Nikolaj Bjorner
7f74382863 capture i by value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:18 +01:00
Nikolaj Bjorner
27971e3f68 exception behavior in C++11 threads? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner
48fc3d752e add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:49:19 -07:00
Nikolaj Bjorner
074ed0d874 fix warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 17:39:19 -08:00
Nikolaj Bjorner
cf4bf7b591 more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-02 18:44:53 -05:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nuno Lopes
cef17c22a1 remove some allocs from exceptions 2018-07-02 17:08:02 +01:00
Nikolaj Bjorner
fa93bc419d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 10:53:36 -07:00
Nikolaj Bjorner
859c68c2ac merge with opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 08:27:54 -07:00
Nikolaj Bjorner
a37303a045 move parallel-tactic to solver level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-16 08:21:21 -07:00
Nikolaj Bjorner
c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00