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

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

Revision: 1744
          http://toss.svn.sourceforge.net/toss/?rev=1744&view=rev
Author:   lukaszkaiser
Date:     2012-07-10 22:44:46 +0000 (Tue, 10 Jul 2012)
Log Message:
-----------
Optimizing SO-finder and its web interface, larger tests.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/Arena.mli
    trunk/Toss/Arena/ArenaParser.mly
    trunk/Toss/Arena/ArenaTest.ml
    trunk/Toss/Arena/DiscreteRuleParser.mly
    trunk/Toss/Client/Drawing.ml
    trunk/Toss/Client/Drawing.mli
    trunk/Toss/Client/JsEval.ml
    trunk/Toss/Client/eval.html
    trunk/Toss/Formula/BoolFormula.ml
    trunk/Toss/Formula/BoolFormula.mli
    trunk/Toss/Formula/FormulaParser.mly
    trunk/Toss/Formula/Lexer.mll
    trunk/Toss/Formula/Sat/Sat.ml
    trunk/Toss/Makefile
    trunk/Toss/Server/Server.ml
    trunk/Toss/Server/Tests.ml
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/Solver.mli
    trunk/Toss/Solver/SolverTest.ml
    trunk/Toss/Solver/Structure.ml
    trunk/Toss/Solver/Structure.mli
    trunk/Toss/Solver/StructureParser.mly
    trunk/Toss/menhir_conf
    trunk/Toss/www/Publications/all.bib
    trunk/Toss/www/create.xml
    trunk/Toss/www/docs.xml
    trunk/Toss/www/index.xml
    trunk/Toss/www/play.xml

Added Paths:
-----------
    trunk/Toss/www/pub/itrs_qmu.pdf

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Arena/Arena.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -255,28 +255,7 @@
     List.map (fun (lab,_) -> lab.lb_rule) l.(player_no).moves in
   List.concat (List.map rules_of_loc (Array.to_list game.graph))
 
-(* Add a defined relation to a structure. *)
-let add_def_rel_single struc (r_name, vars, def_phi) =
-  let def_asg = Solver.M.evaluate struc def_phi in
-  match def_asg with
-    | AssignmentSet.Empty -> 
-      Structure.add_rel_name r_name (List.length vars) struc
-    | _ ->
-      let tuples = AssignmentSet.tuples (Structure.elems struc) vars def_asg in
-      Structure.add_rels struc r_name tuples
 
-let add_def_rels struc rels = List.fold_left add_def_rel_single struc rels
-
-let add_def_fun_single struc (f, v, def_re) =
-  LOG 1 "adding fun %s def %s" f (Formula.real_str def_re);
-  let elems = Structure.elements struc in
-  let asg e = AssignmentSet.FO (v, [(e, AssignmentSet.Any)]) in
-  let fval e = Solver.M.get_real_val ~asg:(asg e) def_re struc in
-  List.fold_left (fun s e-> Structure.change_fun_int s f e (fval e)) struc elems
-
-let add_def_funs struc funs = List.fold_left add_def_fun_single struc funs
-
-
 (* The order of following entries matters: [DefPlayers] adds more
    players, with consecutive numbers starting from first available;
    later [StartStruc], [CurrentStruc], [StateTime] and [StateLoc] entries

Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Arena/Arena.mli	2012-07-10 22:44:46 UTC (rev 1744)
@@ -67,13 +67,7 @@
 (** Rules with which a player with given number can move. *)
 val rules_for_player : int -> game -> string list
 
-val add_def_rels : Structure.structure ->
-  (string * string list * Formula.formula) list -> Structure.structure
 
-val add_def_funs : Structure.structure ->
-  (string * string * Formula.real_expr) list -> Structure.structure
-
-
 (** Print a label as a string. *)
 val label_str : label -> string
 val move_str : (label * int) -> string

Modified: trunk/Toss/Arena/ArenaParser.mly
===================================================================
--- trunk/Toss/Arena/ArenaParser.mly	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Arena/ArenaParser.mly	2012-07-10 22:44:46 UTC (rev 1744)
@@ -38,26 +38,12 @@
         "Syntax error in move definition."
     }
 
-real_expr_err:
-  | rexp = real_expr { rexp }
-  | error
-    { Lexer.report_parsing_error $startpos $endpos
-        "Syntax error in real expression."
-    }
-
-formula_expr_err:
-  | phi = formula_expr { phi }
-  | error
-    { Lexer.report_parsing_error $startpos $endpos
-        "Syntax error in formula expression."
-    }
-
 float_or_int:
   | FLOAT { $1 }
   | INT   { float_of_int $1 }
 
 player_loc_defs:
-  | PAYOFF poff = real_expr_err                         { `Payoff poff }
+  | PAYOFF poff = real_expr                             { `Payoff poff }
   | MOVES moves = separated_list (SEMICOLON, move)      { `Moves moves }
   | COND hs = separated_list (SEMICOLON, float_or_int)  { `Heurs hs }
   | error
@@ -90,14 +76,6 @@
         "Syntax error in location definition."
     }
 
-rel_def_simple:
-  | rel = ID args = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
-    EQ body = formula_expr_err { (rel, args, body) }
-
-fun_def_simple:
-  | COLON f = ID OPEN v = ID CLOSE EQ body = real_expr 
-    { (f, v, body) }
-
 game_move_timed:
   | OPENSQ r = id_int t = FLOAT RARR l = INT EMB 
     emb = separated_list (COMMA, separated_pair (ID, COLON, id_int)) CLOSESQ
@@ -126,35 +104,21 @@
     { DefLoc l }
   | PLAYERS_MOD pnames = separated_list (COMMA, id_int)
     { DefPlayers pnames }
-  | SET_CMD r = real_expr_err 
+  | SET_CMD r = real_expr 
     { DefPattern r }
   | REL_MOD rel = ID
     arg = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
-    body = delimited (OPENCUR, formula_expr_err, CLOSECUR)
+    body = delimited (OPENCUR, formula_expr, CLOSECUR)
     { DefRel (rel, arg, body) }
   | REL_MOD rel = ID
     arg = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
     EQ
-    body = formula_expr_err
+    body = formula_expr
     { DefRel (rel, arg, body) }
   | START model = struct_expr
     { StartStruc model }
-  | START model = struct_expr WITH 
-    defs = separated_list (SEMICOLON, rel_def_simple)
-    { StartStruc (Arena.add_def_rels model defs) }
-  | START model = struct_expr WITH 
-    defs = separated_list (SEMICOLON, rel_def_simple) WITH
-    funs = separated_list (SEMICOLON, fun_def_simple)
-    { StartStruc (Arena.add_def_funs (Arena.add_def_rels model defs) funs) }
   | CURRENT model = struct_expr
     { CurrentStruc model }
-  | CURRENT model = struct_expr WITH 
-    defs = separated_list (SEMICOLON, rel_def_simple)
-    { CurrentStruc (Arena.add_def_rels model defs) }
-  | CURRENT model = struct_expr WITH 
-    defs = separated_list (SEMICOLON, rel_def_simple) WITH
-    funs = separated_list (SEMICOLON, fun_def_simple)
-    { StartStruc (Arena.add_def_funs (Arena.add_def_rels model defs) funs) }
   | MOVES moves = separated_list (SEMICOLON, game_move_timed)
     { History (moves) }
   | TIME_MOD t = FLOAT

Modified: trunk/Toss/Arena/ArenaTest.ml
===================================================================
--- trunk/Toss/Arena/ArenaTest.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Arena/ArenaTest.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -9,31 +9,7 @@
     | Arena.StartStruc struc -> struc
     | _ -> failwith "GameTreeTest:struc_of_str: not a structure"
 
-let rel_str rel struc_str =
-  let s = struc_of_str struc_str in
-  Structure.rel_str s rel (Structure.rel_graph rel s)
-
 let tests = "Arena" >::: [
-  "structure with rels parsing" >::
-    (fun () ->
-      let test p s res = assert_equal ~printer:(fun x -> x) res (rel_str p s) in
-      test "P" "START [ 1 - 5 | | - ] with P(a) = :nbr(a)= 2" "P (e2)";
-      test "P" "START [ 1 - 5 | | - ] with P(a) = :nbr(a)= 2 with :y(a) = 10*&a"
-        "P (e2)";
-      test "P" ("START [ 1 - 10 | | - ] with P(z) = &z > 1 and " ^ 
-		   "all x, y (&x * &y = &z -> (&x = 1 or &y = 1))")
-	"P {e2; e3; e5; e7}";
-      test "P" ("START [ 1 - 3 | | - ] with E(x, y) = &y = &x + 1; " ^ 
-		   "P(x, y) = &x != &y and tc x, y E(x, y)")
-	"P {(e1, e2); (e1, e3); (e2, e3)}";
-      test "S" ("START [ 1 - 10 | | - ] with P(z) = &z > 1 and " ^ 
-		   "all x, y (&x * &y = &z -> (&x = 1 or &y = 1));" ^
-		   "E(x, y) = P(x) and P(y) and &x < &y and " ^
-		   "  all z (&x < &z and &z < &y -> not P(z));" ^
-		   "S(x, y) = x != y and tc x, y E(x, y)")
-	"S {(e2, e3); (e2, e5); (e2, e7); (e3, e5); (e3, e7); (e5, e7)}";
-    );
-
   "simple parsing and printing" >::
     (fun () ->
       let s = "PLAYERS white, black
@@ -120,20 +96,3 @@
 	"[rule 0. -> 1 emb x: 1]"
     );
 ]
