[Preprocessing] Generalise negation normalisation + tests

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

tests/dune

@@ -19,6 +19,7 @@
     ;; Preprocessing tests
     IntroduceITE_tests
     QuantifierElimination_tests
+    NegationNormalisation_tests
 
     ;Simplifier_tests
     RemoveVariadic_tests

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