Nikolaj Bjorner
|
62ea86d5d2
|
fix #2832
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-12-29 10:55:58 -08:00 |
|
Nikolaj Bjorner
|
c476c4a86a
|
smtfd solver that uses lazy iteration around fd to produce theory lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-09-07 17:48:33 +03:00 |
|
Nikolaj Bjorner
|
42e21458ba
|
fix #2479
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-09 17:06:05 -07:00 |
|
Nikolaj Bjorner
|
e2d91ce1fc
|
distribute concat over bvxor and bvor, #2470
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-09 10:03:21 -07:00 |
|
Nikolaj Bjorner
|
8579a004d0
|
distribute concat over bvxor and bvor, #2470
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-07 15:14:58 -07:00 |
|
Nikolaj Bjorner
|
809b0ebca7
|
revert fix to #2417
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 11:24:01 -07:00 |
|
Nikolaj Bjorner
|
db274ebe01
|
relax condition for distributing extract over ite #2359
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-23 16:48:42 -07:00 |
|
Nikolaj Bjorner
|
05663592ee
|
fix #2173
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-03-10 14:42:00 -07:00 |
|
Nikolaj Bjorner
|
0d400a5ad6
|
fix bit2bool bug reported by Jianying Li
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-01-04 07:46:53 -08:00 |
|
Nikolaj Bjorner
|
38b5e6de56
|
fix #2019 - insufficient axioms for special cases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-12-08 13:57:35 +01:00 |
|
Nikolaj Bjorner
|
a20e68facc
|
throttel extract/ite rewriting to avoid perf-bug exposed in example from Lucas Cordeiro and Alessandro Trindade
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-12-07 17:54:49 +00:00 |
|
Florian Pigorsch
|
326bf401b9
|
Fix some spelling errors (mostly in comments).
|
2018-10-20 17:07:41 +02:00 |
|
Nuno Lopes
|
bc8cd7ff55
|
remove a few random mem allocs
|
2018-06-29 18:34:17 +01:00 |
|
Bruce Mitchener
|
2fa304d8de
|
Remove int64, uint64 typedefs in favor of int64_t / uint64_t.
|
2018-03-31 14:45:04 +07:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Nikolaj Bjorner
|
c6722859c2
|
update rewriting of equalities and monomials for regressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-03 14:36:03 -07:00 |
|
Nikolaj Bjorner
|
9e4b2a6795
|
port simplifications on bv2int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-28 02:55:50 -07:00 |
|
Nikolaj Bjorner
|
2b82fd5d0c
|
updated include directives
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-01 10:51:47 -07:00 |
|
Nikolaj Bjorner
|
b19f94ae5b
|
make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-31 13:24:11 -07:00 |
|
Nikolaj Bjorner
|
476b06fa14
|
fix compiler warnings, gcc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-09-28 16:42:07 -07:00 |
|
Mikolas Janota
|
ec47a1df50
|
Adding bv preprocessing techniques.
|
2016-09-16 19:44:37 +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 |
|
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
|
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 |
|
mikolas
|
9ba5bbfd33
|
Re-factoring and comments in bv_trailing.
|
2016-04-06 11:04:13 +01:00 |
|
Mikolas Janota
|
248feace34
|
fixing the behavior in bv_trailing
|
2016-04-06 11:04:11 +01:00 |
|
mikolas
|
fced47386e
|
More work on trailing 0 analysis.
|
2016-04-06 11:04:09 +01:00 |
|
mikolas
|
78cb1e3c7b
|
More work on trailing 0 analysis.
|
2016-04-06 11:04:05 +01:00 |
|
mikolas
|
c7f1746321
|
Starting to work on trailing 0 analysis.
|
2016-04-06 11:04:03 +01:00 |
|
Christoph M. Wintersteiger
|
c8af48d7ef
|
Bugfix for bvurem0 model evaluation (+1 rewriting step)
|
2016-03-17 13:09:52 +00:00 |
|
Nuno Lopes
|
73da4dda07
|
add a bv rewrite pattern:
(bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
|
2016-02-18 17:45:55 +00:00 |
|
Christoph M. Wintersteiger
|
ac19bfb032
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-02-05 13:53:41 +00:00 |
|
Christoph M. Wintersteiger
|
bb5118acbb
|
Bugfix for bv*div0 model construction.
|
2016-02-05 13:53:35 +00:00 |
|
Christoph M. Wintersteiger
|
21b85c27e1
|
whitespace
|
2016-02-05 13:47:14 +00:00 |
|
Nikolaj Bjorner
|
cf970fd76a
|
Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-05 10:59:24 +00:00 |
|
Nikolaj Bjorner
|
0c2334417c
|
fix build warnigs with && vs ||, tuning seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-01-07 06:53:00 -08:00 |
|
Nikolaj Bjorner
|
ee157e47e4
|
fix crash caused by recycling variable names. Stackoverflow segfault-in-bv-rewritermk-mul-eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-01-05 09:19:21 -08:00 |
|
Nikolaj Bjorner
|
8e26c97782
|
tuning bit-vector operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-21 13:09:03 +02:00 |
|
Nuno Lopes
|
0e387b2abe
|
use Z3_fallthrough instead of __falthrough directly to avoid messing with reserved identifiers
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
|
2015-10-09 18:06:49 +01:00 |
|
Ken McMillan
|
c007a5e5bd
|
merged with unstable
|
2014-08-06 11:16:06 -07:00 |
|
Leonardo de Moura
|
a71bb549c6
|
Add option :bv-sort-ac true
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-03-24 14:59:29 -07:00 |
|
Leonardo de Moura
|
8515044f8b
|
Add option bvnot2arith
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-27 20:28:42 -08:00 |
|
Leonardo de Moura
|
cec328cfdc
|
Add get_sort(expr * n) function that does not depend on ast_manager. Move power_of_two to rational class. Add arith_recognizers and bv_recognizers classes. The two new classes contain the 'read-only' methods from arith_util and bv_util.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-18 14:44:51 -08:00 |
|
Leonardo de Moura
|
a99b8fe797
|
exposed rewriter parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-02 22:03:30 -08:00 |
|
Leonardo de Moura
|
cf28cbab0a
|
saved params work
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-29 17:19:12 -08:00 |
|
Leonardo de Moura
|
cb8a6db51b
|
minor fixes after feedback from regression tests...
|
2012-10-30 09:20:28 -07:00 |
|
Leonardo de Moura
|
c5540c7de9
|
new xor simplification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-26 14:57:06 -07:00 |
|
Leonardo de Moura
|
0a4446ae26
|
reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-23 22:14:35 -07:00 |
|