-
-let bigtests = "ArenaBig" >::: [
-  "structure with rels: 3 coloring" >::
-    (fun () ->
-      let test p s res = assert_equal ~printer:(fun x -> x) res (rel_str p s) in
-      test "C" ("START [ 1 - 3 | | - ] with E(x, y) = x != y; " ^ 
-		   "C(z) = ex R, G, B all x, y ( (x in R or x in G or x in B)"^
-		   " and ( E(x,y) -> not ( (x in R and y in R) or (x in G and"^
-		   "  y in G) or (x in B and y in B) ) ) )")
-	"C {e1; e2; e3}";
-      test "C" ("START [ 1 - 4 | | - ] with E(x, y) = x != y; " ^ 
-		   "C(z) = ex R, G, B all x, y ( (x in R or x in G or x in B)"^
-		   " and ( E(x,y) -> not ( (x in R and y in R) or (x in G and"^
-		   "  y in G) or (x in B and y in B) ) ) )")
-	"C:1 {}";
-    );
-]

Modified: trunk/Toss/Arena/DiscreteRuleParser.mly
===================================================================
--- trunk/Toss/Arena/DiscreteRuleParser.mly	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Arena/DiscreteRuleParser.mly	2012-07-10 22:44:46 UTC (rev 1744)
@@ -67,9 +67,6 @@
         DiscreteRule.compile_formula_rule signat defs phi del_part
           add_part pre
       }
-  | MATCH error
-      { Lexer.report_parsing_error $startpos $endpos
-          "Syntax error after the discrete rewrite rule MATCH keyword" }
 
 parse_discrete_rule:
   discrete_rule_expr EOF { $1 };

Modified: trunk/Toss/Client/Drawing.ml
===================================================================
--- trunk/Toss/Client/Drawing.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Client/Drawing.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -38,12 +38,15 @@
 
 let defaultCFill = { red=255 ; green = 228 ; blue = 170 ; opacity = 0.5 }
 let defaultCStroke = { red=38 ; green = 3 ; blue = 20 ; opacity = 0.5 }
-let defaultCRed = {red=242 ; green=92 ; blue=5 ; opacity = 1. }
+let defaultCRed = {red=232 ; green=42 ; blue=51 ; opacity = 1. }
 let defaultCGreen = {red=62 ; green=89 ; blue=24 ; opacity = 1. }
-let defaultCBlue = {red=165 ; green=175 ; blue=170 ; opacity = 1. }
+let defaultCBlue = {red=0 ; green=54 ; blue=76 ; opacity = 1. }
 
 let palette = Hashtbl.create 7
 
+(* Clear all previous color definitions. *)
+let reset_colors () = Hashtbl.clear palette
+
 (* Set a color for a name. *)
 let set_color name color =
   Hashtbl.add palette name color
@@ -219,7 +222,7 @@
     if arity = 1 then
       let elems = Structure.Tuples.elements (Structure.rel_graph rel struc) in
       let col = get_color rel in
-      Aux.concat_map (fun a -> [Circle (pos a.(0), {x=10.; y=10.}, col)]) elems
+      Aux.concat_map (fun a -> [Circle (pos a.(0), {x=5.; y=5.}, col)]) elems
     else if arity = 2 then
       let tuples = Structure.Tuples.elements (Structure.rel_graph rel struc) in
       let c = get_color ~stroke:true rel in
@@ -234,17 +237,19 @@
     let fill = "ctx.fillStyle = \""^(color_to_str col)^"\"; ctx.fill();" in
     if r.x = r.y then
       let s = Printf.sprintf "ctx.arc(%F,%F,%F,0,2*Math.PI,false); " p.x p.y r.x
-      in "ctx.beginPath(); "^ s ^ fill ^ " ctx.stroke(); ctx.closePath(); "
+      in ["ctx.beginPath(); "; s; fill; " ctx.stroke(); ctx.closePath(); "]
     else
       let sc = Printf.sprintf "ctx.scale(%F, %F); " (r.x /.100.) (r.y /.100.) in
       let tr = Printf.sprintf "ctx.translate(%F, %F); " p.x p.y in
-      "ctx.save(); "^ tr ^sc ^"ctx.beginPath(); ctx.arc(0,0,100,0,2*Math.PI); "^
-        fill ^ "ctx.stroke(); ctx.closePath(); ctx.restore(); "
+      ["ctx.save();"; tr;sc; "ctx.beginPath();";"ctx.arc(0,0,100,0,2*Math.PI);";
+       fill; "ctx.stroke(); ctx.closePath(); ctx.restore(); "]
   | Line (f, t, col) -> 
     let fs = Printf.sprintf "ctx.moveTo(%F,%F); " f.x f.y in
     let ts = Printf.sprintf "ctx.lineTo(%F,%F); " t.x t.y in
     let stroke= "ctx.strokeStyle = \""^(color_to_str col)^"\"; ctx.stroke();" in
-    "ctx.beginPath(); " ^ fs ^ ts ^ stroke ^ " ctx.closePath(); "
+    ["ctx.beginPath(); "; fs; ts; stroke; " ctx.closePath(); "]
 
-let shapes_to_canvas l =
-  String.concat " " (List.rev (List.rev_map shape_to_canvas l))
+let shapes_to_canvas ?(attach=[]) l =
+  let shapes = List.fold_left (fun acc shape -> List.rev_append 
+    (shape_to_canvas shape) acc) [] l in
+  Array.of_list (attach @ (List.rev shapes))

Modified: trunk/Toss/Client/Drawing.mli
===================================================================
--- trunk/Toss/Client/Drawing.mli	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Client/Drawing.mli	2012-07-10 22:44:46 UTC (rev 1744)
@@ -40,7 +40,10 @@
     whether for stroke or fill, or a default red, if name starts with '|'. *) 
 val get_color : ?stroke : bool -> string -> color
 
+(** Clear all previous color definitions. *)
+val reset_colors : unit -> unit
 
+
 (** Shapes. *)
 type shape =
   | Circle of point * point * color (** circle, given middle and radiuses *)
@@ -93,4 +96,4 @@
 
 (** Compile the shapes to a JavaScript program drawing the shape on 'ctx'. 
     With [result] in JS do: var ctx = canvas.getContext("2d"); eval (result). *)
-val shapes_to_canvas : shape list -> string
+val shapes_to_canvas : ?attach: string list -> shape list -> string array

Modified: trunk/Toss/Client/JsEval.ml
===================================================================
--- trunk/Toss/Client/JsEval.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Client/JsEval.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -27,46 +27,55 @@
 (* --- Main part: communication with JS and evaluation --- *)
 
 let cur_st = ref (Drawing.empty_struc_coords ())
+let cur_parsed_string = ref ""
 
 (* Parse a formula. *)
 let formula_of_string s = FormulaParser.parse_formula Lexer.lex 
   (Lexing.from_string (Aux.strip_spaces s))
 
 (* Parse a structure. *)
-let structure_of_string s = 
-  let str = "START " ^ (Aux.strip_spaces s) in
-  match ArenaParser.parse_game_defs Lexer.lex (Lexing.from_string str) with
-    | Arena.StartStruc struc -> struc
-    | _ -> failwith "not a structure"
+let structure_of_string s = StructureParser.parse_structure 
+  Lexer.lex (Lexing.from_string (Aux.strip_spaces s))
 
-
 (* Drawing the structure. *)
 let draw_struc_js so_s struc_s =
   let err msg = 
     let js_msg = Js.string ("put_msg('" ^ msg ^ "', 5000);") in
-    Js.array [|js_msg; Js.string "Error"|] in
+    Js.array [|Js.string "Error"; js_msg|] in
   let error_msg where = function
     | Lexer.Parsing_error m when String.length m > 15 && 
         String.sub m 0 15 = "File \"\", lines " ->
       let ms = String.sub m 15 ((String.index m '\n') - 16) in
       let l, c = String.sub ms 0 (String.index ms '-'), String.index ms ',' in
       let chars = String.sub ms (c+1) ((String.length ms)-c-1) in
