Nikolaj Bjorner
|
615e2cf37c
|
don't rewrite empty/non-empty checking predicates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-31 11:47:52 -07:00 |
|
Nikolaj Bjorner
|
aab50ff3f5
|
fixing bugs reported in #4518
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-21 15:50:19 -07:00 |
|
Nikolaj Bjorner
|
c0fbb31379
|
use nonse based seed for transition characters
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-24 12:07:37 -07:00 |
|
Nikolaj Bjorner
|
6d17c656bd
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-28 10:32:38 -07:00 |
|
trinhmt
|
4aa1e60daa
|
fix branch_variable() (#4472)
* fixed branch_variable()
* add docs
|
2020-05-28 10:21:50 -07:00 |
|
Nikolaj Bjorner
|
88e36c6bf3
|
add general purpose emptiness/non-emptiness check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-26 20:42:21 -07:00 |
|
Nikolaj Bjorner
|
5e79eb62fd
|
add some notes to regex
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-26 13:30:52 -07:00 |
|
Nikolaj Bjorner
|
4e01d5b5c1
|
tune axioms for derivatives
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-25 14:11:59 -07:00 |
|
Nikolaj Bjorner
|
b43ed70874
|
extend monomial bounds to handle powers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-14 19:13:17 -07:00 |
|
Nikolaj Bjorner
|
9c3f0190f4
|
fix #4069
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-23 20:53:13 -07:00 |
|
Nikolaj Bjorner
|
95a78b2450
|
updates to seq and bug fixes (#4056)
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4037
* nicer output for skolem functions
* more overhaul of seq, some bug fixes
* na
* added offset_eq file
* na
* fix #4044
* fix #4040
* fix #4045
* updated ignore
* new rewrites for indexof based on #4036
* add shortcuts
* updated ne solver for seq, fix #4025
* use pair vectors for equalities that are reduced by seq_rewriter
* use erase_and_swap
* remove unit-walk
* na
* add check for #3200
* nits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* name a type
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove fp check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove unsound axiom instantiation for non-contains
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix rewrites
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4053
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4052
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-22 13:18:55 -07:00 |
|
Nikolaj Bjorner
|
a9c4984a16
|
more seq overhaul
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-18 19:46:30 -07:00 |
|
Nikolaj Bjorner
|
3e9479d01a
|
a lot of seq churn
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-17 18:21:40 -07:00 |
|
Nikolaj Bjorner
|
501aa7927d
|
split into seq_axioms and seq_skolem
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-17 06:14:52 -07:00 |
|