From 54412b646ff2e4c97bf745eebc6da0c8238e4373 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Thu, 15 Aug 2024 11:56:58 +1000
Subject: [PATCH] Fix the binding of Not formulas in the TseitinEncoder bind
 helper

---
 crates/pindakaas/src/propositional_logic.rs | 23 ++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/crates/pindakaas/src/propositional_logic.rs b/crates/pindakaas/src/propositional_logic.rs
index 8bd49602f1..9051d4e2e0 100644
--- a/crates/pindakaas/src/propositional_logic.rs
+++ b/crates/pindakaas/src/propositional_logic.rs
@@ -52,7 +52,7 @@ impl Formula {
 					*lit
 				}
 			}
-			Formula::Not(f) => !(f.bind(db, name)?),
+			Formula::Not(f) => !(f.bind(db, name.map(|lit| !lit))?),
 			Formula::And(sub) => {
 				match sub.len() {
 					0 => {
@@ -257,6 +257,10 @@ impl<DB: ClauseDatabase> Encoder<DB, Formula> for TseitinEncoder {
 					let neg_els: Formula = !*els.clone();
 					self.encode(&mut cdb, &neg_els)
 				}
+				Formula::Xor(sub) => {
+					let neg_sub = sub.iter().map(|f| !(f.clone())).collect();
+					self.encode(db, &Formula::Xor(neg_sub))
+				}
 				_ => {
 					let l = f.bind(db, None)?;
 					db.add_clause([!l])
@@ -509,4 +513,21 @@ mod tests {
 			vec![lits![-1, -2, -3, -4], lits![-1, -2, 3, 4], lits![1, -2, 3, -4], lits![1, 2, 3, 4], lits![1, 2, -3, 4], lits![1, -2, -3, -4], lits![-1, 2, 3, 4], lits![-1, 2, -3, -4]]
 		);
 	}
+
+	#[test]
+	fn encode_prop_neg_equiv() {
+		// Regression test
+		assert_enc_sol!(
+			TseitinEncoder,
+			2,
+			&Formula::Equiv(vec![
+				Formula::Atom(2.into()),
+				Formula::Not(Box::new(Formula::Xor(vec![Formula::Atom(1.into())]))),
+			])
+			=> vec![
+				lits![1,2], lits![-1,-2]
+			],
+			vec![lits![1,-2], lits![-1,2]]
+		);
+	}
 }