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

2452 commits

Author SHA1 Message Date
Ken McMillan
78848f3ddd working on smt2 and api 2013-03-26 17:25:54 -07:00
Leonardo de Moura
b417ca657d Fix set_interruptable usage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-25 16:52:08 -07:00
Nikolaj Bjorner
26f4d3be20 significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-23 14:11:54 -07:00
Ken McMillan
2b93537366 debugging interpolation 2013-03-06 18:26:46 -08:00
Ken McMillan
ae9276ad9b more work on interpolation 2013-03-05 21:56:09 -08:00
Kenneth McMillan
d66211c007 working on interpolation API 2013-03-04 23:48:01 -08:00
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