[Toss-devel-svn] SF.net SVN: toss:[1704] trunk/Toss

[<luk...@us...>]

Revision: 1704
          http://toss.svn.sourceforge.net/toss/?rev=1704&view=rev
Author:   lukaszkaiser
Date:     2012-05-10 22:22:09 +0000 (Thu, 10 May 2012)
Log Message:
-----------
Corrections to term simplification, renaming example.

Modified Paths:
--------------
    trunk/Toss/Arena/Term.ml
    trunk/Toss/Arena/Term.mli
    trunk/Toss/Arena/TermTest.ml
    trunk/Toss/Client/JsHandler.ml
    trunk/Toss/Client/State.js
    trunk/Toss/Client/index.html
    trunk/Toss/Solver/RealQuantElim/OrderedPoly.ml
    trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli
    trunk/Toss/Solver/RealQuantElim/Poly.ml
    trunk/Toss/Solver/RealQuantElim/Poly.mli

Added Paths:
-----------
    trunk/Toss/Client/img/Cell-Cycle-Tyson-1991.png
    trunk/Toss/examples/Cell-Cycle-Tyson-1991.toss

Removed Paths:
-------------
    trunk/Toss/Client/img/Yeast-Cell-Cycle-Tyson.png
    trunk/Toss/examples/Yeast-Cell-Cycle-Tyson.toss

Modified: trunk/Toss/Arena/Term.ml
===================================================================
--- trunk/Toss/Arena/Term.ml	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Arena/Term.ml	2012-05-10 22:22:09 UTC (rev 1704)
@@ -2,6 +2,8 @@
 
 (* ---------------------- BASIC TYPE DEFINITION ----------------------------- *)
 
+let simp_symb = ref false
+
 type term =
   | Var of string
   | FVar of string * string
@@ -80,27 +82,58 @@
 (* -------------------- SIMPLIFICATION OF CONSTANTS ------------------------- *)
 
 (* Basic simplification, reduces constant terms to floats. *)
-let rec simp_const = function
+let rec simp_const_only = function
   | Var s -> Var s
   | FVar (f, a) -> FVar (f, a)
   | Const n -> Const n
   | Times (p, q) -> (
-    match (simp_const p, simp_const q) with
+    match (simp_const_only p, simp_const_only q) with
       | (Const n, Const m) -> Const (n *. m)
-      | (Const n, Times (Const m, t)) -> Times (Const (n *. m), t)
       | (t, s) -> Times (t, s)
   )
   | Plus (p, q) -> (
-    match (simp_const p, simp_const q) with
+    match (simp_const_only p, simp_const_only q) with
       | (Const n, Const m) -> Const (n +. m)
-      | (Const n, Plus (Const m, t)) -> Plus (Const (n +. m), t)
       | (t, s) -> Plus (t, s)
   )
   | Div (p, q) ->
-    match (simp_const p, simp_const q) with
+    match (simp_const_only p, simp_const_only q) with
       | (Const n, Const m) -> Const (n /. m)
       | (t, s)-> Div (t, s)
 
+let simp_const t =
+  let rec to_poly = function
+    | Var s -> Poly.Var ("V" ^ s)
+    | FVar (f, a) -> Poly.Var ("F" ^ f ^ "#" ^ a)
+    | Const n -> Poly.Const n
+    | Times (p, q) -> Poly.Times (to_poly p, to_poly q)
+    | Plus (p, q) -> Poly.Plus (to_poly p, to_poly q)
+    | Div _ -> raise Not_found in
+  let rec from_ord = function
+    | OrderedPoly.Const _ -> failwith "num after non-num translation"
+    | OrderedPoly.FConst num -> Const (num)
+    | OrderedPoly.Poly (v, coefs) ->
+      let w = if v.[0]= 'V' then Var (String.sub v 1 ((String.length v)-1)) else
+	  let i, l = String.index v '#', String.length v in
+	  FVar (String.sub v 1 (i-1), String.sub v (i+1) (l-i-1)) in
+      let res = List.fold_left (fun acc (a, j) -> 
+	if j = 0 then Plus (acc, from_ord a) else 
+	  match from_ord a with
+	    | Const n when n = 1. -> Plus (acc, pow w j)
+	    | ordt -> Plus (acc, Times (ordt, pow w j))
+      ) (Const 0.) coefs in
+      LOG 1 "res %s" (str res);
+      let rec del_zero = function
+	| Plus (Const n, t) when n = 0. -> t
+	| Plus (t, s) -> Plus (del_zero t, s)
+	| t -> t in
+      del_zero res in
+  match simp_const_only t with
+    | Const n -> Const n
+    | t -> if not !simp_symb then t else
+	try let p = to_poly t in
+	    from_ord (Poly.make_ordered ~use_num:false [] p)
+	with Not_found -> t
 
 (* Convert a term to float, fail on non-constant term. *)
 let term_val t = match simp_const t with

Modified: trunk/Toss/Arena/Term.mli
===================================================================
--- trunk/Toss/Arena/Term.mli	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Arena/Term.mli	2012-05-10 22:22:09 UTC (rev 1704)
@@ -16,6 +16,9 @@
 
 (** {2 Basic functions.} *)
 
+(** Whether to simplify symbolically or not. Set to false by default.
+    It is nice for symbolic stuff, but slows down numerics. *)
+val simp_symb : bool ref
 
 (** Print a term as a string. *)
 val str : term -> string

Modified: trunk/Toss/Arena/TermTest.ml
===================================================================
--- trunk/Toss/Arena/TermTest.ml	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Arena/TermTest.ml	2012-05-10 22:22:09 UTC (rev 1704)
@@ -74,6 +74,39 @@
       assert_equal ~printer:(fun x->x) "0.005"
         (String.sub (str (List.hd (
           rk4_step "t" (Const 0.) (Const 0.1) eqs [Const 0.]))) 0 5);
+    );
 
