Nikolaj Bjorner
|
4b35ef29c9
|
fix #2081
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-01-13 01:18:03 -08:00 |
|
Nikolaj Bjorner
|
64954cc551
|
fix pbge and reduce_tr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-13 09:07:58 -07:00 |
|
Nikolaj Bjorner
|
e7d43ed516
|
fix pb rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-12 11:22:05 -07:00 |
|
Nikolaj Bjorner
|
bee4716a85
|
lia2card simplifications, move up before elim01 (which could be deprecated)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-07 12:56:30 -08:00 |
|
Nikolaj Bjorner
|
354c16454a
|
fix bug in translation of pbeq into sat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-03 22:19:25 -08:00 |
|
Nikolaj Bjorner
|
badb32f9ae
|
neatify rewriting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-03 16:33:14 -08:00 |
|
Nikolaj Bjorner
|
651587ce01
|
merge with master branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-19 09:39:22 -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
|
b482dbd589
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-27 17:02:27 -07:00 |
|
Nikolaj Bjorner
|
244cbc2638
|
ensure that auxiliary PB booleans are recognized during rewriting. Fixes segementation fault #1113, but does not address performance issues with quantifiers and optimization combinations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-26 10:04:50 -07:00 |
|
Nikolaj Bjorner
|
77b2a015a2
|
rewrite pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-05-22 17:47:46 -07:00 |
|
Nikolaj Bjorner
|
cb6c6332b3
|
update conflict resolution for cardinality case
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-28 12:44:30 -08:00 |
|
Nikolaj Bjorner
|
3778048eb4
|
add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-23 20:31:59 -07:00 |
|
Nikolaj Bjorner
|
58198d7cb6
|
add consequence finding to inc-sat-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-16 15:45:39 -04:00 |
|
Nikolaj Bjorner
|
aec59e4ff7
|
add consequence finding to inc-sat-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-16 15:43:28 -04:00 |
|
Nikolaj Bjorner
|
8505ca843b
|
recognize more pb patterns
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-08-08 13:39:39 +02:00 |
|
Nikolaj Bjorner
|
4effa7f0c0
|
debug opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-03-17 21:13:31 -07:00 |
|
Nikolaj Bjorner
|
236b2d2ff3
|
working on incremtal PB theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-01-13 10:12:45 -08:00 |
|
Nikolaj Bjorner
|
24f2fd380c
|
adding pre-processing of BP constraints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-23 01:33:24 -08:00 |
|
Nikolaj Bjorner
|
fe5c42c90f
|
fixes to bugs exposed by regressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-12-15 05:23:47 +02:00 |
|