Nikolaj Bjorner
|
3c9ada54b6
|
tune hoist-rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 11:25:18 -08:00 |
|
Nikolaj Bjorner
|
768e2c1d0d
|
tune hoist-rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 11:25:17 -08:00 |
|
Nikolaj Bjorner
|
ab199dedf9
|
debug arith/mbi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-02 12:13:19 -08:00 |
|
Nikolaj Bjorner
|
0e1def5bd6
|
fix #4736
|
2020-10-30 01:54:42 -07:00 |
|
Nikolaj Bjorner
|
1d199b707b
|
connect mbi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-29 23:51:31 -07:00 |
|
Nikolaj Bjorner
|
367e5fdd52
|
delay internalize (#4714)
* adding array solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use default in model construction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debug delay internalization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* get rid of implied values and bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* redo egraph
* remove out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-28 19:24:16 -07:00 |
|
Nikolaj Bjorner
|
d3d05e2e99
|
add side-constraints in pb2bv-tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-20 07:03:06 -07:00 |
|
Nikolaj Bjorner
|
6f63f8761c
|
optimizations to bv-solver and euf-egraph (#4698)
* additional bit-vector propagators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* rename restrict (not a keyword, but well) #4694, tune euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add pb rewriting to pb2bv #4697
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-20 06:47:27 -07:00 |
|
Nikolaj Bjorner
|
549753845e
|
bv and gc of literals (#4692)
* bv and gc of literals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* overload
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* diseq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* diseq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-17 14:24:07 -07:00 |
|
Nikolaj Bjorner
|
2d52367368
|
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-15 16:45:11 -07:00 |
|
Nikolaj Bjorner
|
2328a6e839
|
add a way to use new smt core for selected logics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-14 10:43:52 -07:00 |
|
Nikolaj Bjorner
|
629e981e01
|
fix regression in get-consequence on QF_FD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-08 12:43:18 -07:00 |
|
Arie Gurfinkel
|
687a16a796
|
SMTFD is back (#4676)
|
2020-09-04 10:50:35 -07:00 |
|
Nikolaj Bjorner
|
54a75d6a91
|
remove SMTFD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-02 12:39:23 -07:00 |
|
Nikolaj Bjorner
|
dbe2c9b305
|
encoding options #4665
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-30 10:24:42 -07:00 |
|
Nikolaj Bjorner
|
11c90cc142
|
move parameters from ast/rewriter to params
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-29 11:11:16 -07:00 |
|
Nikolaj Bjorner
|
5aaa7e0022
|
fix #4648
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-18 22:47:58 -07:00 |
|
Nikolaj Bjorner
|
59d8895d15
|
add accessors for implied values to API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-28 19:46:39 -07:00 |
|
Christoph M. Wintersteiger
|
c321fb7726
|
Correctly report unsupported features in bvarray2uf_rewriter. Fixes #4046 and #4047.
|
2020-07-15 16:16:29 +00:00 |
|
Nuno Lopes
|
f30e8ccec3
|
fix crashes due to my last commit
|
2020-07-12 19:53:22 +01:00 |
|
Nuno Lopes
|
bb26f219fe
|
remove unneeded constructors (last round)
|
2020-07-12 17:41:57 +01:00 |
|
Nikolaj Bjorner
|
d0e20e44ff
|
booyah
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-04 15:56:30 -07:00 |
|
Nikolaj Bjorner
|
278e004385
|
fix #4428, and then there were none, almost
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-04 01:28:26 -07:00 |
|
Nikolaj Bjorner
|
80d5d66158
|
handling cancelation #4425
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-04 01:12:04 -07:00 |
|
Nikolaj Bjorner
|
f645ef7677
|
fix #4461
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-02 18:08:42 -07:00 |
|
Nikolaj Bjorner
|
d603bd7e3b
|
disable selected functionality in SINGLE_THREAD mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 14:47:33 -07:00 |
|
Lev Nachmanson
|
8c92cf1b32
|
restore the tactics with nlsat
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
e32a6714a5
|
call nlsat
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Nikolaj Bjorner
|
2a93ac3d81
|
fix #4200
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-03 18:10:26 -07:00 |
|
Nikolaj Bjorner
|
dc9221e4bd
|
limit iterations on equality solver based on experimenting with #4178
|
2020-05-02 17:10:18 -07:00 |
|
Nikolaj Bjorner
|
47fa6ba7a6
|
fix #4191
|
2020-05-02 11:15:11 -07:00 |
|
Nikolaj Bjorner
|
6088da5159
|
fix #4176
|
2020-05-01 16:34:33 -07:00 |
|
Nikolaj Bjorner
|
dcb75c4b31
|
fix #4174
|
2020-05-01 13:15:51 -07:00 |
|
Nikolaj Bjorner
|
0e77074e84
|
another revision of purify_arith, fix #4144
|
2020-04-29 12:07:02 -07:00 |
|
Nikolaj Bjorner
|
3fc001baea
|
simplifications noticed by trying #4147
The change masks possible bugs in smt.threads and arrays.
|
2020-04-29 12:07:01 -07:00 |
|
Nikolaj Bjorner
|
e67112f289
|
NYI control paths
|
2020-04-28 20:19:20 -07:00 |
|
Nikolaj Bjorner
|
4defe9b6ab
|
reorder
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-28 16:04:37 -07:00 |
|
Nikolaj Bjorner
|
8dde1bf86d
|
compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-28 16:02:32 -07:00 |
|
Nikolaj Bjorner
|
38e0968845
|
fix #4128
|
2020-04-27 17:10:48 -07:00 |
|
Nikolaj Bjorner
|
3a63c3751e
|
fix #4127
|
2020-04-27 13:27:00 -07:00 |
|
Nikolaj Bjorner
|
4938ea7be6
|
fix #4123
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-27 11:44:25 -07:00 |
|
Nikolaj Bjorner
|
1c2aa1076b
|
fix #4125
|
2020-04-27 11:31:02 -07:00 |
|
Nikolaj Bjorner
|
d818233063
|
unused variable warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-26 23:21:48 -07:00 |
|
Nikolaj Bjorner
|
735888145e
|
fix #4112
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-26 21:04:28 -07:00 |
|
Nikolaj Bjorner
|
a884201d62
|
remove using insert_if_not_there2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-25 15:08:51 -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
|
44957894ea
|
more checks for #4013
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 12:43:06 -07:00 |
|
Nikolaj Bjorner
|
339a2568b2
|
fix #4021
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 12:18:18 -07:00 |
|
Nikolaj Bjorner
|
d5eef9dd8b
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-16 18:53:00 -07:00 |
|
Nikolaj Bjorner
|
357ec2fd01
|
fix #3948 - cache has to be reset also when processing 'and' because it could be processed in an incompatible context by the caller
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 13:29:45 -07:00 |
|