Nikolaj Bjorner
|
cc577a431a
|
C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-03-28 09:39:14 -07:00 |
|
Nikolaj Bjorner
|
13e454ad63
|
adding C++ API for optimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-03-28 09:29:21 -07:00 |
|
Nikolaj Bjorner
|
4c95bb4dd9
|
add 'distinct' to C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-03-28 08:51:50 -07:00 |
|
Nikolaj Bjorner
|
457b22b00e
|
add TPTP example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-09-06 21:49:00 -07:00 |
|
Leonardo de Moura
|
ccb36f1ae7
|
Fix issue https://z3.codeplex.com/workitem/54
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-07-09 08:22:17 -07:00 |
|
Leonardo de Moura
|
c8c5f30b49
|
Add new C++ APIs for creating forall/exists expressions.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-05-09 21:30:31 -07:00 |
|
Nikolaj Bjorner
|
2afcc493e0
|
remove reference count debugging, add substitution to C++ header
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-04-18 10:18:26 -07: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 |
|
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 |
|
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 |
|
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
|
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
|
92a29b1e43
|
added Z3_global_param_reset_all API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-04 11:55:12 -08:00 |
|
Leonardo de Moura
|
0ec6e2f218
|
adjusting examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-03 15:19:47 -08:00 |
|
Leonardo de Moura
|
4b27eae47f
|
using doxygen to document z3py API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-22 18:41:43 -08:00 |
|
Leonardo de Moura
|
a9a673bb8a
|
New API website
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-22 17:53:43 -08:00 |
|
Leonardo de Moura
|
7c40c4bd9a
|
Added more comments to the C++ API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-22 17:04:59 -08:00 |
|
Leonardo de Moura
|
caced62f40
|
New API for adding 'tracked assertions'. Added wrappers for creating existential and universal quantifiers in the C++ API fronted. Added new examples for the C++ API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-10 15:54:31 -08:00 |
|
Leonardo de Moura
|
a274cac2a0
|
bindings --> api; and moved nlsat/sat/subpaving tactics
|
2012-10-31 13:25:36 -07:00 |
|