mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-06 04:36:24 +00:00
Code Activity
13111 commits 40 branches 51 tags 168 MiB
Commit graph

170 commits

Author SHA1 Message Date
Nikolaj Bjorner
2c078b01da fix #3422 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-22 16:56:26 -07:00
Nikolaj Bjorner
3d7098ec85 fix #3137 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-09 07:15:06 +01:00
Nikolaj Bjorner
7d976e4f4d fix #3120 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-06 06:52:38 +01:00
Nikolaj Bjorner
bba2cf9f20 fix #3163 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-06 06:31:44 +01:00
Nikolaj Bjorner
2989d9c241 fix #3124 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-03 12:39:25 -08:00
Nikolaj Bjorner
1d0572354b add bit-matrix, avoid flattening and/or after bit-blasting, split pdd_grobner into solver/simplifier, add xlin, add smtfd option for incremental mode logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-01 20:14:20 -08:00
Nikolaj Bjorner
17824df3cd Update inc_sat_solver.cpp 
revert local change
 2019-12-31 11:55:43 -08:00
Nikolaj Bjorner
a7dc50362b fix #2836 2019-12-31 11:55:43 -08:00
Nikolaj Bjorner
185b01dd35 fix #2416 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-23 19:01:49 -07:00
Nikolaj Bjorner
c2264c73f2 debug mutex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-23 19:01:49 -07:00
Nikolaj Bjorner
f1dee935d0 remove UNREACHABLE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 17:07:00 -07:00
Nikolaj Bjorner
8893913c98 remove internal referenes to set_activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:06:05 -07:00
Nikolaj Bjorner
dc0e9c1919 completing user print experience with seq/re #2200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 11:46:36 -07:00
Nikolaj Bjorner
69d7d8ff87 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 11:42:17 -08:00
Nikolaj Bjorner
39f73fa595 ensure that activity works for sat solver from cold state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 16:56:55 -08:00
Nikolaj Bjorner
89bf2d4368 add API for setting variable activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 12:05:24 -08:00
Nikolaj Bjorner
35eb21bc35 fix extraction of trail 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:06:41 -08:00
Nikolaj Bjorner
8d20310758 adding trail/levels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-29 14:45:51 -08:00
Nikolaj Bjorner
498864c582 adding dump facility for cancelation #2095, easing dimacs in/out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 12:21:23 -08:00
Nikolaj Bjorner
63d480fd92 fix cnf check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 21:17:39 -08:00
Nikolaj Bjorner
b8d18c6c6d speed-up handling of cnf input to inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 20:52:19 -08:00
Nikolaj Bjorner
99cc4747c5 fixing #1971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 17:21:04 -08:00
Nikolaj Bjorner
b0b6394c6c fixing #1971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 17:10:37 -08:00
Nikolaj Bjorner
dc77579707 delta faction to control double lookahead eagerness 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-04 23:41:03 -08:00
Nikolaj Bjorner
5bf57c2700 fix cubing semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-02 08:14:19 -07:00
Nikolaj Bjorner
9d0aa4d02d update empty cube case for sat/undef cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 20:22:02 -07:00
Nikolaj Bjorner
90fca8b378 add psat to available tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-30 17:44:28 -07:00
Nikolaj Bjorner
26d40865fa add verbose output to capture cases for empty cube 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-25 23:54:48 -07:00
Nikolaj Bjorner
7335b3bf56 remove debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-24 16:53:15 -07:00
Nikolaj Bjorner
80d0c5cf82 fix #1836 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-24 16:52:25 -07:00
Nikolaj Bjorner
7b3b1b6e9f pop to base before incremental internalization to ensure that units are not lost 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-22 14:04:15 -07:00
Nikolaj Bjorner
84c7df75d6 record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 16:21:27 -07:00
Nikolaj Bjorner
74621e0b7d first eufi example running 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
618d394ab5 unreferenced variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-10 09:41:12 +01:00
Nikolaj Bjorner
96914d8578 update model conversion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 11:46:26 -07:00
Nikolaj Bjorner
f525f43e43 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 09:30:43 -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
cd35caff52 clean up parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-16 03:18:57 -07:00
Nikolaj Bjorner
f7e49501af updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-13 16:22:36 -07:00
Nikolaj Bjorner
c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Nikolaj Bjorner
e7d43ed516 fix pb rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-12 11:22:05 -07:00
Nikolaj Bjorner
4c1379e8c9 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-19 21:49:03 -08:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner
8fb7fb9f98 add missing caching of PB/cardinality constraints, increase limit for compiling cardinalities to circuits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-11 19:27:00 -08:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner
61f99b242e xor to xr to avoid clang issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:25:02 -08:00
Nikolaj Bjorner
fa0c75e76e rename to core2 to avoid overloaded virtual 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:13:13 -08:00
Nikolaj Bjorner
ece5ad90e0 fix model conversion bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-20 17:09:43 -08:00
Nikolaj Bjorner
b129ee764f debugging opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-20 10:20:22 -08:00