mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
7763 commits 49 branches 53 tags 182 MiB
Commit graph

1307 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
93a20d9074 ML API: build fixes 2015-01-19 17:17:10 +00:00
Christoph M. Wintersteiger
42f12ed752 ML API: added interpolation, bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:16:37 +00:00
Christoph M. Wintersteiger
94a8c271d4 ML API bugfix for datatype module (Issue #120). Thanks to user Elarnon for reporting this! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:14:05 +00:00
Christoph M. Wintersteiger
7ec8c81c33 ML API fix for datatype construction (Issue #121). Thanks to Elarnon for reporting this one! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:14:03 +00:00
Christoph M. Wintersteiger
a8f703e034 ML API bugfix. Thanks to Martin Neuhaeusser for reporting this one! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:14:02 +00:00
Christoph M. Wintersteiger
5e2a7e06fd ML API: added constructors for ast_map and ast_vector 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:14:01 +00:00
Christoph M. Wintersteiger
9160925c28 ML API: added Expr.equal and Expr.compare 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:14:00 +00:00
Christoph M. Wintersteiger
a73a66b79c ML API bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:13:59 +00:00
Christoph M. Wintersteiger
e7345f5ea8 ML API bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:13:58 +00:00
Christoph M. Wintersteiger
83690a8fe3 ML API doc fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:13:57 +00:00
Christoph M. Wintersteiger
cc40105919 ML API doc fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:13:55 +00:00
Christoph M. Wintersteiger
409a40a562 ML API: Added get_bit_int and get_ratio 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:13:51 +00:00
Christoph M. Wintersteiger
3d9ad51aae ML API refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:11:18 +00:00
Christoph M. Wintersteiger
eb72afabfb ML API or' is deprecated, changed to ||' 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:11:15 +00:00
Christoph M. Wintersteiger
9dc8021995 Added facilities for ocamlfind in the ML API build 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:11:15 +00:00
Christoph M. Wintersteiger
ee22d40542 ML API bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:40 +00:00
Christoph M. Wintersteiger
54b7f8eec3 ML API bugfix (Codeplex issue 102) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:39 +00:00
Christoph M. Wintersteiger
983a0fb16f ML bindings: list/array are now called z3array/z3list to avoid confusion. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:35 +00:00
Christoph M. Wintersteiger
544a74f034 ML API: bug and build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:34 +00:00
Christoph M. Wintersteiger
e40b69d97f ML API: removing rich layer for now. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:32 +00:00
Christoph M. Wintersteiger
b81bae76b2 ML API: refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:32 +00:00
Christoph M. Wintersteiger
aaa835484f Updates to ML API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:31 +00:00
Christoph M. Wintersteiger
c1e29dabe7 ML API: renamed assert_ to add 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:15 +00:00
Christoph M. Wintersteiger
eea13a087f ML API savegame 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:14 +00:00
Christoph M. Wintersteiger
d293b579f3 ML API: flat & rich layer in place. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:13 +00:00
Christoph M. Wintersteiger
79d0c32c91 ML API: replaced arrays with lists. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:12 +00:00
Christoph M. Wintersteiger
303b4e6735 ML API savepoint 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:11 +00:00
Christoph M. Wintersteiger
dc03e2903f ML API: proper use of datatype API for list/enum/constructor. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:10 +00:00
Christoph M. Wintersteiger
6842acbea8 ML API: Cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:10 +00:00
Christoph M. Wintersteiger
dcdcd7b140 ML API: Build system and error handling fixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:09 +00:00
Christoph M. Wintersteiger
9142901efe ML API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:08 +00:00
Christoph M. Wintersteiger
fd78e45a2a ML API: got rid of "extra" objects on types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:07 +00:00
Christoph M. Wintersteiger
4e8d05dcf6 ML API: formatting. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:07 +00:00
Christoph M. Wintersteiger
7ec027dadb ML API: basic structure and interface 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:07:52 +00:00
Christoph M. Wintersteiger
7eedf15561 ML API: documentation fixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:50 +00:00
Christoph M. Wintersteiger
9845c8ee26 ML API: No more objects; type hierarchy exposed; clean separation into modules. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:49 +00:00
Christoph M. Wintersteiger
12afbfe6db Checkpoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:48 +00:00
Christoph M. Wintersteiger
313ccfbe8d Checkpoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:47 +00:00
Christoph M. Wintersteiger
3a0af6d15f ML API: Added Solver.assert_and_track 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:23 +00:00
Christoph M. Wintersteiger
b895d4c826 ML API: added functions for global parameter management. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:22 +00:00
Christoph M. Wintersteiger
8d1413bcc8 ML API: Symbols are now normal types with visible hierarchy. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:19 +00:00
Christoph M. Wintersteiger
1b3e1d1a6c ML API: moved more objects into normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:19 +00:00
Christoph M. Wintersteiger
3347d7ca8c ML API: moved more objects into normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:18 +00:00
Christoph M. Wintersteiger
6257c56901 ML API: bugfixes; starting to replace objects with normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:18 +00:00
Christoph M. Wintersteiger
1e2b546b03 ML API: changed context from object to normal type. Removed optional array parameters. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:17 +00:00
Christoph M. Wintersteiger
49dd2e4a07 ML API: build system changes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:03:40 +00:00
Christoph M. Wintersteiger
e2f6b10e32 ML API bugfixes 
More ML examples

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:02:17 +00:00
Christoph M. Wintersteiger
c03d5277bc more ML 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:36 +00:00
Christoph M. Wintersteiger
25498345e5 New ML API bugfixes and first example. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:36 +00:00
Christoph M. Wintersteiger
c2ff90720e ML API: mk_context added. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:35 +00:00