1use rustsat::{
4 encodings::pb::{BoundUpper, GeneralizedTotalizer},
5 instances::{BasicVarManager, Cnf, ManageVars},
6 lit,
7 types::{Lit, Var},
8};
9
10macro_rules! lits {
11 () => {
12 [
14 (lit![0], 24),
15 (lit![1], 30),
16 (lit![2], 13),
17 (lit![3], 11),
18 (lit![4], 42),
19 (lit![5], 6),
20 (lit![6], 44),
21 (lit![7], 14),
22 (lit![8], 46),
23 (lit![9], 9),
24 (lit![10], 31),
25 (lit![11], 31),
26 (lit![12], 25),
27 (lit![13], 24),
28 (lit![14], 16),
29 (lit![15], 50),
30 (lit![16], 18),
31 (lit![17], 23),
32 (lit![18], 37),
33 (lit![19], 11),
34 (lit![20], 34),
35 (lit![21], 1),
36 (lit![22], 34),
37 (lit![23], 46),
38 (lit![24], 49),
39 (lit![25], 6),
40 (lit![26], 28),
41 (lit![27], 46),
42 (lit![28], 3),
43 (lit![29], 9),
44 (lit![30], 27),
45 (lit![31], 35),
46 (lit![32], 46),
47 (lit![33], 9),
48 (lit![34], 36),
49 (lit![35], 4),
50 (lit![36], 29),
51 (lit![37], 46),
52 (lit![38], 30),
53 (lit![39], 28),
54 (lit![40], 35),
55 (lit![41], 30),
56 (lit![42], 42),
57 (lit![43], 4),
58 (lit![44], 29),
59 (lit![45], 5),
60 (lit![46], 40),
61 (lit![47], 46),
62 (lit![48], 46),
63 (lit![49], 35),
64 ]
65 };
66}
67
68fn build_full_ub<PBE: BoundUpper + FromIterator<(Lit, usize)>>(lits: &[(Lit, usize)]) {
69 let mut enc = PBE::from_iter(lits.iter().copied());
70 let max_var = lits
71 .iter()
72 .fold(Var::new(0), |mv, (lit, _)| std::cmp::max(lit.var(), mv));
73 let mut var_manager = BasicVarManager::default();
74 var_manager.increase_next_free(max_var + 1);
75 let mut collector = Cnf::new();
76 enc.encode_ub(.., &mut collector, &mut var_manager).unwrap();
77}
78
79fn main() {
80 for idx in 0..1 {
81 build_full_ub::<GeneralizedTotalizer>(&lits!());
82 println!("iteration {idx}");
83 }
84}