mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
4083 commits 49 branches 53 tags 182 MiB
Commit graph

4083 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
271c143de5 update unstable branch with qhc changes that don't have dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-12-10 11:13:04 -08:00
Leonardo de Moura
8bfbdf1e68 fixing clang warnings on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 19:04:21 +00:00
Leonardo de Moura
7f210d55be fixed warnings on Win64 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 07:52:33 -08:00
Leonardo de Moura
8015d8b79a Updated Java README 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 07:52:14 -08:00
Leonardo de Moura
99d0449272 added Java docs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 07:51:45 -08:00
Leonardo de Moura
4981134fd7 Fixing VS warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 06:52:56 -08:00
Leonardo de Moura
1fb0fec7d1 improved jni.h detection 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 06:43:57 -08:00
Leonardo de Moura
af37aa2743 improving java bindings build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-10 06:30:26 -08:00
Leonardo de Moura
840d0aef6d fixed bug in generated code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 18:59:32 -08:00
Leonardo de Moura
ed97a3a180 merged 2012-12-09 16:49:14 -08:00
Leonardo de Moura
d6a1ea82e1 exposed subresultants aka psc-chain procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 16:47:37 -08:00
Leonardo de Moura
84aeba94a5 merged 2012-12-09 15:06:50 -08:00
Leonardo de Moura
6ae6414236 avoiding clang warning messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 15:04:14 -08:00
Leonardo de Moura
9b7946e52d added method for creating ast_manager based on context_params configuration 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 14:24:37 -08:00
Leonardo de Moura
84e79035cb Updated release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 12:24:14 -08:00
Leonardo de Moura
33234a4162 Fixed issue http://z3.codeplex.com/workitem/10 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 12:23:35 -08:00
Leonardo de Moura
7ffba3ebf4 more examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-09 08:02:12 -08:00
Leonardo de Moura
7a31c6bc74 exposed root isolation algorithm in the API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 21:07:17 -08:00
Leonardo de Moura
0d230375be added polynomial evaluation at algebraic point 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 20:39:16 -08:00
Leonardo de Moura
bf2340850a minor change 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 11:11:53 -08:00
Leonardo de Moura
277244098c Adding python interface for computing with algebraic numbers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 10:57:05 -08:00
Leonardo de Moura
47edff2076 fixed bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-08 08:32:06 -08:00
Leonardo de Moura
189fc46b6d working on api for algebraic numbers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 19:06:48 -08:00
Leonardo de Moura
4e2a9e7caf working on api 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 18:44:03 -08:00
Leonardo de Moura
c011b05b61 exposing algebraic numbers in the API (working in progress) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 17:48:57 -08:00
Leonardo de Moura
c350943c78 fixed bug introduced today 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 15:59:54 -08:00
Leonardo de Moura
cba449b75e more parameter issues 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 15:16:46 -08:00
Leonardo de Moura
a07b459fdf Added is_unique_value. Its semantics is equal to the old is_value method. The contract for is_value changed. See comments at ast.h for more information. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 12:53:51 -08:00
Leonardo de Moura
bd0366eef7 Fixed problems in the new parameter setting. Many thanks to Nuno Lopes for sending a benchmark that exposed the problem, a noticing the discrepancy between unstable and master branches. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 11:09:14 -08:00
Leonardo de Moura
e055e0b47c Fixed other parameter setting problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 10:41:50 -08:00
Leonardo de Moura
0a1ba9a9e0 added openmp test, stopped using the compiler name to decide whether openmp will be used or not. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 09:27:19 -08:00
Leonardo de Moura
ac03c9eff7 chasing parameter setting bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 08:27:17 -08:00
Leonardo de Moura
60ebc5c4dd added missing #ifndef to automatically generated hpp files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 06:59:54 -08:00
Leonardo de Moura
684f573c3c Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-07 06:08:25 -08:00
Leonardo de Moura
8d45de02c5 Fixed timer bug on freebsd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 06:07:57 -08:00
Leonardo de Moura
1ad7458d9f missing space 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 18:38:18 -08:00
Leonardo de Moura
5b2dced157 merged 2012-12-06 16:09:54 -08:00
Leonardo de Moura
44ae1a2d70 fixed problem reported by Dejan 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 16:09:10 -08:00
Leonardo de Moura
fc20eba945 another dir issue 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 15:46:36 -08:00
Leonardo de Moura
60b9207485 fixed more problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 15:40:31 -08:00
Leonardo de Moura
a430d53475 merged 2012-12-06 15:35:54 -08:00
Leonardo de Moura
26f616268e fixed warning in 32bit sys 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 15:35:28 -08:00
Leonardo de Moura
017176c720 fixed messy directory separator in mk_util 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 15:33:43 -08:00
Leonardo de Moura
db6e20b2ea cleaning mk_make 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 14:57:07 -08:00
Leonardo de Moura
fdb3e22560 fixed mk_make problem on Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 13:57:35 -08:00
Leonardo de Moura
bca0c0bb5f Merge branch 'contrib' of https://git01.codeplex.com/forks/nguyenthanhvuh/vuz3 into vu 2012-12-06 12:00:50 -08:00
Leonardo de Moura
9ab1210cc2 merged 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 11:05:49 -08:00
ThanhVu (Vu) Nguyen
72a250c01a moving my common z3 stuff to z3util.py … note the vset() call essentially returns a list with no duplicate elements, it's like set but allows the user to add in a function to compute the representation of the list elements. 2012-12-06 13:54:57 -05:00
Leonardo de Moura
68b97024e2 added missing option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 08:54:00 -08:00
Leonardo de Moura
75739fdf7b fixed memory smash 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-06 08:19:42 -08:00