-      let l = string_of_int ((int_of_string l) - 1) in
+      let l = if where = "Formula" then l else
+          string_of_int ((int_of_string l) - 1) in
       err (where ^ " parsing error in line " ^ l ^ "," ^ chars)
     | x -> err (where ^ " error:<br />" ^ 
                   (Aux.str_subst_all "\n" "<br/>" (Printexc.to_string x))) in
   try
-    let st = structure_of_string (Js.to_string struc_s) in
+    let in_string = Js.to_string struc_s in
+    let t = AuxIO.gettimeofday () in
+    let st = if !cur_parsed_string = in_string then !cur_st.Drawing.struc else
+        (let s = structure_of_string in_string in
+         LOG 0 "PUT#Structure constructed at %.3fs" (AuxIO.gettimeofday() -. t);
+         s) in
     try
       let so = Js.to_string so_s in
       let st, so_res = if Aux.strip_spaces so = "" then (st, "No Formula") else
           let so_phi = formula_of_string so in
-          let st, res = Solver.find_so st so_phi in
+          let st, res = Solver.find_so ~logtime:t ~logprefix:"PUT#" st so_phi in
           if res then st, "Formula Satisfied" else st,"Formula Unsatisfiable" in
-      let st_c = Drawing.add_coords 1000. 1000. 50. 50. None None st in
+      let st_c = Drawing.add_coords 500. 500. 25. 25. None None st in
       cur_st := st_c;
-      let draw = Drawing.shapes_to_canvas (Drawing.draw_struc st_c) in
-      Js.array [|Js.string ("clear_canvas (); " ^ draw) ; Js.string so_res |]
+      if so_res = "No Formula" then cur_parsed_string := in_string else
+        cur_parsed_string := "";
+      let shapes = Drawing.draw_struc st_c in
+      LOG 0 "PUT#Shapes constructed at %.3fs" (AuxIO.gettimeofday() -. t);
+      let draw = Drawing.shapes_to_canvas ~attach:[so_res; "clear_canvas();"]
+        shapes in
+      LOG 0 "PUT#Canvas commands issued at %.3fs" (AuxIO.gettimeofday() -. t);
+      Js.array (Array.map Js.string draw);
     with x -> error_msg "Formula" x
   with x -> error_msg "Structure" x
 
@@ -93,7 +102,7 @@
 
 let mousemove_handle x y i = 
   match elem_moving i with
-    | None -> Js.string "" 
+    | None -> Js.array [|Js.string ""|]
     | Some e -> 
       let (x,y), st = (Js.to_float x, Js.to_float y), !cur_st.Drawing.struc in
       let p = Drawing.change_coords !cur_st.Drawing.coordC 
@@ -101,8 +110,9 @@
       let st = Structure.change_fun_int st "x" e p.Drawing.x in
       let st = Structure.change_fun_int st "y" e (-1. *. p.Drawing.y) in
       cur_st := {!cur_st with Drawing.struc = st };
-      let s = Drawing.shapes_to_canvas (Drawing.draw_struc !cur_st) in
-      Js.string ("clear_canvas(); " ^ s)
+      let s = Drawing.shapes_to_canvas ~attach:["clear_canvas(); "]
+        (Drawing.draw_struc !cur_st) in
+      Js.array (Array.map Js.string s)
 
 let mouseup_handle x y i = 
   stop_moving i;
@@ -132,6 +142,7 @@
     match Aux.split_charprop (fun c -> c = ':') d with
       | [rel; c] -> set_color_def (Aux.strip_spaces rel) (Aux.strip_spaces c)
       | _ -> "Incorrect color definition: " ^ (Aux.normalize_spaces d) in
+  Drawing.reset_colors ();
   Js.string (String.concat " <br /> " (List.map parse_def defs))
 
 let _ = set_handle "set_colors" set_colors

Modified: trunk/Toss/Client/eval.html
===================================================================
--- trunk/Toss/Client/eval.html	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Client/eval.html	2012-07-10 22:44:46 UTC (rev 1744)
@@ -13,16 +13,35 @@
 var worker = new Worker ("JsEval.js");
 var worker_handler = new Object ();
 
-worker.onmessage = function (m) {
+var killBT = '<button class="obt" style="position: ' + 
+  'absolute; right: 1em; font-weight: bold;" ' +
+  'onclick="restart_worker()">Kill</button> ';
+
+function init_worker () {
+  worker.onmessage = function (m) {
     if (typeof m.data == 'string') {
         console.log("" + m.data);
+        if (m.data.substr (m.data.indexOf(']')+2, 4) === "PUT#") {
+          var cont = m.data.substring (m.data.indexOf(']')+6, m.data.length);
+          document.getElementById("working").innerHTML = cont + "... " + killBT;
+        }
     } else {
         //console.log ("[ASYNCH] back from " + m.data.fname);
         var handler = worker_handler[m.data.fname];
         handler (m.data.result);
     }
+  }
+  select_colors (true);
 }
 
+function restart_worker () {
+  worker.terminate ();
+  worker = new Worker ("JsEval.js");
+  worker_handler = new Object ();
+  init_worker ();
+  put_msg ("Killed", 2000);
+}
+
 function ASYNCH (action_name, action_args, should_log, cont) {
     worker_handler[action_name] = cont;
     worker.postMessage ({fname: action_name, args: action_args});
@@ -38,7 +57,7 @@
     ctx.clearRect(0, 0, canvas.width, canvas.height);
     ctx.fillStyle = "#ffe4aa";
     ctx.strokeStyle = "#260314";
-    ctx.lineWidth = 5;
+    ctx.lineWidth = 2;
     ctx.lineCap = "round";
     ctx.lineJoin = "round";
 }
@@ -49,7 +68,7 @@
     ctx.clearRect(0, 0, canvas.width, canvas.height);
     ctx.fillStyle = "#ffe4aa";
     ctx.strokeStyle = "#260314";
-    ctx.lineWidth = 5;
+    ctx.lineWidth = 2;
     ctx.lineCap = "round";
     ctx.lineJoin = "round";
 }
@@ -57,7 +76,7 @@
 function draw_it_msg (msg) {
   if (msg) {
     document.getElementById ("working").style.display = 'block'; 
-    document.getElementById ("working").innerHTML = 'Working...';
+    document.getElementById ("working").innerHTML = 'Working... ' + killBT;
   }
   var rels = document.getElementById ("relations").value;
   var pos = document.getElementById ("positions").value;
@@ -69,13 +88,13 @@
     ASYNCH ("draw_struc", ["", struc], true, function (a) { 
        document.getElementById ("working").style.display = 'none';
        var ctx = document.getElementById("canvas").getContext("2d");
-       eval (a[0])
+       for (var i = 1; i < a.length; i++) { eval (a[i]); }
        toggle_to_show ("view");
     })
   } else {
     ASYNCH ("draw_struc", ["", struc], true, function (a) { 
        var ctx = document.getElementById("canvas").getContext("2d");
-       eval (a[0])
+       for (var i = 1; i < a.length; i++) { eval (a[i]); }
     })
   }
 }
@@ -86,7 +105,7 @@
 
 function find_draw_it () {
   document.getElementById ("working").style.display = 'block';
-  document.getElementById ("working").innerHTML = 'Working...';
+  document.getElementById ("working").innerHTML = 'Working... ' + killBT;
   var rels = document.getElementById ("relations").value;
   var pos = document.getElementById ("positions").value;
   var elemsF = document.getElementById ("no-elems-start").value;
@@ -97,9 +116,9 @@
   ASYNCH ("draw_struc", [so, struc], true, function (a) { 
      document.getElementById ("working").style.display = 'none';
      var ctx = document.getElementById("canvas").getContext("2d");
-     eval (a[0]);
+     for (var i = 1; i < a.length; i++) { eval (a[i]); }
      toggle_to_show ("view");
-     if (a[1] !== "Error") { put_msg (a[1], 2000) }
+     if (a[0] !== "Error") { put_msg (a[0], 2000) }
   })
 }
 
@@ -170,9 +189,9 @@
     ALLOW_MOUSE_MOVE = false;
     setTimeout (function () { ALLOW_MOUSE_MOVE = true; }, 100);
     var pos = canvasCoords (e.pageX, e.pageY);
-    ASYNCH ("mousemove_handle", [pos.x, pos.y, 0], false, function (s) { 
+    ASYNCH ("mousemove_handle", [pos.x, pos.y, 0], false, function (a) { 
      var ctx = document.getElementById("canvas").getContext("2d");
-     eval (s);
+     for (var i = 0; i < a.length; i++) { eval (a[i]); }
     })
   }
 }
