Nikolaj Bjorner
|
830a99aab4
|
finish minimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-01 00:04:03 -08:00 |
|
Andres Notzli
|
570bc3c9c1
|
Fix build
Previous commits seem to have removed some variable declarations, so the
build did not work. This patch reintroduces the variables.
|
2016-02-29 23:41:33 -08:00 |
|
|
Nikolaj Bjorner
|
4a15d756d7
|
uint64_t -> uint64 for cross platform
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-29 22:16:03 -08:00 |
|
|
Nikolaj Bjorner
|
b90bc4e685
|
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-29 21:15:44 -08:00 |
|
|
Nikolaj Bjorner
|
3b6eef05c9
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-02-29 20:23:29 -08:00 |
|
|
Nikolaj Bjorner
|
6cf76f2113
|
remove references to _DEBUG use Z3DEBUG instead
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-29 20:23:20 -08:00 |
|
|
Nikolaj Bjorner
|
6f45970b6e
|
Merge pull request #466 from 4tXJ7f/patch-1
Fix documentation for floating-point comparisons
|
2016-02-29 20:22:57 -08:00 |
|
|
Andres Nötzli
|
c9269c1983
|
Fix documentation for floating-point comparisons
|
2016-02-29 19:12:14 -08:00 |
|
|
Nikolaj Bjorner
|
7ac5e67538
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-02-29 17:04:32 -08:00 |
|
|
Nikolaj Bjorner
|
c6c84dd59a
|
update documentation help to be inline with fpLT. Issue #465
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-29 17:04:26 -08:00 |
|
Nuno Lopes
|
43202572ee
|
bv_bounds: switch from rational to uint64
this limits the analysis to 64-bit BVs, but gives a speedup of up to one order of magnitude
|
2016-02-29 17:23:54 +00:00 |
|
|
Nikolaj Bjorner
|
9efc7f4aea
|
turn on model completion in validation code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-29 09:06:20 -08:00 |
|
|
Nikolaj Bjorner
|
d89c39cbe2
|
apply t()
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-29 08:36:25 -08:00 |
|
|
Nuno Lopes
|
006dc147a8
|
fix build with gcc 5
|
2016-02-29 14:34:48 +00:00 |
|
|
Nikolaj Bjorner
|
7656adc483
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-02-28 17:05:52 -08:00 |
|
|
Nikolaj Bjorner
|
df2d7e7628
|
add intersection using symbolic automata facility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-28 17:05:12 -08:00 |
|
|
Nuno Lopes
|
c1eb1cc3f2
|
bv_bounds: improve perf of push/pop
|
2016-02-28 20:07:39 +00:00 |
|
|
Nuno Lopes
|
e7a360ca08
|
ctx_simplify: remove virtual push() method
|
2016-02-28 17:57:40 +00:00 |
|
|
Nuno Lopes
|
51687b2be7
|
bv_bounds: ensure (bvule x maxuint) is simplified to true
|
2016-02-28 10:56:48 +00:00 |
|
|
Nikolaj Bjorner
|
4cf72e23e6
|
fix python 3 compat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-27 09:58:45 -08:00 |
|
|
Nikolaj Bjorner
|
e659845bc0
|
tune handling of contains, avoid redundant equalities, merge use of indexof.left/right with contains.left/right adding only least-ness constraints in the context of index
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-27 09:56:11 -08:00 |
|
|
Nikolaj Bjorner
|
1c630ccc9a
|
Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD
|
2016-02-26 18:15:57 -08:00 |
|
|
Nikolaj Bjorner
|
ce8862d415
|
fix bug in conflict clause generation in seq-branch-variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-26 18:15:45 -08:00 |
|
|
Nuno Lopes
|
97d6098d00
|
bv_bounds: make may_simplify() more aggressive for the common case of a single comparison
fix expr_has_bounds to handle cases like (bvadd (ite c t e) ...)
|
2016-02-25 19:41:01 +00:00 |
|
|
Nuno Lopes
|
6563e458f0
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-02-25 16:53:45 +00:00 |
|
|
Nuno Lopes
|
c693c990df
|
bv_bounds: speedup up to 10x in larger formulas
introduce a may_simplify() function to short-circuit evaluation of expression trees that are guaranteed to not be simplifiable
|
2016-02-25 16:53:35 +00:00 |
|
|
Nuno Lopes
|
d642d5fe4c
|
API: add smt.logic parameter to enable setting the logic through the API
currently only Z3_solver_set_params() is supported
logic has to be set before solver first usage or before solver reset
|
2016-02-25 09:47:51 +00:00 |
|
|
Nuno Lopes
|
c1aa33339d
|
bv_bounds: early exit in is_bound in case the expr is not boolean
~2% speedup
|
2016-02-25 09:32:10 +00:00 |
|
|
Nikolaj Bjorner
|
4c408165ab
|
Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD
|
2016-02-24 08:55:28 -08:00 |
|
|
Nikolaj Bjorner
|
5679fb5d6b
|
experimenting with alternative prefix encodings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-24 08:55:22 -08:00 |
|
|
Nikolaj Bjorner
|
4e7a867cd9
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-02-23 18:42:01 -08:00 |
|
|
Nikolaj Bjorner
|
d5383e2387
|
fix bug in definition of rewrite rule for replace, tighten constraints for tightest-prefix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-23 18:41:56 -08:00 |
|
|
Nikolaj Bjorner
|
8c68aed69e
|
Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD
|
2016-02-23 08:11:09 -08:00 |
|
|
Nuno Lopes
|
64888b6b19
|
ctx_simplify: fix bug in simplification of or exprs
this triggered when the or covers the whole space -> true
|
2016-02-23 10:37:01 +00:00 |
|
|
Nuno Lopes
|
12458b1a84
|
remove dead code in qfufbv
|
2016-02-22 10:22:56 +00:00 |
|
|
Nikolaj Bjorner
|
63c138c08e
|
add option to enable equality propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-21 11:16:13 -08:00 |
|
|
Nikolaj Bjorner
|
8c538fd3f0
|
setting partial equivalence priority lower so that it doesn't intefere with inlining (partial fix to the fact that inlining will remove such implicit relations). Using short-circuit negation in qe to avoid redundant double negations in intermediary results
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-21 10:31:13 -08:00 |
|
|
Nikolaj Bjorner
|
d4f41c0420
|
add goal context for simplifier, disable equality creation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-20 10:13:24 -08:00 |
|
|
Nikolaj Bjorner
|
c7abc11ce0
|
Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD
|
2016-02-19 08:23:32 -08:00 |
|
|
Nikolaj Bjorner
|
bff10527d1
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-19 08:23:27 -08:00 |
|
|
Nuno Lopes
|
7d3af70a63
|
ctx-simplify: fix mem leak of simplifier
|
2016-02-19 11:08:01 +00:00 |
|
|
Nuno Lopes
|
c618838ed9
|
bv_bounds: fix crash in push() when realloc happened
|
2016-02-19 11:06:22 +00:00 |
|
|
Nuno Lopes
|
121b3b60f3
|
bv_bounds/ctx_simplify: improve handling of (ite x a b) where (not x) is proved to be false
|
2016-02-19 09:42:42 +00:00 |
|
|
Nikolaj Bjorner
|
73f93dbadb
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-02-18 18:10:30 -08:00 |
|
|
Nikolaj Bjorner
|
a073b37ce3
|
fix bugs in seq solver: add relevancy and axiom
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-18 18:10:16 -08:00 |
|
|
Nikolaj Bjorner
|
5962ca2a62
|
seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-18 12:08:35 -08: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 |
|
|
Nuno Lopes
|
d32b4c71d1
|
[bv_bounds] introduce a tight bit in intervals to denote they are tight (over and under approx)
use this to ensure certain transformations remain sound
|
2016-02-18 15:53:11 +00:00 |
|
|
Nikolaj Bjorner
|
67958efed2
|
add fixed length heuristic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-02-17 21:20:39 -08:00 |
|
|
Nuno Lopes
|
8718c1c99f
|
bv_bounds: simplify negated expressions as well
|
2016-02-17 19:14:02 +00:00 |
|