1.1 --- a/src/java-tests/isac/bridge/TestBridge.java Thu Feb 21 11:50:28 2008 +0100
1.2 +++ b/src/java-tests/isac/bridge/TestBridge.java Thu Feb 21 14:19:57 2008 +0100
1.3 @@ -469,7 +469,7 @@
1.4 System.out.println(".at " + ci.toSMLString() + ":");
1.5 for (int i = 0; i < tacs.size(); i++)
1.6 System.out.println(".." + ((Tactic) tacs.get(i)).toSMLString());
1.7 - assertEquals("number of appl. tacs = ", tacs.size(), 4);
1.8 + assertEquals("number of appl. tacs = ", tacs.size(), 3);
1.9
1.10 // on CalcHead of subproblem: only Apply_Method
1.11 pos = new Position();//([3],Pbl)
1.12 @@ -500,7 +500,7 @@
1.13 System.out.println(".at " + ci.toSMLString() + ":");
1.14 for (int i = 0; i < tacs.size(); i++)
1.15 System.out.println(".." + ((Tactic) tacs.get(i)).toSMLString());
1.16 - assertEquals("at ([3,1],Res) found: ", tacs.size(), 2);
1.17 + assertEquals("at ([3,1],Res) found: ", tacs.size(), 3);
1.18
1.19 // on the result of the subproblem again all tacs of the rootpbl
1.20 pos = new Position();//([3],Res)
1.21 @@ -515,7 +515,7 @@
1.22 System.out.println(".at " + ci.toSMLString() + ":");
1.23 for (int i = 0; i < tacs.size(); i++)
1.24 System.out.println(".." + ((Tactic) tacs.get(i)).toSMLString());
1.25 - assertEquals("at ([3],Res) found: ", tacs.size(), 4);
1.26 + assertEquals("at ([3],Res) found: ", tacs.size(), 1);
1.27
1.28 // but on the final result there are _NO_ tacs applicable
1.29 pos = new Position();//([],Res)
2.1 --- a/src/java-tests/isac/util/tactics/TestTactic.java Thu Feb 21 11:50:28 2008 +0100
2.2 +++ b/src/java-tests/isac/util/tactics/TestTactic.java Thu Feb 21 14:19:57 2008 +0100
2.3 @@ -8,6 +8,8 @@
2.4 */
2.5 package isac.util.tactics;
2.6
2.7 +import isac.util.formulae.Formula;
2.8 +
2.9 import java.util.Vector;
2.10
2.11 import junit.framework.TestCase;
2.12 @@ -37,4 +39,29 @@
2.13
2.14 System.out.println("---END isac.util.tactics.TestTactic#testTactics");
2.15 }
2.16 +
2.17 + /**
2.18 + * test method showToBeginner
2.19 + */
2.20 + public void testShowToBeginner() throws Exception {
2.21 + System.out
2.22 + .println("---BEGIN isac.util.tactics.TestTactic#testShowToBeginner");
2.23 +
2.24 + Tactic tac = new Rewrite();
2.25 + Theorem thm = new Theorem();
2.26 + Formula form = new Formula();
2.27 + form.setText("[| ?l is_const; ?m is_const |] ==> "
2.28 + + "?l * ?n + ?m * ?n = (?l + ?m) * ?n");
2.29 + thm.setFormula(form);
2.30 + ((Rewrite) tac).setTheorem(thm);
2.31 +
2.32 + String xxx;
2.33 + xxx = form.toString();
2.34 + xxx = (thm.getFormula()).toString();
2.35 + xxx = tac.showToBeginner();
2.36 + System.out.println("xxx="+ tac.showToBeginner());
2.37 +
2.38 + System.out
2.39 + .println("---END isac.util.tactics.TestTactic#testShowToBeginner");
2.40 + }
2.41 }
2.42 \ No newline at end of file
3.1 --- a/src/java/isac/util/tactics/Rewrite.java Thu Feb 21 11:50:28 2008 +0100
3.2 +++ b/src/java/isac/util/tactics/Rewrite.java Thu Feb 21 14:19:57 2008 +0100
3.3 @@ -19,6 +19,13 @@
3.4 }
3.5
3.6 /**
3.7 + *
3.8 + */
3.9 + public String showToBeginner() {
3.10 + return theorem_.getFormula();
3.11 + }
3.12 +
3.13 + /**
3.14 * @return
3.15 */
3.16 public Theorem getTheorem() {
4.1 --- a/src/java/isac/util/tactics/Tactic.java Thu Feb 21 11:50:28 2008 +0100
4.2 +++ b/src/java/isac/util/tactics/Tactic.java Thu Feb 21 14:19:57 2008 +0100
4.3 @@ -102,7 +102,8 @@
4.4 * @see isac.util.CalcElement#getText()
4.5 */
4.6 public String toSMLString() {
4.7 - return null;
4.8 + //return null; ... before WN082021
4.9 + return "WN082021 not implemented for non-rewrite-tacs";
4.10 }
4.11
4.12 /**
5.1 --- a/src/java/isac/util/tactics/Theorem.java Thu Feb 21 11:50:28 2008 +0100
5.2 +++ b/src/java/isac/util/tactics/Theorem.java Thu Feb 21 14:19:57 2008 +0100
5.3 @@ -1,5 +1,5 @@
5.4 /*
5.5 - * @author Richard Rradischnegg
5.6 + * @author Richard Gradischnegg
5.7 * Created on Jun 25, 2004
5.8 */
5.9 package isac.util.tactics;