mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity
18399 commits 23 branches 48 tags 157 MiB
Commit graph

433 commits

Author SHA1 Message Date
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
Nikolaj Bjorner 995e112a18 fix examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:01:59 -08:00
Nikolaj Bjorner 1d4b996765 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 16:39:51 -08:00
Nikolaj Bjorner 9cba63c31f remove deprecated iz3 example. Remove deprecated process control 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 12:32:15 -08:00
Nikolaj Bjorner d7c3e77b66 port test_capi.c to use mostly essentially non-deprecated APIs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-17 18:59:43 -08:00
Nikolaj Bjorner 0f602d652a remove deprecated API functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 13:47:41 -08:00
Christoph M. Wintersteiger 88b027ecce Eliminated unused variable from C example. 2015-10-29 13:32:58 +00:00
Christoph M. Wintersteiger 2818e977b6 Fixed unused variable warnings in examples. 2015-10-29 13:20:56 +00:00
Christoph M. Wintersteiger bd5b455c46 Refactored iz3 example to avoid compiler warnings. 2015-10-29 13:03:19 +00:00
Christoph M. Wintersteiger a1eee6275f Bugfix for C++ examples. 
Relates to #26
 2015-10-19 19:03:36 +01:00
Christoph M. Wintersteiger a6f85f3932 Merge branch 'sudoku-in-c++' of https://github.com/benlaurie/z3 into benlaurie-sudoku-in-c++ 
# Conflicts:
#	examples/c++/example.cpp
 2015-10-19 14:09:36 +01:00