+  "rk4 eq" >::
+    (fun () ->
+      (* Runge-Kutta symbolically with 2 free parameters. *)
+      let tyson = eqs_of_string
+	("   :y(e1)' = 0.015 + -200. * :y(e1) * :y(e4); " ^
+	    ":y(e2)' = -0.6 * :y(e2) + k6 * :y(e5); " ^
+	    ":y(e3)' = -100. * :y(e3) + k6 * :y(e5) + 100. * :y(e4); " ^
+	    ":y(e4)' = -100.*:y(e4) + 100.*:y(e3) + -200.*:y(e1) * :y(e4); " ^
+	    ":y(e5)' = -k6 * :y(e5) + 0.018 * :y(e6) + " ^ 
+	    "  k4 * :y(e6) * :y(e5) * :y(e5); " ^
+	    ":y(e6)' = -0.018 * :y(e6) + 200. * :y(e1) * :y(e4) + " ^ 
+	    "  -k4 * :y(e6) * :y(e5) * :y(e5)") in
+      let init = [Const 0.; Const 0.; Const 1.; Const 0.; Const 0.; Const 0.] in
+      Term.simp_symb := true;
+      let res = rk4_step "t" (Const 0.) (Const 0.005) tyson init in
+      Term.simp_symb := false;
+      let val_str vs = String.concat ", " (List.map str vs) in
+      assert_equal ~printer:(fun x->x) 
+	("6.6076722582e-05, 3.515625e-13 * k6, 3.515625e-13 * k6 + " ^
+	    "0.687499267591, 0.312491809132, -3.515625e-13 * k6 + " ^ 
+	    "6.08239621818e-28 * k4 + 2.02139802246e-10, " ^ 
+	    "-6.08239621818e-28 * k4 + 8.9230752782e-06") (val_str res);
+
+      (* Generate RK4 equations symbolically for [eq], step [n]. *)
+      (*let generate_rksymb eq n t0 tstep =
+	let init m = Array.to_list (Array.mapi (fun i _ ->
+	  Term.Var (Printf.sprintf "v%iat%i" i m)) (Array.of_list eq)) in 
+	let res = rk4_step "t" (Const t0) (Const tstep) eq (init n) in
+	String.concat "\n" (List.map2 (fun t v ->
+	  (Term.str t) ^ " = " ^ (Term.str v) ^ "\n") (init (n+1)) res) in
+      assert_equal ~printer:(fun x->x) "ok" (generate_rksymb tyson 0 0. 0.005);
+      *)
     );
 ]

Modified: trunk/Toss/Client/JsHandler.ml
===================================================================
--- trunk/Toss/Client/JsHandler.ml	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Client/JsHandler.ml	2012-05-10 22:22:09 UTC (rev 1704)
@@ -69,8 +69,8 @@
   ("Hnefatafl", AuxIO.input_file "examples/Hnefatafl.toss");
   ("Rewriting-Example", AuxIO.input_file "examples/Rewriting-Example.toss");
   ("Bounce", AuxIO.input_file "examples/Bounce.toss");
