From 1fb04463a58f64fd81194d9c63110c0664b4d832 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Dac=C3=ADk?= <xdacik00@stud.fit.vutbr.cz>
Date: Mon, 10 Feb 2025 13:33:54 +0100
Subject: [PATCH] [Preprocessing] Generalise negation normalisation + tests

---
 src/preprocessing/NegationNormalisation.ml    | 11 +++++++
 tests/dune                                    |  1 +
 .../NegationNormalisation_tests.ml            | 31 +++++++++++++++++++
 3 files changed, 43 insertions(+)
 create mode 100644 tests/preprocessing/NegationNormalisation_tests.ml

diff --git a/src/preprocessing/NegationNormalisation.ml b/src/preprocessing/NegationNormalisation.ml
index 4797a6c..29d0ab1 100644
--- a/src/preprocessing/NegationNormalisation.ml
+++ b/src/preprocessing/NegationNormalisation.ml
@@ -6,6 +6,9 @@
 
 open SL
 
+let is_negation phi = match SL.view phi with Not _ -> true | _ -> false
+let get_negation phi = match SL.view phi with Not psi -> psi | _ -> assert false
+
 let normalise =
   SL.map_view (function
     | And [f1; f2] -> begin match SL.view f1, SL.view f2 with
@@ -14,6 +17,14 @@ let normalise =
       | _, Not g2       -> SL.mk_gneg f1 g2
       | _, _           -> SL.mk_and @@ [f1; f2]
     end
+    | And psis ->
+      let negated, others = List.partition is_negation psis in
+      begin match negated with
+      | [negation] ->
+        let phi = SL.mk_gneg (SL.mk_and others) (get_negation negation) in
+        SL.print phi;
+        phi
+      end
     | Or [f1; f2] -> begin match SL.view f1, SL.view f2 with
       | Not g1, Not g2 -> SL.mk_not @@ SL.mk_and [g1; g2]
       | Not g1, _      -> SL.mk_not @@ SL.mk_gneg g1 f2
diff --git a/tests/dune b/tests/dune
index 7fda1a2..cab6f68 100644
--- a/tests/dune
+++ b/tests/dune
@@ -19,6 +19,7 @@
     ;; Preprocessing tests
     IntroduceITE_tests
     QuantifierElimination_tests
+    NegationNormalisation_tests
 
     ;Simplifier_tests
     RemoveVariadic_tests
diff --git a/tests/preprocessing/NegationNormalisation_tests.ml b/tests/preprocessing/NegationNormalisation_tests.ml
new file mode 100644
index 0000000..e1839d4
--- /dev/null
+++ b/tests/preprocessing/NegationNormalisation_tests.ml
@@ -0,0 +1,31 @@
+(* Tests for negation normalisation.
+ *
+ * Author: Tomas Dacik (idacik@fit.vut.cz), 2025 *)
+
+module SL = SL_testable
+open SL
+
+let check_apply = SL.check_apply NegationNormalisation.apply
+
+let test1 () =
+  let lhs = SL.mk_pto x x in
+  let rhs = SL.mk_pto y y in
+  let input = SL.mk_and [lhs; SL.mk_not rhs] in
+  let expected = SL.mk_gneg lhs rhs in
+  check_apply ~input ~expected
+
+let test2 () =
+  let psi1 = SL.mk_pto x x in
+  let psi2 = SL.mk_pto y y in
+  let psi3 = SL.mk_pto z z in
+  let input = SL.mk_and [psi1; psi2; SL.mk_not psi3] in
+  let expected = SL.mk_gneg (SL.mk_and [psi1; psi2]) psi3 in
+  check_apply ~input ~expected
+
+let () =
+  run "Negation normalisation" [
+    "apply", [
+      test_case "Binary" `Quick test1;
+      test_case "N-anary" `Quick test2;
+    ];
+  ]