rustsat_tools/
utils.rs

1/// Test a solver under two sets of assumptions and assert that the result is as
2/// given. This is used in the integration tests.
3#[macro_export]
4macro_rules! test_assignment {
5    ($solver:expr, $base_assumps:expr, $assumps:expr, $result:expr) => {{
6        let mut assumps = $base_assumps.clone();
7        assumps.extend($assumps);
8        let res = $solver.solve_assumps(&assumps).unwrap();
9        if res == rustsat::solvers::SolverResult::Sat && res != $result {
10            println!("{}", $solver.full_solution().unwrap());
11        }
12        debug_assert_eq!(res, $result);
13    }};
14}
15
16/// Test a solver under given assumptions while iterating through all possible
17/// assignments of the first 1-4 variables. This is used in the integration
18/// tests.
19#[macro_export]
20macro_rules! test_all {
21    ($solver:expr,
22     $assumps:expr,
23     $r1:expr,
24     $r0:expr ) => {{
25        println!("testing with assumptions {:?}", $assumps);
26        println!("testing 1");
27        test_assignment!($solver, $assumps, [lit![0]], $r1);
28        println!("testing 0");
29        test_assignment!($solver, $assumps, [!lit![0]], $r0);
30    }};
31    ($solver:expr,
32     $assumps:expr,
33     $r11:expr,
34     $r10:expr,
35     $r01:expr,
36     $r00:expr ) => {{
37        println!("testing with assumptions {:?}", $assumps);
38        println!("testing 11");
39        test_assignment!($solver, $assumps, [lit![0], lit![1]], $r11);
40        println!("testing 10");
41        test_assignment!($solver, $assumps, [lit![0], !lit![1]], $r10);
42        println!("testing 01");
43        test_assignment!($solver, $assumps, [!lit![0], lit![1]], $r01);
44        println!("testing 00");
45        test_assignment!($solver, $assumps, [!lit![0], !lit![1]], $r00);
46    }};
47    ($solver:expr,
48     $assumps:expr,
49     $r111:expr,
50     $r110:expr,
51     $r101:expr,
52     $r100:expr,
53     $r011:expr,
54     $r010:expr,
55     $r001:expr,
56     $r000:expr ) => {{
57        println!("testing with assumptions {:?}", $assumps);
58        println!("testing 111");
59        test_assignment!($solver, $assumps, [lit![0], lit![1], lit![2]], $r111);
60        println!("testing 110");
61        test_assignment!($solver, $assumps, [lit![0], lit![1], !lit![2]], $r110);
62        println!("testing 101");
63        test_assignment!($solver, $assumps, [lit![0], !lit![1], lit![2]], $r101);
64        println!("testing 100");
65        test_assignment!($solver, $assumps, [lit![0], !lit![1], !lit![2]], $r100);
66        println!("testing 011");
67        test_assignment!($solver, $assumps, [!lit![0], lit![1], lit![2]], $r011);
68        println!("testing 010");
69        test_assignment!($solver, $assumps, [!lit![0], lit![1], !lit![2]], $r010);
70        println!("testing 001");
71        test_assignment!($solver, $assumps, [!lit![0], !lit![1], lit![2]], $r001);
72        println!("testing 000");
73        test_assignment!($solver, $assumps, [!lit![0], !lit![1], !lit![2]], $r000);
74    }};
75    ($solver:expr,
76     $assumps:expr,
77     $r1111:expr,
78     $r1110:expr,
79     $r1101:expr,
80     $r1100:expr,
81     $r1011:expr,
82     $r1010:expr,
83     $r1001:expr,
84     $r1000:expr,
85     $r0111:expr,
86     $r0110:expr,
87     $r0101:expr,
88     $r0100:expr,
89     $r0011:expr,
90     $r0010:expr,
91     $r0001:expr,
92     $r0000:expr ) => {{
93        println!("testing with assumptions {:?}", $assumps);
94        println!("testing 1111");
95        test_assignment!(
96            $solver,
97            $assumps,
98            [lit![0], lit![1], lit![2], lit![3]],
99            $r1111
100        );
101        println!("testing 1110");
102        test_assignment!(
103            $solver,
104            $assumps,
105            [lit![0], lit![1], lit![2], !lit![3]],
106            $r1110
107        );
108        println!("testing 1101");
109        test_assignment!(
110            $solver,
111            $assumps,
112            [lit![0], lit![1], !lit![2], lit![3]],
113            $r1101
114        );
115        println!("testing 1100");
116        test_assignment!(
117            $solver,
118            $assumps,
119            [lit![0], lit![1], !lit![2], !lit![3]],
120            $r1100
121        );
122        println!("testing 1011");
123        test_assignment!(
124            $solver,
125            $assumps,
126            [lit![0], !lit![1], lit![2], lit![3]],
127            $r1011
128        );
129        println!("testing 1010");
130        test_assignment!(
131            $solver,
132            $assumps,
133            [lit![0], !lit![1], lit![2], !lit![3]],
134            $r1010
135        );
136        println!("testing 1001");
137        test_assignment!(
138            $solver,
139            $assumps,
140            [lit![0], !lit![1], !lit![2], lit![3]],
141            $r1001
142        );
143        println!("testing 1000");
144        test_assignment!(
145            $solver,
146            $assumps,
147            [lit![0], !lit![1], !lit![2], !lit![3]],
148            $r1000
149        );
150        println!("testing 0111");
151        test_assignment!(
152            $solver,
153            $assumps,
154            [!lit![0], lit![1], lit![2], lit![3]],
155            $r0111
156        );
157        println!("testing 0110");
158        test_assignment!(
159            $solver,
160            $assumps,
161            [!lit![0], lit![1], lit![2], !lit![3]],
162            $r0110
163        );
164        println!("testing 0101");
165        test_assignment!(
166            $solver,
167            $assumps,
168            [!lit![0], lit![1], !lit![2], lit![3]],
169            $r0101
170        );
171        println!("testing 0100");
172        test_assignment!(
173            $solver,
174            $assumps,
175            [!lit![0], lit![1], !lit![2], !lit![3]],
176            $r0100
177        );
178        println!("testing 0011");
179        test_assignment!(
180            $solver,
181            $assumps,
182            [!lit![0], !lit![1], lit![2], lit![3]],
183            $r0011
184        );
185        println!("testing 0010");
186        test_assignment!(
187            $solver,
188            $assumps,
189            [!lit![0], !lit![1], lit![2], !lit![3]],
190            $r0010
191        );
192        println!("testing 0001");
193        test_assignment!(
194            $solver,
195            $assumps,
196            [!lit![0], !lit![1], !lit![2], lit![3]],
197            $r0001
198        );
199        println!("testing 0000");
200        test_assignment!(
201            $solver,
202            $assumps,
203            [!lit![0], !lit![1], !lit![2], !lit![3]],
204            $r0000
205        );
206    }};
207}
rustsat_tools/utils.rs

rustsat_tools/
utils.rs
