Christoph M. Wintersteiger
ae54b9d158
Fixed FP math options for x86 cmake build. Fixes #644 .
2016-06-24 18:13:02 +01:00
Christoph M. Wintersteiger
70301ad3c8
Added bv*mul_no*flow handling in bv_rewriter.
...
Fixes #657 .
2016-06-24 16:25:11 +01:00
Christoph M. Wintersteiger
e9eb88e1b3
fixed java build issues. Relates to #648 .
2016-06-24 15:08:56 +01:00
Christoph M. Wintersteiger
3e96a7972f
Merge pull request #648 from cheshire/no_finalizers
...
Replace finalizers with PhantomReferences in Java API
2016-06-24 14:17:29 +01:00
Christoph M. Wintersteiger
1fb672121c
build fix for cygwin/mingw
2016-06-24 13:57:53 +01:00
Christoph M. Wintersteiger
e3a41d0d98
Merge pull request #645 from martin-neuhaeusser/cross-mingw64
...
Extend build scripts to support MinGW64 cross-compilation on Windows.
2016-06-24 13:42:10 +01:00
Christoph M. Wintersteiger
d90a575981
Merge pull request #646 from martin-neuhaeusser/ocaml-c89
...
Make C-layer of OCaml bindings C89 compatible.
2016-06-24 13:40:50 +01:00
Martin R. Neuhäußer
5845e63396
Make cmake not emit -fPIC to mingw64 for Windows builds.
...
This patch detects a mingw64 build of the shared library and does not emit -fPIC to the compiler.
This is necessary to avoid a warning message, as Windows native code DLLs are generally relocatable
and not position independent.
2016-06-24 12:40:16 +02:00
Nikolaj Bjorner
98a34ca51f
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-23 21:39:34 -07:00
Nikolaj Bjorner
c72ed3e6b4
update core minimization code
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-23 21:39:28 -07:00
Christoph M. Wintersteiger
0a575936d0
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-23 19:31:08 +01:00
Christoph M. Wintersteiger
8bde7b8a4c
Added facilities for dumping smt_params for debugging purposes
2016-06-23 19:31:00 +01:00
Nikolaj Bjorner
41edf5f91e
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-22 20:25:55 -07:00
Nikolaj Bjorner
5b497b6249
reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-22 20:25:47 -07:00
Christoph M. Wintersteiger
fad1dffbf0
Added PATH info to successful build message
2016-06-22 19:03:42 +01:00
Christoph M. Wintersteiger
89b1d7d8da
Fixed test case
2016-06-22 18:52:40 +01:00
Christoph M. Wintersteiger
8c191781e7
Fixed warning message
2016-06-22 18:52:30 +01:00
Nikolaj Bjorner
fa6f9b4a37
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-20 16:39:08 -07:00
Nikolaj Bjorner
9c099d6b1b
fix mb maximization logic, so far not accessible
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-20 16:39:03 -07:00
George Karpenkov
b086aac45f
Use constructors instead of static methods for Context.java.
2016-06-16 18:21:55 +02:00
Nikolaj Bjorner
bfe26390f0
fix bug introduced when hiding unused variables in 96e157e
, reported by Mikolas Janota
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-14 08:12:32 -07:00
Nikolaj Bjorner
8da0146318
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-14 08:10:21 -07:00
Nikolaj Bjorner
9253ca9d86
make use of warning_msg safe for formatting. Thanks to Scott McPeak for reporting
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-14 08:10:10 -07:00
Christoph M. Wintersteiger
c8c262fb93
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-14 13:14:30 +01:00
Christoph M. Wintersteiger
3ea71b4b25
Fixed SMT2 scanner to allow 0xFF characters.
...
Thanks to Santiago Zanella-Beguelin for reporting this issue.
2016-06-14 12:49:48 +01:00
Nikolaj Bjorner
b11f9050e3
fix bugs exposed from bad indentation warnings, #650
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-13 18:20:25 -07:00
Nikolaj Bjorner
16ad33bf39
add collection of statistics #652
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-13 18:17:49 -07:00
George Karpenkov
b65d83aacf
Java API: explain the phantom references mechanics in Javadoc.
2016-06-13 12:22:32 +02:00
George Karpenkov
a914822346
JavaAPI: DecRefQueue -- do not use move_limit for now.
2016-06-13 12:18:31 +02:00
George Karpenkov
26d6c99aac
Typo in Javadoc.
2016-06-13 12:11:03 +02:00
George Karpenkov
27aa37946e
Do not lock on context creation and deletion.
2016-06-13 12:09:34 +02:00
Nikolaj Bjorner
c7ff05cc78
enable core minimization with qsat in case it turns out to be useful
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-12 15:58:12 -07:00
George Karpenkov
22ffd65d1e
Java API: split incRef into incRef and addToReferenceQueue
...
One method should do one thing only, it's easy to mix things up
otherwise.
2016-06-12 21:01:58 +02:00
George Karpenkov
2a347f04bf
Java API: FuncInterp.Entry should be an inner static class
...
...as it does not use any fields of the outer FuncInterp object.
2016-06-12 21:00:51 +02:00
George Karpenkov
5657399d55
Bugfix for incorrect order of operations.
2016-06-12 20:39:54 +02:00
George Karpenkov
495ef0f055
Java bindings with no finalizers
...
Replacing finalizers with PhantomReferences, required quite a lot of
changes to the codebase.
2016-06-12 20:27:01 +02:00
George Karpenkov
dfc80d3b69
Do not needlessly catch exceptions in Java bindings
...
A lot of existing code in Java bindings catches exceptions just to
silence them later.
This is:
a) Unnecessary: it is OK for a function to throw a RuntimeException
without declaring it.
b) Highly unidiomatic and not recommended by Java experts (see Effective
Java and others)
c) Confusing as has the potential to hide the existing bugs and have
them resurface at the most inconvenient/unexpected moment.
2016-06-12 14:14:11 +02:00
Nikolaj Bjorner
3ac4709992
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-11 10:39:31 -07:00
Nikolaj Bjorner
ea201a776d
enable qsat-opt
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-11 10:39:27 -07:00
Nikolaj Bjorner
9f5a117443
move mus to solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-10 16:24:14 -07:00
martin-neuhaeusser
f069b1c0e9
Make C-layer of OCaml bindings C89 compatible.
...
This patch ensures that the C code generated for the OCaml stubs complies with C89. It is needed to compile Z3 with OCaml support with Visual Studio versions older than VS2013.
2016-06-10 16:49:06 +02:00
Martin R. Neuhäußer
22097efd4a
Extend build scripts to support MinGW64 cross-compilation on Windows.
2016-06-10 16:43:57 +02:00
Nikolaj Bjorner
19f98547f7
fix memory leak Issue #643
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-09 21:59:10 -07:00
Christoph M. Wintersteiger
bd187e0989
Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models.
...
Fixes #642
2016-06-09 17:51:31 +01:00
Christoph M. Wintersteiger
bfeab9cc15
Added facilities for hiding UFs in smt::model_generator
2016-06-09 17:49:45 +01:00
Christoph M. Wintersteiger
879363157f
Bugfix for fpa2bv_converter
2016-06-09 12:09:53 +01:00
Nikolaj Bjorner
cb29c07f06
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-08 13:56:12 -07:00
Nikolaj Bjorner
5253f3a12b
internalize unsupported operations
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-08 13:56:01 -07:00
Christoph M. Wintersteiger
9b91e6ff0a
Merge branch 'master' of https://github.com/Z3Prover/z3
2016-06-08 12:07:19 +01:00
Christoph M. Wintersteiger
a2eb824590
Added __nonzero__ and __bool__ functions to Python Z3 ASTs to enable use of Python lists (and similar).
...
Thanks to Vlad Shcherbina for the recommendation (see http://stackoverflow.com/questions/37669576/converting-z3-cnf-formula-into-list-of-lists-representation-using-z3py/37679447?noredirect=1#comment62859886_37679447 )!
2016-06-08 12:07:13 +01:00