@@ -184,9 +203,9 @@
     setTimeout (function () { ALLOW_MOUSE_MOVE = true; }, 100);
     for (var i = 0; i < e.targetTouches.length; i++) {
       var p = canvasCoords (e.targetTouches[i].pageX, e.targetTouches[i].pageY);
-      ASYNCH ("mousemove_handle", [p.x, p.y, i], false, function (s) { 
+      ASYNCH ("mousemove_handle", [p.x, p.y, i], false, function (a) { 
        var ctx = document.getElementById("canvas").getContext("2d");
-       eval (s);
+       for (var i = 0; i < a.length; i++) { eval (a[i]); }
       })
     }
   }
@@ -195,16 +214,30 @@
 function handle_elem_click (eid) { console.log (eid); }
 
 function example_basic () {
-  document.getElementById ("struc-name").value = "Basic";
+  document.getElementById ("struc-name").value = "Cycle";
   document.getElementById ("relations").value =
-    "E(x, y) = (&y = &x + 1) ∨ (&x=15 ∧ &y=1)";
+    "E(x, y) = (&y = &x + 1) ∨ (&x=10 ∧ &y=0)";
   document.getElementById ("positions").value = ":x(a) = &a;\n" +
     ":y(a) = &a · (10 - &a) / 10";
-  document.getElementById ("no-elems-start").value = "1";
-  document.getElementById ("no-elems-end").value = "15";
+  document.getElementById ("no-elems-start").value = "0";
+  document.getElementById ("no-elems-end").value = "10";
   draw_it_msg (false);
 }
 
+function example_3x3 () {
+  document.getElementById ("struc-name").value = "3x3 grid";
+  document.getElementById ("relations").value =
+    "C(x, y) = (&y = &x+1) ∧ ¬∃z &x=3*&z + 2;\n" +
+    "R(x, y) = &y = &x+3";
+  document.getElementById ("positions").value = 
+    ":x(a) = (&a - :(∃z &a=3*&z + 1) - :(∃z &a=3*&z + 2)*2)*2;\n" +
+    ":y(a) = (:(∃z &a=3*&z + 2)*3 - :(∃z &a=3*&z)*3)*2";
+  document.getElementById ("no-elems-start").value = "0";
+  document.getElementById ("no-elems-end").value = "8";
+  draw_it_msg (false);
+}
+
+
 function example_primes () {
   document.getElementById ("struc-name").value = "Primes";
   document.getElementById ("relations").value =
@@ -215,6 +248,28 @@
   draw_it_msg (false);
 }
 
+function example_3dnp_struc () {
+  document.getElementById ("struc-name").value = "Triangles";
+  document.getElementById ("relations").value =
+    "E(x, y) = &y=&x+1 ∨ &y=&x+2 ∨ &x=&y+1 ∨ &x=&y+2";
+  document.getElementById ("positions").value = ":x(a) = &a*2;\n" +
+    ":y(a) = :(∃z &a=3*&z + 2)*9";
+  document.getElementById ("no-elems-start").value = "0";
+  document.getElementById ("no-elems-end").value = "9";
+  draw_it_msg (false);
+}
+
+function example_3col_struc () {
+  document.getElementById ("struc-name").value = "Full 3-partite graph";
+  document.getElementById ("relations").value =
+    "E(x, y) = ¬∃ z (&x=&y+3*&z ∨ &y=&x+3*&z)";
+  document.getElementById ("positions").value = ":x(a) = &a;\n" +
+    ":y(a) = :(∃z &a=3*&z + 1)*5 - :(∃z &a=3*&z + 2)*5";
+  document.getElementById ("no-elems-start").value = "0";
+  document.getElementById ("no-elems-end").value = "18";
+  draw_it_msg (false);
+}
+
 function example_tc () {
   document.getElementById ("struc-name").value = "Simple TC";
   document.getElementById ("relations").value =
@@ -227,7 +282,7 @@
 }
 
 function example_heart () {
-  document.getElementById ("struc-name").value = "Heart";
+  document.getElementById ("struc-name").value = "Heart drawing";
   document.getElementById ("relations").value = 
     "E(x, y) = (&y = &x + 1 ∧ &x ≠ 18) ∨ (&x=37 ∧ &y=18)";
   document.getElementById ("positions").rows = 7;
@@ -243,11 +298,26 @@
   draw_it_msg (false);
 }
 
+
+function example_diag () {
+  document.getElementById ("so-name").value = "Diagonal";
+  document.getElementById ("second-order").value = 
+    "∀ x,y ( |Diag(x,y) <-> ∃ u (R(x,u) ∧ C(u, y)) )"
+  find_draw_it ();
+}
+
+function example_last_row () {
+  document.getElementById ("so-name").value = "Last row";
+  document.getElementById ("second-order").value = 
+    "∀ x (|LastRow(x) <-> ∀ y ¬ C(x, y))";
+  find_draw_it ();
+}
+
 function example_matching () {
   document.getElementById ("so-name").value = "Matching";
   document.getElementById ("second-order").value = 
     "∀ x,y ( |M(x, y) -> (\n" +
-    "  ( E(x, y) ∨ E(y, x) ) ∧ ¬∃ z (z≠y ∧ |M(x, z) )\n" +
+    "  ( E(x, y) ∨ E(y, x) ) ∧ ¬∃ z (z≠y ∧ (|M(x, z) ∨ |M(z, x)))\n" +
     ") ) ∧ ∀ x ∃ y |M(x, y)";
   find_draw_it ();
 }
@@ -268,11 +338,16 @@
   find_draw_it ();
 }
 
-function example_tc_so () {
-  document.getElementById ("so-name").value = "TC";
+function example_3dnp () {
+  document.getElementById ("so-name").value = "3-DNP";
+  document.getElementById ("second-order").rows = 6;
   document.getElementById ("second-order").value = 
-    "∀ x,y,z ( ( E(x, y) → |Tc(x, y) ) ∧\n" + 
-    "  ( (|Tc(x, y) ∧ |Tc(y, z)) -> |Tc(x, z) ) )";
+    "∀ x ∃ y,u,v (((|R(x) → ¬(|G(x) ∨ |B(x))) ∧\n" +
+    "  (|G(x) → ¬(|R(x) ∨  |B(x))) ∧\n" +
+    "  (|B(x) → ¬(|R(x) ∨  |G(x)))) ∧\n" +
+    "  (|R(x) ∨ (|R(y) ∧ E(x,y))) ∧\n" +
+    "  (|G(x) ∨ (|G(u) ∧ E(x,u))) ∧\n" +
+    "  (|B(x) ∨ (|B(v) ∧ E(x,v))))";
   find_draw_it ();
 }
 
@@ -311,6 +386,7 @@
   localStorage["TRelStrucExplRel"+name] = rels;
   localStorage["TRelStrucExplPos"+name] = pos;
   list_stored_struc ();
+  put_msg ("Structure Saved", 1000);
 }
 
 function save_so () {
@@ -318,6 +394,7 @@
   var phi = document.getElementById ("second-order").value;
   localStorage["TRelStrucExplSOF"+name] = phi;
   list_stored_so ();
+  put_msg ("Formula Saved", 1000);
 }
 
 function load_struc (name) {
@@ -350,7 +427,7 @@
       var li = document.createElement('li');
       li.innerHTML ='<button class="obt" onclick="load_struc('+"'"+ n +"'"+')">'
         + n +'</button> <button class="ebtr" onclick="del_struc('+ "'"+ n +"'"+
-        ')" style="width: 4em;" title="Delete this structure.">Del</button>';
+        ')" style="width: 2em;" title="Delete this structure.">&#215;</button>';
       saved.appendChild (li);
     }
   }
@@ -365,8 +442,8 @@
       var n = k.substring (16, k.length);
       var li = document.createElement('li');
       li.innerHTML ='<button class="obt" onclick="load_so('+"'"+ n +"'"+')">'
-        + n +'</button> <button class="ebtr" onclick="del_so('+ "'"+ n +
-        "'" +')" style="width: 4em;" title="Delete this formula.">Del</button>';
+        + n +'</button> <button class="ebtr" onclick="del_so('+ "'"+ n +"'" +
+        ')" style="width: 2em;" title="Delete this formula.">&#215;</button>';
       saved.appendChild (li);
     }
   }
