[Toss-devel-svn] SF.net SVN: toss:[1744] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2012-07-10 22:44:55
|
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.">×</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.">×</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> \ -<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()">×</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>⇩</b> button in the respective section to \ + save a structure or a formula, and later the <b>×</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')">«</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')">«</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')"> </button><button - class="ebts" style="background-color: #a5afaa;"; - onclick="add_field('colors', '#a5afaa')"> </button><button + <span style="position: absolute; right: 1px;"> + <button class="ebts" style="background-color: #a5afaa;"; + onclick="add_field('colors', '#a5afaa')"> </button><button + class="ebts" style="background-color: #00364c;"; + onclick="add_field('colors', '#00364c')"> </button><button class="ebts" style="background-color: #93a605;"; onclick="add_field('colors', '#93a605')"> </button><button class="ebts" style="background-color: #3e5916;"; onclick="add_field('colors', '#3e5916')"> </button><button - class="ebts" style="background-color: #f28705;"; - onclick="add_field('colors', '#f28705')"> </button><button - style="background-color: #f25c05;"; class="ebts" - onclick="add_field('colors', '#f25c05')"> </button><button + class="ebts" style="background-color: #f25c05;"; + onclick="add_field('colors', '#f25c05')"> </button><button + style="background-color: #e82a33;"; class="ebts" + onclick="add_field('colors', '#e82a33')"> </button><button style="background-color: #260314;"; class="ebts" onclick="add_field('colors', '#260314')"> </button> - <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')">«</button> + Evaluate Formulas + <span style="position: absolute; right: 1px;"> + <button class="ebt" onclick="save_so()" title="Save current formula." + style="width: 2em;">⇩</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 + <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')">«</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()">⇩</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 <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 - <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> — - <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> - <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> - <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 - <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> - <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')">«</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> +<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> +<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] |