Christoph M. Wintersteiger 114f9834dd Adjusted copyright notice. 2015-10-02 19:51:06 +01:00
Nikolaj Bjorner a0894ac7bf add basic example of using optimizaiton context to Java as raised in issue #179 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-30 11:32:14 -03:00
Nikolaj Bjorner 21201371ed add reference equality to Symbols for .NET 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-11 00:53:13 -07:00
Nikolaj Bjorner 1657cdd8b4 add missing copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-17 12:47:19 -07:00
Nikolaj Bjorner e0068e4065 C/right on python scripts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 12:01:47 -07:00
Nikolaj Bjorner d469a16bb8 add more Copyright notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:59:21 -07:00
Nikolaj Bjorner e3b1ce1fdc also allw n-ary distrinct 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 10:07:09 -07:00
Nikolaj Bjorner 4f02d380aa make use of uninterpreted_sort shorthand 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:34:47 -07:00
Christoph M. Wintersteiger e9f7d558e3 tabs, indentation 2015-05-19 12:40:41 +01:00
Nikolaj Bjorner 0e32c87dc3 fix examples and C++ API - build failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-15 15:43:05 +01:00
Nikolaj Bjorner ab5022888c Merge branch 'opt' of https://github.com/Z3Prover/z3 into unstable 2015-05-14 12:11:17 +01:00
Nikolaj Bjorner 839e3fbb7c add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 19:40:34 -07:00
Nikolaj Bjorner 4a9d97bd02 add concat to z3++, codeplex request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-08 21:29:48 -07:00
Nikolaj Bjorner 3ba2e712b2 merge with unstable branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-12 15:54:52 -07:00
Christoph M. Wintersteiger 8862cb4833 Java example: Removed throws declarations for Z3Exception. 2015-04-09 14:52:50 +01:00
Ben Laurie 0f467eb599 Pull out the solver. 2015-04-05 17:57:21 +01:00
Ben Laurie e8b8393c31 Add Sudoku example. 2015-04-05 17:44:26 +01:00
Nikolaj Bjorner 52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Nikolaj Bjorner e456af142e fix complex.py example with power prompted by suggestion of smilliken 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-27 02:42:08 -07:00
Nikolaj Bjorner 0482e7fe72 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:46:28 -07:00
Nikolaj Bjorner 39892aae10 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:46:17 -07:00
Nikolaj Bjorner 8059a5a0b7 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:36:01 -07:00
Nikolaj Bjorner 86ac20faf6 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:35:44 -07:00
Nikolaj Bjorner 2aa91eee70 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:24:47 -07:00
nikolajbjorner 3ca3c948cf add bit-vector extract shortcuts to C++ API 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-02-27 11:08:49 -08:00
Christoph M. Wintersteiger 9b137d54d3 Bugfix and new examples for implicit assumptions in Z3_solver_assert_and_track. Thanks to Amir Ebrahimi for reporting this issue! 
(See http://stackoverflow.com/questions/28558683/modeling-constraints-in-z3-and-unsat-core-cases)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-18 16:25:27 +00:00
Christoph M. Wintersteiger b96551a1a2 .NET/Java/ML: Moved toggle_warning_messages to Global, added en/disable_trace. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 14:17:39 +00:00
Christoph M. Wintersteiger d7a62baef4 Improved memory use of the Java API. Thanks to Joerg Pfaehler for reporting this issue! 
+ formatting

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-30 21:10:22 -06:00
unknown f020b7c7b8 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-01-28 17:54:26 -08:00
Christoph M. Wintersteiger b92bdaeebe ML API readme fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:51:47 +00:00
Christoph M. Wintersteiger e29abefb12 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 
Conflicts:
	scripts/mk_util.py

+ Cosmetics

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:44:59 +00:00
Christoph M. Wintersteiger 5c7d0380d3 Fixes in the OCaml FPA API and example 2015-01-24 18:29:52 +00:00
Christoph M. Wintersteiger 1c9051016a Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 
Conflicts:
	scripts/mk_util.py
 2015-01-24 18:29:03 +00:00
Christoph M. Wintersteiger 65ccc9a8ea added FPA ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 19:36:47 +00:00
Christoph M. Wintersteiger 48c72d2c38 FPA API: naming consistency 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 18:18:26 +00:00
Christoph M. Wintersteiger ffd10675f4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 11:07:48 +00:00
Christoph M. Wintersteiger 1a6af4385e Fixed C example 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 15:01:50 +00:00
Christoph M. Wintersteiger d56d63e3e8 Merge branch 'fpa-api' of https://git01.codeplex.com/z3 into unstable 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

Conflicts:
	src/tactic/portfolio/default_tactic.cpp
 2015-01-21 14:25:31 +00:00
Christoph M. Wintersteiger ed0fa93245 Minor adjustments after rebase 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:35:19 +00:00
Christoph M. Wintersteiger 10c153bfe4 ML API: build fix 2015-01-19 17:17:13 +00:00
Christoph M. Wintersteiger 05af33ac7d ML API: ocamlfind installation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:13:52 +00:00
Christoph M. Wintersteiger 555a3883b9 ML example doc fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:11:18 +00:00
Christoph M. Wintersteiger 0465ad3ce6 ML example; or' is deprecated, changed to ||' 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:11:16 +00:00
Christoph M. Wintersteiger 9dc8021995 Added facilities for ocamlfind in the ML API build 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:11:15 +00:00
Christoph M. Wintersteiger 54b7f8eec3 ML API bugfix (Codeplex issue 102) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:39 +00:00
Christoph M. Wintersteiger b889b225a0 ML cleanup; makefile removed. The example is built by running make examples in the build directory. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:09:36 +00:00
Christoph M. Wintersteiger c1e29dabe7 ML API: renamed assert_ to add 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:15 +00:00
Christoph M. Wintersteiger 050629536a ML API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:14 +00:00
Christoph M. Wintersteiger eea13a087f ML API savegame 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:14 +00:00
Christoph M. Wintersteiger d293b579f3 ML API: flat & rich layer in place. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:13 +00:00
Christoph M. Wintersteiger 79d0c32c91 ML API: replaced arrays with lists. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:12 +00:00
Christoph M. Wintersteiger 6842acbea8 ML API: Cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:10 +00:00
Christoph M. Wintersteiger 9142901efe ML API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:08:08 +00:00
Christoph M. Wintersteiger 9ed926498f ML API: updated example 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:20 +00:00
Christoph M. Wintersteiger 3347d7ca8c ML API: moved more objects into normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:18 +00:00
Christoph M. Wintersteiger 6257c56901 ML API: bugfixes; starting to replace objects with normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:18 +00:00
Christoph M. Wintersteiger 1e2b546b03 ML API: changed context from object to normal type. Removed optional array parameters. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:06:17 +00:00
Christoph M. Wintersteiger e2f6b10e32 ML API bugfixes 
More ML examples

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:02:17 +00:00
Christoph M. Wintersteiger c03d5277bc more ML 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:36 +00:00
Christoph M. Wintersteiger 25498345e5 New ML API bugfixes and first example. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:36 +00:00
Christoph M. Wintersteiger c2ff90720e ML API: mk_context added. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:35 +00:00
Christoph M. Wintersteiger 49a4e77a6d More new ML API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:34 +00:00
Christoph M. Wintersteiger c28f0e7c8a ML API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:31 +00:00
Christoph M. Wintersteiger 7ae90f0b20 More ML API: 
Fixes in native layer.
Added symbols.
Prepared code for automatic documentation.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:01:29 +00:00
Christoph M. Wintersteiger 1685e3dd6f ML API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:57:10 +00:00
Christoph M. Wintersteiger 0e98d26721 ML API and example compilation. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:56:42 +00:00
Christoph M. Wintersteiger c9cca119c5 File renamed 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:55:24 +00:00
Christoph M. Wintersteiger f7b3529f01 More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:55:22 +00:00
Christoph M. Wintersteiger ccffea2bc9 ML API: build fix 2015-01-19 16:08:38 +00:00
Christoph M. Wintersteiger 1e4b14af67 ML API: ocamlfind installation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:07:00 +00:00
Christoph M. Wintersteiger 2f00968b4f ML example doc fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:05:11 +00:00
Christoph M. Wintersteiger a028f200af ML example; or' is deprecated, changed to ||' 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:02:39 +00:00
Christoph M. Wintersteiger 832e119b98 ML API bugfix (Codeplex issue 102) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 16:01:36 +00:00
Christoph M. Wintersteiger c37eb794c2 ML API: renamed assert_ to add 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:57:20 +00:00
Christoph M. Wintersteiger 13416de27e ML API savegame 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:55:52 +00:00
Christoph M. Wintersteiger 6417f9e648 ML API: flat & rich layer in place. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:54:46 +00:00
Christoph M. Wintersteiger a0f6d1d3df ML API: replaced arrays with lists. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:54:28 +00:00
Christoph M. Wintersteiger 2af1f81ae1 ML API: Cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:53:42 +00:00
Christoph M. Wintersteiger fd2ae5f60e ML API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:53:20 +00:00
Christoph M. Wintersteiger 048e8c1a97 ML API: updated example 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:41 +00:00
Christoph M. Wintersteiger bcc0c14233 ML API: moved more objects into normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:39 +00:00
Christoph M. Wintersteiger bbd1e465bb ML API: bugfixes; starting to replace objects with normal types. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:38 +00:00
Christoph M. Wintersteiger 0e59d05629 ML API: changed context from object to normal type. Removed optional array parameters. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:51:37 +00:00
Christoph M. Wintersteiger 597409c8ac ML API bugfixes 
More ML examples

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:55 +00:00
Christoph M. Wintersteiger cef9c2fa69 more ML 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:23 +00:00
Christoph M. Wintersteiger bffef2e808 New ML API bugfixes and first example. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:22 +00:00
Christoph M. Wintersteiger a42e21ede1 ML API: mk_context added. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:21 +00:00
Christoph M. Wintersteiger 371db347af More new ML API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:20 +00:00
Christoph M. Wintersteiger 2277ad3654 ML API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:18 +00:00
Christoph M. Wintersteiger 794823ba6d More ML API: 
Fixes in native layer.
Added symbols.
Prepared code for automatic documentation.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:49:16 +00:00
Christoph M. Wintersteiger 7efe7a2c16 ML native layer bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:48:40 +00:00
Christoph M. Wintersteiger b193b827ed ML API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:44:42 +00:00
Christoph M. Wintersteiger c001da6188 ML API and example compilation. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:42:23 +00:00
Christoph M. Wintersteiger e7e85dc7b4 File renamed 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:42:22 +00:00
Christoph M. Wintersteiger bea09539cf More ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 15:42:18 +00:00
Christoph M. Wintersteiger 67e04c5dfb Python example: removed function that has no body. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-16 17:40:28 +00:00
Christoph M. Wintersteiger 7fe9ad5cb4 Java FPA API overhaul 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:22:02 +00:00
Christoph M. Wintersteiger ee2c9095c6 .NET FPA API overhaul 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:21:29 +00:00
Christoph M. Wintersteiger 0faf329054 FPA API: bugfixes and examples for .NET and Java 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-03 17:26:58 +00:00
Christoph M. Wintersteiger b46d76cddb New FPA C-API example 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 19:16:44 +00:00
Nikolaj Bjorner 08cb8b8de8 address divergence in the case of shared theory symbols. Codeplex issue 147, thanks to George Karpenkov 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-09 16:04:25 +01:00
Christoph M. Wintersteiger 261fe01cea FPA API bug and consistency fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-11 12:38:59 +00:00
Christoph M. Wintersteiger 8d3ef92383 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 
Conflicts:
	scripts/mk_project.py
	src/api/z3.h
	src/ast/float_decl_plugin.cpp
	src/ast/float_decl_plugin.h
	src/ast/fpa/fpa2bv_converter.cpp
	src/ast/fpa/fpa2bv_rewriter.h
	src/ast/rewriter/float_rewriter.cpp
	src/ast/rewriter/float_rewriter.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-11 11:53:39 +00:00
Nikolaj Bjorner e002fc680f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-31 14:24:35 +01:00
Nikolaj Bjorner b4600ffda0 add print to SMT-LIB format from solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-31 14:24:21 +01:00
Christoph M. Wintersteiger cee7dd3944 fixed newline characters 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 23:52:40 +01:00
Christoph M. Wintersteiger 6a496a1bfb Merge branch 'pure' of https://git01.codeplex.com/z3 into contrib 2014-10-24 21:17:57 +01:00
Christoph M. Wintersteiger 2f9b3c42eb Java API cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 19:43:36 +01:00
Christoph M. Wintersteiger cc99e96786 Java API Cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 18:00:36 +01:00
Nikolaj Bjorner ce18421a7a fix box 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 14:29:39 -07:00
Nikolaj Bjorner e8b04790cf fix build by disabling removed API call from interpolation sample 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-11 09:43:55 -07:00
Nikolaj Bjorner d4a5873dc8 fix lines 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-10 14:31:37 -07:00
Nikolaj Bjorner f651145b4c add optimization front-ends directly to the shell 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-10 14:23:58 -07:00
Christoph M. Wintersteiger 0451a605f4 Interpolation example bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-10 13:05:11 +01:00
Nikolaj Bjorner d1a2e61220 optimization example that parses obp and wcnf formats natively 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-09 17:58:38 -07:00
Nikolaj Bjorner 7ef1e8a3de turn friends into inliers to respect namespace for non-operator friends. Operaor friends will stil be in file scope so do not take name-space qualifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 19:04:15 -07:00
Nikolaj Bjorner 3f8083dfa6 fix push/pop bugs in optimize context, add example to c++, fix bug in arithemtic bounds axiom addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-02 09:32:38 -07:00
Christoph M. Wintersteiger 8b40d4a735 FPA theory bug fixes. 
Also removed unnecessary intermediate variables.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-04 17:00:04 +01:00
Christoph M. Wintersteiger c508b66cf7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 
Conflicts:
	src/ast/float_decl_plugin.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-07-31 17:37:43 +01:00
Nikolaj Bjorner 19050d1c4c merge Fixedpoint.cs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-28 12:20:48 -07:00
Nikolaj Bjorner a5e3713c2c fix unmatched parenthsis and code odor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-14 05:47:42 -07:00
Christoph M. Wintersteiger 129e2f5e23 FPA API fixes and examples 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-06-11 17:55:31 +01:00
Christoph M. Wintersteiger a8b65ebb36 added stubs for theory_fpa 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-23 20:10:53 +01:00
Nikolaj Bjorner d118f07e37 fix maximize name in C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-22 14:48:05 +02:00
Nikolaj Bjorner e180cfe256 optimizing pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-02-25 12:24:48 -08:00
Nikolaj Bjorner e2db1418f9 debugging simplex/pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-02-21 14:39:54 -08:00
Nikolaj Bjorner 23e811d136 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-05 20:44:56 -08:00
Nikolaj Bjorner 8f1a235f00 add app.config 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-27 14:50:04 -08:00
Anh-Dung Phan e223e386fe Add binding redirects 2013-12-27 14:38:57 -08:00
Anh-Dung Phan 8accc49386 Add a README for MSF plugin 2013-12-27 11:39:50 -08:00
Anh-Dung Phan 5cc4cc8226 Add MSF plugins 2013-12-27 11:18:10 -08:00
Christoph M. Wintersteiger 16ebceb9ff Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 
Conflicts:
	scripts/mk_project.py

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-12-04 13:50:42 +00:00
Ken McMillan 3a0947b3ba merged with unstable 2013-10-18 17:26:41 -07:00
Nikolaj Bjorner 4ad6660f35 add const qualifiers to fix warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-09 09:24:35 -07:00
Nikolaj Bjorner 861a31f458 fix build warning from tptp example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-08 13:30:03 -07:00
Nikolaj Bjorner 457b22b00e add TPTP example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-06 21:49:00 -07:00
Christoph M. Wintersteiger 092dfa396a Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-08-07 15:22:06 +01:00
Christoph M. Wintersteiger 210bca8f45 .NET Example: Sudoku example bugfix. Many thanks to Ilya Mironov for reporting this issue. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-07-02 12:57:54 +01:00
Christoph M. Wintersteiger f50016d8a1 bugfix in .NET example 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 13:18:33 +01:00
Christoph M. Wintersteiger 8e497fbbaf Extended FPA dotnet example 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 13:13:14 +01:00
Christoph M. Wintersteiger a9840b291f FPA API: Tied into rest of the API; 
added numeral/value handling through existing functions;
added trivial .NET example.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-10 19:06:45 +01:00
Leonardo de Moura d2a2dbb4b6 Merge branch 'unstable' into contrib 2013-06-05 14:00:59 -07:00
Leonardo de Moura edb2f8554d Add new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-27 17:45:56 -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
Leonardo de Moura 157b5f0d9c Add expr_vector example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-05-07 08:10:43 -07:00
Leonardo de Moura f773f35517 Merge branch 'unstable' into contrib 2013-04-09 08:44:57 -07:00
Ken McMillan 78848f3ddd working on smt2 and api 2013-03-26 17:25:54 -07:00
Ken McMillan ae9276ad9b more work on interpolation 2013-03-05 21:56:09 -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
Leonardo de Moura b4d57e0ab1 Merge branch 'unstable' into contrib 2013-02-19 15:35:05 -08:00
Leonardo de Moura 3b8d72beeb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-02-08 19:32:06 -08:00
Leonardo de Moura 92695277ed Add new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-02-08 19:29:57 -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
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
Leonardo de Moura 4879b8db7a Merge branch 'unstable' into contrib 2013-01-13 09:51:22 -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 1235b3ea24 Fix header 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-31 14:40:52 -08:00
Leonardo de Moura 4681281765 Add example sent by Ganesh 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-31 14:37:54 -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
Leonardo de Moura 7b1fac11e6 Add new C++ examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-19 12:33:14 -08:00
Leonardo de Moura bce9d1440b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-04 11:57:00 -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
Christoph M. Wintersteiger 4d1d784a1c Java+.Net Examples: refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-04 19:32:20 +00:00
Leonardo de Moura 54e452a1af chasing bug in the Java bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 16:58:44 -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 847c5f9691 fixing problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 11:55:24 -08:00
Christoph M. Wintersteiger 692593baaa Java API: 32-bit issues and bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 22:31:07 +00:00
Christoph M. Wintersteiger 0c1f2a8281 Java API: Added exception wrappers and build dependencies. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 15:39:25 +00:00
Leonardo de Moura 001c8487e9 small change to be able to test java example on linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-29 09:13:24 -08:00
Christoph M. Wintersteiger bbfd9dd19f Java API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-28 22:20:36 +00:00
Christoph M. Wintersteiger 1ed4e7c480 Managed API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-28 22:20:02 +00:00
Christoph M. Wintersteiger 519d308b86 Java API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-28 14:59:39 +00:00
Christoph M. Wintersteiger a9883e972f Java API: Bugfixes and Example. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-27 23:06:35 +00: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 a5ceff98ea cleaned exampled 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-08 07:11:22 -08:00
Leonardo de Moura 1cf8d61def new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-08 07:00:27 -08:00
Leonardo de Moura e08c569d8d new qe example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 12:04:02 -07:00
Leonardo de Moura f040db94f8 python example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-28 12:19:45 -07:00
Leonardo de Moura 7f0fcefbe2 C examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-28 11:56:27 -07:00
Leonardo de Moura 91cc6bb768 renamed test_capi 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-28 10:51:50 -07:00
Leonardo de Moura 4278b2dd51 dotnet example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-28 10:50:36 -07:00
Leonardo de Moura 93fbfd5f94 dotnet example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-28 10:48:11 -07:00
Leonardo de Moura be97785253 c++ example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-28 10:06:02 -07:00
Leonardo de Moura 3cddd6977b Added make install/uninstall 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-27 20:22:51 -07:00
Leonardo de Moura b1a5436c3f moved .net example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-23 22:32:46 -07:00
Leonardo de Moura e2f4943b4e moved dll and examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-23 16:33:20 -07:00