Nikolaj Bjorner
e10850e66a
fix #5457
2021-08-05 11:27:03 -07:00
Nikolaj Bjorner
a39d1c6188
fix #5456
2021-08-04 10:07:29 -07:00
Nikolaj Bjorner
939860148f
#5452
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-03 20:03:34 -07:00
Nikolaj Bjorner
40f5270ae2
fix #5452
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-03 17:23:41 -07:00
Nikolaj Bjorner
da8530e2db
#5447
...
That the bug went away is a fluke. It wasnt fixed.
It is in pb-preprocess, an essentially unused tactic. The special subsumption resolution rule wasn't accounting for membership of all variables.
2021-08-02 09:03:15 -07:00
Nikolaj Bjorner
322531e95c
fix #5303
2021-05-25 10:20:20 -07:00
Nuno Lopes
f1e0d5dc8a
remove a hundred implicit constructors/destructors
2021-05-23 14:25:01 +01:00
Nikolaj Bjorner
e63e4587a4
build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-21 15:41:12 -07:00
Nikolaj Bjorner
4a6083836a
call it data instead of c_ptr for approaching C++11 std::vector convention.
2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
2fef6dc502
more scaffolding
2021-03-21 11:31:14 -07:00
Nikolaj Bjorner
8c66691e6d
disable propagation in proof mode as it produces ill-formed proof objects. Fixes #5063
2021-03-03 09:51:56 -08:00
Nuno Lopes
d6ce9cce95
fix clang warnings
2021-02-19 10:59:22 +00:00
Nikolaj Bjorner
8f577d3943
remove ast_manager get_sort method entirely
2021-02-02 13:57:01 -08:00
Nikolaj Bjorner
937b61fc88
fix build, refactor
2021-02-02 05:26:57 -08:00
Nikolaj Bjorner
3ae4c6e9de
refactor get_sort
2021-02-02 04:45:54 -08:00
Nikolaj Bjorner
4455f6caf8
move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail
2021-02-02 03:58:19 -08:00
Nikolaj Bjorner
96ab9edbfd
fix #4923
2021-01-09 01:21:50 -08:00
Nikolaj Bjorner
bb56443e71
more #4932
2021-01-08 15:24:12 -08:00
Nikolaj Bjorner
2679ae517b
fix #4912
2020-12-23 15:04:25 -08:00
Nikolaj Bjorner
259a8ff786
fix #4907
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-12-20 11:02:19 -08:00
Nikolaj Bjorner
28a6da4532
fix #4902
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-12-18 14:43:00 -08:00
Nikolaj Bjorner
0ef8ebe89f
fix #4895
2020-12-14 15:05:51 -08:00
Nikolaj Bjorner
9b9d906702
fix #4871
2020-12-07 22:07:30 -08:00
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
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
f645ef7677
fix #4461
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-02 18:08:42 -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
dcb75c4b31
fix #4174
2020-05-01 13:15:51 -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
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
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
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
Nikolaj Bjorner
d0f94055e7
fix #3966
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-15 11:05:02 -07:00
Nikolaj Bjorner
5f81913292
fix #3951
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-14 10:51:16 -07:00
Nikolaj Bjorner
299a6f4aee
fix #3939
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-13 14:00:21 -07:00
Nuno Lopes
3313590b95
fix #3713 : too much caching in dom-simplify for OR expressions
2020-04-06 12:11:26 +01:00
Nikolaj Bjorner
426e4cc75c
fix #3557
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-03 16:37:59 -07:00
Nikolaj Bjorner
896a1b2048
fix #3679
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-02 15:04:56 -07:00
Nikolaj Bjorner
c6b4641050
fix #3649
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-01 10:56:27 -07:00
Nikolaj Bjorner
ae447cfdad
fix #3603 - false positive, it is an irrational algebraic numeral
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-31 15:15:39 -07:00
Nikolaj Bjorner
a1f68a619d
fix #3612
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-31 15:09:12 -07:00
Nuno Lopes
79eb6a0e66
reduce_invertible: fix mk_diagonal for BV 0
...
switch from -x to ~x
2020-03-31 12:22:43 +01:00
Nuno Lopes
91497f923a
reduce_invertible: recognize (* x -1) as the same as (- x)
2020-03-31 10:54:03 +01:00
Nikolaj Bjorner
296e56c28f
fix #3575
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 17:26:43 -07:00
Nikolaj Bjorner
330b3cc8d6
fix #3584
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-30 16:50:53 -07:00