diff --git a/src/report.rs b/src/report.rs index af15e49..69c874a 100644 --- a/src/report.rs +++ b/src/report.rs @@ -12,7 +12,7 @@ impl std::fmt::Debug for Report { if let Some(source) = self.0.source() { writeln!(f, "\n\nCaused by:")?; - for (i, e) in std::iter::successors(Some(source), |e| e.source()).enumerate() { + for (i, e) in std::iter::successors(Some(source), |e| e.clone().source()).enumerate() { writeln!(f, " {}: {}", i, e)?; } } diff --git a/src/solver/dpll.rs b/src/solver/dpll.rs index 0bc7c11..29d4581 100644 --- a/src/solver/dpll.rs +++ b/src/solver/dpll.rs @@ -17,10 +17,10 @@ mod inner { } impl Watch { - pub fn new(clauses: &[Clause]) -> Self { + pub fn new(clauses: &[Clause], num_variabels: usize) -> Self { let mut watch = Self { - positive: vec![Vec::new(); clauses.len()], - negative: vec![Vec::new(); clauses.len()], + positive: vec![Vec::new(); num_variabels], + negative: vec![Vec::new(); num_variabels], }; for (idx, clause) in clauses.iter().enumerate() { @@ -171,7 +171,7 @@ impl Solver for DpllSolver { let num_variables = formula.num_variables(); let num_clauses = formula.clauses().len(); - let watch = Watch::new(formula.clauses()); + let watch = Watch::new(formula.clauses(), num_variables); let assignment = vec![None; num_variables]; let clause_stats = vec![Default::default(); num_clauses]; diff --git a/src/tests.rs b/src/tests.rs index e8c7625..fe8d07f 100644 --- a/src/tests.rs +++ b/src/tests.rs @@ -63,6 +63,8 @@ sat_testcase!(satch_cnfs, unit7); unsat_testcase!(satch_cnfs, unit8); unsat_testcase!(satch_cnfs, unit9); +sat_testcase!(satch_cnfs, var4clause3); + unsat_testcase!(satch_cnfs, full2); unsat_testcase!(satch_cnfs, full3); unsat_testcase!(satch_cnfs, full4); diff --git a/testcases/satch_cnfs/var4clause3.cnf b/testcases/satch_cnfs/var4clause3.cnf new file mode 100644 index 0000000..9c69db9 --- /dev/null +++ b/testcases/satch_cnfs/var4clause3.cnf @@ -0,0 +1,4 @@ +p cnf 4 3 +-1 2 0 +-2 -3 0 +3 -4 0