Nikolaj Bjorner
|
1dca6402fb
|
move model and proof converters to self-contained module
|
2022-11-03 05:23:01 -07:00 |
|
Bruce Mitchener
|
5d0dea05aa
|
Remove empty leaf destructors. (#6211)
|
2022-07-30 10:07:03 +01:00 |
|
Nikolaj Bjorner
|
9f2b18cac5
|
add tactic name
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-12-07 13:37:57 -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
|
51e459d02b
|
fix #3294
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-14 10:46:03 -07:00 |
|
Nikolaj Bjorner
|
c513f3ca09
|
merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-25 14:57:01 -07:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Bruce Mitchener
|
b7d1753843
|
Use override rather than virtual.
|
2018-02-09 21:19:27 +07:00 |
|
Nikolaj Bjorner
|
e4f29a7b8a
|
debugging mc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-01-19 21:09:52 -08:00 |
|
Nikolaj Bjorner
|
2f218b0bdc
|
remove also cores as arguments to tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-19 12:18:50 -08:00 |
|
Nikolaj Bjorner
|
4bbece6616
|
re-organize proof and model converters to be associated with goals instead of external
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-18 16:33:54 -08:00 |
|
Nikolaj Bjorner
|
df6b1a707e
|
remove proof_converter from tactic application, removing nlsat_tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-17 23:32:29 -08:00 |
|
Nikolaj Bjorner
|
dc0b2a8acf
|
remove extension model converter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-17 17:25:35 -08:00 |
|
Nikolaj Bjorner
|
0d15b6abb7
|
add stubs for converting assertions, consolidate filter_model_converter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-17 14:51:13 -08:00 |
|
Nikolaj Bjorner
|
3de8c193ea
|
implementing model updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-30 16:11:51 -05: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
|
b516f22549
|
refine test for non-fd to be more inclusive while addressing #1092
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-21 08:01:03 -07:00 |
|
Nikolaj Bjorner
|
a3ee785923
|
disable dt2bv for quantified variables as enum2bv does not handle them. #1092
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-21 07:29:21 -07:00 |
|
Nikolaj Bjorner
|
899843b7cd
|
fix unhandled finite domain sort rewrite case. Issue #918
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-26 17:20:54 -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
|
881e82e3fa
|
remove legacy interface to dt2bv tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-18 23:04:17 -04:00 |
|
Nikolaj Bjorner
|
d060359f01
|
add fd solver for finite domain queries
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-18 22:34:34 -04:00 |
|
Nikolaj Bjorner
|
9e4450228e
|
adding unit test for enumeration types
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-17 14:52:37 -04:00 |
|
Nikolaj Bjorner
|
d4539b8887
|
fix dt2bv transformation to only work with constants, issue #725
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-08-30 11:42:14 +08:00 |
|
Nikolaj Bjorner
|
5f5ef8b38d
|
adding support for distinct for dt2bv, re-entry harness for ~Context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-27 09:02:56 -07:00 |
|
Nikolaj Bjorner
|
a85c5f0fac
|
add handling of recognizers to enumeration types
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-24 17:29:17 -07:00 |
|
Nikolaj Bjorner
|
6bf446dfc2
|
add tactic to eliminate enumeration sorts in favor of bit-vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-23 14:13:40 -07:00 |
|
Nikolaj Bjorner
|
083939ab0e
|
add tactic to eliminate enumeration sorts in favor of bit-vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-23 14:11:21 -07:00 |
|