]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/app/src/main/java/com/example/furt/myapplication/RuleAndElimination.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / app / src / main / java / com / example / furt / myapplication / RuleAndElimination.java
diff --git a/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleAndElimination.java b/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleAndElimination.java
new file mode 100644 (file)
index 0000000..5970a86
--- /dev/null
@@ -0,0 +1,41 @@
+package com.example.furt.myapplication;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class RuleAndElimination implements EliminationRule
+{
+    String ruleName;
+    FormulaAnd Fn;
+    RuleAndElimination(FormulaAnd F){
+        Fn=F;
+        ruleName="∧e";
+    }
+    public Node createNodes(Formula F,askFormula ask)
+    {
+            Formula C;
+            if (F==null) //applicazione Top-Down: chiamo la callback
+                C=ask.Ask();
+            else
+                C=F; //applicazione bottom-up: il nuovo nodo è la formula F passata
+            Node cNode=new Node(C);
+            if ((C.toString().equals(Fn.leftF.toString())) || (C.toString().equals(Fn.rightF.toString()))) //Posso utilizzare le regole di eliminazione sinistra o destra
+            {
+                cNode.addChild(new Node(Fn));
+                cNode.ruleName=ruleName;
+                return cNode;
+            }
+            Node elNode=new Node(Fn);
+            List<Formula> HP=new ArrayList<Formula>();
+            HP.add(Fn.leftF);
+            HP.add(Fn.rightF);
+            cNode.addHPFormula(HP,true);
+            Node rNode=new Node(C);
+            rNode.addChild(elNode);
+            rNode.addChild(cNode);
+            rNode.ruleName=ruleName;
+            return rNode;
+    }
+}
+
+