[Toss-devel-svn] SF.net SVN: toss:[1742] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2012-07-05 00:25:45
|
Revision: 1742 http://toss.svn.sourceforge.net/toss/?rev=1742&view=rev Author: lukaszkaiser Date: 2012-07-05 00:25:38 +0000 (Thu, 05 Jul 2012) Log Message: ----------- Work on the structure explorer interface and making stuff tail-recursive in BoolFormula and Solver. Modified Paths: -------------- trunk/Toss/Client/Drawing.ml trunk/Toss/Client/Drawing.mli trunk/Toss/Client/DrawingTest.ml trunk/Toss/Client/JsEval.ml trunk/Toss/Client/Style.css trunk/Toss/Client/eval.html trunk/Toss/Formula/BoolFormula.ml trunk/Toss/README trunk/Toss/Solver/Solver.ml trunk/Toss/Solver/SolverTest.ml trunk/Toss/www/contact.xml trunk/Toss/www/index.xml Modified: trunk/Toss/Client/Drawing.ml =================================================================== --- trunk/Toss/Client/Drawing.ml 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Client/Drawing.ml 2012-07-05 00:25:38 UTC (rev 1742) @@ -34,16 +34,19 @@ { x = q.x *. cosa -. q.y *. sina ; y = q.x *. sina +. q.y *. cosa } +: start (* Colors in RBGA format. *) -type color = { red: int; blue: int; green: int; alpha: int } +type color = { red: int; blue: int; green: int; opacity: float } -let defaultCFill = { red=255 ; green = 228 ; blue = 170 ; alpha = 0 } -let defaultCStroke = { red=38 ; green = 3 ; blue = 20 ; alpha = 0 } -let defaultCRed = {red=242 ; green=92 ; blue=5 ; alpha = 0 } -let defaultCGreen = {red=62 ; green=89 ; blue=24 ; alpha = 0 } -let defaultCBlue = {red=165 ; green=175 ; blue=170 ; alpha = 0 } +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 defaultCGreen = {red=62 ; green=89 ; blue=24 ; opacity = 1. } +let defaultCBlue = {red=165 ; green=175 ; blue=170 ; opacity = 1. } -let color_to_hex c = - Printf.sprintf "%s%.2x%.2x%.2x" "#" c.red c.green c.blue +let color_to_str c = + let op = string_of_float c.opacity in + let l = String.length op - 1 in + let op = if op.[l] = '.' then String.sub op 0 l else op in + Printf.sprintf "rgba(%i, %i, %i, %s)" c.red c.green c.blue op (* Various shapes. *) type shape = @@ -207,8 +210,8 @@ Aux.concat_map (fun a -> [Circle (pos a.(0), {x=10.; y=10.}, col)]) elems else if arity = 2 then let tuples = Structure.Tuples.elements (Structure.rel_graph rel struc) in - Aux.concat_map (fun a -> - arrow defaultCStroke (pos_draw a.(0)) (pos_draw a.(1))) tuples + let c = if rel.[0] = '|' then defaultCRed else defaultCStroke in + Aux.concat_map (fun a -> arrow c (pos_draw a.(0)) (pos_draw a.(1))) tuples else [] in elem_drawings @ (Aux.concat_map draw_rel (Structure.rel_signature struc)) @@ -216,7 +219,7 @@ (* Compile the shape to a JavaScript program drawing the shape on 'ctx'. *) let shape_to_canvas = function | Circle (p, r, col) -> - let fill = "ctx.fillStyle = \""^(color_to_hex col)^"\"; ctx.fill();" in + 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(); " @@ -228,7 +231,7 @@ | 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_hex col)^"\"; ctx.stroke();" in + let stroke= "ctx.strokeStyle = \""^(color_to_str col)^"\"; ctx.stroke();" in "ctx.beginPath(); " ^ fs ^ ts ^ stroke ^ " ctx.closePath(); " let shapes_to_canvas l = Modified: trunk/Toss/Client/Drawing.mli =================================================================== --- trunk/Toss/Client/Drawing.mli 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Client/Drawing.mli 2012-07-05 00:25:38 UTC (rev 1742) @@ -25,8 +25,15 @@ val rotate : point -> float -> point -> point (** Colors in RBGA format. *) -type color = { red: int; blue: int; green: int; alpha: int } +type color = { red: int; blue: int; green: int; opacity: float } +(** Default filling color. *) +val defaultCFill : color + +(** Default stroke color. *) +val defaultCStroke : color + + (** Shapes. *) type shape = | Circle of point * point * color (** circle, given middle and radiuses *) Modified: trunk/Toss/Client/DrawingTest.ml =================================================================== --- trunk/Toss/Client/DrawingTest.ml 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Client/DrawingTest.ml 2012-07-05 00:25:38 UTC (rev 1742) @@ -8,6 +8,8 @@ let str p = Printf.sprintf "(%F, %F)" p.x p.y in assert_equal ~printer:(fun l -> String.concat ", " (List.map str l)) pl ql +let circ p q = Circle (p, q, defaultCFill) + let tests = "Drawing" >::: [ "change coords" >:: (fun () -> @@ -20,10 +22,10 @@ "crossings" >:: (fun () -> let z, o, hsq2 = {x=0.;y=0.}, {x=1.;y=1.}, (sqrt 2.) *. 0.5 in - eq_point_list [o*!hsq2; o *! (-1.*.hsq2)] (crossings z o [Circle (z, o)]); - eq_point_list [{x=1.;y=0.}] (crossings z {x=1.;y=0.} [Circle (o, o)]); + eq_point_list [o*!hsq2; o *! (-1.*.hsq2)] (crossings z o [circ z o]); + eq_point_list [{x=1.;y=0.}] (crossings z {x=1.;y=0.} [circ o o]); eq_point_list [{x = 2. ; y = 0.}; {x = -2. ; y = 0.}] - (crossings z {x=1.; y=0.} [Circle (z, o *! 2.)]); + (crossings z {x=1.; y=0.} [circ z (o *! 2.)]); ); ] Modified: trunk/Toss/Client/JsEval.ml =================================================================== --- trunk/Toss/Client/JsEval.ml 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Client/JsEval.ml 2012-07-05 00:25:38 UTC (rev 1742) @@ -30,11 +30,11 @@ (* Parse a formula. *) let formula_of_string s = FormulaParser.parse_formula Lexer.lex - (Lexing.from_string (Aux.normalize_spaces s)) + (Lexing.from_string (Aux.strip_spaces s)) (* Parse a structure. *) let structure_of_string s = - let str = "START " ^ (Aux.normalize_spaces s) in + 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" @@ -42,15 +42,33 @@ (* Drawing the structure. *) let draw_struc_js so_s struc_s = - let st, so = structure_of_string (Js.to_string struc_s), Js.to_string so_s in - let st, so_res = if Aux.strip_spaces so = "" then (st, "none") else - let so_phi = formula_of_string so in - let st, res = Solver.find_so st so_phi in - if res then st, "true" else st, "false" in - let st_c = Drawing.add_coords 1000. 1000. 50. 50. 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 |] + let err msg = + let js_msg = Js.string ("put_msg('" ^ msg ^ "', 5000);") in + Js.array [|js_msg; Js.string "Error"|] 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 + 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 + 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 + 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 + 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 |] + with x -> error_msg "Formula" x + with x -> error_msg "Structure" x let _ = set_handle "draw_struc" draw_struc_js Modified: trunk/Toss/Client/Style.css =================================================================== --- trunk/Toss/Client/Style.css 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Client/Style.css 2012-07-05 00:25:38 UTC (rev 1742) @@ -64,7 +64,7 @@ float: right; } -.obt, .boldobt, .gamebt, .ebt { +.obt, .boldobt, .gamebt, .ebt, .ebts { text-align: left; border-color: #260314; border-radius: 4px; @@ -76,7 +76,7 @@ font-family: Verdana, 'TeXGyreHerosRegular', sans; } -.obt:hover, .ebt:hover, .boldobt:hover, .gamebt:hover { +.obt:hover, .ebt:hover, .ebts:hover, .boldobt:hover, .gamebt:hover { cursor: pointer; text-decoration: underline; } @@ -86,9 +86,10 @@ font-size: 1em; } -.ebt { +.ebt, .ebts { /*font-weight: bold;*/ - border-width: 2px; + text-align: center; + border-width: 1px; } .gamebt { @@ -902,6 +903,7 @@ position: relative; left: 2em; top: 5em; + width: 30em; } #board { @@ -929,6 +931,7 @@ background-color: #400827; padding: 1em; border: 1px solid #260314; + z-index: 100; } #opening { @@ -1006,8 +1009,8 @@ } #canvas { - width: 28em; - height: 28em; + width: 29em; + height: 29em; border: 2px solid #260314; } Modified: trunk/Toss/Client/eval.html =================================================================== --- trunk/Toss/Client/eval.html 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Client/eval.html 2012-07-05 00:25:38 UTC (rev 1742) @@ -53,8 +53,8 @@ var pos = document.getElementById ("positions").value; var elemsF = document.getElementById ("no-elems-start").value; var elemsT = document.getElementById ("no-elems-end").value; - var struc = "[ " + elemsF + " - " + elemsT + " | | - ] with " + - rels + " with " + pos; + var struc = "[ " + elemsF + " - " + elemsT + " | | - ] with \n" + + rels + " with \n" + pos; ASYNCH ("draw_struc", ["", struc], true, function (a) { var ctx = document.getElementById("canvas").getContext("2d"); eval (a[0]) @@ -67,12 +67,12 @@ var elemsF = document.getElementById ("no-elems-start").value; var elemsT = document.getElementById ("no-elems-end").value; var so = document.getElementById ("second-order").value; - var struc = "[ " + elemsF + " - " + elemsT + " | | - ] with " + - rels + " with " + pos; + var struc = "[ " + elemsF + " - " + elemsT + " | | - ] with \n" + + rels + " with \n" + pos; ASYNCH ("draw_struc", [so, struc], true, function (a) { var ctx = document.getElementById("canvas").getContext("2d"); eval (a[0]); - alert (a[1]) + if (a[1] !== "Error") { put_msg (a[1], 2000) } }) } @@ -200,6 +200,14 @@ draw_it (); } +function example_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" + + ") ) ∧ ∀ x ∃ y |M(x, y)"; + find_draw_it (); +} + function example_2col () { document.getElementById ("second-order").value = "∀ x,y ( (|R(x) ∨ |G(x)) ∧ ( E(x,y) → " + @@ -254,7 +262,7 @@ draw_it (); } -function save () { +function save_struc () { var name = document.getElementById ("struc-name").value; var elems1 = document.getElementById ("no-elems-start").value; var elems2 = document.getElementById ("no-elems-end").value; @@ -264,10 +272,17 @@ localStorage["TRelStrucExplEl2"+name] = elems2; localStorage["TRelStrucExplRel"+name] = rels; localStorage["TRelStrucExplPos"+name] = pos; - list_stored (); + list_stored_struc (); } -function load (name) { +function save_so () { + var name = document.getElementById ("so-name").value; + var phi = document.getElementById ("second-order").value; + localStorage["TRelStrucExplSOF"+name] = phi; + list_stored_so (); +} + +function load_struc (name) { document.getElementById ("struc-name").value = name; document.getElementById ("no-elems-start").value = localStorage["TRelStrucExplEl1"+name]; @@ -280,7 +295,14 @@ draw_it (); } -function list_stored () { +function load_so (name) { + document.getElementById ("so-name").value = name; + document.getElementById ("second-order").value = + localStorage["TRelStrucExplSOF"+name]; + find_draw_it (); +} + +function list_stored_struc () { var saved = document.getElementById("saved-strucs"); while (saved.childNodes.length > 0) { saved.removeChild(saved.firstChild); } for (var i=0; i < localStorage.length; i++) { @@ -288,55 +310,109 @@ if (k.substring (0, 16) === "TRelStrucExplEl1") { var n = k.substring (16, k.length); var li = document.createElement('li'); - li.innerHTML = '<button class="obt" onclick="load('+ "'"+ n +"'" +')">' + - n +'</button> (<button class="obt" onclick="del_saved('+ "'"+ n + + li.innerHTML ='<button class="obt" onclick="load_struc('+"'"+ n +"'"+')">' + + n +'</button> (<button class="obt" onclick="del_struc('+ "'"+ n + "'" +')" title="Delete this structure.">-</button>)'; saved.appendChild (li); } } } -function del_saved (name) { +function list_stored_so () { + var saved = document.getElementById("saved-so"); + while (saved.childNodes.length > 0) { saved.removeChild(saved.firstChild); } + for (var i=0; i < localStorage.length; i++) { + var k = localStorage.key(i); + if (k.substring (0, 16) === "TRelStrucExplSOF") { + 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="obt" onclick="del_so('+ "'"+ n + + "'" +')" title="Delete this formula.">-</button>)'; + saved.appendChild (li); + } + } +} + +function list_stored () { + list_stored_struc (); + list_stored_so (); +} + +function del_so (name) { + localStorage.removeItem("TRelStrucExplSOF"+name); + list_stored_so (); +} + +function del_struc (name) { localStorage.removeItem("TRelStrucExplEl1"+name); localStorage.removeItem("TRelStrucExplEl2"+name); localStorage.removeItem("TRelStrucExplRel"+name); localStorage.removeItem("TRelStrucExplPos"+name); - list_stored (); + list_stored_struc (); } -function toggle_edit () { +function toggle_edit_view () { var bt = document.getElementById("editbt"); if (bt.innerHTML == "Edit") { document.getElementById('edit').style.display = 'block'; - document.getElementById('board-left').style.left = '38em'; - bt.innerHTML = "Hide Edit"; + document.getElementById('board-left').style.display = 'none'; + bt.innerHTML = "View"; } else { document.getElementById('edit').style.display = 'none'; - document.getElementById('board-left').style.left = '2em'; + document.getElementById('board-left').style.display = 'block'; bt.innerHTML = "Edit"; } } -function toggle_view () { - var bt = document.getElementById("viewbt"); - if (bt.innerHTML == "View") { - document.getElementById('board-left').style.display = 'block'; - bt.innerHTML = "Hide View"; - } else { - document.getElementById('board-left').style.display = 'none'; - bt.innerHTML = "View"; - } -} - function adjust_to_width () { var e = document.getElementById ("edit"); var em_size = document.defaultView.getComputedStyle(e,null).getPropertyValue('font-size'); var em_size_int = parseInt (em_size.substring (0, em_size.length - 2)); - if (window.innerWidth > 80 * em_size_int) { // enough space for edit - toggle_edit () + if (window.innerWidth > 80 * em_size_int) { // enough space for view + document.getElementById('board-left').style.left = '35em'; + document.getElementById('board-left').style.display = 'block'; + document.getElementById('editbt').style.display = 'none'; } } + +function put_msg (content, time) { + document.getElementById("working").innerHTML = content; + document.getElementById ("working").style.display = "block"; + setTimeout (function () { + document.getElementById ("working").style.display = "none"; + }, time); +} + +function show_help () { + document.getElementById ("working").style.textAlign = "left"; + document.getElementById ("working").style.fontWeight = "normal"; + document.getElementById("working").innerHTML = '\ +<b>Welcome to Relational Structures Explorer</b> \ +<p><b>Relational structures</b> consist of a set of <em>elements</em> and \ +of <em>relations</em> defined by <em>formulas</em>.</p> \ +<p><b>Elements</b> are numbered. You can change their range and you can access \ +the number of the element corresponding to a variable <em>x</em> in a formula \ +by writing <em>&x</em> or <em>:nbr(x)</em>.</p> \ +<p><b>Formulas</b> are written in first-order logic. You can use relation \ +symbols, Boolean combinations and quantifiers. Additionally, you can use \ +arithmetic operations (+-*/^) on element numbers and element positions.</p> \ +<p><b>Positions</b> of elements are determined by their <em>x</em> and \ +<em>y</em> coordinates. Define and access them as in <b>:x(a)</b> and \ +<b>:y(a)</b>. You can again use arithmetic operations and also conditionals \ +on formulas, written <b>:(formula)</b>.</p> \ +<p><b>Relation Finder</b>, placed at the bottom, automatically finds relations \ +that satisfy the given property. Use <b>|</b> in front of the relation symbol \ +to be found, as in <b>|R(x)</b>.</p> \ +'; + document.getElementById ("working").style.display = "block"; + setTimeout (function () { + document.getElementById ("working").style.display = "none"; + document.getElementById ("working").style.textAlign = "center"; + document.getElementById ("working").style.fontWeight = "bold"; + }, 20000); +} //--> </script> </head> @@ -353,12 +429,12 @@ <span style="position: relative; left: 2em; top: 0.5em; font-size: 1.2em"> Relational Structures Explorer</span> <span id="toprighttab" style="display: block;"> - <button class="obt" id="editbt" onclick="toggle_edit()">Edit</button> - <button class="obt" id="viewbt" onclick="toggle_view()">Hide View</button> + <button class="obt" id="editbt" onclick="toggle_edit_view()">View</button> + <button class="obt" id="editbt" onclick="show_help()">Help</button> </span> </div> -<div id="board-left"> +<div id="board-left" style="display: none;"> <canvas id="canvas" height="1100" width="1100" onmouseup="mouseup_handle(event)" onmousedown="mousedown_handle(event)" @@ -370,72 +446,118 @@ </canvas> </div> -<div id="edit" style="position: absolute; top: 4em; left: 2em; display: none"> +<div id="working" style="display: none; width: 30em;"></div> +<div id="edit" style="position: absolute; top: 4em; left: 2em;"> + <p>Name - <input id="struc-name" type="text" size="20" value="MyStructure1" - style="width: 10em"></input> - <button class="ebt" onclick="save()">Save</button> + <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> </p> <p>Elements <input id="no-elems-start" type="text" size="2" value="1" - style="width: 2em"></input> — + style="width: 4em"></input> — <input id="no-elems-end" type="text" size="4" value="15" - style="width: 2em"></input> - <button class="ebt" onclick="add_elem()">+</button> - <button class="ebt" onclick="del_elem()">-</button> + style="width: 4em"></input> + <span style="position: absolute; right: 2px;"> + <button class="ebt" style="width: 2em;" title="Remove last element." + onclick="del_elem()">-</button><button title="Add one element." + style="width: 2em;" class="ebt" onclick="add_elem()">+</button> + </span> </p> -<p>Relations - <button class="ebt" title="Conjunction. You can also write 'and' or '&'." - onclick="add_field('relations', '∧')">∧</button> - <button class="ebt" title="Disjunction. You can also write 'or' or '|'." - onclick="add_field('relations', '∨')">∨</button> - <button class="ebt" title="Negation. You can also write 'not'." - onclick="add_field('relations', '¬')">¬</button> - <button class="ebt" title="Implication. You can also write '->'." - onclick="add_field('relations', '→')">→</button> - <button title="Existential Quantifier. You can also write 'ex' or '\E'." - class="ebt" onclick="add_field('relations', '∃')">∃</button> - <button title="Universal Quantifier. You can also write 'all' or '\A'." - class="ebt" onclick="add_field('relations', '∀')">∀</button> - <button class="ebt" onclick="draw_it()">Redraw</button> +<p>Relations + <span style="position: absolute; right: 2px;"> + <button class="ebts" title="Not equal. You can also write '<>' or '!='." + onclick="add_field('relations', '≠')">≠</button><button + class="ebts" title="Less or equal. You can also write '=<'." + onclick="add_field('relations', '≤')">≤</button><button + class="ebts" title="Conjunction. You can also write 'and' or '&'." + 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'." + onclick="add_field('relations', '¬')">¬</button><button + class="ebts" title="Implication. You can also write '->'." + onclick="add_field('relations', '→')">→</button><button + title="Existential Quantifier. You can also write 'ex' or '\E'." + 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> + <button class="ebt" onclick="draw_it()" style="width: 4em;" + title="Redraw current structure.">Draw</button> + </span> </p> -<textarea id="relations" rows="3" cols="70"> +<textarea id="relations" rows="3" cols="60"> E(x, y) = (&y = &x + 1) ∨ (&x=15 ∧ &y=1) </textarea> -<p>Positions - <button class="ebt" onclick="add_field('positions', '+')">+</button> - <button class="ebt" onclick="add_field('positions', '-')">-</button> - <button class="ebt" onclick="add_field('positions', '·')">·</button> - <button class="ebt" onclick="add_field('positions', '/')">/</button> - <button class="ebt" onclick="add_field('positions', '^')">^</button> - <button class="ebt" onclick="draw_it()">Redraw</button> +<p>Positions + <span style="position: absolute; right: 2px;"> + <button class="ebts" title="Not equal. You can also write '<>' or '!='." + onclick="add_field('positions', '≠')">≠</button><button + class="ebts" title="Less or equal. You can also write '=<'." + onclick="add_field('positions', '≤')">≤</button><button + class="ebts" title="Conjunction. You can also write 'and' or '&'." + onclick="add_field('positions', '∧')">∧</button><button + class="ebts" title="Disjunction. You can also write 'or' or '|'." + onclick="add_field('positions', '∨')">∨</button><button + class="ebts" title="Negation. You can also write 'not'." + onclick="add_field('positions', '¬')">¬</button><button + class="ebts" title="Implication. You can also write '->'." + onclick="add_field('positions', '→')">→</button><button + title="Existential Quantifier. You can also write 'ex' or '\E'." + 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> + <button class="ebt" onclick="draw_it()" style="width: 4em;" + title="Redraw current structure.">Draw</button> + </span> </p> - -<textarea id="positions" rows="3" cols="70"> +<textarea id="positions" rows="3" cols="60"> :x(a) = &a; :y(a) = &a · (10 - &a) / 10 </textarea> -<p>Second-Order Finder - <button class="ebt" title="Conjunction. You can also write 'and' or '&'." - onclick="add_field('second-order', '∧')">∧</button> - <button class="ebt" title="Disjunction. You can also write 'or' or '|'." - onclick="add_field('second-order', '∨')">∨</button> - <button class="ebt" title="Negation. You can also write 'not'." - onclick="add_field('second-order', '¬')">¬</button> - <button class="ebt" title="Implication. You can also write '->'." - onclick="add_field('second-order', '→')">→</button> - <button title="Existential Quantifier. You can also write 'ex' or '\E'." - class="ebt" onclick="add_field('second-order', '∃')">∃</button> - <button title="Universal Quantifier. You can also write 'all' or '\A'." - class="ebt" onclick="add_field('second-order', '∀')">∀</button> - <button class="ebt" onclick="find_draw_it()">Find</button> + +<p style="width:100%; border-top: 1px solid; padding-top: 1em;"> + Formula Name + <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> -<textarea id="second-order" rows="3" cols="70"> + +<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="Less or equal. You can also write '=<'." + 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> + <button class="ebt" onclick="find_draw_it()" style="width: 4em;" + title="Find relations that satisfy the formula.">Find</button> + </span> +</p> +<textarea id="second-order" rows="3" cols="60"> </textarea> </div> @@ -454,10 +576,16 @@ <li><button class="obt" onclick="example_heart()">Heart Drawing</button></li> </ul> -<p>Second-Order Formulas</p> +<p style="border-top: 1px solid; padding-top: 1em">Your Formulas</p> +<ul id="saved-so" style="list-style: square; margin-left: -1.5em"> +<li>Nothing here yet</li> +</ul> + +<p>Examples</p> <ul style="list-style: square; margin-left: -1.5em"> <li><button class="obt" onclick="example_2col()">2-coloring</button></li> <li><button class="obt" onclick="example_3col()">3-coloring</button></li> +<li><button class="obt" onclick="example_matching()">Matching</button></li> </ul> </div> Modified: trunk/Toss/Formula/BoolFormula.ml =================================================================== --- trunk/Toss/Formula/BoolFormula.ml 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Formula/BoolFormula.ml 2012-07-05 00:25:38 UTC (rev 1742) @@ -626,11 +626,11 @@ | _ -> raise (FormulaError "Clauses must not contain non-literals!") in let list_of_clause = function | BVar v -> [v] - | BOr (bflist) -> List.map int_of_literal bflist + | BOr (bflist) -> List.rev_map int_of_literal bflist | _ -> raise (FormulaError "This is not a clause!") in match phi with | BVar v -> [[v]] - | BAnd (bflist) -> List.map list_of_clause bflist + | BAnd (bflist) -> List.rev_map list_of_clause bflist | _ -> raise (FormulaError "This is not a CNF!") Modified: trunk/Toss/README =================================================================== --- trunk/Toss/README 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/README 2012-07-05 00:25:38 UTC (rev 1742) @@ -18,7 +18,8 @@ * AUTHORS The current version of Toss is developed by -- Łukasz Kaiser (ka...@li...) +- Łukasz Kaiser (luk...@gm...) +- Faried Abu Zaid - Łukasz Stafiniak Many other friends helped us with discussion and code at some point. Modified: trunk/Toss/Solver/Solver.ml =================================================================== --- trunk/Toss/Solver/Solver.ml 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Solver/Solver.ml 2012-07-05 00:25:38 UTC (rev 1742) @@ -429,17 +429,17 @@ (QAnd [], []) else (QOr [], []) | And phil -> - let resl = (List.map (fun phi -> (so_to_qbf_rec asgn phi)) phil) in - let qphil = (Aux.unique_sorted (List.map (fst) resl)) in - let dictl = (List.map snd resl) in + 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, List.concat dictl) ) + with Not_found -> (make_conj qphil, dictl) ) | Or phil -> - let resl = (List.map (fun phi -> (so_to_qbf_rec asgn phi)) phil) in - let qphil = (Aux.unique_sorted (List.map (fst) resl)) in - let dictl = (List.map (snd) resl) in + 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 = QAnd []) qphil, []) - with Not_found -> (make_disj qphil, List.concat dictl) + with Not_found -> (make_disj qphil, dictl) ) | Not phi -> let (qphi, dict) = so_to_qbf_rec asgn phi in @@ -448,12 +448,12 @@ else (QNot qphi, dict) | Ex ([], phi) -> so_to_qbf_rec asgn phi | Ex (var::tl, phi) when is_fo var -> - let asgn_list = List.map (fun x -> (Formula.to_fo var, x)::asgn) elems in - let res = List.map (fun x -> so_to_qbf_rec x (Ex (tl, phi))) asgn_list in - let (qphil, dictl) = - ((Aux.unique_sorted (List.map (fst) res)), List.map (snd) res) in + let asgn_l = List.rev_map (fun x -> (Formula.to_fo var, x)::asgn) elems in + let res = List.rev_map (fun x -> so_to_qbf_rec x (Ex (tl, phi))) asgn_l in + let qphil = Aux.unique_sorted (List.rev_map fst res) in + let dictl = List.fold_left (fun a (_,l) -> List.rev_append l a) [] res in (try (List.find (fun x -> x = QAnd []) qphil, []) - with Not_found ->(make_disj qphil, List.concat dictl) + with Not_found -> (make_disj qphil, dictl) ) | Ex (var::tl, phi) when is_so var -> let (qbf_phi, dict_phi) = (so_to_qbf_rec asgn (Ex (tl, phi))) in @@ -466,12 +466,12 @@ | Ex (var::tl, phi) -> (*stub*) failwith "not implemented yet (so_qbf_Ex)" | All ([], phi) -> so_to_qbf_rec asgn phi | All (var::tl, phi) when is_fo var -> - let asgn_list = List.map (fun x -> (Formula.to_fo var, x)::asgn) elems in - let res = List.map (fun x -> so_to_qbf_rec x (All (tl, phi))) asgn_list in - let (qphil, dictl) = - ((Aux.unique_sorted (List.map (fst) res)), List.map (snd) res) in + let asgn_l = List.rev_map (fun x -> (Formula.to_fo var, x)::asgn) elems in + let res = List.rev_map (fun x ->so_to_qbf_rec x (All (tl, phi))) asgn_l in + let qphil = Aux.unique_sorted (List.rev_map fst res) in + let dictl = List.fold_left (fun a (_,l) -> List.rev_append l a) [] res in (try (List.find (fun x -> x = (QOr [])) qphil, []) - with Not_found -> (make_conj qphil, List.concat dictl) + with Not_found -> (make_conj qphil, dictl) ) | All (var::tl, phi) when is_so var -> let (qbf_phi, dict_phi) = so_to_qbf_rec asgn (All (tl, phi)) in Modified: trunk/Toss/Solver/SolverTest.ml =================================================================== --- trunk/Toss/Solver/SolverTest.ml 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/Solver/SolverTest.ml 2012-07-05 00:25:38 UTC (rev 1742) @@ -179,17 +179,13 @@ (BoolFormula.qbf_str ~names:names_tbl qbf_res) in qbf_str_eq "[ a, b | T { a } | ]" "ex |R all x, y (T(x) or |R (x, y))" - "(ex R.2.1, R.2.2 (R.2.1 and R.2.2))"; + "(ex R.2.2, R.2.1 (R.2.2 and R.2.1))"; qbf_str_eq "[ a, b | T { a } | ]" "all |Q all x, y (T(x) or Q(y) or (x = y))" "false"; qbf_str_eq "[ a, b, c | E { (a,b); (b,c); (c,a) } | ]" ("ex |R, |G all x, y ( (|R(x) or |G(x)) and (" ^ " E(x,y) -> not ( (|R(x) and |R(y)) " ^ " or (|G(x) and |G(y)))))") - ("(ex R.1, R.2, R.3 (ex G.1, G.2, G.3 ((R.1 or G.1) and (R.1 or G.1) " ^ - "and (not ((R.1 and R.2) or (G.1 and G.2))) and (R.2 or G.2) and " ^ - "(R.2 or G.2) and (not ((R.2 and R.3) or (G.2 and G.3))) and " ^ - "(R.3 or G.3) and (R.3 or G.3) and " ^ - "(not ((R.1 and R.3) or (G.1 and G.3))))))"); + ("(ex R.3, R.2, R.1 (ex G.3, G.2, G.1 ((R.3 or G.3) and (R.3 or G.3) and (not ((R.3 and R.1) or (G.3 and G.1))) and (R.2 or G.2) and (R.2 or G.2) and (not ((R.3 and R.2) or (G.3 and G.2))) and (R.1 or G.1) and (R.1 or G.1) and (not ((R.2 and R.1) or (G.2 and G.1))))))"); let col3 = ("all x, y ( (|R(x) or |G(x) or |B(x)) and (" ^ @@ -198,7 +194,7 @@ let triangle = "[ | E { (a, b); (b, c); (c, a) } | ] " in let (col3,triangle) = (formula_of_string col3,struc_of_string triangle) in assert_equal ~printer:(fun x -> x) - "[a, b, c | E {(a, b); (b, c); (c, a)}; |B (c); |G (b); |R (a) | ]" + "[a, b, c | E {(a, b); (b, c); (c, a)}; |B (a); |G (b); |R (c) | ]" (Structure.str (fst (Solver.find_so triangle col3))); ); Modified: trunk/Toss/www/contact.xml =================================================================== --- trunk/Toss/www/contact.xml 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/www/contact.xml 2012-07-05 00:25:38 UTC (rev 1742) @@ -80,9 +80,10 @@ <section title="Team"> <par>Toss originates from our work in the <a href="http://www.algosyn.rwth-aachen.de/">AlgoSyn</a> research group. - Many people contributed, here we name just a few. Current leaders:</par> + Many people contributed, here we name just a few. Currently working:</par> <itemize> <item>Łukasz Kaiser (<mailto address="luk...@gm..."/>)</item> + <item>Faried Abu Zaid</item> <item>Łukasz Stafiniak</item> </itemize> <par>Friends who helped us a lot with discussion and code.</par> Modified: trunk/Toss/www/index.xml =================================================================== --- trunk/Toss/www/index.xml 2012-07-03 23:55:21 UTC (rev 1741) +++ trunk/Toss/www/index.xml 2012-07-05 00:25:38 UTC (rev 1742) @@ -35,14 +35,22 @@ <section title="News"> <itemize> + <newsitem date="04/07/12"> + First version of Relational Structures Explorer with SO finding</newsitem> + <newsitem date="27/06/12"> + Second-order (SO) evaluation by reduction to QBF</newsitem> + <newsitem date="25/06/12"> + Full support for Unicode in formulas</newsitem> <newsitem date="07/06/12"> Switching to a new ODE solver which uses the Cash-Karp method</newsitem> <newsitem date="02/06/12"> - Starting work on an interface for structures and formula evaluation</newsitem> - <newsitem date="27/05/12"> - First structures defined using the term rewriting system syntax</newsitem> - <newsitem date="24/05/12"> - Code for Term functions cleaned up and made JS compatible</newsitem> + Starting work on an interface for structures and formula + evaluation</newsitem> + <oldnewsitem date="27/05/12"> + First structures defined using the term rewriting system + syntax</oldnewsitem> + <oldnewsitem date="24/05/12"> + Code for Term functions cleaned up and made JS compatible</oldnewsitem> <oldnewsitem date="13/05/12"> Toss release 0.8 with full JS compatibility with dynamics</oldnewsitem> <oldnewsitem date="04/05/12"> This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |