Fix the binding of Not formulas in the TseitinEncoder bind helper

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]]
+		);
+	}
 }