diff options
Diffstat (limited to 'vendor/varisat/tests/cnfs.rs')
-rw-r--r-- | vendor/varisat/tests/cnfs.rs | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/vendor/varisat/tests/cnfs.rs b/vendor/varisat/tests/cnfs.rs new file mode 100644 index 000000000..8797c6596 --- /dev/null +++ b/vendor/varisat/tests/cnfs.rs @@ -0,0 +1,27 @@ +use std::collections::HashSet; + +use varisat::{solver::Solver, Lit}; + +macro_rules! test_cnf { + ($name:ident, $result:expr) => { + #[test] + fn $name() { + let cnf = include_bytes!(concat!("cnfs/", stringify!($name), ".cnf")); + let mut solver = Solver::new(); + solver.enable_self_checking(); + let formula = varisat_dimacs::DimacsParser::parse(&cnf[..]).expect("parsing failed"); + solver.add_formula(&formula); + let result = $result; + assert_eq!(solver.solve().expect("solve failed"), result); + if result { + let model: HashSet<Lit> = solver.model().unwrap().into_iter().collect(); + for clause in formula.iter() { + assert!(clause.iter().any(|&lit| model.contains(&lit))); + } + } + } + }; +} + +test_cnf!(sgen1_unsat_57_0, false); +test_cnf!(sgen1_sat_90_0, true); |