mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
6881 commits 24 branches 48 tags 158 MiB
Commit graph

1206 commits

Author SHA1 Message Date
Nikolaj Bjorner
90a38c9a35 Merge pull request #1073 from chaserhkj/funcdecl-translate-java 
Add translate method for FuncDecl in java api
 2017-06-13 13:27:12 -07:00
KangJing Huang (Chaserhkj)
5799947183 Fix docstrings for FuncDecl.translate 2017-06-13 02:37:41 -04:00
KangJing Huang (Chaserhkj)
3a692fe33c Add translate method for FuncDecl in java api 2017-06-13 00:37:02 -04:00
Nikolaj Bjorner
f5b54f042c apply correction by ddcc #1069 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-11 11:40:39 -07:00
Dan Liew
c629dcc53f [Doxygen] Rewrite documentation of Z3_mk_solver() and 
`Z3_mk_simple_solver()` to try to make it clearer what the differences
are between these APIs.

This an attempt to address issues noted in #1035.
 2017-06-11 14:04:18 +01:00
Dan Liew
bcb3981c5f [Doxygen] Fixed mismatched @{ and @} declaration which prevented 
the `capi` group from being declared properly. For example this
prevented from `Z3_mk_solver()` from appearing in the `capi` group.
 2017-06-07 18:49:43 +01:00
Dan Liew
85c7f5d865 [Doxygen] Fix some Doxygen warnings for z3_optimization.h 2017-06-07 18:45:12 +01:00
Christoph M. Wintersteiger
0137104683 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-06 16:04:45 +01:00
Christoph M. Wintersteiger
83e9c40265 Added __deepcopy__ operators to ref-counted objects in the Python API 2017-06-06 16:04:38 +01:00
Nikolaj Bjorner
af285d02c3 add documentation per #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-05 08:38:28 -07:00
Nikolaj Bjorner
4f04301305 add documentation per #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-05 07:55:32 -07:00
Nikolaj Bjorner
efd5727676 add shorthand for enumerating constants in a model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:35:09 -07:00
Nikolaj Bjorner
fda59f5a24 expose operator kinds for internal functions using their sequence variants. Issue #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:32:17 -07:00
Nikolaj Bjorner
52e0f3b539 add string accessors to managed APIs #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:10:49 -07:00
KangJing Huang (Chaserhkj)
8092dd5aa3 Fix Expr.update in java API returning superclass 2017-05-29 20:51:42 -04:00
Nikolaj Bjorner
b782ec35cc avoid print statements from assertions when the assertion does not trigger. Stackoverflow question http://stackoverflow.com/questions/44094927/creating-formula-taking-too-much-time-in-z3py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-21 10:35:59 -07:00
Owlz
aad186f6a5 Fixing z3 binary setup to data_files 2017-05-14 15:25:17 -04:00
Christoph M. Wintersteiger
248dd601ae Whitespace, newlines 2017-05-10 12:44:25 +01:00
Nikolaj Bjorner
69aa5ca877 Merge pull request #984 from delcypher/cmake_doxygen 
[CMake][Doxygen] Support building/installing API documentation and fix lots of bugs
 2017-04-27 06:58:32 -07:00
Nikolaj Bjorner
a048d74bae adding interval designator to output of non-optimal objectives, fix python doc test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-26 14:05:33 -07:00
Dan Liew
fe702d7782 [Doxygen] Fix warning about non-existent functions. 
`Z3_push` and `Z3_pop` should be `Z3_solver_push` and `Z3_solver_pop`
respectively.
 2017-04-26 10:42:57 +01:00
Dan Liew
7242a77a3f [Doxygen] Fix typo found with Doxygen warning 
```
warning: Found unknown command `\s'
```
 2017-04-26 10:42:57 +01:00
Dan Liew
eb1c985a94 [Doxygen] Fixed malformed code blocks in z3_api.h. 
These malformed `\code` blocks caused broken documentation to
be generated.
 2017-04-26 10:42:57 +01:00
Bruce Collie
ce67c8277c Return check result in fixedpoint object 
This is a small change to fix a missing return statement.
 2017-04-24 12:59:44 +00:00
Nikolaj Bjorner
8b5627e361 additional API per #977 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-16 12:13:30 +09:00
Nikolaj Bjorner
9933c36050 replace long by int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 17:06:03 +08:00
Nikolaj Bjorner
ab6abe901f replace long by int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:57:30 +08:00
Nikolaj Bjorner
87c3b5ee51 replace uint by long 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:29:02 +08:00
Nikolaj Bjorner
e4b9080165 include timeout/rlimit parameters in optmize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:04:13 +08:00
Nikolaj Bjorner
7bb5e72e07 add missing string/re operations #977 and adding Pseudo-Boolean operations to Java API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 09:09:30 +07:00
Nikolaj Bjorner
c4b26cd691 add bypass to allow recursive functions from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 16:38:15 -07:00
Nikolaj Bjorner
8f798fef1a fix python interface for string extract to take symbolic indices per bug report from Kun Wei 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-31 08:24:12 -07:00
Nikolaj Bjorner
62e87d6474 fix double ownership of enode marking causing crash during tracing. Issue #952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-23 11:10:19 -07:00
Nikolaj Bjorner
1ab7ab9d74 fix double ownership of enode marking causing crash during tracing. Issue #952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-23 11:09:36 -07:00
Nikolaj Bjorner
0668ba5f6c add pb shorthands to C++. Issue #694 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 07:58:39 -07:00
Nikolaj Bjorner
7634f8b93e Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-14 07:47:51 -07:00
Nikolaj Bjorner
1dd2de61ec add sum shorthand to C++. Issue #694 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 07:43:26 -07:00
hume
0b1d564509 added no exception support to z3++.h 2017-03-14 18:11:00 +08:00
James Bornholt
559c5e5ae6 z3py: With tactical should not try to use context as a parameter 2017-03-11 16:09:25 -08:00
Nikolaj Bjorner
509f7409ba adding fixedpoint object to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-10 23:01:43 +01:00
George Karpenkov
be1e9918f0 Class Optimize#Handle should be static, 
as it already includes an explicit reference to the Optimize class.
 2017-02-27 18:49:02 +01:00
George Karpenkov
b3be83e7c5 Sane indentation + removing extra spaces for Optimize.java 2017-02-27 18:48:44 +01:00
George Karpenkov
d6c79facc7 Java API for getting the objective value as a triple 
See #911 for the motivation,
and e02160c674 for the relevant change
in C API.
 2017-02-27 18:42:44 +01:00
Nikolaj Bjorner
e02160c674 expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:07:40 -08:00
Nikolaj Bjorner
c67cf1653c use non _ method from z3printer module so to be resilient against how _ is handled as indicator of private functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-15 08:46:58 -08:00
Nikolaj Bjorner
216e17e5e2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-13 08:16:43 -08:00
Nikolaj Bjorner
e7a21dfac2 add par_and_then 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-13 08:16:39 -08:00
Nikolaj Bjorner
6fcba26ea6 make parameters accessible from expressions. Issue #896 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-12 09:56:49 -08:00
Nikolaj Bjorner
b3dabc7ccf add missing mod/rem/is_int functionality to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 16:28:15 -05:00
Nikolaj Bjorner
4c6efbbc8b expose numerator/denominators for Martin and Giles 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 16:02:51 -05:00