mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
1904 commits 49 branches 53 tags 182 MiB
Commit graph

1904 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
01dc79fcd4 More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:42:20 +00:00
Christoph M. Wintersteiger
bea09539cf More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:42:18 +00:00
Christoph M. Wintersteiger
2dde851ed7 More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:42:16 +00:00
Christoph M. Wintersteiger
a965d65901 ML API temp files added to .gitignore 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:41:17 +00:00
Christoph M. Wintersteiger
d5f135c432 More new ML API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:40:52 +00:00
Christoph M. Wintersteiger
8d30fabc0a New native ML API layer. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:40:40 +00:00
Christoph M. Wintersteiger
65ddf2be49 More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:40:39 +00:00
Christoph M. Wintersteiger
f5a0520b83 More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:40:37 +00:00
Christoph M. Wintersteiger
03a5c88ded More new ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:40:10 +00:00
Christoph M. Wintersteiger
70f0d2f423 Beginnings of a new ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:38:52 +00:00
Nikolaj Bjorner
9790784488 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-01-18 04:50:20 +05:30
Nikolaj Bjorner
6af9782927 set default file format to smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-18 04:50:00 +05:30
Christoph M. Wintersteiger
67e04c5dfb Python example: removed function that has no body. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-16 17:40:28 +00:00
Christoph M. Wintersteiger
bb722b24c1 Added call to memory::finalize() to ease memory leak debugging 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-16 17:34:01 +00:00
Nikolaj Bjorner
b9bbfbdbb7 fix interval dependencies bug. Codeplex issue 163 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-16 12:05:12 +05:30
Nikolaj Bjorner
ec384d3d31 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-01-15 17:23:37 +05:30
Nikolaj Bjorner
dbc9bebd18 fix instance test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-15 16:47:10 +05:30
Christoph M. Wintersteiger
376614a782 Java API: slight overhaul in preparation for the FP additions 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-03 15:09:52 +00:00
Christoph M. Wintersteiger
8e7278f02c Java API: Removed unnecessary imports 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-02 18:10:47 +00:00
Christoph M. Wintersteiger
9dd4d7b011 Python API bugfix. Thanks to Tom Ball for reporting this one. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-21 20:43:26 +00:00
Nikolaj Bjorner
18c3c1d9d6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-12-16 11:21:24 -08:00
Nikolaj Bjorner
f4d256ef30 fix issue 153: assert rem/mod axiom no matter what is status of second argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-16 11:20:34 -08:00
Christoph M. Wintersteiger
d53fdb2848 typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-16 15:36:31 +00:00
Christoph M. Wintersteiger
1244d5a22e Python API: Added BVRedAnd, BVRedOr 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-16 15:28:52 +00:00
Ken McMillan
882dbfc706 merge 2014-12-08 16:16:52 -08:00
Ken McMillan
8181b15a1b attempted interp fixes 2014-12-08 15:46:55 -08:00
Nikolaj Bjorner
45755bbd14 fix context sensitivity. Codeplex issue 148, thanks to clockish 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-03 08:55:14 +09:00
Christoph M. Wintersteiger
61c59fb4bf Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-12-02 14:35:29 +00:00
Christoph M. Wintersteiger
c88b2f6b5e .NET API: Added build instructions for .NET 3.5 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-02 14:35:15 +00:00
Nuno Lopes
1a396b0bd2 [BV size reduction] fix bug in detection of signed upperbound 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-11-25 18:13:24 +00:00
Christoph M. Wintersteiger
59dfd2abe4 fixed problem with Python 3.4.x complainging of inconsistent use of spaces/tabs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-25 14:54:47 +00:00
Christoph M. Wintersteiger
53cfa47214 bugfix for bv_size_reduction 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-25 14:22:50 +00:00
Christoph M. Wintersteiger
213d816c0a Bugfix for bv_size_reduction. Thanks to user rsas for reporting this isse! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-24 18:10:54 +00:00
Nikolaj Bjorner
4c5753f321 be classy with your friends 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-13 18:08:24 -08:00
Nikolaj Bjorner
025d6c3108 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-11-12 20:28:36 -08:00
Nikolaj Bjorner
a309dbfdc2 coerce equality and ite upward instead of downward for int2real coercions. Fixes bug reported by Enric Carbonell 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-12 20:28:11 -08:00
Christoph M. Wintersteiger
005bb82a17 eliminated unused variables 2014-11-07 16:04:02 +00:00
Nikolaj Bjorner
cf8ad072d0 remove unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-07 16:03:27 +01:00
Nikolaj Bjorner
ce7303b5e2 fix reset logic and load only logics admitted by context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-07 15:44:21 +01:00
Nikolaj Bjorner
23bc982ad2 move initialization to support more sort usage scenarios 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-06 16:53:51 +01:00
Nikolaj Bjorner
adeae18471 delay initializing internal manager so that parser does not choke on proper SMT-LIB logics. Reported by Venkateshan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-06 13:09:25 +01:00
Christoph M. Wintersteiger
591f6d096f .NET API project directories fixed. Thanks to Marc Brockschmidt for reporting this. 2014-11-03 14:53:48 +00:00
Nikolaj Bjorner
e002fc680f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-31 14:24:35 +01:00
Nikolaj Bjorner
b4600ffda0 add print to SMT-LIB format from solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-31 14:24:21 +01:00
Ken McMillan
a6f58bdd17 fixes and performance improvements for interp and duality 2014-10-30 17:22:34 -07:00
Christoph M. Wintersteiger
f50a8b0a59 Bumped version number. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-25 17:05:02 +01:00
Christoph M. Wintersteiger
6b51f7a610 Added item to release notes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-25 16:59:24 +01:00
Christoph M. Wintersteiger
cb3e9c9644 Bugfix for FPA models 2014-10-25 16:58:16 +01:00
Christoph M. Wintersteiger
0713535fa6 Documentation website fixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 21:00:23 +01:00
Ken McMillan
61905a10db merge interp change 2014-10-24 11:54:00 -07:00