mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity
3446 commits 23 branches 48 tags 157 MiB
Commit graph

2869 commits

Author SHA1 Message Date
Nuno Lopes 6ab167f0c7 fix debug build 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-01-25 18:31:04 +00:00
Nikolaj Bjorner 37fca65517 fuse join with projection avoiding double insert (but at cost of double projection) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-25 04:37:42 -08:00
Nikolaj Bjorner 761c7d9a40 adding annotation to logging to show number of columns and rows, adding dual propagation sketch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-25 04:01:18 -08:00
Christoph M. Wintersteiger b92bdaeebe ML API readme fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:51:47 +00:00
Christoph M. Wintersteiger 2f3ea1f39d removed legacy ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:48:51 +00:00
Christoph M. Wintersteiger 5c7d0380d3 Fixes in the OCaml FPA API and example 2015-01-24 18:29:52 +00:00
Christoph M. Wintersteiger 1c9051016a Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 
Conflicts:
	scripts/mk_util.py
 2015-01-24 18:29:03 +00:00
Christoph M. Wintersteiger 9cb50c9f28 FPA API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 17:33:26 +00:00
Christoph M. Wintersteiger 5f527fa562 documentation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 15:54:32 +00:00
Nikolaj Bjorner aae37c2317 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-01-23 13:06:27 -08:00
Nikolaj Bjorner 552cbd840f adding soft-assertions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-23 13:06:11 -08:00
Andrey Rybalchenko 044f2a93e7 fix build with gcc 2015-01-23 19:53:14 +00:00
Christoph M. Wintersteiger 65ccc9a8ea added FPA ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 19:36:47 +00:00
Christoph M. Wintersteiger 145e025959 FPA API naming consistency 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 18:14:49 +00:00
Christoph M. Wintersteiger 89bfbd38c8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 17:11:57 +00:00
Christoph M. Wintersteiger 06051989be FPA API: Naming consistency 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 17:11:12 +00:00
Nuno Lopes 036a56e360 DoC: remove another unused variable 2015-01-23 17:09:17 +00:00
Christoph M. Wintersteiger 3bf3de17e9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 17:04:18 +00:00
Nuno Lopes 93db50ff64 DoC: further code simplifications 2015-01-23 17:04:09 +00:00
Christoph M. Wintersteiger 3d91510565 FPA API: naming consistency fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 17:03:56 +00:00
Nuno Lopes 92f6dd4de4 DoC: factorize join and join_project code so that join_project learns need tricks (i.e., prune empty vectors upfront) 2015-01-23 16:55:02 +00:00
Christoph M. Wintersteiger 724e04174e Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 15:32:01 +00:00
Christoph M. Wintersteiger 8cd69acaca build fix 2015-01-23 11:34:08 +00:00
Christoph M. Wintersteiger ffd10675f4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 11:07:48 +00:00
Christoph M. Wintersteiger 0c2e2d78dd renamed function to avoid compilation issues 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-22 18:52:28 +00:00
Christoph M. Wintersteiger 034e4f469e Fixed memory leak 2015-01-22 18:43:23 +00:00
Christoph M. Wintersteiger c3ff342bea Bugfixes for the Python FPA API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-22 18:31:30 +00:00
Christoph M. Wintersteiger 0ab54b9e0c bugfix for FPA numerals 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 19:43:26 +00:00
Christoph M. Wintersteiger 880cbb936e fixed portability issue 2015-01-21 19:37:49 +00:00
Christoph M. Wintersteiger 560fa79d1f eliminated unused variable 2015-01-21 19:36:41 +00:00
Christoph M. Wintersteiger 25011bc034 eliminated unused variables 2015-01-21 19:35:29 +00:00
Christoph M. Wintersteiger 826d295981 build fixes and removed unused variables 2015-01-21 19:29:31 +00:00
Christoph M. Wintersteiger 84ed1c19a0 Bugfixes for the Java FPA API 
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 19:20:43 +00:00
Christoph M. Wintersteiger 42162f1ea5 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-01-21 19:10:34 +00:00
Christoph M. Wintersteiger bf28eb32c6 Merge branch 'fpa-api' of https://git01.codeplex.com/z3 into unstable 2015-01-21 19:09:48 +00:00
Christoph M. Wintersteiger b6a7d60043 Added FPA functions to Java API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 19:09:22 +00:00
Christoph M. Wintersteiger 95300e801d fixed build errors and warnings 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 18:24:36 +00:00
Christoph M. Wintersteiger 71042bbf6d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-01-21 18:04:11 +00:00
Christoph M. Wintersteiger 2cb84280d8 Final adjustments for the FP integration 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 17:58:31 +00:00
Christoph M. Wintersteiger 1209302fe6 Fixed integration issues 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 15:34:21 +00:00
Christoph M. Wintersteiger 9a53fe43e6 Removed unnecessary #includes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 15:31:12 +00:00
Christoph M. Wintersteiger 74e60fc955 disabled debug output 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 15:01:35 +00:00
Christoph M. Wintersteiger e5c5c801c7 fixed botched merge 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 14:40:18 +00:00
Christoph M. Wintersteiger d56d63e3e8 Merge branch 'fpa-api' of https://git01.codeplex.com/z3 into unstable 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

