mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-05 01:27:41 +00:00
Code Activity
13155 commits 67 branches 52 tags 179 MiB
Commit graph

113 commits

Author SHA1 Message Date
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Bruce Mitchener
dda62ae78c Use bool literals instead of 0/1. 2018-10-17 22:42:57 +07:00
Michał Janiszewski
cfd0486582 Catch exceptions by const-reference 
Exceptions caught by value incur needless cost in C++, most of them can
be caught by const-reference, especially as nearly none are actually
used. This could allow compiler generate a slightly more efficient code.
 2018-10-16 19:16:07 +02:00
Bruce Mitchener
373b691709 Use 'override' where possible. 2018-10-02 10:26:38 +07:00
Arie Gurfinkel
7bff74dec0 Minor pass on synchronize transform 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
24044429a7 Rename cache to m_cache 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
0516e6f21f Integrating synchronize pass 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
8400122596 mk_synchronize rule transformation 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
5d1149adb2 Transformation to eliminate term-ite expressions from DL rules 2018-07-02 17:09:56 -04:00
Arie Gurfinkel
6d75c31468 First draft of elim_term_ite xform. Not working. 2018-07-02 17:09:56 -04:00
Nikolaj Bjorner
7844476a7d fixes to term-graph, add proof-checker routines for PR_BIND, remove orphaned file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 17:04:47 -07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
caca07c85f fix path to moved header file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-15 15:28:18 -07:00
Arie Gurfinkel
9109968e55 Cleanup fixedpoint options 
Replace pdr options with spacer
Repace fixedpoint module with fp
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
ff0f257102 remove iff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
fa93bc419d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 10:53: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
Bruce Mitchener
878a6ca14f Fix typos. 2018-03-09 14:30:43 +07:00
Nikolaj Bjorner
718e5a9b6c add unit extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-06 01:08:17 -08:00
Nikolaj Bjorner
9279cbfbac don't reinit assumptions when the solver is unsat. fixes #1502 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-24 16:30:08 +09:00
Nikolaj Bjorner
7b6f51941c fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 22:18:47 +09:00
Nikolaj Bjorner
54b00f357b fix rule inlining, add WithParams to pass parameters directly to python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 21:57:54 +09:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner
e4f29a7b8a debugging mc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-19 21:09:52 -08:00
Nikolaj Bjorner
5159291d57 add missing interpreted tail during bottom-up simplification #1452 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-12 19:29:42 -08:00
Nikolaj Bjorner
4bbece6616 re-organize proof and model converters to be associated with goals instead of external 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-18 16:33:54 -08:00
Nikolaj Bjorner
dc0b2a8acf remove extension model converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 17:25:35 -08:00
Nikolaj Bjorner
0d15b6abb7 add stubs for converting assertions, consolidate filter_model_converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 14:51:13 -08:00
Nikolaj Bjorner
cde41cf16c fix slicer for unsoundness. #1304 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 16:39:09 -08:00
Nikolaj Bjorner
2c97eb1393 include information whether rule is reachable in del_rule model converter for simpler model presentation #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 11:46:28 -08:00
Nikolaj Bjorner
116094022f insert total relations in model converter. #1291 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 09:10:15 -08:00
Nikolaj Bjorner
429edf175f fix model converter bug in coi-filter #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 19:16:04 -08:00
Nikolaj Bjorner
3de8c193ea implementing model updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 16:11:51 -05:00
Nikolaj Bjorner
eac659f748 deal with empty set of post-orders 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:34:14 +01:00
Christoph M. Wintersteiger
00651f8f21 Tabs, formatting. 2017-09-17 14:54:09 +01:00
Nikolaj Bjorner
881f90d17d remove simplify dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-26 00:48:49 -07:00
Nikolaj Bjorner
a7bb41fd49 fix build issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-24 09:19:35 -07:00
Nikolaj Bjorner
7dd28781ab remove simplifier dependencies from cmakelist.txt files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-23 16:33:36 -07:00
Nikolaj Bjorner
655b3d9c19 removing dependency on simplifier in pattern_inference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-23 12:17:30 -07:00
Arie Gurfinkel
88a35119b9 moved obj_equiv_class to ast 2017-08-01 19:24:50 -04:00
Nikolaj Bjorner
22a2aae486 trying to fix build break on use of iterator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 11:47:55 -07:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Arie Gurfinkel
f465a2225a fixing include paths 2017-07-31 17:14:43 -04:00
Arie Gurfinkel
7168451201 eager quantifier instantiation for quantified array properties 2017-07-31 17:04:16 -04:00
Arie Gurfinkel
2c7a39d580 Optionally blast arrays 
This changes the default behavior of always blasting arrays.
The old behavior can be restored using

   fixedpoint.xform.array_blast=true
 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
f5fa6b0bcb optionally disable subsumption checker 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
33c81524d2 optionally disable propagate variable equivalences in interp_tail_simplifier 2017-07-31 17:03:18 -04: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