test/Tools/isac/Minisubpbl/600-postcond.sml
author Walther Neuper <neuper@ist.tugraz.at>
Fri, 20 May 2011 14:49:07 +0200
branchdecompose-isar
changeset 42018 11cf93cd02c6
parent 42009 5f5807893ceb
child 59253 f0bb15a046ae
permissions -rw-r--r--
tuned
neuper@42009
     1
(* Title:  600-postcond.sml
neuper@41998
     2
   Author: Walther Neuper 1105
neuper@41998
     3
   (c) copyright due to lincense terms.
neuper@41998
     4
*)
neuper@41998
     5
neuper@41998
     6
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@41998
     7
val (dI',pI',mI') =
neuper@41998
     8
  ("Test", ["sqroot-test","univariate","equation","test"],
neuper@41998
     9
   ["Test","squ-equ-test-subpbl1"]);
neuper@41998
    10
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@41998
    11
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    12
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    13
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    14
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    15
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    16
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    17
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    18
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    19
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    20
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
neuper@42018
    21
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    22
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    23
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    24
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    25
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    26
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    27
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    28
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    29
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    30
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    31
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    32
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    33
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42018
    34
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42007
    35
if nxt = ("End_Proof'", End_Proof') andalso p = ([], Res) 
neuper@42007
    36
andalso get_obj g_res pt (fst p) = str2term "[x=1]" then ()
neuper@42007
    37
else error "calculation not finished correctly";