mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 03:02:29 +00:00
Code Activity
11761 commits 49 branches 53 tags 180 MiB
Commit graph

1846 commits

Author SHA1 Message Date
Ken McMillan
9792f6dd33 more work on incorporating iz3 2013-03-04 18:41:30 -08:00
Leonardo de Moura
e8140f5c1f Fix compilation problems when using Visual Studio 32 bit compiler 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-26 12:34:52 -08:00
Christoph M. Wintersteiger
5fe58c2f2d Java API: renamed assert_(...) to add(...) 
.NET API: added alias Add(...) for Assert(...)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-26 19:13:48 +00:00
Leonardo de Moura
b2810592e6 Add enumeration_sort method to C++ API. Add as_expr method to goal class in C++ API. Add enum_sort_example to C++ examples/c++/example.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-26 08:29:01 -08:00
Christoph M. Wintersteiger
6075ae28fc ML/Java: Proper use of Datatype API for List/Enum/Constructor 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-20 19:40:48 +00:00
Leonardo de Moura
b4d57e0ab1 Merge branch 'unstable' into contrib 2013-02-19 15:35:05 -08:00
Leonardo de Moura
030aef5d5a Fix bug reported by Andrey Kupriyanov 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-14 09:55:42 -08:00
Christoph M. Wintersteiger
92e7384bf5 Java API: final adjustments 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-13 17:21:08 +00:00
Leonardo de Moura
3a15db5244 Fix uninterpreted sort definition. There was a mismatch in the behavior of the API and SMT front-ends. The SMT front-ends were using user_sorts to be able to support parametric uninterpreted sorts. After this fix, the API also creates user_sorts. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-12 14:34:31 -08:00
Christoph M. Wintersteiger
91402f2060 C API: fixed mk_context/mk_context_rc exception behaviour 
Adjusted .NET/Java APIs accordingly.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-08 18:54:44 +00:00
Leonardo de Moura
4624919786 Improve html pretty printer for RCF package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-27 11:24:23 -08:00
Leonardo de Moura
77f58269ed Add html pretty printing mode for RCF package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-27 10:19:54 -08:00
Leonardo de Moura
a895506dac Fix issue reported at http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-25 09:29:03 -08:00
Leonardo de Moura
6dd4cb832b Fix problem reported by Alex Horn 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 16:42:34 -08:00
Leonardo de Moura
711abc75fb Fix issue reported at http://z3.codeplex.com/workitem/14 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 13:22:28 -08:00
Christoph M. Wintersteiger
4b18c8f9c4 Java API: syntactic adjustments, getters, setters, 
... convenience parameters, etc.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-17 19:31:02 +00:00
Christoph M. Wintersteiger
3abf397560 Added Solver.AssertAndTrack 
Convenience fixes.
Renamed Context.Const to Context.ConstProbe

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-17 19:30:00 +00:00
Leonardo de Moura
c9b7ea35b6 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-16 08:39:24 -08:00
Christoph M. Wintersteiger
5f0cb28ca3 .NET and Java APIs: added functions for global parameter management. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-15 17:05:31 +00:00
Leonardo de Moura
799fe073db Add API for extracting numerator/denominator of RCF numerals. Add field to store the original isolating interval before refinement. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 18:29:08 -08:00
Leonardo de Moura
742f2b07dd Add support for compact string representation in the RCF API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 11:08:32 -08:00
Leonardo de Moura
4879b8db7a Merge branch 'unstable' into contrib 2013-01-13 09:51:22 -08:00
Leonardo de Moura
7312f49f88 Fix Visual Studio warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 09:06:07 -08:00
Leonardo de Moura
93f37bdf9f Merge branch 'realclosure' into unstable 2013-01-12 22:03:40 -08:00
Leonardo de Moura
4cd2998743 Add power operator to C and Python RCF APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 13:05:47 -08:00
Christoph M. Wintersteiger
dd127c2f71 Java API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-10 18:16:29 +00:00
Christoph M. Wintersteiger
3482b8f4f1 .NET API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-10 18:08:56 +00:00
Leonardo de Moura
4ea06b8040 Fix Z3_enable_trace API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 16:22:47 -08:00
Leonardo de Moura
56db84a0e5 Fix RCF API logging bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 15:10:16 -08:00
Leonardo de Moura
09b5724d82 Simplify RCF C API. Add Z3_rcf_mk_roots (C API) and MkRoots (Python API). Implement basic root isolation support. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 12:25:28 -08:00
Leonardo de Moura
3e19df0441 Fix API logging bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 21:25:46 -08:00
Leonardo de Moura
1c8101419b Add Python API for RCF module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 20:59:00 -08:00
Leonardo de Moura
9fbbdb56e4 Implement RCF external C API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 20:06:27 -08:00
Leonardo de Moura
47c6a73e19 Add RCF external API skeletons 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 22:24:56 -08:00
Leonardo de Moura
c430fe26aa Add ite operator to the C++ API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 08:29:25 -08:00
Leonardo de Moura
6a6015e335 Merge branch 'unstable' into contrib 2012-12-31 13:48:44 -08:00
Leonardo de Moura
a51c6d125d Add support for Python Fraction object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-28 13:39:34 -08:00
Leonardo de Moura
9a523defa2 Add pp (debugging function) for params_ref 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-28 09:13:18 -08:00
Leonardo de Moura
fbce816025 Merge branch 'unstable' into contrib 2012-12-22 14:36:30 -08:00
Leonardo de Moura
3cc9d57438 Fix pytest, it should work with Python 2.7.x and 3.x 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-21 16:58:10 -08:00
Leonardo de Moura
a0a505e1b8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-20 17:48:30 -08:00
Leonardo de Moura
6602803850 Add Python 3.x support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-20 17:47:38 -08:00
Josh Berdine
d7b8110cc8 Regenerate ml api 2012-12-20 12:58:21 +00:00
Josh Berdine
a7f89dcdd2 Move Z3_get_implied_equalities from v3 to v4 ml api as it now needs Z3_solver type 2012-12-20 12:54:44 +00:00
Josh Berdine
fd5372d7a2 Z3_search_failure type not needed in v4 ml api 2012-12-20 12:53:05 +00:00
Josh Berdine
32896a15e6 Fix for compiling ml api 2012-12-20 12:49:17 +00:00
Josh Berdine
27438b0fc9 Fix newlines 2012-12-20 12:48:49 +00:00
Leonardo de Moura
d92efeb0c5 Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 17:14:25 -08:00
Leonardo de Moura
607fab486c Fix incorrect uses of set_cancel() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 18:48:10 -08:00
Leonardo de Moura
f8014f54c1 Fix bug reported at http://stackoverflow.com/questions/13923316/unprintable-solver-model 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-17 15:13:05 -08:00