Nikolaj Bjorner
|
999d17e29b
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2017-02-02 11:29:19 -08:00 |
|
Nikolaj Bjorner
|
bd0bd6052a
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2017-02-02 10:19:21 -08:00 |
|
Nikolaj Bjorner
|
9ca52a3361
|
fix bug in lexicographic handling in maxres: previous assumptions were not committed in corner cases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-02 10:19:11 -08:00 |
|
Nikolaj Bjorner
|
2e89c2de3d
|
add par_or tactic to C++ API. #873
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-02 09:35:04 -08:00 |
|
Doug Woos
|
d6fbfe401e
|
add and use new is_pattern recognizer
|
2017-02-01 16:21:15 -08:00 |
|
Doug Woos
|
44c417904b
|
correctly pretty-print
|
2017-02-01 16:21:01 -08:00 |
|
Doug Woos
|
a147e2bc35
|
use is_uninterp
|
2017-02-01 16:20:40 -08:00 |
|
Nikolaj Bjorner
|
9cfd412cd0
|
enable pb theory always as pb terms can be introduced during transformations. Issue #884
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-01 15:28:29 -08:00 |
|
Nikolaj Bjorner
|
256a0e2d82
|
move exchange par
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-01 12:12:26 -08:00 |
|
Nikolaj Bjorner
|
40177f7bac
|
bypass combined solver when logic is set to QF_FD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-01 08:05:04 -08:00 |
|
Nikolaj Bjorner
|
4d8d705b3f
|
bypass combined solver when logic is set to QF_BV or QF_FD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-01 08:02:24 -08:00 |
|
Nikolaj Bjorner
|
f015e3e4cc
|
fix bug in propagation of parameters to combined solvers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-31 17:17:58 -08:00 |
|
Nikolaj Bjorner
|
bdfa84c6fe
|
fix issues with running parallel solver: random strategy should not be a default on all solvers. Also reuse base solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-31 13:22:03 -08:00 |
|
Doug Woos
|
d9e43f0e6d
|
use insert_if_not_there
|
2017-01-31 11:48:52 -08:00 |
|
Doug Woos
|
89ba99918e
|
reindent
|
2017-01-31 11:48:52 -08:00 |
|
Doug Woos
|
c0bb6dd2be
|
delete unused args
|
2017-01-31 11:48:51 -08:00 |
|
Doug Woos
|
da63f6b0ff
|
delete comment
|
2017-01-31 11:48:51 -08:00 |
|
Doug Woos
|
b00c4d2e64
|
add name
|
2017-01-31 11:48:51 -08:00 |
|
Murphy Berzish
|
19779f1a9b
|
fix string operators in theory_str, this breaks theory_seq temporarily
|
2017-01-31 11:49:10 -05:00 |
|
Nikolaj Bjorner
|
1d1949e395
|
ensure that parallel threads are only invoked when thread count > 1
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-30 18:30:06 -08:00 |
|
Doug Woos
|
8196173e29
|
Introduce and use labels_vec
|
2017-01-30 15:50:34 -08:00 |
|
Doug Woos
|
3791810920
|
add const &
|
2017-01-30 15:09:57 -08:00 |
|
Murphy Berzish
|
ebcfa966c7
|
data structure refactor in theory_str
|
2017-01-30 16:07:32 -05:00 |
|
Nikolaj Bjorner
|
af0ea13570
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2017-01-30 11:30:52 -08:00 |
|
Nikolaj Bjorner
|
76bc4f0b38
|
refine parsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-30 11:30:42 -08:00 |
|
Christoph M. Wintersteiger
|
841b5be40b
|
Merge pull request #885 from martin-neuhaeusser/master
Fix off-by-one bug in array indexing in the OCaml bindings
|
2017-01-30 17:58:42 +00:00 |
|
martin-neuhaeusser
|
0e966f21ff
|
Fix off-by-one bug in array indexing in the OCaml bindings
This patch fixes an off-by-one bug that occurred in the construction of output arrays
in the OCaml bindings.
|
2017-01-30 17:28:24 +01:00 |
|
Nikolaj Bjorner
|
dadcc6e8ff
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2017-01-30 02:09:26 -08:00 |
|
Nikolaj Bjorner
|
37ee4c95c3
|
adding parallel threads
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-30 02:09:08 -08:00 |
|
Murphy Berzish
|
fa1ec0b80f
|
smtlib25 draft standard in theory_str
|
2017-01-27 16:49:40 -05:00 |
|
Murphy Berzish
|
a879b24011
|
add str.prefixof, str.suffixof in theory_str
|
2017-01-27 16:26:30 -05:00 |
|
Doug Woos
|
a9d61d48ae
|
Add basic Sine Qua Non filtering
|
2017-01-27 11:22:39 -08:00 |
|
Doug Woos
|
5796e15088
|
Thread labels through tactic system
|
2017-01-27 11:07:13 -08:00 |
|
Nikolaj Bjorner
|
b70f1f0319
|
fix overflow exposed in #880
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-27 09:47:18 -08:00 |
|
Nikolaj Bjorner
|
962979b09c
|
rework sat.mus to use restart count for bounded minimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-26 13:28:40 -08:00 |
|
Nikolaj Bjorner
|
c3eb279637
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2017-01-26 08:37:54 -08:00 |
|
Nikolaj Bjorner
|
a0a81fc2d7
|
add format #879
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-26 08:37:37 -08:00 |
|
Nikolaj Bjorner
|
7386e2f3e9
|
add warning for scearios of #876
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-25 18:29:30 -08:00 |
|
Nikolaj Bjorner
|
6e6c5935d7
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2017-01-25 18:09:37 -08:00 |
|
Nikolaj Bjorner
|
777091e653
|
fix part 1 of #875
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-25 18:09:27 -08:00 |
|
Nikolaj Bjorner
|
4782e19086
|
fix bug in sat-simplifier decreasing heap values of variables that are not in the heap
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-25 16:21:51 -08:00 |
|
Nikolaj Bjorner
|
60783e5696
|
fix regression for z3num
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-25 13:26:58 -08:00 |
|
Nikolaj Bjorner
|
4ec4abd7e3
|
fix test for int-value
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-23 13:31:43 -08:00 |
|
Murphy Berzish
|
09ac5645e4
|
parameterize theory-aware activity of overlap
|
2017-01-22 23:21:20 -05:00 |
|
Christoph M. Wintersteiger
|
adf8072eaa
|
Added option to limit the distance of unsat core extension through patterns.
|
2017-01-21 12:28:37 +00:00 |
|
Murphy Berzish
|
50e2273dbd
|
substr bugfix
|
2017-01-20 17:39:32 -05:00 |
|
Nikolaj Bjorner
|
1bfd09e16b
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2017-01-19 19:31:24 -08:00 |
|
Nikolaj Bjorner
|
e23509797a
|
access parameters from Python API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-19 19:28:20 -08:00 |
|
Christoph M. Wintersteiger
|
43d083bafb
|
Windows build fix.
|
2017-01-19 11:19:29 +00:00 |
|
Christoph M. Wintersteiger
|
b9bfd4ddf5
|
Merge pull request #854 from angr/fix/fpic-arm
Add -fpic to armv7/armv8 build
|
2017-01-18 21:55:52 +00:00 |
|