-  ("Yeast-Cell-Cycle-Tyson", 
-   AuxIO.input_file "examples/Yeast-Cell-Cycle-Tyson.toss");
+  ("Cell-Cycle-Tyson-1991", 
+   AuxIO.input_file "examples/Cell-Cycle-Tyson-1991.toss");
 ]
 
 let gSel_games = ref [compile_game_data "Tic-Tac-Toe"

Modified: trunk/Toss/Client/State.js
===================================================================
--- trunk/Toss/Client/State.js	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Client/State.js	2012-05-10 22:22:09 UTC (rev 1704)
@@ -56,7 +56,7 @@
 function State (game, info_obj, mirror) {
     // We create an SVG box with margins depending on the game.
     this.game = game;
-    this.mirror = mirror || (game == "Yeast-Cell-Cycle-Tyson");
+    this.mirror = mirror || (game == "Cell-Cycle-Tyson-1991");
 
     var create_svg_box = function (margx, margy, parent_id) {
 	var svg_e = document.getElementById("svg");
@@ -198,7 +198,7 @@
 function square_elements_game (game) {
     return (game !== "Connect4" && 
 	    game !== "Bounce" && 
-	    game !== "Yeast-Cell-Cycle-Tyson" && 
+	    game !== "Cell-Cycle-Tyson-1991" && 
 	    game !== "Rewriting-Example")
 }
 

Copied: trunk/Toss/Client/img/Cell-Cycle-Tyson-1991.png (from rev 1703, trunk/Toss/Client/img/Yeast-Cell-Cycle-Tyson.png)
===================================================================
(Binary files differ)

Deleted: trunk/Toss/Client/img/Yeast-Cell-Cycle-Tyson.png
===================================================================
(Binary files differ)

Modified: trunk/Toss/Client/index.html
===================================================================
--- trunk/Toss/Client/index.html	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Client/index.html	2012-05-10 22:22:09 UTC (rev 1704)
@@ -172,11 +172,11 @@
 </button>
 </div>
 <div class="game-picdiv3">
-<button onclick="new_play_click ('Yeast-Cell-Cycle-Tyson')" class="game-picbt">
-  <img class="game-picimg" src="img/Yeast-Cell-Cycle-Tyson.png" 
-       alt="Yeast-Cell-Cycle-Tyson" />
-  <span id="pdescYeast-Cell-Cycle-Tyson" class="game-picspan">
-    <span class="game-pictxt">Yeast-Cell-Cycle-Tyson</span>
+<button onclick="new_play_click ('Cell-Cycle-Tyson-1991')" class="game-picbt">
+  <img class="game-picimg" src="img/Cell-Cycle-Tyson-1991.png" 
+       alt="Cell-Cycle-Tyson-1991" />
+  <span id="pdescCell-Cycle-Tyson-1991" class="game-picspan">
+    <span class="game-pictxt">Cell-Cycle-Tyson-1991</span>
   </span>
 </button>
 </div>
@@ -462,8 +462,8 @@
     <p><b>Bounce</b> is the basic example we use to illustrate how continuous
       dynamics and invariants work with structure rewriting.</p>
   </div>
-  <div class="game-desc" id="Yeast-Cell-Cycle-Tyson-desc">
-    <p><b>Yeast Cell Cycle</b> model by <b>Tyson</b> (1991),
+  <div class="game-desc" id="Cell-Cycle-Tyson-1991-desc">
+    <p>Yeast <b>Cell Cycle</b> model by <b>Tyson (1991)</b>, 
       <a href="http://www.cellerator.org/notebooks/Tyson6.html">described
 	here</a>, is a model of the cell cycle based on the interactions
       between cdc2 and cyclin. We use it as an example of non-linear

Modified: trunk/Toss/Solver/RealQuantElim/OrderedPoly.ml
===================================================================
--- trunk/Toss/Solver/RealQuantElim/OrderedPoly.ml	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Solver/RealQuantElim/OrderedPoly.ml	2012-05-10 22:22:09 UTC (rev 1704)
@@ -12,7 +12,10 @@
      Poly (z, [(Poly(y, [(Poly (x, [(Const 1, 1)]), 0)]), 2); 
                (Poly(y, [(Poly (x, [(Const 2, 0)]), 0)]), 0)]) *)
 
-type polynomial = Const of num | Poly of string * (polynomial * int) list
+type polynomial = 
+  | FConst of float 
+  | Const of num 
+  | Poly of string * (polynomial * int) list
 
 type t = polynomial (* to be compatible with OrderedType signature *)
 
@@ -26,7 +29,8 @@
 
 (* Print the given ordered polynomial as a string. *)
 let rec str = function
-    Const n -> string_of_num n
+  | FConst n -> string_of_float n
+  | Const n -> string_of_num n
   | Poly (v, clist) -> 
       let estr (p, d) = 
         if d = 0 then "(" ^ (str p) ^ ")" else if d = 1 then 
@@ -41,7 +45,8 @@
 
 (* Check if the given ordered polynomial is equal to zero. *)
 let rec is_zero = function
-    Const n -> (sign_num n) = 0
+  | FConst n -> n = 0.
+  | Const n -> (sign_num n) = 0
   | Poly (_, []) -> true
   | Poly (_, [(c, n)]) -> n = 0 && is_zero c
   | _ -> false
@@ -50,11 +55,14 @@
    do not assume that both arguments are over the same set of variables. *)
 let rec rcompare p1 p2 = 
   match (p1, p2) with
-      (Const n, Const m) -> 
-        let c = sign_num ((abs_num n) -/ (abs_num m)) in
-          if c <> 0 then c else sign_num (n -/ m)
+    | (FConst n, FConst m) -> if n > m then 1 else if m > n then -1 else 0
+    | (Const n, Const m) ->
+      let c = sign_num ((abs_num n) -/ (abs_num m)) in
+      if c <> 0 then c else sign_num (n -/ m)
     | (Const _, _) -> -1
     | (_, Const _) -> 1
+    | (FConst _, _) -> -1
+    | (_, FConst _) -> 1
     | (Poly (v, [(c, d)]), Poly (w, [])) -> if d = 0 && is_zero c then 0 else 1
     | (Poly (w, []), Poly (v, [(c, d)])) -> if d = 0 && is_zero c then 0 else -1
     | (Poly (_, _::_), Poly (_, [])) -> 1
@@ -62,19 +70,19 @@
     | (Poly (_, []), Poly (_, [])) -> 0
     | (Poly (v, _), Poly (w, _)) when v <> w -> String.compare v w
     | (Poly (v, (c1, d1)::r1), Poly (w, (c2, d2)::r2)) ->
-        if d1 <> d2 then d1 - d2 else 
-          let c = rcompare c1 c2 in
-            if c <> 0 then c else rcompare (Poly (v, r1)) (Poly (w, r2))
+      if d1 <> d2 then d1 - d2 else 
+        let c = rcompare c1 c2 in
+        if c <> 0 then c else rcompare (Poly (v, r1)) (Poly (w, r2))
 
 let rec deg_sum acc = function
-    Const _ -> acc
+  | Const _   | FConst _ -> acc
   | Poly (v, lst) -> 
-      let deg_sumi acc (p, i) = deg_sum (i + acc) p in
-        List.fold_left deg_sumi acc lst
+    let deg_sumi acc (p, i) = deg_sum (i + acc) p in
+    List.fold_left deg_sumi acc lst
 
 let compare p q =
   let d = (deg_sum 0 p) - (deg_sum 0 q) in
-    if d <> 0 then d else rcompare p q
+  if d <> 0 then d else rcompare p q
 
 (* Check if two polynomials are equal. *)
 let equal p1 p2 = (compare p1 p2 = 0)
@@ -85,78 +93,80 @@
 
 (* Helper function to extract main variable from an ordered polynomial. *)
 let var = function
-    Const _ -> raise Unmatched_variables
+  | Const _ | FConst _ -> raise Unmatched_variables
   | Poly (v, _) -> v
 
 (* Lower the number of variables of a polynomial - remove the highest. *)
 let lower = function
-    Poly (v, [(q, d)]) when d = 0 -> q
+  | Poly (v, [(q, d)]) when d = 0 -> q
   | _ -> failwith "cannot lower non-constant or zero polynomial"
 
 (* Check if the given ordered polynomial has constant value. *)
 let rec constant_value = function
-    Const n -> Some n
+  | FConst n -> failwith "constant value for FConst; TODO move from Poly.ml"
+  | Const n -> Some n
   | Poly (_, []) -> Some (num_of_int 0)
   | Poly (_, (c, d) :: rest) when d = 0 -> constant_value c
   | _ -> None
 
 (* Degree of the given polynomial in its highest variable. *)
 let deg = function
-    Poly (_, (_, d) :: _) -> d
+  | Poly (_, (_, d) :: _) -> d
   | _ -> 0
 
 (* Leading coefficient of the given polynomial, represented as ordered
    polynomial, multiplied by main variable raised to [n]-th power. *)
 let leading_coeff n = function
-    Poly (v, (c, _) :: _) -> Poly (v, [(c, n)])
+  | Poly (v, (c, _) :: _) -> Poly (v, [(c, n)])
   | Poly (v, []) -> Poly (v, [])
   | Const n -> Const n
+  | FConst n -> FConst n
 
 (* Degree 0 coefficient of the given polynomial, if it exists and is non-0. *)
 let rec const_coeff = function
-    Poly (v, [(q, d)]) as p when d = 0 && not (is_zero q) -> Some p
+  | Poly (v, [(q, d)]) as p when d = 0 && not (is_zero q) -> Some p
   | Poly (v, _ :: rs) -> const_coeff (Poly (v, rs))
   | _ -> None
 
 
 (* Omit leading coefficient in the given polynomial. *)
 let omit_leading = function
-    Poly (v, _ :: rest) -> Poly (v, rest)
+  | Poly (v, _ :: rest) -> Poly (v, rest)
   | x -> x
 
 (* Calculate n * p for a given polynomial p. *)
 let rec multiple n = function
-    Const m -> Const ((num_of_int n) */ m)
+  | FConst m -> FConst ((float_of_int n) *. m)
+  | Const m -> Const ((num_of_int n) */ m)
   | Poly (v, l) -> 
-      if n = 0 then Poly (v, []) else
-        Poly (v, List.map (fun (c, d) -> (multiple n c, d)) l)
+    if n = 0 then Poly (v, []) else
+      Poly (v, List.map (fun (c, d) -> (multiple n c, d)) l)
 
 let rec multiple_num n = function
-    Const m -> Const (n */ m)
+  | FConst m -> failwith "multiple num for FConst; TODO move from Poly.ml"
+  | Const m -> Const (n */ m)
   | Poly (v, l) -> 
-      if sign_num n = 0 then Poly (v, []) else
-        Poly (v, List.map (fun (c, d) -> (multiple_num n c, d)) l)
+    if sign_num n = 0 then Poly (v, []) else
+      Poly (v, List.map (fun (c, d) -> (multiple_num n c, d)) l)
 
 
 (* If c1 * p = c2 * q for constants (c1,c2) <> (0,0), return them; else None. *)
 let rec constant_factors p0 q0 =
   match (p0, q0) with
-      (Const n, Const m) -> 
-        if (sign_num m) <> 0 or (sign_num n) <> 0 then 
-          Some (m, n) 
-        else None
+    | (Const n, Const m) -> 
+      if (sign_num m) <> 0 or (sign_num n) <> 0 then Some (m, n) else None
     | (Poly (v, []), _) -> 
-        if is_zero q0 then None else Some (num_of_int 1, num_of_int 0)
+      if is_zero q0 then None else Some (num_of_int 1, num_of_int 0)
     | (_, Poly (v, [])) -> 
-        if is_zero p0 then None else Some (num_of_int 0, num_of_int 1)
+      if is_zero p0 then None else Some (num_of_int 0, num_of_int 1)
     | (Poly (v, (p, d)::ps), Poly (w, (q, e)::qs)) when w = v -> (
-        if d <> e then None else match constant_factors p q with
-            None -> None
-          | Some (a, b) -> 
-              if equal (multiple_num a p0) (multiple_num b q0) then 
-                Some (a,b) 
-              else None
-      )
+      if d <> e then None else match constant_factors p q with
+        | None -> None
+        | Some (a, b) -> 
+          if equal (multiple_num a p0) (multiple_num b q0) then 
+	    Some (a,b) 
+          else None
+    )
     | _ -> raise Unmatched_variables
 
 
