From 4b5cc9d00753e1d1c708115f868ef87aab708dea Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 19 Aug 2024 11:15:33 +1000 Subject: [PATCH] Fix the binding of empty `Or` formulas in the TseitinEncoder --- crates/pindakaas/src/propositional_logic.rs | 26 ++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/crates/pindakaas/src/propositional_logic.rs b/crates/pindakaas/src/propositional_logic.rs index 9051d4e2e0..f0f5a12013 100644 --- a/crates/pindakaas/src/propositional_logic.rs +++ b/crates/pindakaas/src/propositional_logic.rs @@ -79,7 +79,11 @@ impl Formula { } Formula::Or(sub) => { match sub.len() { - 0 => return Err(Unsatisfiable), + 0 => { + let name = name.unwrap_or_else(|| db.new_var().into()); + db.add_clause([!name])?; + name + } 1 => return sub[0].bind(db, name), _ => { let name = name.unwrap_or_else(|| db.new_var().into()); @@ -365,6 +369,16 @@ mod tests { => vec![lits![-1, -2, 3], lits![1, -3], lits![2, -3]], vec![lits![1, 2, 3], lits![-1, 2, -3], lits![-1, -2, -3], lits![1, -2, -3]] ); + // Regression test: empty and + assert_enc_sol!( + TseitinEncoder, + 1, + &Formula::Equiv(vec![ + Formula::Atom(1.into()), + Formula::And(vec![]) + ]) + => vec![lits![1]], vec![lits![1]] + ); } #[test] @@ -393,6 +407,16 @@ mod tests { => vec![lits![1, 2, -3], lits![-1, 3], lits![-2, 3]], vec![lits![1, 2, 3], lits![-1, 2, 3], lits![-1, -2, -3], lits![1, -2, 3]] ); + // Regression test: empty or + assert_enc_sol!( + TseitinEncoder, + 1, + &Formula::Equiv(vec![ + Formula::Atom(1.into()), + Formula::Or(vec![]) + ]) + => vec![lits![-1]], vec![lits![-1]] + ); } #[test]