3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 19:01:50 +00:00
Commit graph

5497 commits

Author SHA1 Message Date
Nikolaj Bjorner b303fd59c0 add some version information (and date) to log file to make it easier to trap version mismatch on log files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-28 18:11:30 -07:00
Nikolaj Bjorner e4a00f6f6f re-include get_error_msg_ex per issue #660
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-28 17:48:11 -07:00
Nikolaj Bjorner 84aec95eda fix up use-list in 3x3 resolution case. Regression RND_3_24.smt2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-28 11:41:57 -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 b66d457b19 move arithmetical mbp functionality to model_based_opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-26 16:12:14 -07:00
Nikolaj Bjorner 7fc294d329 move arithmetical mbp functionality to model_based_opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-26 14:30:35 -07:00
Christoph M. Wintersteiger 628a6378c2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-24 18:13:08 +01:00
Christoph M. Wintersteiger ae54b9d158 Fixed FP math options for x86 cmake build. Fixes #644. 2016-06-24 18:13:02 +01:00
Nikolaj Bjorner 30cf0d19eb use of mk_bool_val
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-24 09:11:45 -07:00
Nikolaj Bjorner f72d9c25c6 merge with update to bv rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-24 09:08:01 -07:00
Nikolaj Bjorner 017165c474 fix bug with model completion and remove spurious std::cout
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-24 09:02:12 -07:00
Christoph M. Wintersteiger 70301ad3c8 Added bv*mul_no*flow handling in bv_rewriter.
Fixes #657.
2016-06-24 16:25:11 +01:00
Nikolaj Bjorner 67ea78a4a5 Add basic MARCO example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-24 08:00:23 -07:00
Nikolaj Bjorner 914bf2ff3b extend constant folding for bit-vector overflow/underflow operators, #657
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-06-24 07:43:05 -07: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