@@ -165,23 +175,24 @@
 (* Add two ordered polynomials [p1] and [p2] in the same variable. *)
 let rec add p1 p2 = 
   match (p1, p2) with
-      (Const n, Const m) -> Const (n +/ m)
+    | (FConst n, FConst m) -> FConst (n +. m)
+    | (Const n, Const m) -> Const (n +/ m)
     | (Poly (v, l1), Poly (w, l2)) when v = w -> Poly (v, add_lists (l1, l2))
     | _ -> raise Unmatched_variables
 
 and add_lists = function
-    ([(p, d)], []) when d = 0 && is_zero p -> []
+  | ([(p, d)], []) when d = 0 && is_zero p -> []
   | ([], [(p, d)]) when d = 0 && is_zero p -> []
   | (l1, []) -> l1
   | ([], l2) -> l2
   | ((c1, d1) :: r1, (c2, d2) :: r2) ->
-      if d1 > d2 then 
-        (c1, d1) :: (add_lists (r1, (c2, d2) :: r2)) 
-      else if d2 > d1 then
-        (c2, d2) :: (add_lists ((c1, d1) :: r1, r2))
-      else let c = add c1 c2 in
-        if is_zero c then add_lists (r1, r2) else
-          (c, d1) :: (add_lists (r1, r2))
+    if d1 > d2 then 
+      (c1, d1) :: (add_lists (r1, (c2, d2) :: r2)) 
+    else if d2 > d1 then
+      (c2, d2) :: (add_lists ((c1, d1) :: r1, r2))
+    else let c = add c1 c2 in
+         if is_zero c then add_lists (r1, r2) else
+           (c, d1) :: (add_lists (r1, r2))
 
 (* Given a polynomial p, returns -p. *)
 let neg p = multiple (-1) p
@@ -192,76 +203,78 @@
 (* Multiply two polynomials [p1] and [p2] in the same variables. *)
 let rec mul p1 p2 =
   match (p1, p2) with
-      (Const n, Const m) -> Const (n */ m)
+    | (FConst n, FConst m) -> FConst (n *. m)
+    | (Const n, Const m) -> Const (n */ m)
     | (Poly (v, l1), Poly (w, l2)) when v = w -> Poly (v, mul_lists l1 l2)
     | _ -> raise Unmatched_variables
 
 and mul_lists l1 = function
     | [] -> []
     | [(c2, d2)] -> 
-        let append_coeff_mul (c1, d1) acc =
-          let c = mul c2 c1 in
-            if is_zero c then acc else (c, d1 + d2) :: acc 
-        in
-          List.fold_right append_coeff_mul l1 []
+      let append_coeff_mul (c1, d1) acc =
+        let c = mul c2 c1 in
+        if is_zero c then acc else (c, d1 + d2) :: acc in
+      List.fold_right append_coeff_mul l1 []
     | c :: rest ->
