Christoph M. Wintersteiger
1f29cebd4d
Fixed backwards compatibility problem in maxsat example
2017-06-28 14:44:41 +00:00
Nikolaj Bjorner
7db1847f51
fix bitrot in maxsat example reference management #1116
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-26 09:36:53 -07:00
Nikolaj Bjorner
404db5759a
Merge pull request #1115 from delcypher/cmake_maxsat_example
...
[CMake] Teach CMake to build the `maxsat` example
2017-06-26 08:19:51 -07:00
Dan Liew
4d6cbd3788
[CMake] Teach CMake to build the maxsat
example as an external
...
project. The project can be built by building the new `c_maxsat_example`
target.
2017-06-26 11:58:51 +01:00
Dan Liew
896aae5606
Fix Python API examples so they work with Python 3 as well as Python 2.
2017-06-26 11:31:08 +01:00
Dan Liew
849eb389e6
[CMake] Add missing python example files.
...
We have to flatten the hierarchy when copying across so that all
Python examples have the `z3` directory in their directory.
2017-06-26 11:30:59 +01:00
Christoph M. Wintersteiger
d8a02bc040
Fixed AST translation functions in .NET and Java APIs. Fixes #1073 .
2017-06-14 13:24:54 +01:00
Dan Liew
4b517b96df
[CMake] Move CMake files into their intended location so the
...
`contrib/cmake/bootstrap.py` script no longer needs to be executed.
The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461 . While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.
The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.
This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Christoph M. Wintersteiger
a334020f2c
Added .NET 3.5 solution/project files
2017-01-18 12:32:02 +00:00
Christoph M. Wintersteiger
7f923c6a33
Include Python API files in distributions.
2016-11-07 22:00:28 +00:00
Nikolaj Bjorner
f609ee6298
add documentation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-10-23 20:44:25 -07:00
Nikolaj Bjorner
ec5d4f1119
add example to exercise at-most-1 constraints
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-10-23 20:35:20 -07:00
Nikolaj Bjorner
5d9820f3e2
add example of parsing with external declarations
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-10-07 12:57:07 -07:00
Mathieu Roger
9245e61775
Update socrates.py
2016-09-14 21:36:39 +02:00
Nikolaj Bjorner
e7f36a2d35
remove special characters
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-09-14 10:32:17 -07:00
Mathieu Roger
a7e3a9df5a
Create socrates.py
...
Classical syllogism in Z3.
Many samples talks about integer, reals. Not much sample available on non integer things.
2016-09-14 19:10:49 +02:00
Nikolaj Bjorner
f2b5c11d1c
add option for prettier proof printing, Issue #706
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-08-20 03:52:45 -07:00
Nikolaj Bjorner
2263be1b4d
adding consequence examples
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-29 17:24:14 -07:00
Christoph M. Wintersteiger
6f874c5c1d
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-07-28 18:07:48 +01:00
Christoph M. Wintersteiger
3587baaf24
Added full version strings and associated API functions.
2016-07-28 18:06:02 +01:00
Nikolaj Bjorner
1239c8f8e8
update MSF example
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-27 11:20:31 -07:00
Nikolaj Bjorner
67c6f9be91
have the classifier revert to full arithmetic on non-difference logic, reported on http://stackoverflow.com/questions/38594208/changing-order-of-z3-fixepoint-queries-changes-the-result/38596187#3
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-26 10:32:54 -07:00
Nikolaj Bjorner
16e3a91bdf
fix issues reported by Geoff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-21 07:56:21 -07:00
Nikolaj Bjorner
f522d995d1
apply 'to-real' coercion only on integers. bug reported by Geoff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-20 19:03:25 -07:00
Nikolaj Bjorner
f3d657ebd1
add tptp5 example to cmake, adding output SZS directives for Geoff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-07-15 12:09:23 -07:00
Nikolaj Bjorner
014c693fa5
fix explain map to use negations
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-27 15:22:13 -07:00
Nikolaj Bjorner
f786ab15fb
add example for MSS enumeration
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-26 20:58:48 -07:00
Nikolaj Bjorner
67ea78a4a5
Add basic MARCO example
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-24 08:00:23 -07:00
Christoph M. Wintersteiger
e9eb88e1b3
fixed java build issues. Relates to #648 .
2016-06-24 15:08:56 +01:00
Christoph M. Wintersteiger
8c191781e7
Fixed warning message
2016-06-22 18:52:30 +01:00
Christoph M. Wintersteiger
b178420797
Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api
2016-03-31 18:11:30 +01:00
Takeshi Abe
5c2969c0f0
Fix typo
2016-03-23 12:51:41 +09:00
Christoph M. Wintersteiger
b27977ea90
Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api
2016-03-02 15:14:12 +00:00
Christoph M. Wintersteiger
3b92128ed8
Fixed old-style C variable declaration problem in interpolation C example.
2016-02-16 12:12:59 +00:00
Christoph M. Wintersteiger
b99fcb9c8a
More new OCaml API
2016-02-14 19:56:22 +00:00
Christoph M. Wintersteiger
9dbb8057ca
Merge pull request #449 from kenmcmil/issue243
...
fixed logging on return of Z3_compute_interpolant...
2016-02-12 12:40:01 +00:00
Nikolaj Bjorner
8d61d36c3f
add documentation methods to param_descrs, add C++ API and example for param_descrs. Issue #443
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-02-12 11:45:00 +00:00
Ken McMillan
8b90bc9e91
fixed logginf on return of Z3_compute_interpolant and added interpolation example to test_capi.c
2016-02-11 16:09:54 -08:00
Nikolaj Bjorner
6c6da44f8f
removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-02-09 22:24:37 +00:00
Nikolaj Bjorner
5ce85aba40
removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-02-09 22:23:37 +00:00
Christoph M. Wintersteiger
7e3676e24a
bugfix for ML example
2016-01-08 13:25:14 +00:00
Christoph M. Wintersteiger
de3cb7e5dc
More FPA exponent/siginficand order consistency
2016-01-05 18:05:21 +00:00
Dan Liew
83e2b1c6e5
Typo in comment in C api example.
2015-12-15 11:52:35 +00:00
Christoph M. Wintersteiger
134b93b43e
ML API build fixes for Windows.
2015-12-14 14:41:19 +00:00
Christoph M. Wintersteiger
771caba9db
update ML example readme
2015-12-13 17:44:50 +00:00
Nikolaj Bjorner
64b9a301ed
add python visitor example in response to Stackoverflow question
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-06 20:09:13 -08:00
Christoph M. Wintersteiger
cbda38ee80
Added finite domain expressions and numerals to the .NET, Java, and Python APIs.
...
Relates to #318
2015-12-02 17:01:52 +00:00
Christoph M. Wintersteiger
52bbd67cd3
Whitespace
2015-12-02 14:40:47 +00:00
Nikolaj Bjorner
436a51d8f0
fix build of maxsat.c
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-22 22:10:22 -08:00
Nikolaj Bjorner
3be279dc29
fix build break on maxsat.c example
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-21 10:36:24 -08:00