corrected negation embedding with more parentheses

leoprover · Jan 19, 2021 · 746e3ef · 746e3ef
1 parent b98f145
commit 746e3ef
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/lib_embedding/src/main/java/transformation/ModalTransformator.java b/lib_embedding/src/main/java/transformation/ModalTransformator.java
@@ -365,7 +365,12 @@ private void replaceNullaryAndUnaryOperators(Node leaf) throws AnalysisException
                 usedConnectives.add("mfalse");
                 break;
             case "~":
-                leaf.setLabel("mnot @");
+                Node operatorTree = leaf.getNextTopBranchingNode(); // should be thf_unary_formula
+                if (!operatorTree.getRule().equals("thf_unary_formula")) throw new ImplementationError("~ ... is not a thf_unary_formula.");
+                operatorTree.replaceChildAt(0, new Node("t_mnot", "mnot @"));
+                operatorTree.addChildAt(new Node("t_left_paren", "("), 0);
+                operatorTree.addChild(new Node("t_right_paren", ")"));
+//                leaf.setLabel("mnot @");
                 usedConnectives.add("mnot");
                 break;
             // embed simple modality