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 |
|