-        add_lists ((mul_lists l1 [c]), (mul_lists l1 rest))
+      add_lists ((mul_lists l1 [c]), (mul_lists l1 rest))
 
 (* Raise [p] to n-th power. *)
 let rec pow p n =
   if n < 1 then failwith "we only support powers > 0" else if n = 1 then p else
-    let q = pow p (n / 2) in
+      let q = pow p (n / 2) in
       if n mod 2 = 0 then mul q q else mul p (mul q q)
 
 (* Given [u] and [p] return, if possible, q and r with [u] = q*[p] + r. *)
 (* Based on code from Jean-Christophe Filliatre, cf. Knuth volume 2, 4.6.1. *)
 let rec div ?(allow_frac=false) p q =
-    match (p, q) with
-        (Const n, Const m) ->
-          if allow_frac then Const (n // m) else
-            if sign_num (mod_num n m) = 0 then Const (n // m) else
-              raise Not_found
-      | (Poly (v, _), Poly (w, _)) -> 
-          if v <> w then raise Unmatched_variables else
-            let (l, r) = div_rest ~allow_frac:allow_frac p q in 
-              if is_zero r then l else raise Not_found
-      | _ -> raise Unmatched_variables
+  match (p, q) with
+    | (Const n, Const m) ->
+      if allow_frac then Const (n // m) else
+        if sign_num (mod_num n m) = 0 then Const (n // m) else
+          raise Not_found
+    | (Poly (v, _), Poly (w, _)) -> 
+      if v <> w then raise Unmatched_variables else
+        let (l, r) = div_rest ~allow_frac:allow_frac p q in 
+        if is_zero r then l else raise Not_found
+    | _ -> raise Unmatched_variables
     
 and div_rest ?(allow_frac=false) u = function
-    Poly (_, []) -> raise Not_found
+  | Poly (_, []) -> raise Not_found
+  | FConst _ -> failwith "div_rest: FConst arg"
   | Const n -> (
-      match u with
-          Const m -> 
-            if allow_frac then (Const (n // m), Const (num_of_int 0)) else
-              let r = mod_num n m in (Const ((n -/ r) // m), Const r)
-        | Poly (_, _) -> raise Unmatched_variables
-    )
+    match u with
+      | FConst _ -> failwith "div_rest: FConst u"
+      | Const m -> 
+        if allow_frac then (Const (n // m), Const (num_of_int 0)) else
+          let r = mod_num n m in (Const ((n -/ r) // m), Const r)
+      | Poly (_, _) -> raise Unmatched_variables
+  )
   | Poly (v, (p, d) :: ps) ->
-	let rec loop k = function
-	    u when k < 0 -> (Poly (v, []), u)
-          | Poly (w, _) when w <> v -> raise Unmatched_variables
-	  | Poly (_, (q, i) :: qs) when i = d + k ->
-	      let qk = div ~allow_frac:allow_frac q p in
-	      let mqkxk = Poly (v, [(neg qk, k)]) in
-              let added = add (Poly (v, qs)) (mul mqkxk (Poly (v, ps))) in
-              let (q, r) = loop (k - 1) added in (
-                  match q with
-                      Poly (_, ql) -> (Poly (v, (qk, k) :: ql), r)
-                    | _ -> failwith "error by division"
-                )
-	  | u -> loop (k - 1) u
-	in
-	  loop (deg u - d) u
+    let rec loop k = function
+      | u when k < 0 -> (Poly (v, []), u)
+      | Poly (w, _) when w <> v -> raise Unmatched_variables
+      | Poly (_, (q, i) :: qs) when i = d + k ->
+	let qk = div ~allow_frac:allow_frac q p in
+	let mqkxk = Poly (v, [(neg qk, k)]) in
+        let added = add (Poly (v, qs)) (mul mqkxk (Poly (v, ps))) in
+        let (q, r) = loop (k - 1) added in (
+          match q with
+            | Poly (_, ql) -> (Poly (v, (qk, k) :: ql), r)
+            | _ -> failwith "error by division"
+        )
+      | u -> loop (k - 1) u in
+    loop (deg u - d) u
 
 
 (* -------------------------- DIFFERENTIATION ------------------------------- *)
 
 let rec diff = function
-    Const n -> Const (num_of_int 0)
+  | FConst _ -> FConst (0.)
+  | Const _ -> Const (num_of_int 0)
   | Poly (v, l) -> Poly (v, diff_list l)
 
 and diff_list = function
-    [] -> []
+  | [] -> []
   | (c, d) :: r -> if d > 0 then (multiple d c, d-1) :: (diff_list r) else []
 
 
@@ -277,21 +290,20 @@
 *)
 let modified_remainder p1 q = 
   match q with 
-      Const _ -> raise Unmatched_variables
+    | Const _ | FConst _ -> raise Unmatched_variables
     | Poly (v, _) when var p1 <> v -> raise Unmatched_variables
     | Poly (v, _) ->
-        let (m, b, q') = (deg q, leading_coeff 0 q, omit_leading q) in
-          if m > deg p1 then failwith "Modified reminder: wrong degree." else
-            let rec mr p = 
-              let (n, a) = (deg p, leading_coeff 0 p) in
-	        if n < m then p
-	        else if n = m then 
-                  sub (mul b  p) (mul a q)
-	        else 
-                  let bp = mul b (omit_leading p) in
-                  let d = sub bp (mul (leading_coeff (n-m) p) q') in
-                    if n - 1 = deg d then mr d else
-                      let bpow = pow b (n - 1 - (deg d)) in
-                        mr (mul bpow d)
-            in 
-              mr p1
+      let (m, b, q') = (deg q, leading_coeff 0 q, omit_leading q) in
+      if m > deg p1 then failwith "Modified reminder: wrong degree." else
+        let rec mr p = 
+          let (n, a) = (deg p, leading_coeff 0 p) in
+	  if n < m then p
+	  else if n = m then 
+            sub (mul b  p) (mul a q)
+	  else 
+            let bp = mul b (omit_leading p) in
+            let d = sub bp (mul (leading_coeff (n-m) p) q') in
+            if n - 1 = deg d then mr d else
+              let bpow = pow b (n - 1 - (deg d)) in
+              mr (mul bpow d) in 
+        mr p1

Modified: trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli
===================================================================
--- trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli	2012-05-10 22:22:09 UTC (rev 1704)
@@ -3,7 +3,10 @@
 
 (** {2 Basic Type Definitions} *)
 
-type polynomial = Const of Numbers.num | Poly of string * (polynomial*int) list
+type polynomial =
+  | FConst of float
+  | Const of Numbers.num 
+  | Poly of string * (polynomial * int) list
 
 type t = polynomial (** to be compatible with OrderedType signature *)
 

Modified: trunk/Toss/Solver/RealQuantElim/Poly.ml
===================================================================
--- trunk/Toss/Solver/RealQuantElim/Poly.ml	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Solver/RealQuantElim/Poly.ml	2012-05-10 22:22:09 UTC (rev 1704)
@@ -3,7 +3,7 @@
 (* ---------------------- BASIC TYPE DEFINITION ----------------------------- *)
 
 type polynomial =
-    Var of string
+  | Var of string
   | Const of float
   | Times of polynomial * polynomial
   | Plus of polynomial * polynomial
@@ -13,16 +13,18 @@
 
 (* Print a polynomial as a string. *)
 let rec str = function
-    Var s -> s
+  | Var s -> s
   | Const n -> string_of_float n
-  | Times (Const n, q) -> if n = 1. then str q else poly_pair_str "*" (Const n) q
+  | Times (Const n, q) -> 
+    if n = 1. then str q else poly_pair_str "*" (Const n) q
   | Times (p, q) -> poly_pair_str "*" p q
-  | Plus (p, Const n) -> if n = 0. then str p else poly_pair_str " + " p (Const n)
+  | Plus (p, Const n) -> 
+    if n = 0. then str p else poly_pair_str " + " p (Const n)
   | Plus (p, q) -> poly_pair_str " + " p q
 
 and poly_pair_str sep p q =
   let brack s = if String.length s < 2 then s else "(" ^ s ^ ")" in
-    (brack (str p)) ^ sep ^ (brack (str q))
+  (brack (str p)) ^ sep ^ (brack (str q))
 
 
 (* ------------------ HELPER POWER FUNCTION USED IN PARSER ------------------ *)
@@ -33,27 +35,28 @@
 
 (* Basic simplification, reduces constant polynomials to integers. *)
 let rec simp_const = function
-    Var s -> Var s
+  | Var s -> Var s
   | Const n -> Const n
   | Times (p, q) -> (
       match (simp_const p, simp_const q) with
-          (Const n, Const m) -> Const (n *. m)
+        | (Const n, Const m) -> Const (n *. m)
         | _ -> Times (p, q)
-    )
+  )
   | Plus (p, q) ->
-      match (simp_const p, simp_const q) with
-          (Const n, Const m) -> Const (n +. m)
-        | _ -> Plus (p, q)
+    match (simp_const p, simp_const q) with
+      | (Const n, Const m) -> Const (n +. m)
+      | _ -> Plus (p, q)
 
 
 (* ----------------- CONVERTION TO UNORDERED POLYNOMIALS -------------------- *)
 
 let rec make_unordered = function
+  | OrderedPoly.FConst n -> Const (n)
   | OrderedPoly.Const n -> Const (Numbers.float_of_num n)
   | OrderedPoly.Poly (v, lst) -> make_unordered_list v lst
 
 and make_unordered_list v = function
-    [] -> Const 0.
+  | [] -> Const 0.
   | [(p, d)] when d = 0 -> make_unordered p
   | [(p, d)] -> Times (make_unordered p, pow (Var v) d)
   | (p, d) :: ls -> 
@@ -82,7 +85,7 @@
 
 (* List variables in the given polynomial. *)
 let rec vars = function
-    Var s -> [s]
+  | Var s -> [s]
   | Const _ -> []
   | Times (p, q) -> combine (vars p) (vars q)
   | Plus (p, q) -> combine (vars p) (vars q)
@@ -91,51 +94,52 @@
 let vars_list pl = List.fold_left (fun vs p -> combine vs (vars p)) [] pl
 
 (* Make an ordered polynomial from a constant [n] in given ordered variables. *)
-let rec make_ordered_const n = function
-    [] -> OrderedPoly.Const (num_of_float n)
-  | v :: vs -> OrderedPoly.Poly (v, [(make_ordered_const n vs, 0)])
+let rec make_ordered_const use_num n = function
+  | [] -> if use_num then OrderedPoly.Const (num_of_float n) else 
+      OrderedPoly.FConst (n)
+  | v :: vs -> OrderedPoly.Poly (v, [(make_ordered_const use_num n vs, 0)])
 
 (* Make an ordered polynomial from a variable [v] in given ordered variables. *)
-let rec make_ordered_var v = function
-    [] -> failwith "given variable not found among all variables"
-  | w :: ws when v = w -> OrderedPoly.Poly (v, [(make_ordered_const 1. ws, 1)])
-  | w :: ws -> OrderedPoly.Poly (w, [(make_ordered_var v ws, 0)])
+let rec make_ordered_var use_num v = function
+  | [] -> failwith "given variable not found among all variables"
+  | w :: ws when v = w -> 
+    OrderedPoly.Poly (v, [(make_ordered_const use_num 1. ws, 1)])
+  | w :: ws -> OrderedPoly.Poly (w, [(make_ordered_var use_num v ws, 0)])
 
 (* Make an ordered polynomial in given ordered variables [vars]. *)
-let rec make_ordered_poly vars = function
-    Const n -> make_ordered_const n vars
-  | Var v -> make_ordered_var v vars
-  | Times (p, q) -> 
-      OrderedPoly.mul (make_ordered_poly vars p) (make_ordered_poly vars q)
-  | Plus (p, q) -> 
-      OrderedPoly.add (make_ordered_poly vars p) (make_ordered_poly vars q)
+let rec make_ordered_poly use_num vars = function
+  | Const n -> make_ordered_const use_num n vars
+  | Var v -> make_ordered_var use_num v vars
+  | Times (p, q) -> OrderedPoly.mul
+    (make_ordered_poly use_num vars p) (make_ordered_poly use_num vars q)
+  | Plus (p, q) -> OrderedPoly.add 
+    (make_ordered_poly use_num vars p) (make_ordered_poly use_num vars q)
 
 (* Order on strings respecting priority given in [prio_list]. This means
    that if x appears in [prio_list] before y then x < y. Strings not appearing
    in [prio_list] at all are considered smaller than any string that appears. *)
 let compare prio_list x y =
   let rec cmp = function
-      [] -> String.compare x y
+    | [] -> String.compare x y
     | v :: vs when v = x -> if List.mem y vs then -1 else 1
     | v :: vs when v = y -> if List.mem x vs then 1 else -1
-    | v :: vs -> cmp vs
-  in
-    if x = y then 0 else cmp prio_list
+    | v :: vs -> cmp vs in
+  if x = y then 0 else cmp prio_list
 
 (* Make an ordered polynomial from [p] with [prio_list] order on variables. *)
-let make_ordered prio_list p =
+let make_ordered ?(use_num=true) prio_list p =
   let inc_cmp x y = (-1) * (compare prio_list x y) in
   let ord_vars = List.sort inc_cmp (vars p) in
-    make_ordered_poly ord_vars p
+  make_ordered_poly use_num ord_vars p
 
 (* Make ordered polynomials from [ps] with [prio_list] order on variables. *)
 let make_ordered_list prio_list ps =
   let vars = vars_list ps in
   let ord_vars = List.sort (fun x y -> (-1) * (compare prio_list x y)) vars in
-    List.rev_map (make_ordered_poly ord_vars) ps
+  List.rev_map (make_ordered_poly true ord_vars) ps
 
 (* Make ordered polynomials from first components of [ps], [prio_list] order. *)
 let make_ordered_pair_list prio_list ps =
   let vars = List.fold_left (fun vs (p, _) -> combine vs (vars p)) [] ps in
   let ord_vars = List.sort (fun x y -> (-1) * (compare prio_list x y)) vars in
-    List.rev_map (fun (p, x) -> (make_ordered_poly ord_vars p, x)) ps
+  List.rev_map (fun (p, x) -> (make_ordered_poly true ord_vars p, x)) ps

Modified: trunk/Toss/Solver/RealQuantElim/Poly.mli
===================================================================
--- trunk/Toss/Solver/RealQuantElim/Poly.mli	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/Solver/RealQuantElim/Poly.mli	2012-05-10 22:22:09 UTC (rev 1704)
@@ -43,7 +43,8 @@
 (** Make an ordered polynomial from [p] with [prio_list] order on variables,i.e.
     if x appears in [prio_list] before y then x < y. Strings not appearing
     in [prio_list] at all are considered smaller than any string that appears.*)
-val make_ordered : string list -> polynomial -> OrderedPoly.polynomial
+val make_ordered : ?use_num: bool ->
+  string list -> polynomial -> OrderedPoly.polynomial
 
 (** Make ordered polynomials from [ps] with [prio_list] order on variables. *)
 val make_ordered_list : string list -> polynomial list -> 

Copied: trunk/Toss/examples/Cell-Cycle-Tyson-1991.toss (from rev 1703, trunk/Toss/examples/Yeast-Cell-Cycle-Tyson.toss)
===================================================================
--- trunk/Toss/examples/Cell-Cycle-Tyson-1991.toss	                        (rev 0)
+++ trunk/Toss/examples/Cell-Cycle-Tyson-1991.toss	2012-05-10 22:22:09 UTC (rev 1704)
@@ -0,0 +1,75 @@
+PLAYERS 1, 2
+
+RULE k1:
+  [ e1 | Cyc(e1) | ] -> [ e1 | Cyc(e1) | ]
+  dynamics
+    :y(e1)' = k1
+
+RULE k3:
+  [ e1, e2, e3 | Cyc(e1); Cdc2P1(e2); Cdc2CycP1P2(e3) | ] -> 
+  [ e1, e2, e3 | Cyc(e1); Cdc2P1(e2); Cdc2CycP1P2(e3) | ]
+  dynamics
+    :y(e1)' = -k3 * :y(e1) * :y(e2);
+    :y(e2)' = -k3 * :y(e1) * :y(e2);
+    :y(e3)' = k3 * :y(e1) * :y(e2)
+
+RULE k4p:
+  [ e1, e2 | Cdc2CycP1P2(e1); Cdc2CycP1(e2) | ] -> 
+  [ e1, e2 | Cdc2CycP1P2(e1); Cdc2CycP1(e2) | ]
+  dynamics
+    :y(e1)' = -k4p * :y(e1);
+    :y(e2)' = k4p * :y(e1)
+
+RULE k4:
+  [ e1, e2 | Cdc2CycP1P2(e1); Cdc2CycP1(e2) | ] -> 
+  [ e1, e2 | Cdc2CycP1P2(e1); Cdc2CycP1(e2) | ]
+  dynamics
+    :y(e1)' = -k4 * :y(e1) * :y(e2) * :y(e2);
+    :y(e2)' = k4 * :y(e1) * :y(e2) * :y(e2)
+
+RULE k6:
+  [ e1, e2, e3 | Cdc2CycP1(e1); CycP1(e2); Cdc2(e3) | ] -> 
+  [ e1, e2, e3 | Cdc2CycP1(e1); CycP1(e2); Cdc2(e3) | ]
+  dynamics
+    :y(e1)' = -k6 * :y(e1);
+    :y(e2)' = k6 * :y(e1);
+    :y(e3)' = k6 * :y(e1)
+
+RULE k7:
+  [ e1 | CycP1(e1) | ] -> [ e1 | CycP1(e1) | ]
+  dynamics
+    :y(e1)' = -k7 * :y(e1)
+
+RULE k8:
+  [ e1, e2 | Cdc2(e1); Cdc2P1(e2) | ] -> [ e1, e2 | Cdc2(e1); Cdc2P1(e2) | ]
+  dynamics
+    :y(e1)' = -k8 * :y(e1);
+    :y(e2)' = k8 * :y(e1)
+
+RULE k9:
+  [ e1, e2 | Cdc2P1(e1); Cdc2(e2) | ] -> [ e1, e2 | Cdc2P1(e1); Cdc2(e2) | ]
+  dynamics
+    :y(e1)' = -k9 * :y(e1);
+    :y(e2)' = k9 * :y(e1)
+
+RULE Move:
+  [ e1 | Cyc(e1) | ] -> [ e1 | Cyc(e1) | ]
+
+LOC 0 {
+  PLAYER 1 { PAYOFF 0. MOVES [Move, 
+    t  : 9. -- 9.,
+    k1 : 0.015 -- 0.015,
+    k3 : 200. -- 200.,
+    k4p: 0.018 -- 0.018,
+    k4 : 180. -- 180.,
+    k6 : 1. -- 1.,
+    k7 : 0.6 -- 0.6,
+    k8 : 100. -- 100.,
+    k9 : 100. -- 100.   -> 0] }
+  PLAYER 2 { PAYOFF 0. }
+  UNIVERSAL { k1, k3, k4p, k4, k6, k7, k8, k9 }
+} 
+START [ e1, e2, e3, e4, e5, e6 | Cyc(e1); CycP1(e2); Cdc2(e3); Cdc2P1(e4); 
+                                 Cdc2CycP1(e5); Cdc2CycP1P2(e6) |
+  x { e1->1, e2->2, e3->3, e4->4, e5->5, e6->6 }; 
+  y { e1->0, e2->0, e3->1, e4->0, e5->0, e6->0 } ]

Deleted: trunk/Toss/examples/Yeast-Cell-Cycle-Tyson.toss
===================================================================
--- trunk/Toss/examples/Yeast-Cell-Cycle-Tyson.toss	2012-05-09 19:41:58 UTC (rev 1703)
+++ trunk/Toss/examples/Yeast-Cell-Cycle-Tyson.toss	2012-05-10 22:22:09 UTC (rev 1704)
@@ -1,75 +0,0 @@
-PLAYERS 1, 2
-
-RULE k1:
-  [ e1 | Cyc(e1) | ] -> [ e1 | Cyc(e1) | ]
-  dynamics
-    :y(e1)' = k1
-
-RULE k3:
-  [ e1, e2, e3 | Cyc(e1); Cdc2P1(e2); Cdc2CycP1P2(e3) | ] -> 
-  [ e1, e2, e3 | Cyc(e1); Cdc2P1(e2); Cdc2CycP1P2(e3) | ]
-  dynamics
-    :y(e1)' = -k3 * :y(e1) * :y(e2);
-    :y(e2)' = -k3 * :y(e1) * :y(e2);
-    :y(e3)' = k3 * :y(e1) * :y(e2)
-
-RULE k4p:
-  [ e1, e2 | Cdc2CycP1P2(e1); Cdc2CycP1(e2) | ] -> 
-  [ e1, e2 | Cdc2CycP1P2(e1); Cdc2CycP1(e2) | ]
-  dynamics
-    :y(e1)' = -k4p * :y(e1);
-    :y(e2)' = k4p * :y(e1)
-
-RULE k4:
-  [ e1, e2 | Cdc2CycP1P2(e1); Cdc2CycP1(e2) | ] -> 
-  [ e1, e2 | Cdc2CycP1P2(e1); Cdc2CycP1(e2) | ]
-  dynamics
-    :y(e1)' = -k4 * :y(e1) * :y(e2) * :y(e2);
-    :y(e2)' = k4 * :y(e1) * :y(e2) * :y(e2)
-
-RULE k6:
-  [ e1, e2, e3 | Cdc2CycP1(e1); CycP1(e2); Cdc2(e3) | ] -> 
-  [ e1, e2, e3 | Cdc2CycP1(e1); CycP1(e2); Cdc2(e3) | ]
-  dynamics
-    :y(e1)' = -k6 * :y(e1);
-    :y(e2)' = k6 * :y(e1);
-    :y(e3)' = k6 * :y(e1)
-
-RULE k7:
-  [ e1 | CycP1(e1) | ] -> [ e1 | CycP1(e1) | ]
-  dynamics
-    :y(e1)' = -k7 * :y(e1)
-
-RULE k8:
-  [ e1, e2 | Cdc2(e1); Cdc2P1(e2) | ] -> [ e1, e2 | Cdc2(e1); Cdc2P1(e2) | ]
-  dynamics
-    :y(e1)' = -k8 * :y(e1);
-    :y(e2)' = k8 * :y(e1)
-
-RULE k9:
-  [ e1, e2 | Cdc2P1(e1); Cdc2(e2) | ] -> [ e1, e2 | Cdc2P1(e1); Cdc2(e2) | ]
-  dynamics
-    :y(e1)' = -k9 * :y(e1);
-    :y(e2)' = k9 * :y(e1)
-
-RULE Move:
-  [ e1 | Cyc(e1) | ] -> [ e1 | Cyc(e1) | ]
-
-LOC 0 {
-  PLAYER 1 { PAYOFF 0. MOVES [Move, 
-    t  : 9. -- 9.,
-    k1 : 0.015 -- 0.015,
-    k3 : 200. -- 200.,
-    k4p: 0.018 -- 0.018,
-    k4 : 180. -- 180.,
-    k6 : 1. -- 1.,
-    k7 : 0.6 -- 0.6,
-    k8 : 100. -- 100.,
-    k9 : 100. -- 100.   -> 0] }
-  PLAYER 2 { PAYOFF 0. }
-  UNIVERSAL { k1, k3, k4p, k4, k6, k7, k8, k9 }
-} 
-START [ e1, e2, e3, e4, e5, e6 | Cyc(e1); CycP1(e2); Cdc2(e3); Cdc2P1(e4); 
-                                 Cdc2CycP1(e5); Cdc2CycP1P2(e6) |
-  x { e1->1, e2->2, e3->3, e4->4, e5->5, e6->6 }; 
-  y { e1->0, e2->0, e3->1, e4->0, e5->0, e6->0 } ]

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.