1.1 --- a/test/Tools/isac/Knowledge/rational.sml Wed Dec 05 09:58:28 2012 +0100
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Dec 05 10:21:35 2012 +0100
1.3 @@ -45,6 +45,7 @@
1.4 "----------- get_denominator ----------------------------";
1.5 "--------- several errpats in complicated term -------------------";
1.6 "--------------------------------------------------------";
1.7 +"-------- nonterminating cancel_p, norm_Rational 2002 ---";
1.8 "--------------------------------------------------------";
1.9 "--------------------------------------------------------";
1.10
1.11 @@ -2098,3 +2099,149 @@
1.12 autoCalculate 1 CompleteCalc;
1.13 val ((pt,p),_) = get_calc 1; show_pt pt;
1.14
1.15 +"-------- nonterminating cancel_p, norm_Rational 2002 ---";
1.16 +"-------- nonterminating cancel_p, norm_Rational 2002 ---";
1.17 +"-------- nonterminating cancel_p, norm_Rational 2002 ---";
1.18 +(*------------------------------------------------------------------------------------\
1.19 +"--- WN121204: searched rational.sml for "nonterm", added new numbering" ^
1.20 +" and thoroughly tested with this numbering subsequently";
1.21 +"--- 1 ---";
1.22 +WN.2.6.03 from rlang.sml 56a
1.23 +val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
1.24 +val NONE = rewrite_set_ thy false common_nominator_p t;
1.25 +"--- 2 ---";
1.26 +WN060831 nonterm.SK7
1.27 +val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.28 +val NONE = add_fraction_p_ thy t;
1.29 +"--- 3 ---";
1.30 +nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
1.31 +val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.32 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
1.33 +"--- 4 ---";
1.34 +val t = str2term
1.35 +"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
1.36 +WN060831 nonterm.SK10
1.37 +val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.38 +term2str t;
1.39 +"--- 5 ---";
1.40 +val t = str2term
1.41 +"(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.42 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.43 +if term2str t =
1.44 +then ()
1.45 +else error "rational.sml: diff.behav. in norm_Rational_mg 42";
1.46 +"--- 6 ---";
1.47 +val t = str2term
1.48 +"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.49 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.50 +... non terminating.
1.51 +"--- 7 ---";
1.52 +val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1.53 +"(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
1.54 +val SOME (t,_) = rewrite_set_ thy false cancel_p t';
1.55 +"--- 8 ---";
1.56 +val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1.57 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.58 +"--- 9 ---";
1.59 +val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
1.60 + "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1.61 + "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
1.62 + "(20*x*y/(x^^^2 - 25*y^^^2))";
1.63 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.64 +"--- 10 ---";
1.65 +SK060904-2a non-termination of add_fraction_p_";
1.66 +val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
1.67 + " (-1 * a + b * x) / (a + b * x) ");
1.68 +(* nonterm.SK
1.69 +val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
1.70 +"--- 11 ---";
1.71 +common_nominator_p_ thy t;
1.72 +" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + " ^
1.73 +" (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
1.74 +"--- 12 ---";
1.75 +add_fraction_p_ thy t;
1.76 +" ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /" ^
1.77 +" ((a + b * x)*(-1 * a + b * x)) ";
1.78 +--------------------------------------------------------------------------------------/*)
1.79 +
1.80 +(*------------------------------------------------------------------------------------\
1.81 +"WN121205: thoroughly tested with the above numbering.";
1.82 +" errors in cancel_p: --- 4,5,6,7.";
1.83 +" error in common_nominator_p, common_nominator_p_: --- 10; 1,2?.";
1.84 +" errors caused by ruleset norm_Rational: --- 8,9.";
1.85 +trace_rewrite := true;
1.86 +
1.87 +"--- 1 ---: non-terminating with ### add_fract: done t22 ";
1.88 +val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
1.89 +trace_rewrite:= true;
1.90 +rewrite_set_ thy false common_nominator_p t;
1.91 +
1.92 +"--- 2 ---: non-terminating with ### add_fract: done t22 ";
1.93 +val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.94 +add_fraction_p_ thy t;
1.95 +
1.96 +"--- 3 ---: norm_Rational calls Rrls cancel_p with non-normalised polys";
1.97 +val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.98 +rewrite_set_ thy false norm_Rational t;
1.99 +(*tracing end...#### rls: cancel_p on:
1.100 +(a * x ^^^ 2 + -2 * (a * (x * y)) + a * y ^^^ 2 + b * x ^^^ 2 + -2 * (b * (x * y)) + b * y ^^^ 2) /
1.101 +(a ^^^ 2 * x ^^^ 2 + -1 * (a ^^^ 2 * y ^^^ 2) + -1 * (b ^^^ 2 * x ^^^ 2) + b ^^^ 2 * y ^^^ 2) *)
1.102 +
1.103 +"--- 4 ---: non-terminating with Rrls cancel_p on plausible input";
1.104 +val t = str2term (
1.105 +"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /"^
1.106 +"(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)");
1.107 +rewrite_set_ thy false cancel_p t;
1.108 +(*# rls: cancel_p on:
1.109 +(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /
1.110 +(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2) *)
1.111 +
1.112 +"--- 5 ---: non-terminating with Rrls cancel_p on plausible input";
1.113 +val t = str2term "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.114 +rewrite_set_ thy false norm_Rational t;
1.115 +(*#### rls: cancel_p on:
1.116 +(2304 + -1152 * x + -2304 * y + 144 * x ^^^ 2 + 1152 * (x * y) + -144 * (x ^^^ 2 * y)) /
1.117 +(48 + -12 * x + -96 * y + 24 * (x * y) + 48 * y ^^^ 2 + -12 * (x * y ^^^ 2)) *)
1.118 +
1.119 +"--- 6 ---: non-terminating with Rrls cancel_p on plausible input";
1.120 +val t = str2term
1.121 +"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.122 +rewrite_set_ thy false norm_Rational t;
1.123 +(*### rls: cancel_p on: (-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * (x * y) +
1.124 + 144 * (x ^^^ 2 * y)) /
1.125 +(-48 + 12 * x + 96 * y + -24 * (x * y) + -48 * y ^^^ 2 + 12 * (x * y ^^^ 2)) *)
1.126 +
1.127 +"--- 7 ---: non-terminating with Rrls cancel_p on plausible input";
1.128 +val t' = str2term (
1.129 +"(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /"^
1.130 +"(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)");
1.131 +rewrite_set_ thy false cancel_p t';
1.132 +
1.133 +"--- 8 ---: bottom of output cannot be looked ad (due to looping?)";
1.134 +val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1.135 +val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.136 +
1.137 +"--- 9 ---: probably error in norm_Rational";
1.138 +val t = str2term (
1.139 +"((12*x*y / (9*x^^^2 - y^^^2)) / (1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1.140 + "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2) / (20*x*y/(x^^^2 - 25*y^^^2))");
1.141 +rewrite_set_ thy false norm_Rational t;
1.142 +(*#### rls: cancel_p on: (19440 * (x ^^^ 8 * y ^^^ 2) + -490320 * (x ^^^ 6 * y ^^^ 4) +
1.143 + 108240 * (x ^^^ 4 * y ^^^ 6) +
1.144 + -6000 * (x ^^^ 2 * y ^^^ 8)) /
1.145 +(2160 * (x ^^^ 8 * y ^^^ 2) + -108240 * (x ^^^ 6 * y ^^^ 4) +
1.146 + 1362000 * (x ^^^ 4 * y ^^^ 6) +
1.147 + -150000 * (x ^^^ 2 * y ^^^ 8)) *)
1.148 +
1.149 +"--- 10 ---: non-terminating with ### add_fract: done t22: error in common_nominator_p ";
1.150 +val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)");
1.151 +rewrite_set_ thy false common_nominator_p t; (*### add_fract: done t22 *)
1.152 +common_nominator_p_ thy t; (*loops without output*)
1.153 +"--- reformulated 10:";
1.154 +val t = str2term "(a + -1 * (b * x)) / (a + b * x)";
1.155 +rewrite_set_ thy false cancel_p t = NONE;
1.156 +"--- 11 ---";
1.157 +"--- 12 ---";
1.158 +"...both are to be considered after common_nominator_p_ is improved";
1.159 +--------------------------------------------------------------------------------------/*)
1.160 +
2.1 --- a/test/Tools/isac/Knowledge/rational2.sml Wed Dec 05 09:58:28 2012 +0100
2.2 +++ b/test/Tools/isac/Knowledge/rational2.sml Wed Dec 05 10:21:35 2012 +0100
2.3 @@ -36,6 +36,9 @@
2.4 "----------- fun pp -------------------------------------";
2.5 "----------- fun GCD_MOD --------------------------------";
2.6 "--------------------------------------------------------";
2.7 +"----------- non-termination errors in cancel_p ----";
2.8 +"--------------------------------------------------------";
2.9 +"--------------------------------------------------------";
2.10 "--------------------------------------------------------";
2.11
2.12 "----------- values used for many tests -----------------";
2.13 @@ -449,8 +452,64 @@
2.14 "----------- fun %/% -------------------------------";
2.15 "----------- fun %/% -------------------------------";
2.16
2.17 -"----------- fun %/% -------------------------------";
2.18 -"----------- fun %/% -------------------------------";
2.19 -"----------- fun %/% -------------------------------";
2.20 +"----------- non-termination errors in cancel_p ----";
2.21 +"----------- non-termination errors in cancel_p ----";
2.22 +"----------- non-termination errors in cancel_p ----";
2.23 +(*------------------------------------------------------------------------------------\
2.24 +"WN121205: thoroughly tested with the numbering from rational.sml,";
2.25 +" see --- nonterminating cancel_p, norm_Rational 2002 ---.";
2.26 +" non-termination errors in cancel_p: --- 4,5,6,7.";
2.27 +trace_rewrite := true;
2.28
2.29 +"--- 4 ---: non-terminating with Rrls cancel_p on plausible input";
2.30 +val t = str2term (
2.31 +"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /"^
2.32 +"(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)");
2.33 +rewrite_set_ thy false cancel_p t;
2.34 +(*# rls: cancel_p on:
2.35 +(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /
2.36 +(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2) *)
2.37
2.38 +"--- 5 ---: non-terminating with Rrls cancel_p on plausible input";
2.39 +val t = str2term "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
2.40 +rewrite_set_ thy false norm_Rational t;
2.41 +(*#### rls: cancel_p on:
2.42 +(2304 + -1152 * x + -2304 * y + 144 * x ^^^ 2 + 1152 * (x * y) + -144 * (x ^^^ 2 * y)) /
2.43 +(48 + -12 * x + -96 * y + 24 * (x * y) + 48 * y ^^^ 2 + -12 * (x * y ^^^ 2)) *)
2.44 +
2.45 +"--- 6 ---: non-terminating with Rrls cancel_p on plausible input";
2.46 +val t = str2term
2.47 +"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
2.48 +rewrite_set_ thy false norm_Rational t;
2.49 +(*### rls: cancel_p on: (-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * (x * y) +
2.50 + 144 * (x ^^^ 2 * y)) /
2.51 +(-48 + 12 * x + 96 * y + -24 * (x * y) + -48 * y ^^^ 2 + 12 * (x * y ^^^ 2)) *)
2.52 +
2.53 +"--- 7 ---: non-terminating with Rrls cancel_p on plausible input";
2.54 +val t' = str2term (
2.55 +"(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y)
2.56 + (-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2) ");
2.57 +rewrite_set_ thy false cancel_p t';
2.58 +--------------------------------------------------------------------------------------/*)
2.59 +*}
2.60 +ML {*
2.61 +"--- 4 ---: non-terminating with Rrls cancel_p on plausible input";
2.62 +val t = @{term
2.63 +"(a * x ^ 2 + -2 * a * x * y + a * y ^ 2 + b * x ^ 2 + -2 * b * x * y + b * y ^ 2) /
2.64 + (a ^ 2 * x ^ 2 + -1 * a ^ 2 * y ^ 2 + -1 * b ^ 2 * x ^ 2 + b ^ 2 * y ^ 2)"};
2.65 +
2.66 +"--- 5 ---: non-terminating with Rrls cancel_p on plausible input";
2.67 +val t = @{term
2.68 +"(2304 + -1152 * x + -2304 * y + 144 * x ^ 2 + 1152 * (x * y) + -144 * (x ^ 2 * y)) /
2.69 + (48 + -12 * x + -96 * y + 24 * (x * y) + 48 * y ^ 2 + -12 * (x * y ^ 2))"};
2.70 +
2.71 +"--- 6 ---: non-terminating with Rrls cancel_p on plausible input";
2.72 +val t = @{term
2.73 +"(-2304 + 1152 * x + 2304 * y + -144 * x ^ 2 + -1152 * (x * y) + 144 * (x ^ 2 * y)) /
2.74 + (-48 + 12 * x + 96 * y + -24 * (x * y) + -48 * y ^ 2 + 12 * (x * y ^ 2))"};
2.75 +
2.76 +"--- 7 ---: non-terminating with Rrls cancel_p on plausible input";
2.77 +val t = @{term
2.78 +"(-2304 + 1152 * x + 2304 * y + -144 * x ^ 2 + -1152 * x * y + 144 * x ^ 2 * y) /
2.79 + (-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^ 2 + 12 * x * y ^ 2)"};
2.80 +