mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-16 17:36:39 +00:00
Code Activity
13010 commits 43 branches 51 tags 169 MiB
Commit graph

41 commits

Author SHA1 Message Date
Nikolaj Bjorner
6c1d0f6ea0 fix #3438 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-22 11:27:20 -07:00
Nikolaj Bjorner
974541e244 fix #3299 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:44:25 -07:00
Nikolaj Bjorner
c613ab0ba0 fix #3286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:42:26 -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
d530d1314b fix #3276 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 11:20:12 -07:00
Nikolaj Bjorner
825fbf1832 fix #3268 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 10:49:39 -07:00
Nikolaj Bjorner
ba79700096 remove mc printing from goals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-02 18:06:23 -08:00
Nikolaj Bjorner
8b720a0d66 fix #3115 fix #3116 regressions from #3111 etc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-02 16:38:33 -08:00
Nikolaj Bjorner
dcd4fff284 fixes to cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-21 18:06:57 -08:00
Nikolaj Bjorner
f128398bf9 add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:57:19 -07: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
dc5e4ca1c5 fix drat generation in asymmetric branch simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 13:19:09 -08:00
Nikolaj Bjorner
e4d6aa07dc use vectors instead of hash-tables in dimacs serialization to avoid hash-table contention 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 11:05:00 -08:00
Nikolaj Bjorner
c4e4139ab6 fix clause check in goal2dimacs, redo rewriting of mod to avoid deeply nested mod 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 21:33:53 -07:00
Nikolaj Bjorner
f96133f4d9 fix #1729 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-05 07:17:08 -07:00
Nikolaj Bjorner
1eb8ccad59 overhaul of error messages. Add warning in dimacs conversion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-04 16:04:37 -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
aa2721517b model conversion and acce tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-30 16:24:22 -07:00
Nikolaj Bjorner
a81a8de975 remove lns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 19:54:11 -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
Nikolaj Bjorner
2f218b0bdc remove also cores as arguments to tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-19 12:18:50 -08:00
Nikolaj Bjorner
00f5308a0e fix copy function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 23:50:48 -08:00
Nikolaj Bjorner
df6b1a707e remove proof_converter from tactic application, removing nlsat_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 23:32:29 -08:00
Nikolaj Bjorner
2746528aab fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-07 17:16:36 -08:00
Nikolaj Bjorner
651587ce01 merge with master branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-19 09:39:22 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
b482dbd589 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 17:02:27 -07:00
Nikolaj Bjorner
49cf3f8008 update documentation according to #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 07:44:55 -07:00
Nikolaj Bjorner
7d245be4e1 enable exposing internal solver state on interrupted solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-30 17:33:27 -07:00
Nikolaj Bjorner
305e080239 enable unsat core extraction in nlsat_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-01 17:57:28 +01:00
Nikolaj Bjorner
4cb57cd4da fix regression introduced by using ref-vectors on non-ref'ed output parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 17:22:47 -07:00
Christoph M. Wintersteiger
5d0db6d256 Fixed memory leak in goal::update. 
Fixes #567
 2016-04-18 17:18:16 +01:00
Christoph M. Wintersteiger
3ffcea0fe4 whitespace 2016-04-18 16:52:12 +01:00
Ken McMillan
ea127c8ab9 some confusion about proof generation 2013-06-27 12:24:18 -07:00
Leonardo de Moura
4922d62311 Fix bug reported at http://z3.codeplex.com/workitem/23 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-21 11:02:13 -08:00
Leonardo de Moura
b70687acc9 cleanning solver initialization, and fixing named assertion support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 16:35:08 -07:00
Leonardo de Moura
ef0ee9a0c4 code reorg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-01 12:47:24 -07:00
Leonardo de Moura
56ab7a7495 checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-21 18:12:34 -07:00
Leonardo de Moura
6bdb009c3e Reorganizing the code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 20:42:28 -07:00
Leonardo de Moura
ded42feeb6 Reorganizing code base 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-20 16:33:01 -07:00
Renamed from lib/goal.cpp (Browse further)