]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/src/com/example/furt/myapplication/RuleAndElimination.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / src / com / example / furt / myapplication / RuleAndElimination.java
diff --git a/mainActivity/src/com/example/furt/myapplication/RuleAndElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleAndElimination.java
deleted file mode 100755 (executable)
index 5970a86..0000000
+++ /dev/null
@@ -1,41 +0,0 @@
-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;
-    }
-}
-
-