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

4652 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
4db8db7484 extend tracing for rule transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-25 12:40:16 -07:00
Nikolaj Bjorner
5c145dcd4b fix parameter checking on quantifiers (thanks to Esteban Pavese), fix query tracking in rel_context (thanks to Nuno Lopes), fix counter for free variables under quantfiers (thanks to Tomer Weiss) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-22 15:00:52 -07:00
Nikolaj Bjorner
0b56440cba fix convex converter for multi-arity addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-19 19:48:09 -07:00
Nikolaj Bjorner
e9ad4ab584 fix scaling 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-19 18:57:10 -07:00
Nikolaj Bjorner
7c9e3c3b70 debug scale transformer, add model converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-19 14:44:34 -07:00
Nikolaj Bjorner
bdee860622 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-08-19 11:53:57 -07:00
Nikolaj Bjorner
3b1344f681 working on scale transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-19 11:53:35 -07:00
Nikolaj Bjorner
e43383b6a8 filter query predicates from models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-18 21:11:14 -07:00
Ken McMillan
07bb534d65 some duality fixes 2013-08-16 18:38:24 -07:00
Nikolaj Bjorner
7bbabcdf6d updated documentation for finite domain sizes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-16 14:47:48 -07:00
Nikolaj Bjorner
01d59d2c91 fix bugs reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-15 18:36:27 -07:00
Nikolaj Bjorner
8f515ef356 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-08-14 17:56:26 -07:00
Nikolaj Bjorner
04678d9628 improve error message when sorts are non-numeric 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-14 17:56:07 -07:00
Nikolaj Bjorner
6c5f7741b2 more on polynorm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-14 11:55:23 -07:00
Nikolaj Bjorner
0fd94a033f change non-null test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-12 09:52:10 -07:00
Nikolaj Bjorner
f82d055e60 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-08-12 08:55:48 -07:00
Nikolaj Bjorner
661fe7eec9 add missing detach in coi_filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-11 19:10:46 -07:00
Nikolaj Bjorner
6a820adfed fix logic for adding cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-11 09:43:17 -07:00
Nikolaj Bjorner
0f83e7a251 fix bug masked by default configuration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-10 12:23:34 -07:00
Nikolaj Bjorner
1c3f715e26 switch between convex and interior hull, add multiple cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-10 12:21:49 -07:00
Nikolaj Bjorner
a20656de35 fix unused variable warning in unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-10 10:57:25 -07:00
Nikolaj Bjorner
e7f458101c add normalizer of monomial coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-10 10:53:46 -07:00
Nikolaj Bjorner
d94f1b3fd6 add normalizer of monomial coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-10 10:50:03 -07:00
Nikolaj Bjorner
3b64265c27 remove duplicated definition of is_store and is_select 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-09 09:15:04 -07:00
Nikolaj Bjorner
c2b26300fb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-08-09 09:00:52 -07:00
Nikolaj Bjorner
cb06ce295e add comments to generalizer code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-09 09:00:40 -07:00
Nikolaj Bjorner
30df2837fb fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-08 15:38:13 -07:00
Nikolaj Bjorner
af700e88cf fix coi filter to consider 0 cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-08 15:02:18 -07:00
Nikolaj Bjorner
a0d79c8dd7 fix coi filter to consider 0 cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-08 15:01:35 -07:00
Nikolaj Bjorner
dc58bce052 initial test for polynormalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-08 14:09:45 -07:00
Nikolaj Bjorner
0595fe8cec remove tracing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-08 09:36:31 -07:00
Nikolaj Bjorner
85391b6f35 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-08-07 19:58:44 -07:00
Nikolaj Bjorner
5b9ec3dec7 add scoped class for controlling Farkas generalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-07 19:58:21 -07:00
Nikolaj Bjorner
ec22156ae1 fix bug in get_answer reported by Anvesh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-07 14:52:34 -07:00
Nikolaj Bjorner
a7ed218636 generalize ackerman reduction to work with nested terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-07 13:16:46 -07:00
Christoph M. Wintersteiger
092dfa396a Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-08-07 15:22:06 +01:00
Nikolaj Bjorner
327b2bbe9c add control over Farkas parameter for Arie 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-07-17 00:03:38 +04:00
Nikolaj Bjorner
0cd3c3364b add control over Farkas parameter for Arie 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-07-16 23:42:50 +04:00
Nikolaj Bjorner
f1d3a13b7f add missing case handlers for internal bit-vector operators that leak during simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-07-16 11:46:29 +04:00
Christoph M. Wintersteiger
bbdcf2deaa Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-07-15 12:22:12 +01:00
Christoph M. Wintersteiger
6ce0e7cf25 .NET build changes to include /linkresource 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-07-15 12:22:01 +01:00
Nikolaj Bjorner
9a49f5f204 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-07-10 17:21:16 +03:00
Nikolaj Bjorner
784455d1fc detect approximate relations to return unknown, fix product relations, fix symbolic magic set transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-07-10 17:20:44 +03:00
Leonardo de Moura
9879d8aa62 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-07-09 08:22:30 -07:00
Leonardo de Moura
ccb36f1ae7 Fix issue https://z3.codeplex.com/workitem/54 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-09 08:22:17 -07:00
Christoph M. Wintersteiger
210bca8f45 .NET Example: Sudoku example bugfix. Many thanks to Ilya Mironov for reporting this issue. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-07-02 12:57:54 +01:00
Leonardo de Moura
b7c2d9054b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-28 19:21:34 -07:00
Leonardo de Moura
d9941c0ccc Add code for rejecting bitvector constants of size 0 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-28 19:21:27 -07:00
Christoph M. Wintersteiger
10df5e950d Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-28 12:14:53 +01:00
Christoph M. Wintersteiger
9dfd202fdb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-28 12:14:33 +01:00