@@ -424,18 +501,18 @@
 
 function toggle (name) {
   var bt = document.getElementById ("hide_" + name + "_bt");
-  if (bt.innerHTML == "Hide") {
-    bt.innerHTML = "Show";
+  if (bt.innerHTML == "«") {
+    bt.innerHTML = "»";
     document.getElementById ("div_" + name + "_full").style.display = 'none';
   } else {
-    bt.innerHTML = "Hide";
+    bt.innerHTML = "«";
     document.getElementById ("div_" + name + "_full").style.display = 'block';
   }
 }
 
 function toggle_to_show (name) {
   var bt = document.getElementById ("hide_" + name + "_bt");
-  if (bt.innerHTML !== "Hide") { toggle (name); }
+  if (bt.innerHTML !== "«") { toggle (name); }
 }
 
 function show_help (content) {
@@ -443,7 +520,8 @@
   document.getElementById ("working").style.fontWeight = "normal";
   document.getElementById("working").innerHTML = '\
 <b>Relational Structures Explorer Help</b> &nbsp; &nbsp;\
-<button class="obt" style="position: absolute; right: 1em;" onclick="hide_working()">Hide</button> ' + content;
+<button class="obt" style="position: absolute; right: 1em; font-weight: bold;"\
+  onclick="hide_working()">&#215;</button> ' + content;
   document.getElementById ("working").style.display = "block";
 }
 
@@ -458,8 +536,9 @@
 function show_help_saved () {
   show_help('\
 <p><b>Saved structures and formulas</b> are stored in the browser local \
-  storage. Press the <b>Save</b> button in the respective edit field to save \
-  a structure or a formula, and later the <b>Del</b> button to delete it.</p>\
+  storage. Press the <b>&#x21e9;</b> button in the respective section to \
+  save a structure or a formula, and later the <b>&#215;</b> button to \
+  delete it.</p>\
   ');
 }
 
@@ -505,12 +584,12 @@
 </script>
 </head>
 
-<body onload="init_canvas (); select_colors (true) ; list_stored (); draw_it_msg (false); adjust_to_width()">
+<body onload="init_worker (); init_canvas (); list_stored (); draw_it_msg (false); adjust_to_width()">
 <div id="main">
 
 <div id="top">
 <div id="logo">
-  <a id="leftupperlogo-link" href="eval.html">
+  <a id="leftupperlogo-link" href="index.html">
     <img id="leftupperlogo-img" src="img/logo.png" alt="back" />
   </a>
 </div>
@@ -529,15 +608,15 @@
 <div id="div_right_col_full" style="width: 30em;">
 
 <p class="headerp">
-  <button class="ebtl" style="width: 4em;" title="Show/Hide structure view."
-          id="hide_view_bt" onclick="toggle('view')">Hide</button>
+  <button class="ebtl" style="width: 2em;" title="Show/Hide structure view."
+          id="hide_view_bt" onclick="toggle('view')">&#171;</button>
   View Structure
-  <button class="ebtr" style="width: 4em;" title="Structure viewing help."
-          onclick="show_help_view()">Help</button>
+  <button class="ebtr" style="width: 2em;" title="Structure viewing help."
+          onclick="show_help_view()">?</button>
 </p>
 
 <div id="div_view_full" style="width: 30em;">
-<canvas id="canvas" height="1100" width="1100"
+<canvas id="canvas" height="550" width="550"
         onmouseup="mouseup_handle(event)"
         onmousedown="mousedown_handle(event)"
         onmousemove="mousemove_handle(event)"
@@ -549,62 +628,110 @@
 </div>
 
 <p class="headerp">
-  <button class="ebtl" style="width: 4em;" title="Show/Hide color selector."
-          id="hide_colors_bt" onclick="toggle ('colors')">Hide</button>
+  <button class="ebtl" style="width: 2em;" title="Show/Hide color selector."
+          id="hide_colors_bt" onclick="toggle ('colors')">&#171;</button>
   Select Colors
-  <button class="ebtr" style="width: 4em;" title="Color selector help."
-            onclick="show_help_colors()">Help</button>
+  <span style="position: absolute; right: 1px;">
+  <button class="ebt" onclick="select_colors(false)" style="width: 4em;"
+          title="Select these colors.">Select</button><button
+      class="ebt" style="width: 2em;" title="Color selector help."
+      onclick="show_help_colors()">?</button>
+  </span>
 </p>
 
 <div id="div_colors_full">
 <p>Colors
-  <span style="position: absolute; right: 2px;">
-  <button class="ebts" style="background-color: #e5effa;";
-          onclick="add_field('colors', '#e5effa')">&nbsp;</button><button
-      class="ebts" style="background-color: #a5afaa;";
-      onclick="add_field('colors', '#a5afaa')">&nbsp;</button><button
+  <span style="position: absolute; right: 1px;">
+  <button class="ebts" style="background-color: #a5afaa;";
+          onclick="add_field('colors', '#a5afaa')">&nbsp;</button><button
+      class="ebts" style="background-color: #00364c;";
+      onclick="add_field('colors', '#00364c')">&nbsp;</button><button
     class="ebts" style="background-color: #93a605;";
     onclick="add_field('colors', '#93a605')">&nbsp;</button><button
       class="ebts" style="background-color: #3e5916;";
       onclick="add_field('colors', '#3e5916')">&nbsp;</button><button
-    class="ebts" style="background-color: #f28705;";
-    onclick="add_field('colors', '#f28705')">&nbsp;</button><button
-      style="background-color: #f25c05;"; class="ebts"
-      onclick="add_field('colors', '#f25c05')">&nbsp;</button><button
+    class="ebts" style="background-color: #f25c05;";
+    onclick="add_field('colors', '#f25c05')">&nbsp;</button><button
+      style="background-color: #e82a33;"; class="ebts"
+      onclick="add_field('colors', '#e82a33')">&nbsp;</button><button
     style="background-color: #260314;"; class="ebts" 
     onclick="add_field('colors', '#260314')">&nbsp;</button>
-  &nbsp; <button class="ebt" onclick="select_colors(false)" style="width: 4em;"
-                 title="Select these colors.">Select</button>
   </span>
 </p>
 <textarea id="colors" rows="1" cols="60" class="textar">
-|R : #f25c05 ; |G : #3e5916  ; |B : #a5afaa</textarea> 
+R : #f25c05 ; |R : #e82a33 ; |G : #3e5916  ; |B : #00364c</textarea> 
 </div>
 
 </div> <!-- end right column -->
 
 <p class="headerp">
-  <button class="ebtl" style="width: 4em;" title="Show/Hide structure editing."
-          id="hide_struc_bt" onclick="toggle('struc')">Hide</button>
+  <button class="ebtl" style="width: 2em;" title="Show/Hide formula evaluator."
+          id="hide_formula_bt" onclick="toggle ('formula')">&#171;</button>
+  Evaluate Formulas
+  <span style="position: absolute; right: 1px;">
+    <button class="ebt" onclick="save_so()" title="Save current formula."
+            style="width: 2em;">&#x21e9;</button><button
+        class="ebt" style="width: 2em;" title="Formula evaluator help."
+        onclick="show_help_formula()">?</button>
+  </span>
+</p>
+
+<div id="div_formula_full">
+<p>
+  Formula Name &nbsp; &nbsp;
+  <input id="so-name" type="text" size="20" value="My Formula 1"
+         style="width: 12em"></input>
+  <button class="ebtr" onclick="find_draw_it()" style="width: 4em;"
+          title="Evaluate the formula.">Eval</button>
+</p>
+
+<p>Formula
+  <span style="position: absolute; right: 2px;">
+  <button class="ebts" title="Not equal. You can also write '<>' or '!='."
+          onclick="add_field('second-order', '≠')">≠</button><button
+      class="ebts" title="Conjunction. You can also write 'and' or '&'."
+      onclick="add_field('second-order', '∧')">∧</button><button
+    class="ebts" title="Disjunction. You can also write 'or' or '|'."
+    onclick="add_field('second-order', '∨')">∨</button><button
+      class="ebts" title="Negation. You can also write 'not' or '~' or '!'."
+      onclick="add_field('second-order', '¬')">¬</button><button
+    class="ebts" title="Implication. You can also write '->'."
+    onclick="add_field('second-order', '→')">→</button><button
+      title="Existential Quantifier. You can also write 'ex' or '\E'."
+      class="ebts" onclick="add_field('second-order', '∃')">∃</button><button
+    title="Universal Quantifier. You can also write 'all' or '\A'."
+    class="ebts" onclick="add_field('second-order', '∀')">∀</button>
+  </span>
+</p>
+<textarea id="second-order" rows="3" cols="60" class="textar">
+</textarea> 
+
+</div>
+
+<p class="headerp">
+  <button class="ebtl" style="width: 2em;" title="Show/Hide structure editing."
+          id="hide_struc_bt" onclick="toggle('struc')">&#171;</button>
   Edit Structure
-  <button class="ebtr" style="width: 4em;" title="Structure editing help."
-          onclick="show_help_struc()">Help</button>
+  <span style="position: absolute; right: 1px;">
+    <button class="ebt" style="width: 2em;" title="Save current structure."
+            onclick="save_struc()">&#x21e9;</button><button
+          class="ebt" style="width: 2em;" title="Structure editing help."
+          onclick="show_help_struc()">?</button>
+  </span>
 </p>
 
 <div id="div_struc_full">
 <p>Name &nbsp; &nbsp; &nbsp; &nbsp;
   <input id="struc-name" type="text" size="20" value="My Structure 1"
          style="width: 12em"></input>
-  <span style="position: absolute; right: 2px;">
-    <button class="ebt" style="width: 4em;" title="Save current structure."
-            onclick="save_struc()">Save</button>
-  </span>
+  <button class="ebtr" onclick="draw_it()" style="width: 4em;"
+          title="Draw current structure.">Draw</button>
 </p>
 
 <p>Elements &nbsp; &nbsp;
-  <input id="no-elems-start" type="text" size="2" value="1"
+  <input id="no-elems-start" type="text" size="2" value="0"
          style="width: 4em"></input> &nbsp; &mdash; &nbsp;
-  <input id="no-elems-end" type="text" size="4" value="15"
+  <input id="no-elems-end" type="text" size="4" value="10"
          style="width: 4em"></input>
   <span style="position: absolute; right: 2px;">
   <button class="ebt" style="width: 2em;" title="Remove last element."
@@ -621,7 +748,7 @@
       onclick="add_field('relations', '∧')">∧</button><button
     class="ebts" title="Disjunction. You can also write 'or' or '|'."
     onclick="add_field('relations', '∨')">∨</button><button
-      class="ebts" title="Negation. You can also write 'not'."
+      class="ebts" title="Negation. You can also write 'not' or '~' or '!'.""
       onclick="add_field('relations', '¬')">¬</button><button
     class="ebts" title="Implication. You can also write '->'."
     onclick="add_field('relations', '→')">→</button><button
@@ -629,12 +756,10 @@
       class="ebts" onclick="add_field('relations', '∃')">∃</button><button
     title="Universal Quantifier. You can also write 'all' or '\A'."
     class="ebts" onclick="add_field('relations', '∀')">∀</button>
-  &nbsp; <button class="ebt" onclick="draw_it()" style="width: 4em;"
-                 title="Redraw current structure.">Draw</button>
   </span>
 </p>
 <textarea id="relations" rows="3" cols="60" class="textar">
-E(x, y) = (&y = &x + 1) ∨ (&x=15 ∧ &y=1)
+E(x, y) = (&y = &x + 1) ∨ (&x=10 ∧ &y=0)
 </textarea> 
 
 <p>Positions
@@ -653,8 +778,6 @@
       class="ebts" onclick="add_field('positions', '∃')">∃</button><button
     title="Universal Quantifier. You can also write 'all' or '\A'."
     class="ebts" onclick="add_field('positions', '∀')">∀</button>
-  &nbsp; <button class="ebt" onclick="draw_it()" style="width: 4em;"
-                 title="Redraw current structure.">Draw</button>
   </span>
 </p>
 <textarea id="positions" rows="3" cols="60" class="textar">
@@ -664,86 +787,68 @@
 </div>
 
 <p class="headerp">
-  <button class="ebtl" style="width: 4em;" title="Show/Hide formula evaluator."
-          id="hide_formula_bt" onclick="toggle ('formula')">Hide</button>
-  Evaluate Formulas
-  <button class="ebtr" style="width: 4em;" title="Formula evaluator help."
-            onclick="show_help_formula()">Help</button>
-</p>
-
-<div id="div_formula_full">
-<p>
-  Formula Name &nbsp; &nbsp;
-  <input id="so-name" type="text" size="20" value="My Formula 1"
-         style="width: 12em"></input>
-  <span style="position: absolute; right: 2px;">
-    <button class="ebt" onclick="save_so()" title="Save current formula."
-            style="width: 4em;">Save</button>
-    </span>
-</p>
-
-<p>Formula
-  <span style="position: absolute; right: 2px;">
-  <button class="ebts" title="Not equal. You can also write '<>' or '!='."
-          onclick="add_field('second-order', '≠')">≠</button><button
-      class="ebts" title="Conjunction. You can also write 'and' or '&'."
-      onclick="add_field('second-order', '∧')">∧</button><button
-    class="ebts" title="Disjunction. You can also write 'or' or '|'."
-    onclick="add_field('second-order', '∨')">∨</button><button
-      class="ebts" title="Negation. You can also write 'not'."
-      onclick="add_field('second-order', '¬')">¬</button><button
-    class="ebts" title="Implication. You can also write '->'."
-    onclick="add_field('second-order', '→')">→</button><button
-      title="Existential Quantifier. You can also write 'ex' or '\E'."
-      class="ebts" onclick="add_field('second-order', '∃')">∃</button><button
-    title="Universal Quantifier. You can also write 'all' or '\A'."
-    class="ebts" onclick="add_field('second-order', '∀')">∀</button>
-  &nbsp; <button class="ebt" onclick="find_draw_it()" style="width: 4em;"
-                 title="Evaluate the formula.">Eval</button>
-  </span>
-</p>
-<textarea id="second-order" rows="3" cols="60" class="textar">
-</textarea> 
-
-</div>
-
-<p class="headerp">
-  <button class="ebtl" style="width: 4em;" title="Show/Hide examples & saved."
-          id="hide_saved_bt" onclick="toggle('saved')">Hide</button>
+  <button class="ebtl" style="width: 2em;" title="Show/Hide examples & saved."
+          id="hide_saved_bt" onclick="toggle('saved')">&#171;</button>
   Examples & Saved
   <button class="ebtr" title="Saved structures and formulas help."
-          style="width: 4em;" onclick="show_help_saved()">Help</button>
+          style="width: 2em;" onclick="show_help_saved()">?</button>
 </p>
 
 <div id="div_saved_full">
-<p>Saved Structures</p>
-<ul id="saved-strucs" style="list-style: square; margin-left: -1.5em">
+<p style="padding-right: 1.5em; text-align: left">Saved Formulas</p>
+<ul id="saved-so" style="list-style: square; margin-left: -1.5em">
 <li>Nothing here yet</li>
 </ul>
 
 <p>Examples
 <span style="position: absolute; right: 1px;">
-<button class="ebt" onclick="example_basic()">Basic</button>
-<button class="ebt" onclick="example_primes()">Primes</button>
-<button class="ebt" onclick="example_tc()">Simple TC</button>
-<button class="ebt" onclick="example_heart()">Heart</button>
+<button class="ebt" style="width: 7em;"
+        onclick="example_diag()">Diagonal</button>
+<button class="ebt" style="width: 7em;"
+        onclick="example_last_row()">Last row</button>
+<button class="ebt" style="width: 7em;"
+        onclick="example_2col()">2-coloring</button>
 </span>
 </p>
 
-<p style="padding-right: 1.5em; text-align: left">Saved Formulas</p>
-<ul id="saved-so" style="list-style: square; margin-left: -1.5em">
+<p>&nbsp;
+<span style="position: absolute; right: 1px;">
+<button class="ebt" style="width: 7em;"
+        onclick="example_3col()">3-coloring</button>
+<button class="ebt" style="width: 7em;"
+        onclick="example_3dnp()">3-DNP</button>
+<button class="ebt" style="width: 7em;"
+        onclick="example_matching()">Matching</button>
+</span>
+</p>
+
+<p>Saved Structures</p>
+<ul id="saved-strucs" style="list-style: square; margin-left: -1.5em">
 <li>Nothing here yet</li>
 </ul>
 
 <p>Examples
 <span style="position: absolute; right: 1px;">
-<button class="ebt" onclick="example_tc_so()">TC</button>
-<button class="ebt" onclick="example_2col()">2-coloring</button>
-<button class="ebt" onclick="example_3col()">3-coloring</button>
-<button class="ebt" onclick="example_matching()">Matching</button>
+<button class="ebt" style="width: 7em;"
+        onclick="example_basic()">Cycle</button>
+<button class="ebt" style="width: 7em;" 
+        onclick="example_3col_struc()">3-partite</button>
+<button class="ebt" style="width: 7em;" 
+        onclick="example_3x3()">3x3 grid</button>
 </span>
 </p>
 
+<p> &nbsp;
+<span style="position: absolute; right: 1px;">
+<button class="ebt" style="width: 7em;" 
+        onclick="example_primes()">Primes</button>
+<button class="ebt" style="width: 7em;" 
+        onclick="example_3dnp_struc()">Triangles</button>
+<button class="ebt" style="width: 7em;" 
+        onclick="example_heart()">Heart</button>
+</span>
+</p>
+
 </div>
 
 </div>

Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Formula/BoolFormula.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -1,7 +1,7 @@
 (* Represent Boolean combinations of integer literals. *)
 
 (* 0 : no generation is performed and to_cnf transforms a DNF
-   1 : use Tseitin to construct a CNF with auxiliary variables
+   1 : use Tseitin to construct a NF with auxiliary variables
    2 : use Plaisted-Greenbaum to construct a CNF with auxiliary variables *)
 let auxcnf_generation = ref 2
 let set_auxcnf i = (auxcnf_generation := i)
@@ -594,6 +594,8 @@
   let rec index_formula ?(neg=false) = function
     | BVar v -> v
     | BNot phi -> - index_formula ~neg:(not neg) phi
+    | BOr [phi] -> index_formula ~neg phi
+    | BAnd [phi] -> index_formula ~neg phi
     | BOr bflist -> 
       let indlist = List.rev_map (index_formula ~neg:neg) bflist in
       free_idx := !free_idx + 1;
@@ -641,13 +643,57 @@
     List.for_all (fun x -> List.exists (fun y -> y=x) b) a in
   List.filter (fun x -> List.for_all (fun y -> x=y || not(subset y x)) cnf) cnf
 
-let find_model phi =
-  let phi1 = to_nnf ~neg:true phi in
-  let arg = flatten phi1 in
+(* Check if a CNF formula is satisfiable and find a model.
+   Faster than Sat.sat due to lack of formula registration *)
+let find_sat cnf = 
+  MiniSAT.reset ();
+  let vars = Hashtbl.create 15 in
+  let var v = try Hashtbl.find vars v with Not_found ->
+    (let w = MiniSAT.new_var () in Hashtbl.add vars v w; w) in
+  let lit v = let w = var (abs v) in
+              if v > 0 then MiniSAT.pos_lit w else MiniSAT.neg_lit w in
+  let add_clause cl = MiniSAT.add_clause (List.rev_map lit cl) in
+  List.iter add_clause cnf;
+  match MiniSAT.solve () with
+    | MiniSAT.UNSAT -> MiniSAT.reset (); None
+    | MiniSAT.TIMEOUT -> MiniSAT.reset (); failwith "do_sat: timeout"
+    | MiniSAT.SAT -> 
+      let res = ref [] in
+      let update v mv = 
+        if MiniSAT.value_of mv = 0 then res := (-v) :: !res
+        else if MiniSAT.value_of mv = 1 then res := v :: !res in
+      Hashtbl.iter update vars;
+      MiniSAT.reset ();
+      Some (!res)
+
+(* Print the CNF formula in dimacs format. *)
+let print_dimacs cnf =
+  let maxvar cl = List.fold_left (fun acc b -> max acc (abs b)) 0 cl in
+  let mvar = List.fold_left (fun acc cl -> max acc (maxvar cl)) 0 cnf in
+  let cl_str cl = (String.concat " " (List.map string_of_int cl)) ^ " 0\n" in
+  AuxIO.print ("p cnf " ^ (string_of_int mvar) ^ " " ^ 
+                  (string_of_int (List.length cnf)) ^ "\n");
+  List.iter (fun cl -> AuxIO.print (cl_str cl)) cnf
+
+
+(* Find a model of a Boolean formula. Uses P.-G. conversion. *)
+let find_model ?logtime ?(logprefix="") phi =
+  let arg = flatten (to_nnf ~neg:true phi) in
   let (sep, aux_phi) = pg_auxcnf_of_bool_formula arg in
-  match Sat.sat (listcnf_of_boolcnf aux_phi) with
-    | None -> None
+  (match logtime with None -> () | Some t ->
+    LOG 0 "%sCNF constructed at %.3fs" logprefix (AuxIO.gettimeofday () -. t));
+  let cnf = listcnf_of_boolcnf aux_phi in
+  (* print_dimacs cnf; *)
+  let reg_t = AuxIO.gettimeofday () in
+  let log_finish () =
+    match logtime with None -> () | Some t ->
+      let cur_t = AuxIO.gettimeofday () in
+      LOG 0 "%sSolver finished at %.3fs (ran %.3fs)" logprefix
+        (cur_t-.t) (cur_t-.reg_t) in
+  match find_sat cnf with
+    | None -> log_finish (); None
     | Some l -> 
+      log_finish ();
       let valid = List.filter (fun v -> v < sep && v > -sep) l in
       Some (Aux.unique_sorted valid)
 

Modified: trunk/Toss/Formula/BoolFormula.mli
===================================================================
--- trunk/Toss/Formula/BoolFormula.mli	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Formula/BoolFormula.mli	2012-07-10 22:44:46 UTC (rev 1744)
@@ -54,7 +54,8 @@
 val to_nnf : ?neg : bool -> bool_formula -> bool_formula
 
 (** Find a model for a Boolean formula. *)
-val find_model : bool_formula -> int list option
+val find_model : ?logtime : float -> ?logprefix : string ->
+  bool_formula -> int list option
 
 (** Convert a Boolean formula to CNF. If you only want SAT, use find_model. *)
 val convert : ?disc_vars: int list -> bool_formula -> int list list

Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Formula/FormulaParser.mly	2012-07-10 22:44:46 UTC (rev 1744)
@@ -64,6 +64,10 @@
   | OPEN real_expr CLOSE            { $2 }
   | LET_CMD COLON v = ID EQ def = real_expr IN_MOD re = real_expr
       { RLet (":" ^ v, def, re) }
+  | error
+    { Lexer.report_parsing_error $startpos $endpos
+        "Syntax error in real expression."
+    }
 
 real_ineq:
   | real_expr GR real_expr 
@@ -134,8 +138,11 @@
   | LET_CMD rel = ID args = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
       EQ body = formula_expr IN_MOD phi = formula_expr
       { Let (rel, args, body, phi) } %prec LET_CMD
+  | error
+    { Lexer.report_parsing_error $startpos $endpos
+        "Syntax error in formula expression."
+    }
 
-
 expr_eq_expr: /* only standard equations here for now (no differentials) */
   | COLON ID OPEN ID CLOSE EQ real_expr       { (($2, $4), $7) }
   | COLON ID OPEN INT CLOSE EQ real_expr      { (($2, string_of_int $4), $7) }
@@ -146,6 +153,10 @@
 %public expr_eq_sys:
   | expr_eq_expr                        { [$1] }
   | expr_eq_expr SEMICOLON expr_eq_sys  { $1 :: $3 }
+  | error
+    { Lexer.report_parsing_error $startpos $endpos
+        "Syntax error in equation system."
+    }
 
 parse_expr_eqs:
     expr_eq_sys EOF { $1 };

Modified: trunk/Toss/Formula/Lexer.mll
===================================================================
--- trunk/Toss/Formula/Lexer.mll	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Formula/Lexer.mll	2012-07-10 22:44:46 UTC (rev 1744)
@@ -197,6 +197,7 @@
   | "⊕"             { XOR }
   | "not"           { NOT }
   | "¬"             { NOT }
+  | "~"             { NOT }
   | "ex"            { EX }
   | "\\E"           { EX }
   | "exists"        { EX }

Modified: trunk/Toss/Formula/Sat/Sat.ml
===================================================================
--- trunk/Toss/Formula/Sat/Sat.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Formula/Sat/Sat.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -186,7 +186,7 @@
 let sat cnf = 
   register_new_formula (simplify [] cnf);
   match solve () with
-      None -> None
+    | None -> None
     | Some m -> Some m
 
 let is_sat cnf = match sat cnf with Some _ -> true | None -> false

Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Makefile	2012-07-10 22:44:46 UTC (rev 1744)
@@ -199,6 +199,9 @@
 	cp _build/Server/Server.native TossServer
 	OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -fulltest Solver -v
 
+SolverTestsExtra: Server/Server.native TossServer
+	OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ./TossServer -extratest Solver
+
 # Term tests
 TermTests: Server/Server.native
 	cp _build/Server/Server.native TossServer

Modified: trunk/Toss/Server/Server.ml
===================================================================
--- trunk/Toss/Server/Server.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Server/Server.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -413,7 +413,7 @@
     ("-fulltest", Arg.String (fun s -> test_s := s; test_full := true),
      "full unit tests for given path, might take longer");
     ("-extratest", Arg.String (fun s -> test_s := "#EXTRA$" ^ s),
-     "extra unit tests, take very long; use 'GGP' or 'Learn' as argument");
+     "extra unit tests, take very long; write 'GGP' or 'Learn' or 'Solver'");
     ("-noprecache", Arg.Unit (fun ()-> precache := false), "do no pre-caching");
     ("-nohttpcache", Arg.Unit (fun ()-> cache_html := false), 
      "re-read files from disk on each HTTP GET request");
