mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-29 02:39:24 +00:00
Code Activity
1167 commits 46 branches 52 tags 179 MiB
Commit graph

266 commits

Author SHA1 Message Date
Leonardo de Moura
f46c7f9bd9 Fix the build on g++, Fix g++ warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-15 16:36:57 -08:00
Nikolaj Bjorner
a242ac46b6 hilbert validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-15 15:05:39 -08:00
Nikolaj Bjorner
aaf0c16e08 working on hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-15 09:09:58 -08:00
Nikolaj Bjorner
3a68affb1b cal modifications 2013-02-14 15:10:52 -08:00
Nikolaj Bjorner
6e7d04f94e working on hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-14 15:06:17 -08:00
Nikolaj Bjorner
0c641cdf95 hilbert basis experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-13 16:53:56 -08:00
Nikolaj Bjorner
1317a71a1a Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-13 09:42:12 -08:00
Nikolaj Bjorner
706cbd3872 hilbert basis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-12 21:45:20 -08:00
Nikolaj Bjorner
ff03da9e67 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-12 15:44:32 -08:00
Nikolaj Bjorner
0fc44a43e1 add hilbert basis utility for extracting auxiliary invariants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-12 14:58:44 -08:00
Nikolaj Bjorner
ce9a098f16 local changes to pdr_generalizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-09 10:58:37 -08:00
Nikolaj Bjorner
3ad43c60a9 working on pdr gen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-08 16:54:05 -08:00
Nikolaj Bjorner
9e868cdef3 fix pretty printer bug found by ken 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-08 16:04:46 -08:00
Nikolaj Bjorner
2e2fa84d40 experiment with arithmetic core generalizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-07 19:21:52 -08:00
Nikolaj Bjorner
0fd1c00053 fix reference counting bug in qe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-06 09:40:16 -08:00
Nikolaj Bjorner
8354c2dfb1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-06 08:10:32 -08:00
Nikolaj Bjorner
7fd4e7861f tidy verbose mode a bit, ackermannize special cases of arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-05 21:19:32 -08:00
Nikolaj Bjorner
6022d14b02 remove incorrect code for double loop with widening 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-05 15:03:45 -08:00
Nikolaj Bjorner
ca74b2d6cf towards acceleration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-02-01 10:36:23 -08:00
Nikolaj Bjorner
3c9c7574f7 add release mode to vs build, work on delta extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-31 17:32:07 -08:00
Nikolaj Bjorner
affea51c21 fix compilation warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-30 11:12:40 -08:00
Nikolaj Bjorner
0eea0bea9a update scoring function for tab context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-28 10:37:31 -08:00
Nikolaj Bjorner
8e2298c327 fix extraction of statistics for horn tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-25 19:24:48 -08:00
Nikolaj Bjorner
a6cf5281eb working on tab context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-24 19:20:08 -08:00
Nikolaj Bjorner
521382e37f working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-24 12:50:19 -08:00
Nikolaj Bjorner
d3025569c2 working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-24 12:45:58 -08:00
Leonardo de Moura
afaef63bfa Fix compilation error when using gcc. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 12:38:37 -08:00
Nikolaj Bjorner
c89531bcf8 working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-23 21:44:42 -08:00
Nikolaj Bjorner
b61c1b0ded working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-23 19:05:38 -08:00
Nikolaj Bjorner
085ccf5eff working on tab context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-21 22:28:25 -08:00
Nikolaj Bjorner
87e9015675 working on tab_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-20 18:41:41 -08:00
Nikolaj Bjorner
99f5a5bddb working on tab_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-18 17:36:42 -08:00
Nikolaj Bjorner
cab908bfef working on horn tab solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-18 09:56:35 -08:00
Nikolaj Bjorner
8daf100c65 working on tab Horn solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-17 18:03:34 -08:00
Nikolaj Bjorner
b19a47176b working on tab 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-17 08:17:21 -08:00
Nikolaj Bjorner
50bf845b40 add tabulation/subsumption engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-16 17:16:44 -08:00
Nikolaj Bjorner
f8f23382dc bug fix: unsound pruning of assumptions. remove deprecated reduce() feature from smt_kernel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-03 17:36:21 -08:00
Nikolaj Bjorner
eee4b1a37b fix g++ build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-02 20:17:33 -08:00
Nikolaj Bjorner
51a5d22f23 experiments wtih QHC 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-02 09:50:31 -08:00
Nikolaj Bjorner
d318aab7d1 experiments wtih QHC 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-02 09:49:27 -08:00
Nikolaj Bjorner
63b7f7ecd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-28 16:40:36 -08:00
Nikolaj Bjorner
9f2743309f fix to proof hypothesis removal facility reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-28 16:40:29 -08:00
Nikolaj Bjorner
c513f7e9c2 fixed slicing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-26 15:44:54 -08:00
Nikolaj Bjorner
8b8fb74fd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-26 11:31:09 -08:00
Nikolaj Bjorner
bc77a97e92 qe lite checks 2012-12-26 11:28:05 -08:00
Leonardo de Moura
7d97f407c2 Remove non-ascii characters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-20 11:22:03 -08:00
Leonardo de Moura
d92efeb0c5 Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 17:14:25 -08:00
Leonardo de Moura
607fab486c Fix incorrect uses of set_cancel() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 18:48:10 -08:00
Nikolaj Bjorner
1dfea1324e Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-14 16:55:04 -08:00
Nikolaj Bjorner
0a3f95bdaa quantifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-14 16:54:59 -08:00