Conflicts:
	src/tactic/portfolio/default_tactic.cpp
 2015-01-21 14:25:31 +00:00
Christoph M. Wintersteiger 079204d1aa FPA Python API cosmetics 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 14:22:47 +00:00
Christoph M. Wintersteiger 052baaabe4 FPA API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 14:22:35 +00:00
Christoph M. Wintersteiger d0a7246f00 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-21 13:51:00 +00:00
Christoph M. Wintersteiger ae792f1891 avoid spurious warning message 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:47:32 +00:00
Christoph M. Wintersteiger a603f76b6c BV-SLS build fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:47:17 +00:00
Christoph M. Wintersteiger e20dc9f9a4 typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:35:25 +00:00
Christoph M. Wintersteiger 71e5f03b44 build fix 2015-01-21 13:04:05 +00:00
Christoph M. Wintersteiger 83023c7211 build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:02:18 +00:00
Nikolaj Bjorner e50e02e656 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-01-20 16:38:55 -08:00
Nikolaj Bjorner e24db56650 integrating new integer primal loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-20 16:38:45 -08:00
Nikolaj Bjorner f1d9228b94 fix bug in context push/pop for sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-20 16:30:46 -08:00
Christoph M. Wintersteiger 0746ede537 BV SLS: Final adjustments 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:59:25 +00:00
Christoph M. Wintersteiger 61ba7f5e09 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into unstable 
Conflicts:
	src/tactic/portfolio/default_tactic.cpp

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:15:31 +00:00
Christoph M. Wintersteiger d20c7bc9ee Added is_qfaufbv_probe and is_qfauflia_probe. 
Potential performance disruption for some users:
Changed default_tactic to call the respective tactics,
where previously they would have run the default 'smt'
tactic.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 18:19:43 +00:00
Christoph M. Wintersteiger d8f90802c0 Added FPA setup to default kernel setup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 18:14:22 +00:00
Christoph M. Wintersteiger e754aa1c11 Minor adjustments after rebasing ml-ng onto unstable. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:17:58 +00:00
Christoph M. Wintersteiger 011b700c20 ML API: build fix 2015-01-19 17:17:13 +00:00
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
Christoph M. Wintersteiger 77679dc1f5 More new ML API; Status: everything is there except for error handling. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:34 +00:00
Christoph M. Wintersteiger 49a4e77a6d More new ML API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:34 +00:00
Christoph M. Wintersteiger f1ecf3ae0b New ML API savepoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:33 +00:00
Christoph M. Wintersteiger 954d92a513 More new ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:32 +00:00
Christoph M. Wintersteiger 2a6c74bc13 New ML API savepoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:32 +00:00
Christoph M. Wintersteiger c28f0e7c8a ML API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:31 +00:00
Christoph M. Wintersteiger a2ad7d91bc New ML API savepoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:31 +00:00
Christoph M. Wintersteiger 7ae90f0b20 More ML API: 
Fixes in native layer.
Added symbols.
Prepared code for automatic documentation.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:29 +00:00
Christoph M. Wintersteiger d8ed9be98e ML native layer bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:00:22 +00:00
Christoph M. Wintersteiger cfa099007a ML build system checks 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:59:51 +00:00
Christoph M. Wintersteiger 18a57267d1 added temporary Makefile for ML annotations. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:57:11 +00:00
Christoph M. Wintersteiger 1685e3dd6f ML API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:57:10 +00:00
Christoph M. Wintersteiger 50560ba791 more ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:56:43 +00:00
Christoph M. Wintersteiger 0e98d26721 ML API and example compilation. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:56:42 +00:00
Christoph M. Wintersteiger f614f6824e More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:55:23 +00:00
Christoph M. Wintersteiger f7b3529f01 More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:55:22 +00:00
Christoph M. Wintersteiger d2d4bf7f83 More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:53:56 +00:00
Christoph M. Wintersteiger 1ef9013c8e More new ML API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:50:44 +00:00
Christoph M. Wintersteiger a40433aae8 More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:13:58 +00:00
Christoph M. Wintersteiger 90cb046684 Beginnings of a new ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:12:13 +00:00
Christoph M. Wintersteiger ae2c4d738c ML API: build fix 2015-01-19 16:08:37 +00:00
Christoph M. Wintersteiger f0d66388d4 ML API: build fixes 2015-01-19 16:08:34 +00:00
Christoph M. Wintersteiger 16ba29e991 ML API: added interpolation, bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:36 +00:00
Christoph M. Wintersteiger 30a30e8dd0 ML API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:35 +00:00
Christoph M. Wintersteiger 45ec0c1b99 ML API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:33 +00:00
Christoph M. Wintersteiger 2a67befe9d ML API: added .cmxs to the distribution. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:31 +00:00
Christoph M. Wintersteiger d84e728f7a 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 16:07:08 +00:00
Christoph M. Wintersteiger 8bd4ea293e 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 16:07:07 +00:00
Christoph M. Wintersteiger bcbfaad3cc ML API bugfix. Thanks to Martin Neuhaeusser for reporting this one! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:06 +00:00
Christoph M. Wintersteiger ce94a8b2e0 ML API: added constructors for ast_map and ast_vector 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:05 +00:00
Christoph M. Wintersteiger 1c34842ca6 ML API: added Expr.equal and Expr.compare 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:05 +00:00
Christoph M. Wintersteiger 4c54b6816a ML API bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:04 +00:00
Christoph M. Wintersteiger 2a67301c50 ML API bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:03 +00:00
Christoph M. Wintersteiger 47997e175f ML API doc fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:02 +00:00
Christoph M. Wintersteiger d8a84c9f89 ML API doc fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:01 +00:00
Christoph M. Wintersteiger e2f0dc31f4 ML API: Added get_bit_int and get_ratio 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:06:59 +00:00
Christoph M. Wintersteiger 10fe6b7759 ML API refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:04:40 +00:00
Christoph M. Wintersteiger 20be39006e ML API or' is deprecated, changed to ||' 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:02:38 +00:00
Christoph M. Wintersteiger 0da912e557 ML API bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:01:37 +00:00
Christoph M. Wintersteiger 832e119b98 ML API bugfix (Codeplex issue 102) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:01:36 +00:00
Christoph M. Wintersteiger 2ee3ff518f ML bindings: list/array are now called z3array/z3list to avoid confusion. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:00:30 +00:00
Christoph M. Wintersteiger 3e336592a2 ML API: bug and build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:00:29 +00:00
Christoph M. Wintersteiger 755ba2a2f7 ML API: removing rich layer for now. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:00:28 +00:00
Christoph M. Wintersteiger 9726ee4c5f ML API: refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:00:28 +00:00
Christoph M. Wintersteiger c0df764039 Updates to ML API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:57:38 +00:00
Christoph M. Wintersteiger 17005a413b Removed unnecessary file 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:57:21 +00:00
Christoph M. Wintersteiger c37eb794c2 ML API: renamed assert_ to add 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:57:20 +00:00
Christoph M. Wintersteiger 13416de27e ML API savegame 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:55:52 +00:00
Christoph M. Wintersteiger 6417f9e648 ML API: flat & rich layer in place. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:54:46 +00:00
Christoph M. Wintersteiger a0f6d1d3df ML API: replaced arrays with lists. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:54:28 +00:00
Christoph M. Wintersteiger 576591086d ML API savepoint 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:54:11 +00:00
Christoph M. Wintersteiger 9d15c95856 ML API: proper use of datatype API for list/enum/constructor. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:53:58 +00:00
Christoph M. Wintersteiger 2af1f81ae1 ML API: Cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:53:42 +00:00
Christoph M. Wintersteiger 09aa02759f ML API: Build system and error handling fixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:53:21 +00:00
Christoph M. Wintersteiger fd2ae5f60e ML API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:53:20 +00:00
Christoph M. Wintersteiger a27945f297 ML API: got rid of "extra" objects on types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:53:17 +00:00
Christoph M. Wintersteiger 23febf13c4 ML API: basic structure and interface 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:52:08 +00:00
Christoph M. Wintersteiger 34a72942bf ML API: documentation fixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:48 +00:00
Christoph M. Wintersteiger 276c5a5cdc ML API: No more objects; type hierarchy exposed; clean separation into modules. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:47 +00:00
Christoph M. Wintersteiger 0138d0c11c Checkpoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:46 +00:00
Christoph M. Wintersteiger 7b51dc9bdd Checkpoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:45 +00:00
Christoph M. Wintersteiger 1eae7a6bac ML API: Added Solver.assert_and_track 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:44 +00:00
Christoph M. Wintersteiger 7befc262d1 ML API: added functions for global parameter management. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:43 +00:00
Christoph M. Wintersteiger 69138924e5 ML API: Symbols are now normal types with visible hierarchy. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:40 +00:00
Christoph M. Wintersteiger d0fea5e740 ML API: moved more objects into normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:39 +00:00
Christoph M. Wintersteiger bcc0c14233 ML API: moved more objects into normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:39 +00:00
Christoph M. Wintersteiger bbd1e465bb ML API: bugfixes; starting to replace objects with normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:38 +00:00
Christoph M. Wintersteiger 0e59d05629 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 15:51:37 +00:00
Christoph M. Wintersteiger 9eea0f3232 ML API: build system changes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:33 +00:00
Christoph M. Wintersteiger 597409c8ac ML API bugfixes 
More ML examples

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:55 +00:00
Christoph M. Wintersteiger cef9c2fa69 more ML 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:23 +00:00
Christoph M. Wintersteiger bffef2e808 New ML API bugfixes and first example. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:22 +00:00
Christoph M. Wintersteiger a42e21ede1 ML API: mk_context added. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:21 +00:00
Christoph M. Wintersteiger 39e538a8bc More new ML API; Status: everything is there except for error handling. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:21 +00:00
Christoph M. Wintersteiger 371db347af More new ML API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:20 +00:00
Christoph M. Wintersteiger 3684b3a87d New ML API savepoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:19 +00:00
Christoph M. Wintersteiger d6a2048785 More new ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:19 +00:00
Christoph M. Wintersteiger 524336ea3e New ML API savepoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:18 +00:00
Christoph M. Wintersteiger 2277ad3654 ML API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:18 +00:00
Christoph M. Wintersteiger dab162886e New ML API savepoint. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:17 +00:00
Christoph M. Wintersteiger fc227e3c96 .NET API documentation bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:16 +00:00
Christoph M. Wintersteiger 794823ba6d More ML API: 
Fixes in native layer.
Added symbols.
Prepared code for automatic documentation.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:16 +00:00
Christoph M. Wintersteiger 7efe7a2c16 ML native layer bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:48:40 +00:00
Christoph M. Wintersteiger 8e83f8d034 ML build system checks 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:46:54 +00:00
Christoph M. Wintersteiger 518da6b6e2 move old files 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:44:44 +00:00
Christoph M. Wintersteiger e87feb8e45 added temporary Makefile for ML annotations. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:44:42 +00:00
Christoph M. Wintersteiger b193b827ed ML API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:44:42 +00:00
Christoph M. Wintersteiger 0fad5abd19 more ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:43:28 +00:00
Christoph M. Wintersteiger c001da6188 ML API and example compilation. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:42:23 +00:00