@@ -431,6 +431,9 @@
     else if !test_s = "#EXTRA$Learn" then 
       let etst = LearnGameTest.extratests in
       ignore (OUnit.run_test_tt ~verbose:true etst)
+    else if !test_s = "#EXTRA$Solver" then 
+      let etst = SolverTest.extratests in
+      ignore (OUnit.run_test_tt ~verbose:true etst)
     else (
       let (name, full) = (!test_s, !test_full) in
       let len = String.length name in

Modified: trunk/Toss/Server/Tests.ml
===================================================================
--- trunk/Toss/Server/Tests.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Server/Tests.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -43,7 +43,7 @@
 let arena_tests = "Arena", [
   "DiscreteRuleTest",   [DiscreteRuleTest.tests];
   "ContinuousRuleTest", [ContinuousRuleTest.tests];
-  "ArenaTest",          [ArenaTest.tests; ArenaTest.bigtests];
+  "ArenaTest",          [ArenaTest.tests];
 ]
 
 let play_tests = "Play", [

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2012-07-06 01:06:25 UTC (rev 1743)
+++ trunk/Toss/Solver/Solver.ml	2012-07-10 22:44:46 UTC (rev 1744)
@@ -299,7 +299,7 @@
     | Fun (s, v) ->
       (try
         let e = List.assoc v assgn in
-          Poly.Const (Structure.fun_val model s e)
+        Poly.Const (Structure.fun_val model s e)
        with Not_found ->
          (*failwith (
            "Solver.assignment_of_real_expr: partial function " ^
@@ -322,22 +322,70 @@
       let asg = join (eval fp model elems fo_aset guard) r_a in
       sum_polys asg (* Note: above "sgn" is irrelevant! *)
     | RLet _ as re -> poly_of assgn (FormulaSubst.expand_real_expr re) in
+  let rec crude_val asg = function
+    | Const v -> v
+    | Plus (e1, e2) -> (crude_val asg e1) +. (crude_val asg e2)
+    | Times (e1, e2) -> (crude_val asg e1) *. (crude_val asg e2)
+    | Pow (e1, e2) -> (crude_val asg e1) ** (crude_val asg e2)
+    | Fun (fname, var) ->
+      let e = List.assoc var asg in
+      Structure.fun_val model fname e
+    | RLet _ as re -> crude_val asg (FormulaSubst.expand_real_expr re)
+    | _ -> raise Not_found in
+  let rec crude_eq keep asg = function
+    | Const v -> Const v
+    | Plus (e1, e2) -> Plus (crude_eq keep asg e1, crude_eq keep asg e2)
+    | Times (e1, e2) -> Times (crude_eq keep asg e1, crude_eq keep asg e2)
+    | Pow (e1, e2) -> Pow (crude_eq keep asg e1, crude_eq keep asg e2)
+    | Fun (fname, var) ->
+      if List.mem var keep then Fun (fname, var) else
+        let e = List.assoc var asg in
+        Const (Structure.fun_val model fname e)
+    | RLet _ as re -> crude_eq keep asg (FormulaSubst.expand_real_expr re)
+    | _ -> raise Not_found in
+  let check_sign_op_bool x = function
+    | EQZero -> x = 0. | GZero -> x > 0. | LZero -> x < 0.
+    | GEQZero -> x >= 0. | LEQZero -> x <= 0. | NEQZero -> x <> 0. in
+  let check_sign_op x s = if check_sign_op_bool x s then Any else Empty in
   let rec process_vars assgn = function
-    | [] -> 
-      let poly = poly_of assgn p in
-      if check then
-        if not (RealQuantElim.sat [(poly, sgn)]) then Empty else
-          if RealQuantElim.sat [(poly, SignTable.neg_sign_op sgn)] then
-            Real [[(poly, sgn)]]
-          else Any
-      else Real [[(poly, sgn)]]
+    | [] -> (
+      try check_sign_op (crude_val assgn p) sgn with Not_found ->
+        let poly = poly_of assgn p in
+        if check then
+          if not (RealQuantElim.sat [(poly, sgn)]) then Empty else
+            if RealQuantElim.sat [(poly, SignTable.neg_sign_op sgn)] then
+              Real [[(poly, sgn)]]
+            else Any
+        else Real [[(poly, sgn)]]
+    )
     | v :: vs -> 
-      let append_elem_asg acc e =
-        let asg = process_vars ((v, e)::assgn) vs in
-        if asg = Empty then acc else (e, asg) :: acc in
-      let asg_list = List.fold_left append_elem_asg [] (slist elems) in
-      if asg_list = [] then Empty else
-        FO (var_str v, List.rev asg_list) in
+      try
+        let eq = if vs = [] && sgn = EQZero then crude_eq [v] assgn p else
+            raise Not_found in
+        let eq = FormulaOps.simplify_re eq in
+        let rec calc rhs = function
+          | Plus (Const x, f) -> calc (rhs -.x) f
+          | Times (Const x, f) when x = 0. -> if rhs = 0. then Any else Empty
+          | Times (Const x, f) -> calc (rhs /. x) f
+          | Fun (fn, v) -> (
+            match Structure.elems_with_val model fn rhs with
+              | [] -> Empty
+              | [e] -> FO (var_str v, [(e, Any)])
+              | elst -> let els = Aux.unique_sorted elst in
+                        let asg = List.map (fun e -> (e, Any)) els in
+                        FO (var_str v, asg)
+          )
+          | _ -> raise Not_found in
+        let res = calc 0. eq in
+        LOG 1 "%s calc: %s" (Formula.real_str eq) (AssignmentSet.str res);
+        res
+      with Not_found ->
+        let append_elem_asg acc e =
+          let asg = process_vars ((v, e)::assgn) vs in
+          if asg = Empty then acc else (e, asg) :: acc in
+        let asg_list = List.fold_left append_elem_asg [] (slist elems) in
+        if asg_list = [] then Empty else
+          FO (var_str v, List.rev asg_list) in
   process_vars [] (List.sort cmp_vars (fo_vars_real p))
 
 let eval_counter = ref 0
@@ -400,7 +448,9 @@
 let so_to_qbf struc psi =
   let assoc_or_zero asgn x = try List.assoc x asgn with Not_found -> 0 in
   let ids, rev_ids, free_id = Hashtbl.create 7, Hashtbl.create 7, ref 0 in
-  let elems = Structure.elements struc in
+  let elems, dict = Structure.elements struc, ref (Hashtbl.create 7) in
+  let get_dict v = try Hashtbl.find !dict v with Not_found -> [] in
+  let add_dict v x = Hashtbl.replace !dict v (x :: (get_dict v)) in
   let get_id x = try Hashtbl.find ids x with Not_found ->
     (Hashtbl.add ids x (!free_id +1); 
      Hashtbl.add rev_ids (!free_id +1) x; 
@@ -418,72 +468,62 @@
   (* Reduce the Evaluation Problem of SO formulae to QBF *)
   let rec so_to_qbf_rec asgn  = function
     | SO (rel, args) ->
-      let v = (compute_id (var_str rel) args asgn) in		 
-      (QVar v, [(var_str rel, v)])
+      let v = (compute_id (var_str rel) args asgn) in
+      add_dict (var_str rel) v;
+      QVar v
     | Rel (rel, va) -> 
       let args = Array.map (assoc_or_zero asgn) va in
-      if (Structure.check_rel struc rel args) then (QAnd [], []) 
-      else (QOr [], [])
-    | Eq (var1, var2) -> 
-      if assoc_or_zero asgn var1 = assoc_or_zero asgn var2 then
-        (QAnd [], []) 
-      else (QOr [], [])
+      if (Structure.check_rel struc rel args) then QAnd [] else QOr []
+    | Eq (v1, v2) -> 
+      if assoc_or_zero asgn v1 = assoc_or_zero asgn v2 then QAnd [] else QOr []
     | And phil ->
-      let resl = (List.rev_map (fun phi -> (so_to_qbf_rec asgn phi)) phil) in
-      let qphil = (Aux.unique_sorted (List.rev_map (fst) resl)) in
-      let dictl = List.fold_left (fun a (_,l) -> List.rev_append l a) [] resl in
-      (try (List.find (fun x -> x = QOr []) qphil, []) 
-       with Not_found -> (make_conj qphil, dictl) )
+      (* let cur_dict = Hashtbl.copy !dict in *)
+      let resl = List.rev_map (so_to_qbf_rec asgn) phil in
+      if List.exists (fun x -> x = QOr []) resl then (
+        (* dict := cur_dict; *) QOr []
+      ) else make_conj resl
     | Or phil ->
-      let resl = (List.rev_map (fun phi -> (so_to_qbf_rec asgn phi)) p...
 
[truncated message content]