[Toss-devel-svn] SF.net SVN: toss:[1682] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1682] trunk/Toss
|
From: <luk...@us...> - 2012-03-05 23:24:50
|
Revision: 1682
http://toss.svn.sourceforge.net/toss/?rev=1682&view=rev
Author: lukaszkaiser
Date: 2012-03-05 23:24:41 +0000 (Mon, 05 Mar 2012)
Log Message:
-----------
Moving to LOG for debug-logging.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/Arena.mli
trunk/Toss/Arena/ArenaTest.ml
trunk/Toss/Arena/ContinuousRule.ml
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Arena/DiscreteRule.mli
trunk/Toss/Arena/DiscreteRuleTest.ml
trunk/Toss/Formula/AuxIO.ml
trunk/Toss/Formula/AuxIO.mli
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/BoolFormula.mli
trunk/Toss/Formula/BoolFormulaTest.ml
trunk/Toss/Formula/BoolFunction.ml
trunk/Toss/Formula/BoolFunction.mli
trunk/Toss/Formula/BoolFunctionTest.ml
trunk/Toss/Formula/FFTNF.ml
trunk/Toss/Formula/FFTNF.mli
trunk/Toss/Formula/FFTNFTest.ml
trunk/Toss/Formula/Formula.ml
trunk/Toss/Formula/FormulaMapTest.ml
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/Formula/FormulaOpsTest.ml
trunk/Toss/Formula/FormulaSubst.ml
trunk/Toss/Formula/FormulaSubst.mli
trunk/Toss/Formula/FormulaSubstTest.ml
trunk/Toss/Formula/OUnit.ml
trunk/Toss/Formula/Sat/Sat.ml
trunk/Toss/Formula/Sat/Sat.mli
trunk/Toss/Formula/Sat/SatTest.ml
trunk/Toss/GGP/GDL.ml
trunk/Toss/GGP/GDL.mli
trunk/Toss/GGP/GDLTest.ml
trunk/Toss/GGP/GameSimpl.ml
trunk/Toss/GGP/GameSimpl.mli
trunk/Toss/GGP/GameSimplTest.ml
trunk/Toss/GGP/TranslateFormula.ml
trunk/Toss/GGP/TranslateFormula.mli
trunk/Toss/GGP/TranslateGame.ml
trunk/Toss/GGP/TranslateGame.mli
trunk/Toss/GGP/TranslateGameTest.ml
trunk/Toss/Learn/Distinguish.ml
trunk/Toss/Learn/Distinguish.mli
trunk/Toss/Learn/DistinguishTest.ml
trunk/Toss/Learn/LearnGame.ml
trunk/Toss/Learn/LearnGame.mli
trunk/Toss/Learn/LearnGameTest.ml
trunk/Toss/Play/GameTree.ml
trunk/Toss/Play/GameTree.mli
trunk/Toss/Play/GameTreeTest.ml
trunk/Toss/Play/Heuristic.ml
trunk/Toss/Play/Heuristic.mli
trunk/Toss/Play/HeuristicTest.ml
trunk/Toss/Play/Play.ml
trunk/Toss/Play/Play.mli
trunk/Toss/Play/PlayTest.ml
trunk/Toss/Server/Server.ml
trunk/Toss/Solver/Assignments.ml
trunk/Toss/Solver/Assignments.mli
trunk/Toss/Solver/Class.ml
trunk/Toss/Solver/Class.mli
trunk/Toss/Solver/ClassTest.ml
trunk/Toss/Solver/RealQuantElim/RealQuantElim.ml
trunk/Toss/Solver/RealQuantElim/RealQuantElimTest.ml
trunk/Toss/Solver/RealQuantElim/SignTable.ml
trunk/Toss/Solver/RealQuantElim/SignTable.mli
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
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Arena/Arena.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,11 +1,10 @@
(* Represent the game arena and operate on it. *)
open Printf
-let debug_level = ref 0
-
(* The label's time interval defaults to this point. *)
let cDEFAULT_TIMESTEP = 0.1
+
(* ------------------------ BASIC TYPE DEFINITIONS -------------------------- *)
(* A single move consists of applying a rewrite rule for a time from the
@@ -98,17 +97,11 @@
raise Not_found))
match_str
with Not_found ->
- (* {{{ log entry *)
- if !debug_level > 0 then (
- Printf.printf "matching_of_names: failed at STRUC=\n%s\nMATCH=%s\n%!"
- (Structure.str state.struc)
- (String.concat "; "
- (List.map (fun (v,e) ->v^"<-"^e) match_str))
- );
- (* }}} *)
+ LOG 1 "matching_of_names: failed at STRUC=\n%s\nMATCH=%s\n%!"
+ (Structure.str state.struc)
+ (String.concat "; " (List.map (fun (v,e) ->v^"<-"^e) match_str));
failwith ("emb_of_names: could not find " ^
- String.concat "; "
- (List.map (fun (v,e) ->v^"<-"^e) match_str))
+ String.concat "; " (List.map (fun (v,e) ->v^"<-"^e) match_str))
(* Rules with which a player with given number can move. *)
let rules_for_player player_no game =
@@ -217,12 +210,8 @@
List.map (fun (rel, (args, body)) -> rel, args, body) game.defined_rels,
gstate.struc, gstate.time, gstate.cur_loc,
game.patterns, game.data in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf "process_definition: %d old rules, %d old locs\n%!"
- (List.length old_rules) (List.length old_locs);
- );
- (* }}} *)
+ LOG 3 "process_definition: %d old rules, %d old locs\n%!"
+ (List.length old_rules) (List.length old_locs);
let rules, locations, players, defined_rels,
state, time, cur_loc, patterns, data, hist =
List.fold_left (fun (rules, locations, players, defined_rels,
@@ -261,12 +250,8 @@
state, time, cur_loc, patterns, data @ more_data, hist)
) ([], [], players, [],
state, time, cur_loc, patterns, data, []) defs in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf "process_definition: %d new rules, %d new defined rels\n%!"
- (List.length rules) (List.length defined_rels);
- );
- (* }}} *)
+ LOG 3 "process_definition: %d new rules, %d new defined rels\n%!"
+ (List.length rules) (List.length defined_rels);
let defined_rels = old_defined_rels @ List.rev defined_rels in
let def_rels_pure =
List.map (fun (rel, args, body) -> (rel, (args, body))) defined_rels in
@@ -275,19 +260,11 @@
(Array.of_list players)) in
let num_players = List.length player_names in
let signature = Structure.rel_signature state in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf "process_definition: parsing new rules...%!";
- );
- (* }}} *)
+ LOG 3 "process_definition: parsing new rules...%!";
let rules =
old_rules @ List.map (fun (name, r) ->
name, r signature def_rels_pure name) rules in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf " parsed\n%!";
- );
- (* }}} *)
+ LOG 3 " parsed\n%!";
let rules =
List.sort (fun (rn1,_) (rn2,_)->String.compare rn1 rn2) rules in
let updated_locs =
@@ -301,21 +278,13 @@
let sub_p l =
{ l with payoff = FormulaSubst.subst_rels_expr def_rels_pure l.payoff } in
i, Array.map sub_p loc in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf "process_definition: parsing locations (registering payoffs)...%!";
- );
- (* }}} *)
+ LOG 3 "process_definition: parsing locations (registering payoffs)...%!";
let locations =
List.map (fun loc -> add_def_rel (loc player_names)) locations in
let locations =
List.filter (fun (i,_) -> not (List.mem_assoc i locations))
updated_locs @ locations in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf " parsed\n%!";
- );
- (* }}} *)
+ LOG 3 " parsed";
let graph = Aux.array_from_assoc (List.rev locations) in
let pats=List.rev_map (FormulaSubst.subst_rels_expr def_rels_pure) patterns in
let apply_moves rules mvs s = List.fold_left (apply_move rules) s mvs in
Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Arena/Arena.mli 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,7 +1,5 @@
(** Represent the game arena and operate on it. *)
-val debug_level : int ref
-
(** A single move consists of applying a rewrite rule for a time from the
[time_in] interval, and parameters from the interval list. *)
type label = {
Modified: trunk/Toss/Arena/ArenaTest.ml
===================================================================
--- trunk/Toss/Arena/ArenaTest.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Arena/ArenaTest.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,54 +1,11 @@
(* Test for game arena and support functions. *)
open OUnit
-
-(*let req_of_str s =
- ArenaParser.parse_request Lexer.lex (Lexing.from_string s) *)
-
let gs_of_str s =
ArenaParser.parse_game_state Lexer.lex (Lexing.from_string s)
-(*let apply_rule gs rname match_str =
- let s = "SET RULE " ^ rname ^ " MODEL " ^ match_str ^ " 0.1" in
- snd (Arena.handle_request Arena.empty_state (req_of_str s))
-*)
let tests = "Arena" >::: [
- "adding rule" >::
- (fun () -> assert true);
-(*
- let rule_a =
- "[a, b | R (a, b) | ] -> [c, d | R (c, d) | ] with [c <- a, d <- b] inv true post true" in
- let s = "SET RULE rule_a " ^ rule_a in
- let (gs, _) = Arena.handle_request Arena.empty_state (req_of_str s) in
- let (_, msg) = Arena.handle_request gs (req_of_str "GET RULE rule_a") in
- assert_equal ~msg:"Adding rule" ~printer:(fun x->x)
- rule_a msg;
-
- let rule_e =
- "[ | | ] -> [ | | ] with [] inv true post true" in
- let s =
- "SET RULE e " ^ rule_e in
- let (gs,_) =
- Arena.handle_request Arena.empty_state (req_of_str s) in
- let (_, msg) = Arena.handle_request gs (req_of_str "GET RULE e") in
- assert_equal ~msg:"Adding empty rule" ~printer:(fun x->x)
- rule_e msg;
-
- let rule_1 =
- "[ 1 | | vx { 1->0. }; vy { 1->0. }; x { 1->-15.4 }; y { 1->-50.6 } ] -> [ 1, 2 | | vx { 1->0., 2->0. }; vy { 1->0., 2->0. }; x { 1->-14.3, 2->6.6 }; y { 1->-77., 2->2.2 } ] with [1 <- 1] update :x(1) = 1 inv true post true "in
- let rule_1_res =
- "[1 | | vx {1->0.}; vy {1->0.}; x {1->-15.4}; y {1->-50.6}] -> [1, 2 | | vx {1->0., 2->0.}; vy {1->0., 2->0.}; x {1->-14.3, 2->6.6}; y {1->-77., 2->2.2}] with [1 <- 1]
-update
- :x(1) = 1.
- inv true post true" in
- let s = "SET RULE 1 " ^ rule_1 in
- let (gs,_) = Arena.handle_request Arena.empty_state (req_of_str s) in
- let (_, msg) = Arena.handle_request gs (req_of_str "GET RULE 1") in
- assert_equal ~msg:"Adding another rule" ~printer:(fun x->x)
- rule_1_res msg;
- );
-
"simple parsing and printing" >::
(fun () ->
let s = "PLAYERS white, black
@@ -115,14 +72,10 @@
(fun () ->
(* skip_if true "Change to simpler and stable example."; *)
let fname = "./examples/rewriting_example.toss" in
- let file = open_in fname in
- let contents = AuxIO.input_file file in
- let s = "SET STATE #" ^ fname ^ "#" ^ contents in
- let (gs,_) = Arena.handle_request Arena.empty_state (req_of_str s) in
- let (_, msg) =
- Arena.handle_request gs (req_of_str "GET STATE") in
- assert_equal ~msg:("Set "^fname) ~printer:(fun x->x)
- contents msg;
- ); *)
+ let contents = AuxIO.input_file fname in
+ let gs = gs_of_str contents in
+ assert_equal ~printer:(fun x->x) ~msg:"from file, curly braces style"
+ contents (Arena.sprint_state gs);
+ );
]
Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Arena/ContinuousRule.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -4,9 +4,7 @@
let get_time_step () = !time_step
let set_time_step x = (time_step := x)
-let debug_level = ref 0;
-
(* ---------------- BASIC TYPE DEFINITION AND CONSTRUCTOR ------------------- *)
(* Specification of a continuous rewriting rule, as in modelling document. *)
@@ -98,7 +96,7 @@
(* For now, we rewrite only single rules. Does not check postcondition. *)
let rewrite_single_nocheck struc cur_time m r t params =
let time = ref cur_time in
- if !debug_level > 1 then print_endline ("ct: " ^ (string_of_float !time));
+ LOG 2 "current time: %f" !time;
let p_vars, p_vals = List.split params in
let subst_params tm =
List.hd
@@ -131,7 +129,7 @@
let cur_vals = ref init_vals in
let all_vals = ref [] in
let end_time = !time +. t -. (0.01 *. !time_step) in (*TODO: 1% is decimals!*)
- if !debug_level > 1 then print_endline ("et: " ^ (string_of_float end_time));
+ LOG 2 "end time: %f" end_time;
let is_inv s = Solver.M.check s r.inv in
let lhs_to_model ((f, a), _) =
(* dynamics refer to elements by LHS matches *)
@@ -153,13 +151,10 @@
all_vals := !cur_vals :: !all_vals ;
last_struc := !cur_struc
) else (
- if (!debug_level > 1) then (
- print_endline "Invariant failed.";
- print_endline (Structure.str !cur_struc);
- print_endline (Formula.sprint r.inv);
- ) ;
+ LOG 2 "Invariant failed.\n%s\n%s"
+ (Structure.str !cur_struc) (Formula.sprint r.inv);
cur_vals := List.hd !all_vals;
- ) ;
+ );
let lhs_to_model_str x =
let (f, i) = lhs_to_model x in
f, Structure.elem_str struc i in
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Arena/DiscreteRule.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,7 +1,5 @@
(* Discrete structure rewriting. *)
-let debug_level = ref 0
-
let approximate_monotonic = ref true
let prune_indef_vars = ref true
@@ -156,14 +154,9 @@
args
| Some rlmap ->
Array.map (fun e->List.assoc e rlmap) args in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "compose_pre: rel=%s; args=%s; lhs_args=%s\n%!"
- rel
- (String.concat ", " (Array.to_list args))
- (String.concat ", " (Array.to_list lhs_args))
- );
- (* }}} *)
+ LOG 4 "compose_pre: rel=%s; args=%s; lhs_args=%s" rel
+ (String.concat ", " (Array.to_list args))
+ (String.concat ", " (Array.to_list lhs_args));
(* remove potential condition for absence/presence of the
fluent being just added / deleted *)
let body = FormulaMap.map_formula
@@ -178,22 +171,12 @@
if b && Aux.Strings.mem rel nega_frels then Formula.And []
else if b && Aux.Strings.mem rel posi_frels then Formula.Or []
else Formula.Rel (b_rel, b_args))} body in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf "fluent_preconds: body before pruning:\n%s\n%!"
- (Formula.sprint body)
- );
- (* }}} *)
+ LOG 3 "fluent_preconds: body before pruning:\n%s" (Formula.sprint body);
(* remove closed subformulas and indefinite fluents *)
let indef_vars = collect_indef_vars body in
let body =
FormulaOps.remove_subformulas (rem_closed indef_vars) body in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf "fluent_preconds: body after pruning:\n%s\n%!"
- (Formula.sprint body)
- );
- (* }}} *)
+ LOG 3 "fluent_preconds: body after pruning:\n%s" (Formula.sprint body);
let args = Array.to_list args in
let body, other_vars, numap_cstr =
match r.rlmap with
@@ -224,13 +207,8 @@
| [phi] -> phi
| _ -> Formula.Or disjs in
let precond = FormulaOps.prune_unused_quants precond in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf "fluent_preconds: result -- rel=%s(%s), precond=\n%s\n%!"
- rel (String.concat ", " nu_args)
- (Formula.sprint precond)
- );
- (* }}} *)
+ LOG 3 "fluent_preconds: result -- rel=%s(%s), precond=\n%s"
+ rel (String.concat ", " nu_args) (Formula.sprint precond);
rel, (nu_args, precond) in
List.map (fluent_precond true) (Aux.Strings.elements posi_frels) @
List.map (fluent_precond false) (Aux.Strings.elements nega_frels)
@@ -295,23 +273,11 @@
(* Find all embeddings of a rule. Does not guarantee that rewriting
will succeed for all of them. *)
let find_matchings model rule =
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "find_matchings: match_formula=\n%s\n...%!"
- (Formula.sprint rule.match_formula);
- );
- if !debug_level > 4 then (
- Printf.printf "find_matchings: model=\n%s\n...%!"
- (Structure.sprint model);
- );
- (* }}} *)
+ LOG 4 "find_matchings: match_formula=\n%s\n..."
+ (Formula.sprint rule.match_formula);
+ LOG 5 "find_matchings: model=\n%s\n..." (Structure.sprint model);
let res = Solver.M.evaluate model rule.match_formula in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "find_matchings: result=%s\n%!"
- (AssignmentSet.str res)
- );
- (* }}} *)
+ LOG 4 "find_matchings: result=%s" (AssignmentSet.str res);
res
(* Choose an arbitrary matching of a rule from the matchings returned
@@ -696,15 +662,11 @@
let arg_tup = Array.of_list args in
map_some (fun (brel, ar) ->
let selector = Structure.free_for_rel brel ar in
- let asgn =
- Solver.M.evaluate selector rphi in
- (* {{{ log entry *)
- if !debug_level > 3 && asgn<>AssignmentSet.Empty then (
- Printf.printf "compile_rule.expand_defrel_tups: %s {%s} over\
- %s = %s\n%!" drel (Formula.str rphi) (Structure.str selector)
- (AssignmentSet.str asgn)
+ let asgn = Solver.M.evaluate selector rphi in
+ if asgn <> AssignmentSet.Empty then (
+ LOG 4 "compile_rule.expand_defrel_tups: %s {%s} over %s = %s" drel
+ (Formula.str rphi) (Structure.str selector) (AssignmentSet.str asgn)
);
- (* }}} *)
let btup = Array.init ar (fun i->i+1) in
(* [selector] has only [btup] with its elements *)
let selvars =
@@ -735,24 +697,14 @@
List.map fst (List.filter (fun (rel, ar) ->
let selector = Structure.free_for_rel rel ar in
let res = Solver.M.check selector rphi in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "compile_rule.expand_def_rels: %s on %s = %b\n%!"
- rel (Structure.str selector) res
- );
- (* }}} *)
+ LOG 4 "compile_rule.expand_def_rels: %s on %s = %b\n%!"
+ rel (Structure.str selector) res;
res
) signat)
else [rel] in
- unique(*_sorted *) (=)
- (concat_map expand_def_rels rule_src.emb_rels) in
- (* {{{ log entry *)
- if !debug_level > 1 then (
- Printf.printf "compile_rule: emb=%s -- base_emb_rels=%s\n%!"
- (String.concat ", " rule_src.emb_rels)
- (String.concat ", " base_emb_rels);
- );
- (* }}} *)
+ Aux.unique_sorted (concat_map expand_def_rels rule_src.emb_rels) in
+ LOG 2 "compile_rule: emb=%s -- base_emb_rels=%s"
+ (String.concat ", " rule_src.emb_rels) (String.concat ", " base_emb_rels);
let tups_union ts1 ts2 = Aux.unique (=) (ts1 @ ts2)
and tups_empty = []
and tups_diff ts1 ts2 =
@@ -843,23 +795,20 @@
let lhs_opt_rels, lhs_pos_tups, lhs_pos_expanded =
compile_opt_rels lhs_rels in
(* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "compile_rule: lhs_pos_tups=%s\n%!"
- (String.concat "; "(List.map (fun (rel,tups)->
- rel^"{"^String.concat ";"(List.map (fun tup ->
- "("^String.concat ", "
- (Array.to_list (Array.map (
- Structure.elem_name rule_src.lhs_struc) tup))^")") tups)^"}")
- lhs_pos_tups));
- Printf.printf "compile_rule: lhs_pos_expanded=%s\n%!"
- (String.concat "; "(List.map (fun (rel,tups)->
- rel^"{"^String.concat ";"(List.map (fun tup ->
- "("^String.concat ", "
- (Array.to_list (Array.map (
- Structure.elem_name rule_src.lhs_struc) tup))^")") tups)^"}")
- lhs_pos_expanded));
- );
- (* }}} *)
+ LOG 4 "compile_rule: lhs_pos_tups=%s"
+ (String.concat "; "(List.map (fun (rel,tups)->
+ rel ^ "{" ^ String.concat ";" (List.map (fun tup ->
+ "("^String.concat ", "
+ (Array.to_list (Array.map (
+ Structure.elem_name rule_src.lhs_struc) tup))^")") tups)^"}")
+ lhs_pos_tups));
+ LOG 4 "compile_rule: lhs_pos_expanded=%s"
+ (String.concat "; "(List.map (fun (rel,tups)->
+ rel^"{"^String.concat ";"(List.map (fun tup ->
+ "("^String.concat ", "
+ (Array.to_list (Array.map (
+ Structure.elem_name rule_src.lhs_struc) tup))^")") tups)^"}")
+ lhs_pos_expanded));
let lhs_all_tups n =
List.map Array.of_list (Aux.product (
Aux.fold_n (fun acc -> lhs_elems::acc) [] n)) in
@@ -886,17 +835,13 @@
with Not_found -> failwith
("not in signature: " ^ rel))))
base_emb_rels in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "compile_rule: lhs_neg_tups=%s\n%!"
- (String.concat "; "(List.map (fun (rel,tups)->
- rel^"{"^String.concat ";"(List.map (fun tup ->
- "("^String.concat ", "
- (Array.to_list (Array.map (
- Structure.elem_name rule_src.lhs_struc) tup))^")") tups)^"}")
- lhs_neg_tups));
- );
- (* }}} *)
+ LOG 4 "compile_rule: lhs_neg_tups=%s\n%!"
+ (String.concat "; "(List.map (fun (rel,tups)->
+ rel^"{"^String.concat ";"(List.map (fun tup ->
+ "("^String.concat ", "
+ (Array.to_list (Array.map (
+ Structure.elem_name rule_src.lhs_struc) tup))^")") tups)^"}")
+ lhs_neg_tups));
(* injectivity checking *)
let nondistinct = List.map
(Array.map lhs_name_of) nondistinct in
@@ -998,15 +943,8 @@
rel, List.map (fun tup -> Array.map rhs_name_of tup) tups)
del_tuples in
(* Optimizing the embedding formula. *)
- (* {{{ log entry *)
- if !debug_level > 1 then (
- Printf.printf "compile_rule: embedding formula = %s\n%!"
- (Formula.sprint emb)
- );
- if !debug_level > 2 then (
- Printf.printf "compile_rule: done.\n%!";
- );
- (* }}} *)
+ LOG 2 "compile_rule: embedding formula = %s" (Formula.sprint emb);
+ LOG 3 "compile_rule: done.";
{
struc_rule = Some rule_src;
lhs_vars = lhs_vars;
@@ -1097,16 +1035,9 @@
(Aux.concat_map (fun (_,arg) -> Array.to_list arg) add) in
assert (Aux.list_diff rhs_names struc_elems = []);
let rewritable args =
- Aux.array_for_all (fun v -> List.mem (Formula.var_str v) struc_elems)
- args in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- FormulaOps.set_debug_level !debug_level;
- Printf.printf "translate_from_precond:\n%!"
- );
- (* }}} *)
- let conjs =
- FormulaOps.as_conjuncts (FormulaOps.remove_redundant precond) in
+ Aux.array_for_all (fun v-> List.mem (Formula.var_str v) struc_elems) args in
+ LOG 5 "translate_from_precond:";
+ let conjs = FormulaOps.as_conjuncts (FormulaOps.remove_redundant precond) in
let posi, conjs = Aux.partition_map (function
| Formula.Rel (rel, args) when rewritable args ->
Left (rel,args)
@@ -1117,18 +1048,13 @@
Left (rel,args)
| phi -> Right phi) conjs in
let lhs_extracted = posi @ nega in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf
- "translate_from_precond:\nposi:\n%s\nnega:\n%s\norig-precond:\n%s\nsimpl-precond:%s\n%!"
- (Formula.sprint (Formula.And (List.map (fun (rel,args) ->
- Formula.Rel (rel,args)) posi)))
- (Formula.sprint (Formula.And (List.map (fun (rel,args) ->
- Formula.Rel (rel,args)) nega)))
- (Formula.sprint precond)
- (Formula.sprint (Formula.And conjs))
- );
- (* }}} *)
+ LOG 3 "translate_from_precond:\nposi:\n%s\nnega:\n%s\norig-precond:\n%s\nsimpl-precond:%s\n%!"
+ (Formula.sprint (Formula.And (List.map (fun (rel,args) ->
+ Formula.Rel (rel,args)) posi)))
+ (Formula.sprint (Formula.And (List.map (fun (rel,args) ->
+ Formula.Rel (rel,args)) nega)))
+ (Formula.sprint precond)
+ (Formula.sprint (Formula.And conjs));
let precond = Formula.And conjs in
let fvars = FormulaSubst.free_vars precond in
let local_vars =
@@ -1153,20 +1079,16 @@
let extracted =
List.map (Array.map Formula.var_str)
(Aux.assoc_all rel lhs_extracted) in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "translate_from_precond: _opt_%s -- extracted %s -- \
+ LOG 5 "translate_from_precond: _opt_%s -- extracted %s -- \
remaining %s\n%!" rel
- (String.concat "; "
- (List.map (fun args ->
- String.concat " " (Array.to_list args)) extracted))
- (String.concat "; "
- (List.map (fun args ->
- String.concat " " (Array.to_list args))
- (Aux.list_diff tups extracted)))
- );
- (* }}} *)
- let tups = Aux.list_diff tups extracted in
+ (String.concat "; "
+ (List.map (fun args ->
+ String.concat " " (Array.to_list args)) extracted))
+ (String.concat "; "
+ (List.map (fun args ->
+ String.concat " " (Array.to_list args))
+ (Aux.list_diff tups extracted)));
+ let tups = Aux.list_diff tups extracted in
List.map (fun args -> "_opt_"^rel, args) tups
with Not_found -> [])
emb_rels in
@@ -1182,20 +1104,15 @@
Aux.fold_n (fun acc -> struc_elems::acc) [] arity)) in
let modified =
Aux.assoc_all rel add @ Aux.assoc_all rel del in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf
- "translate_from_precond: RHS _opt_%s -- modified %s -- \
+ LOG 5 "translate_from_precond: RHS _opt_%s -- modified %s -- \
remaining %s\n%!" rel
- (String.concat "; "
- (List.map (fun args ->
- String.concat " " (Array.to_list args)) modified))
- (String.concat "; "
- (List.map (fun args ->
- String.concat " " (Array.to_list args))
- (Aux.list_diff tups modified)))
- );
- (* }}} *)
+ (String.concat "; "
+ (List.map (fun args ->
+ String.concat " " (Array.to_list args)) modified))
+ (String.concat "; "
+ (List.map (fun args ->
+ String.concat " " (Array.to_list args))
+ (Aux.list_diff tups modified)));
let tups = Aux.list_diff tups modified in
List.map (fun args -> "_opt_"^rel, args) tups
with Not_found -> [])
@@ -1216,12 +1133,7 @@
let lhs_struc = add_rels lhs_struc opt_s in
let lhs_struc = add_rels lhs_struc
(List.map (fun tup-> "_nondistinct_", tup) nondistinct) in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- FormulaOps.set_debug_level 0;
- Printf.printf "translate_from_precond: end\n%!"
- );
- (* }}} *)
+ LOG 5 "translate_from_precond: end";
{
lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
Modified: trunk/Toss/Arena/DiscreteRule.mli
===================================================================
--- trunk/Toss/Arena/DiscreteRule.mli 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Arena/DiscreteRule.mli 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,7 +1,5 @@
(** Discrete structure rewriting rules construction and rewriting. *)
-val debug_level : int ref
-
(** If [true], ignore what happens on RHSes of rules when assessing
if fluents are positive / negative (only check whether their
LHS+precondition occurrences are negative/positive). *)
Modified: trunk/Toss/Arena/DiscreteRuleTest.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRuleTest.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Arena/DiscreteRuleTest.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,8 +1,6 @@
open OUnit
open DiscreteRule
-FormulaOps.set_debug_level 0 ;;
-
let struc_of_str s =
try
StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
Modified: trunk/Toss/Formula/AuxIO.ml
===================================================================
--- trunk/Toss/Formula/AuxIO.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/AuxIO.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -220,6 +220,18 @@
print_string s; flush stdout
) ENDIF
+let sprint_of_fprint fprint_fun x =
+ ignore (Format.flush_str_formatter ());
+ Format.fprintf Format.str_formatter "@[%a@]" fprint_fun x;
+ Format.flush_str_formatter ()
+
+let print_of_fprint fprint_fun x =
+ IFDEF JAVASCRIPT THEN (
+ print (sprint_of_fprint fprint_fun x)
+ ) ELSE (
+ fprint_fun Format.std_formatter x
+ ) ENDIF
+
let log module_name debug_lev s =
let s = "["^string_of_int debug_lev^"@"^module_name^"] "^s in
IFDEF JAVASCRIPT THEN (
Modified: trunk/Toss/Formula/AuxIO.mli
===================================================================
--- trunk/Toss/Formula/AuxIO.mli 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/AuxIO.mli 2012-03-05 23:24:41 UTC (rev 1682)
@@ -65,3 +65,9 @@
(** Printing for JS and native. *)
val print : string -> unit
+
+(** Given formatter printing function, creates a to-string printing function. *)
+val sprint_of_fprint : (Format.formatter -> 'a -> unit) -> 'a -> string
+
+(** Given formatter printing function, creates a to-console printing function.*)
+val print_of_fprint : (Format.formatter -> 'a -> unit) -> 'a -> unit
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/BoolFormula.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,14 +1,5 @@
(* Represent Boolean combinations of integer literals. *)
-let debug_level = ref 0
-let debug_elim = ref false
-let set_debug_level i = (
- Sat.set_debug_level (i-1);
- debug_level := i;
- if i > 0 then debug_elim := true
-)
-let set_debug_elim b = (debug_elim := b;)
-
(* 0 : no generation is performed and to_cnf transforms a DNF
1 : use Tseitin to construct a CNF with auxiliary variables
2 : use Plaisted-Greenbaum to construct a CNF with auxiliary variables *)
@@ -210,9 +201,7 @@
try
let id = Hashtbl.find ids phi in if pos then id else -1 * id
with Not_found ->
- if !debug_level > 2 then
- print_endline ("Added " ^ (Formula.str phi) ^ " as " ^
- (string_of_int !free_id));
+ LOG 3 "Added %s as %i" (Formula.str phi) !free_id;
Hashtbl.add ids phi (!free_id);
Hashtbl.add rev_ids (!free_id) phi;
Hashtbl.add rev_ids (-1 * !free_id) (Formula.Not phi);
@@ -402,9 +391,8 @@
let res_lits = (* obtain list of feasible pivot-literals *)
List.filter (fun lit1 ->
List.exists (fun lit2 -> lit2 = -lit1) cl2_lits) cl1_lits in
- if !debug_level > 3 then
- print_endline ("res_lits: " ^ String.concat ", "
- (List.map string_of_int res_lits));
+ LOG 4 "res_lits: %s"
+ (String.concat ", " (List.map string_of_int res_lits));
(* if there is more than one possible pivot-literal, the resulting
clause will be equivalent to true, so we don't care *)
if (List.length res_lits) <> 1 then BAnd []
@@ -446,14 +434,10 @@
then ( (* do nothing, since the resolvent is useless *) ) else
res_clauses := cl_res :: !res_clauses;
) clauses)) clauses;
- if !debug_level > 2 then (
- print_endline("Resolvents: " ^
- String.concat ", " (List.map str !res_clauses));
- print_endline("Subsumed clauses: " ^
- String.concat ", " (List.map str !subsumed));
- print_endline("Reduced Resolvents: " ^
- str (singularise (BAnd !res_clauses)));
- );
+ LOG 3 "Resolvents: %s\nSubsumed clauses: %s\nReduced Resolvents: %s"
+ (String.concat ", " (List.map str !res_clauses))
+ (String.concat ", " (List.map str !subsumed))
+ (str (singularise (BAnd !res_clauses)));
let total =
(List.filter
(fun clause ->
@@ -504,9 +488,8 @@
(fun resolvent ->
List.exists (fun phi -> subclause resolvent phi) non_resolvents)
resolvents in
- if !debug_level > 2 then
- print_endline("Useful resolvents: " ^
- String.concat ", " (List.map str useful_resolvents));
+ LOG 3 "Useful resolvents: %s"
+ (String.concat ", " (List.map str useful_resolvents));
let new_clauses =
List.map (function
| BOr lits ->
@@ -538,9 +521,8 @@
let y = f x in
if y=x then x else fp f y in
fp (fun phi -> (simp_fun phi)) phi in
- if !debug_level > 1 then
- print_endline ("Simplification:\nphi " ^ str phi ^
- "\nwas simplified to " ^ str simplified);
+ LOG 2 "Simplification:\nphi %s\nwas simplified to %s"
+ (str phi) (str simplified);
simplified
let subst_simp vars f =
@@ -650,28 +632,21 @@
(to_reduced_form (flatten (to_nnf ~neg:false phi)))
| 2 -> (* or Plaisted-Greenbaum conversion *)
let arg = flatten (to_nnf ~neg:false phi) in
- if !debug_level > 0 then print_endline "CNF conv: arg computed";
+ LOG 1 "CNF conv: arg computed";
pg_auxcnf_of_bool_formula arg
| _ -> failwith "undefined parameter value" in
- if !debug_level > 0 then (
- print_endline ("Separator is: " ^ string_of_int aux_separator);
- if !debug_level > 1 then
- print_endline ("Converting Aux-CNF: " ^ str aux_cnf_formula);
- );
+ LOG 1 "Separator is: %i" aux_separator;
+ LOG 2 "Converting Aux-CNF: %s" (str aux_cnf_formula);
let aux_cnf = listcnf_of_boolcnf aux_cnf_formula in
let cnf_llist = Sat.convert_aux_cnf ~disc_vars aux_separator aux_cnf in
- if !debug_level > 0 then print_endline ("Converted CNF. ");
- if !debug_level > 1 then
- print_endline ("Converted CNF: " ^ (Sat.cnf_str cnf_llist));
+ LOG 1 "Converted CNF. ";
+ LOG 2 "Converted CNF: %s" (Sat.cnf_str cnf_llist);
let simplified =
if (!simplification land 1) > 0 then
subsumption_filter cnf_llist
else cnf_llist in
- if !debug_level > 1 then (
- if (!simplification land 1) > 0 then
- print_endline ("Subsumption turned on");
- print_endline ("Simplified CNF: " ^ (Sat.cnf_str simplified))
- );
+ LOG 2 "Subsumption %b; Simplified CNF: %s"
+ ((!simplification land 1) > 0) (Sat.cnf_str simplified);
simplified
@@ -749,8 +724,6 @@
let (tm_jump, cutvar, has_vars_mem) = (1.1, 2, Hashtbl.create 31)
-let _ () = debug_elim := true
-
(* Returns a quantifier-free formula equivalent to All (vars, phi).
The list [vars] contains only positive literals and [phi] is in NNF. *)
let rec elim_all_rec ?(nocheck=false) prefix tout vars in_phi =
@@ -758,8 +731,8 @@
| BVar v -> if List.mem (abs v) vars then BOr [] else (BVar v)
| BNot _ -> failwith "error (elim_all_rec): BNot in NNF Boolean formula"
| BAnd fs ->
- if !debug_elim && prefix.[0] <> 'S' then
- Printf.printf "%s vars %i list %i (same sign)\n%!"
+ if prefix.[0] <> 'S' then
+ LOG 1 "%s vars %i list %i (same sign)"
prefix (List.length vars) (List.length fs);
let do_elim (acc, i) f =
if f = BOr [] || acc = [BOr []] then ([BOr []], i+1) else
@@ -768,16 +741,13 @@
if elim_f = BOr [] then ([BOr []], i+1) else
if elim_f = BAnd [] then (acc, i+1) else (elim_f :: acc, i+1) in
let (simp_fs, _) = List.fold_left do_elim ([], 0) fs in
- if !debug_elim && prefix.[0] <> 'S' then
- Printf.printf "%s done %!" prefix;
+ if prefix.[0] <> 'S' then LOG 1 "%s done " prefix;
let res = match to_dnf ~tm:(5. *. tout) (BAnd simp_fs) with
| None ->
- if !debug_elim && prefix.[0] <> 'S' then
- Printf.printf "(non-dnf %i)\n%!" (size (BAnd simp_fs));
+ if prefix.[0] <> 'S' then LOG 1 "(non-dnf %i)" (size (BAnd simp_fs));
BAnd simp_fs
| Some psi ->
- if !debug_elim && prefix.[0] <> 'S' then
- Printf.printf "(dnf %i)\n%!" (size psi);
+ if prefix.[0] <> 'S' then LOG 1 "(dnf %i)" (size psi);
psi in
neutral_absorbing (flatten res)
| BOr [] -> BOr []
@@ -797,9 +767,9 @@
let res = has_vars sgn vl in
Hashtbl.add has_vars_mem (sgn, vl) res;
res in
- if !debug_elim && prefix.[0] <> 'S' then
- Printf.printf "%s vars %i list %i (partition)\n%!" prefix
- (List.length vars) (List.length fs);
+ if prefix.[0] <> 'S' then
+ LOG 1 "%s vars %i list %i (partition)"
+ prefix (List.length vars) (List.length fs);
let (fs_yes, fs_no) = List.partition (has_vars_memo false vars) fs in
if Hashtbl.length has_vars_mem > 10000 then Hashtbl.clear has_vars_mem;
if fs_no <> [] then (
@@ -811,9 +781,8 @@
let (res, msg ) = match to_dnf ~tm:(5. *. tout) sub with
| None -> (simplify sub, "no dnf")
| Some dnf -> (simplify dnf, "dnf") in
- if !debug_elim then
- Printf.printf "%s vars %i list %i (%s)\n%!" prefix
- (List.length vars) (List.length fs) msg;
+ LOG 1 "%s vars %i list %i (%s)"
+ prefix (List.length vars) (List.length fs) msg;
res
) else if List.length vars < cutvar then (
let insert psi v = neutral_absorbing (flatten (univ v psi)) in
@@ -821,58 +790,51 @@
let (res, msg ) = match to_dnf ~tm:(3. *. tout) sub with
| None -> (simplify sub, "no dnf")
| Some dnf -> (simplify dnf, "dnf") in
- if !debug_elim then
- Printf.printf "%s vars %i list %i (%s)\n%!" prefix
- (List.length vars) (List.length fs) msg;
+ LOG 1 "%s vars %i list %i (%s)"
+ prefix (List.length vars) (List.length fs) msg;
res
) else (
- if !debug_elim then
- Printf.printf "%s vars %i list %i (inside %i)\n%!" prefix
- (List.length vars) (List.length fs) (size phi);
+ LOG 1 "%s vars %i list %i (inside %i)"
+ prefix (List.length vars) (List.length fs) (size phi);
try
if nocheck then raise (Aux.Timeout "!!out");
- if !debug_elim then
- Printf.printf "%s vars %i list %i (cnf conv) %!" prefix
- (List.length vars) (List.length fs);
+ LOG 1 "%s vars %i list %i (cnf conv) "
+ prefix (List.length vars) (List.length fs);
let bool_cnf = match to_cnf ~disc_vars:vars ~tm:(3.*.tout) phi with
| None -> raise (Aux.Timeout "!!none")
| Some psi -> psi in
- if !debug_elim then Printf.printf "success \n%!";
+ LOG 1 "success";
let cnf = elim_all_rec prefix tout vars bool_cnf in
let xsize = function BAnd l -> List.length l | _ -> 0 in
- if !debug_elim && prefix.[0] <> 'S' then
- Printf.printf "%s vars %i list %i (cnf after conv %i) %!" prefix
- (List.length vars) (List.length fs) (xsize cnf);
+ if prefix.[0] <> 'S' then
+ LOG 1 "%s vars %i list %i (cnf after conv %i)"
+ prefix (List.length vars) (List.length fs) (xsize cnf);
match to_dnf ~tm:(5. *. tout) cnf with
| None ->
- if !debug_elim && prefix.[0] <> 'S' then Printf.printf "\n%!"; cnf
+ if prefix.[0] <> 'S' then LOG 1 "(none)"; cnf
| Some dnf ->
- if !debug_elim && prefix.[0] <> 'S' then
- Printf.printf "(dnf) \n%!"; dnf
+ if prefix.[0] <> 'S' then LOG 1 "(dnf)"; dnf
with Aux.Timeout s ->
- if !debug_elim && s<>"!!out" then Printf.printf "failed\n%!";
+ if s <> "!!out" then LOG 1 "failed";
let elim nbr_left timeout psi v =
try
- if !debug_elim then
- Printf.printf "%s eliminating %i%!" prefix v;
+ LOG 1 "%s eliminating %i" prefix v;
if nbr_left > 2 then (
Sat.set_timeout (timeout);
) else ( Sat.set_timeout (3. *. timeout) );
let res = elim_all_rec "S" tout [v] psi in
Sat.clear_timeout ();
- if !debug_elim then Printf.printf " success.\n%!";
+ LOG 1 " success.";
Some res
with Aux.Timeout _ ->
- if !debug_elim then Printf.printf " failed\n%!";
+ LOG 1 " failed.";
None in
let try_elim_var timeout (left_vars,cur_phi,elim_nbr,step,all_nbr) v =
if not (has_vars_memo true [-v] cur_phi) then (
- if !debug_elim then
- Printf.printf "%s elimineted %i (only pos)\n%!" prefix v;
+ LOG 1 "%s elimineted %i (only pos)" prefix v;
(left_vars, subst_simp [-v] cur_phi, elim_nbr+1, step+1, all_nbr)
) else if not (has_vars_memo true [v] cur_phi) then (
- if !debug_elim then
- Printf.printf "%s elimineted %i (only neg)\n%!" prefix v;
+ LOG 1 "%s elimineted %i (only neg)" prefix v;
(left_vars, subst_simp [v] cur_phi, elim_nbr+1, step+1, all_nbr)
) else if 2*step > all_nbr && elim_nbr > 0 &&
step+2 < all_nbr && all_nbr - elim_nbr > cutvar then
@@ -887,7 +849,7 @@
elim_all_rec prefix tout left_vars new_phi
else
let (big_v, rest_vars) = (List.hd left_vars, List.tl left_vars) in
- if !debug_elim then Printf.printf "branch %i\n%!" big_v;
+ LOG 1 "branch %i" big_v;
elim_all_rec prefix (tm_jump *.tout) rest_vars (univ big_v new_phi)
)
@@ -996,34 +958,28 @@
| QEx (vars, qphi) ->
Hashtbl.clear has_vars_mem;
let inside, len = elim_quant qphi, List.length vars in
- if !debug_elim then Printf.printf "EX %i START\n%!" len;
+ LOG 1 "EX %i START" len;
let res_raw = elim_ex vars (inside) in
let res = match to_dnf ~tm:3. res_raw with
| None ->
- if !debug_elim then (
- Printf.printf "EX ELIM NO DNF\n%!";
- (* Printf.printf "%s \n%!" (str res_raw); *)
- );
+ LOG 1 "EX ELIM NO DNF";
res_raw
| Some r ->
- if !debug_elim then Printf.printf "EX ELIM IN DNF\n%!";
+ LOG 1 "EX ELIM IN DNF";
r in
- if !debug_elim then Printf.printf "EX %i FIN\n%!" len;
+ LOG 1 "EX %i FIN" len;
res
| QAll (vars, qphi) ->
Hashtbl.clear has_vars_mem;
let inside, len = elim_quant qphi, List.length vars in
- if !debug_elim then Printf.printf "ALL %i START\n%!" len;
+ LOG 1 "ALL %i START" len;
let res_raw = elim_all vars (inside) in
let res = match to_cnf ~tm:3. res_raw with
| None ->
- if !debug_elim then (
- Printf.printf "ALL ELIM NO CNF\n%!";
- (* Printf.printf "%s \n%!" (str res_raw); *)
- );
+ LOG 1 "ALL ELIM NO CNF";
res_raw
| Some r ->
- if !debug_elim then Printf.printf "ALL ELIM IN CNF\n%!";
+ LOG 1 "ALL ELIM IN CNF";
r in
- if !debug_elim then Printf.printf "ALL %i FIN\n%!" len;
+ LOG 1 "ALL %i FIN" len;
res
Modified: trunk/Toss/Formula/BoolFormula.mli
===================================================================
--- trunk/Toss/Formula/BoolFormula.mli 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/BoolFormula.mli 2012-03-05 23:24:41 UTC (rev 1682)
@@ -91,12 +91,7 @@
val elim_quant : qbf -> bool_formula
-(** {2 Debugging} *)
+(** {2 Parameters} *)
-(** Debugging information. At level 0 nothing is printed out. *)
-val set_debug_level : int -> unit
-
-val set_debug_elim : bool -> unit
-
val set_auxcnf : int -> unit
val set_simplification : int -> unit
Modified: trunk/Toss/Formula/BoolFormulaTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFormulaTest.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/BoolFormulaTest.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,17 +1,14 @@
open OUnit
open Formula
-open BoolFormula;;
+open BoolFormula
-BoolFormula.set_debug_level 0;;
-BoolFormula.set_auxcnf 2;; (* Tseitin: 1 Plaisted-Greenbaum: 2 *)
+BoolFormula.set_auxcnf 2 (* Tseitin: 1 Plaisted-Greenbaum: 2 *)
let formula_of_string s =
FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
-;;
let formula_of_string s =
FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
-;;
let flat_reduce_formula form_str =
let form = formula_of_string form_str in
@@ -411,8 +408,10 @@
AuxIO.set_optimized_gc ();
let (file) = (ref "") in
let opts = [
- ("-v", Arg.Unit (fun () -> set_debug_elim true), "be verbose");
- ("-d", Arg.Int (fun i -> set_debug_level i), "set debug level");
+ ("-v", Arg.Unit (fun () -> AuxIO.set_debug_level "BoolFormula" 1),
+ "be verbose");
+ ("-d", Arg.Int (fun i -> AuxIO.set_debug_level "BoolFormula" i),
+ "set debug level");
("-f", Arg.String (fun s -> file := s), "process file");
] in
Arg.parse opts (fun _ -> ()) "Try -help for help or one of the following.";
Modified: trunk/Toss/Formula/BoolFunction.ml
===================================================================
--- trunk/Toss/Formula/BoolFunction.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/BoolFunction.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,13 +1,7 @@
(* Represent Boolean functions. *)
open BoolFormula
-let debug_level = ref 0
-let set_debug_level i = (
- debug_level := i;
- if i > 2 then BoolFormula.set_debug_elim true;
-)
-
(* ----------------------- BASIC TYPE DEFINITION -------------------------- *)
(* This type describes Boolean functions *)
@@ -31,6 +25,8 @@
let fprint_mod_var_list = Aux.fprint_sep_list "," fprint_mod_var
+let mod_vars_str m = String.concat "," (List.map (fun (a, b) -> a ^ " " ^ b) m)
+
(* Print to formatter. *)
let rec fprint f = function
| Fun (s, vars) ->
@@ -294,25 +290,21 @@
| Or fl -> Or (List.map elim_quant fl)
| Ex (vs, f) ->
let elim = to_nnf (triv_simp (elim_quant f)) in
- if !debug_level > 1 then Format.printf "Eliminating@ Ex@ %a@ .@ %a@\n%!"
- fprint_mod_var_list vs fprint elim;
+ LOG 2 "Eliminating Ex %s . %s" (mod_vars_str vs) (str elim);
let elim_bool = to_bool elim in
let cvars (c, n) = List.map (fun v -> (n, v)) (List.assoc c classes) in
let ex_vars = List.map nbr (List.flatten (List.map cvars vs)) in
let noquant_bool = elim_ex ex_vars elim_bool in
let res = from_bool (BoolFormula.flatten_sort (simplify noquant_bool)) in
- if !debug_level > 1 then Format.printf "Eliminated@ :@ %a@\n%!"
- fprint res;
+ LOG 2 "Eliminated : %s" (str res);
res in
let elim_simp = elim_quant (triv_simp (to_nnf f)) in
- if !debug_level > 0 then
- Format.printf "BoolFunction: Computing %s@\n%!" msg;
+ LOG 1 "BoolFunction: Computing %s" msg;
match boolf (to_bool elim_simp) with
- | None -> if !debug_level > 0 then Format.printf "Failed.@\n%!"; None
+ | None -> LOG 1 "Failed."; None
| Some boolphi ->
let res = triv_simp (from_bool boolphi) in
- if !debug_level > 0 then
- Format.printf "BoolFunction: Computed %s:@\n%a@\n%!" msg fprint res;
+ LOG 1 "BoolFunction: Computed %s:\n%s" msg (str res);
Some (res)
(* Convert a function to DNF with eliminated quantifiers. *)
Modified: trunk/Toss/Formula/BoolFunction.mli
===================================================================
--- trunk/Toss/Formula/BoolFunction.mli 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/BoolFunction.mli 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,11 +1,5 @@
(** Represent Boolean functions. *)
-(** {2 Debugging} *)
-
-(** Set debugging level. *)
-val set_debug_level : int -> unit
-
-
(** {2 Basic Type Definition} *)
(** This type describes Boolean functions *)
Modified: trunk/Toss/Formula/BoolFunctionTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFunctionTest.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/BoolFunctionTest.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -1,8 +1,6 @@
open OUnit
open BoolFunction
-let _ = ( BoolFunction.set_debug_level 0; )
-
let bf_of_string s =
BoolFunctionParser.parse_bool_function Lexer.lex (Lexing.from_string s)
@@ -108,7 +106,7 @@
let main () =
AuxIO.set_optimized_gc ();
let (file, print_bool, debug_level) = (ref "", ref false, ref 0) in
- let dbg_level i = (debug_level := i; BoolFunction.set_debug_level i) in
+ let dbg_level i = (debug_level:= i; AuxIO.set_debug_level "BoolFunction" i) in
let (only_inline, only_fp, nf) = (ref false, ref false, ref 0) in
let opts = [
("-v", Arg.Unit (fun () -> dbg_level 1), "be verbose (= -d 1)");
@@ -145,14 +143,14 @@
Aux.unsome (dnf cl inline_goal) in
if !only_inline || !only_fp || !debug_level > 0 then
print_defs ~print_bool:!print_bool new_defs;
- print_endline "\n\n// GOAL FORMULA\n";
+ AuxIO.print "\n\n// GOAL FORMULA\n\n";
print new_goal;
- print_endline ";\n";
+ AuxIO.print ";\n\n";
with Lexer.Parsing_error err -> (
- print_endline res_s;
+ AuxIO.print (res_s ^ "\n");
let msg_raw = String.sub err 9 ((String.length err)-9) in
let msg = Aux.replace_regexp ~regexp:"\n" ~templ:"\n// " msg_raw in
- print_endline ("// ERROR: NOT PARSED\n//\n// " ^ msg ^ "\n");
+ AuxIO.print ("// ERROR: NOT PARSED\n//\n// " ^ msg ^ "\n\n");
)
Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml 2012-02-28 02:36:29 UTC (rev 1681)
+++ trunk/Toss/Formula/FFTNF.ml 2012-03-05 23:24:41 UTC (rev 1682)
@@ -141,19 +141,14 @@
*)
-(*
- *)
open Formula
open Aux
-open Printf
let parsimony_threshold_1 = ref 100
let parsimony_threshold_2 = ref 200
-let debug_level = ref 0
-
(* Reduce a formula to Partially Prenex Normal Negation Normal Form
with existential-first minimized alternation: when merging prefixes
of subformulas, the number of (artificially introduced)
@@ -465,7 +460,7 @@
| Let _ as phi -> unpack_flat (FormulaSubst.expand_formula phi)
let location_str loc =
- sprintf "%s#[%s]"
+ Printf.sprintf "%s#[%s]"
(Formula.sprint (unpack_flat (
formula_of_tree
(zip_nonflat {loc with n={
@@ -635,17 +630,10 @@
| ExNode (ctx, vs) | AllNode (ctx, vs) ->
let vs1' = Vars.diff vs1 vs
and vs2' = Vars.diff vs2 vs in
- (* {{{ log entry *)
- if !debug_level > 6 then (
- printf "cmp_vars_lits: Q=%s; vs1'=%s; vs2'=%s\n%!"
- (String.concat ", "
- (List.map Formula.var_str (Vars.elements vs)))
- (String.concat ", "
- (List.map Formula.var_str (Vars.elements vs1')))
- (String.concat ", "
- (List.map Formula.var_str (Vars.elements vs2')))
- );
- (* }}} *)
+ LOG 7 "cmp_vars_lits: Q=%s; vs1'=%s; vs2'=%s"
+ (String.concat ", " (List.map Formula.var_str (Vars.elements vs)))
+ (String.concat ", " (List.map Formula.var_str (Vars.elements vs1')))
+ (String.concat ", " (List.map Formula.var_str (Vars.elements vs2')));
if Vars.is_empty vs1' && Vars.is_empty vs2'
then cmp_lits lit1 lit2
else
@@ -660,12 +648,8 @@
| Right _, Left _ -> false
| Right (vs1, lit1), Right (vs2, lit2) ->
let res = cmp_vars_lits ctx vs1 vs2 lit1 lit2 in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- printf "find_unprot: comparing lits %s < %s = %s\n%!"
- (Formula.str lit1) (Formula.str lit2) (if res then "T" else "F")
- );
- (* }}} *)
+ LOG 4 "find_unprot: comparing lits %s < %s = %s"
+ (Formula.str lit1) (Formula.str lit2) (if res then "T" else "F");
res in
(* find next location in the tree *)
let rec aux ctx = function
@@ -705,8 +689,7 @@
(* The rewriting steps. Uses a callback to process subtasks
recursively before putting them in their final locations. *)
let rec pull_out parl1 subproc (task_id, task_lit as task) loc =
- let _ = if !debug_level > 4 then
- printf "\npull-out_step_location: %s\n" (location_str loc) in
+ LOG 5 "\npull-out_step_location: %s" (location_str loc);
let lit_vs, put_result =
match task_lit with
| Left subt ->
@@ -725,23 +708,25 @@
let vs'' = Vars.diff vs vs' in
(* a1
pull-out(context'[],[Qn.[fill-loc]]) *)
- if Vars.is_empty vs' then
- let _ = if !debug_level > 2 then printf "a1\n" in
+ if Vars.is_empty vs' then (
+ LOG 3 "a1";
pull_out parl1 subproc task {x=ctx'; n=qT loc.x (vs,loc.n)}
+ )
(* a2
context'[Qn'.(L /\ Qn''.[fill-loc])] *)
- else
- let _ = if !debug_level > 2 then printf "a2\n" in
+ else (
+ LOG 3 "a2";
zip {x=ctx'; n=qT loc.x (vs', conj_flat (
Lazy.force put_result, qT loc.x (vs'', loc.n)))}
+ )
(* b
pull-out(context'[],[[fill-loc] /\ C]) *)
| AndNode (ctx', subts) ->
- let _ = if !debug_level > 2 then printf "b\n" in
+ LOG 3 "b";
pull_out parl1 subproc task
- {x=ctx'; n=zip {loc with x=AndNode (Top, subts)}}
+ {x=ctx'; n=zip {loc with x=AndNode (Top, subts)}}
(* c *)
| OrNode (AllNode (ctx', vs) as qN, subts)
@@ -765,31 +750,30 @@
(* c1
pull-out(context'[Qn2.[] \/ Qn4.D],[fill-loc]) *)
- else if Vars.is_empty vs3 then
- let _ = if !debug_level > 2 then printf "c1\n" in
+ else if Vars.is_empty vs3 then (
+ LOG 3 "c1";
pull_out parl1 subproc task
- {loc with x= qNode qN (
- orNode_flat (ctx', [qT qN (vs4, disj)]), vs2)}
+ {loc with x= qNode qN (orNode_flat (ctx', [qT qN (vs4, disj)]), vs2)}
+ )
(* c2
context'[Qn3.(Qn1\Qn3.(L /\ Qn5.[fill-loc]) \/ Qn4.D)] *)
else if not (Vars.is_empty vs1) &&
(not (Vars.is_empty vs1_3) ||
Vars.is_empty (Vars.diff vs3 vs1))
- then
- let _ = if !debug_level > 2 then printf "c2\n" in
+ then (
+ LOG 3 "c2";
let subt =
- disj_flat (
- qT qN (vs1_3, conj_flat
- (Lazy.force put_result, qT qN (vs5, loc.n))),
- qT qN (vs4, disj)) in
+ disj_flat (qT qN (vs1_3, conj_flat
+ (Lazy.force put_result, qT qN (vs5, loc.n))), qT qN (vs4, disj)) in
zip {x=ctx'; n=qT qN (vs3, subt)}
+ )
(* c3
pull-out(context'[Qn2+3.[] \/ Qn3+4.D],[fill-loc]) *)
else if (match qN with ExNode _ -> true | _ -> false)
then (
- if !debug_level > 2 then printf "c3\n";
+ LOG 3 "c3";
pull_out parl1 subproc task
{loc with x=qNode qN
(orNode_flat (ctx', [qT qN (vsD, disj)]), vs0)}
@@ -798,15 +782,12 @@
pull-out(context'[Qn.(([] \/ D) /\ ([fill-loc] \/
D))],[T]) *)
) else (
- if !debug_level > 2 then printf "c4\n";
+ LOG 3 "c4";
pull_out parl1 subproc task
- {x=
- orNode_flat (
- (* no need for andNode_flat here *)
- AndNode (
- qNode qN (ctx', vs), [
- disj_flat (loc.n, disj)]),
- [disj]);
+ {x = orNode_flat (
+ (* no need for andNode_flat here *)
+ AndNode (qNode qN (ctx', vs), [
+ disj_flat (loc.n, disj)]), [disj]);
n= {fvs=Vars.empty; t=TAnd []}}
)
(* d *)
@@ -836,68 +817,68 @@
(* d1
pull-out(context'[Qn2.([] \/ D) /\ Qn4.C],[fill-loc]) *)
- else if Vars.is_empty vs3 then
- let _ = if !debug_level > 2 then printf "d1\n" in
+ else if Vars.is_empty vs3 then (
+ LOG 3 "d1";
pull_out parl1 subproc task
{loc with x= orNode_flat (
qNode qN (andNode_flat (
ctx', qT qN (vs4, conj)), vs2),
or_subts)}
+ )
(* d2
pull-out(context'[Qn2+3.([] \/ D) /\ Qn3+4.C]) *)
else if (match qN with AllNode _ -> true | _ -> false)
- then
- let _ = if !debug_level > 2 then printf "d2\n" in
+ then (
+ LOG 3 "d2";
pull_out parl1 subproc task
{loc with x= orNode_flat (
qNode qN (andNode_flat (ctx', qT qN (vsC, conj)), vsFLD)
, or_subts)}
-
- (* d3
- pull-out(context'[Qn6.([] /\ C) \/ Qn5.(D /\
- C)],[fill-loc]) *)
- else
+ )
+ (* d3
+ pull-out(context'[Qn6.([] /\ C) \/ Qn5.(D /\ C)],[fill-loc]) *)
+ else (
let vs5 = Vars.union vsD vsC in
let vs6 = Vars.union vsFL vsC in
- let _ = if !debug_level > 2 then printf "d3\n" in
+ LOG 3 "d3";
pull_out parl1 subproc task
{loc with x= andNode_flat (
qNode qN (
orNode_flat(
ctx', [qT qN (vs5, conj_flat (disj,conj))]), vs6),
conj)}
+ )
| OrNode (OrNode _,_) ->
failwith "pull_out: malformed context (nonflat disjunction)"
- (* e
- context[fill-loc] *)
+ (* e
+ context[fill-loc] *)
| OrNode (Top, _) ->
- let _ = if !debug_level > 2 then printf "e\n" in
+ LOG 3 "e";
zip {loc with n=conj_flat (Lazy.force put_result, loc.n)}
+
| OrNode (ctx',_) when not (quant_in_scope ctx') ->
- let _ = if !debug_level > 2 then printf "e\n" in
+ LOG 3 "e";
zip {loc with n=conj_flat (Lazy.force put_result, loc.n)}
- (* f1
- context[L /\ [fill-loc]] *)
+ (* f1
+ context[L /\ [fill-loc]] *)
| OrNode (AndNode (Top, _), _) ->
- let _ = if !debug_level > 2 then printf "f1\n" in
+ LOG 3 "f1";
zip {loc with n=
conj_flat (Lazy.force put_result, loc.n)}
- | OrNode (AndNode (ctx', _), _)
- when Vars.subset (scope_vars ctx') lit_vs ->
- let _ = if !debug_level > 2 then printf "f1\n" in
- zip {loc with n=
- conj_flat (Lazy.force put_result, loc.n)}
- (* f2
- pull-out(context'[([] /\ C) \/ (D /\ C)], [fill-loc]) *)
- (* same as (d) of FFSEP *)
- | OrNode (AndNode (ctx', conjs), disjs)
- when not (univ_next_in_scope ctx') ->
- let _ = if !debug_level > 2 then printf "f2\n" in
+ | OrNode (AndNode (ctx', _), _) when Vars.subset (scope_vars ctx') lit_vs ->
+ LOG 3 "f1";
+ zip {loc with n = conj_flat (Lazy.force put_result, loc.n)}
+
+ (* f2
+ pull-out(context'[([] /\ C) \/ (D /\ C)], [fill-loc]) *)
+ (* same as (d) of FFSEP *)
+ | OrNode (AndNode (ctx', conjs), disjs) when not (univ_next_in_scope ctx')->
+ LOG 3 "f2";
let d = List.fold_right (fun a b->disj_flat (a,b)) disjs
{fvs=Vars.empty; t=TOr []} in
let c = List.fold_right (fun a b->conj_flat (a,b)) conjs
@@ -906,11 +887,11 @@
{loc with x= andNode_flat (
orNode_flat (ctx', [conj_flat (d,c)]), c)}
- (* f3
- pull-out(context'[([] \/ D \/ E) /\ (C \/ E)], [fill-loc]) *)
- (* same as (f) of FFSEP *)
+ (* f3
+ pull-out(context'[([] \/ D \/ E) /\ (C \/ E)], [fill-loc]) *)
+ (* same as (f) of FFSEP *)
| OrNode (AndNode (OrNode (ctx', esjs), conjs), disjs) ->
- let _ = if !debug_level > 2 then printf "f3\n" in
+ LOG 3 "f3";
let e = List.fold_right (fun a b->disj_flat (a,b)) esjs
{fvs=Vars.empty; t=TOr []} in
let c = List.fold_right (fun a b->conj_flat (a,b)) conjs
@@ -932,69 +913,38 @@
if size < !parsimony_threshold_1 then 0
else if size < !parsimony_threshold_2 then 1
else 2 in
- (* {{{ log entry *)
- if !debug_level > 1 then (
- printf "ff_tnf: parsimony_level=%d\n%!" parsimony_level
- );
- (* }}} *)
+ LOG 2 "ff_tnf: parsimony_level=%d" parsimony_level;
let loc = init ~do_pnf:(parsimony_level<2) phi in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf "\ninit_location: %s\n" (location_str loc)
- );
- (* }}} *)
+ LOG 3 "\ninit_location: %s" (location_str loc);
(* a bit redundant -- only the first call is a nontrivial location *)
let rec loop i loc =
match find_unprotected cmp_lits loc with
| Some (subt_lit, loc) ->
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf "\nfound_subtask-literal: %s\n"
- (match subt_lit with
- | Left subt -> Formula.sprint (Not subt)
- | Right (_,lit) -> Formula.str lit);
- printf "location: %s\n" (location_str loc)
- );
- (* }}} *)
+ LOG 3 "\nfound_subtask-literal: %s\nlocation: %s"
+ (match subt_lit with
+ | Left subt -> Formula.sprint (Not subt)
+ | Right (_,lit) -> Formula.str lit)
+ (location_str loc);
let phi =
pull_out (parsimony_level>0) subproc (i, subt_lit) loc in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf "\npull-out_result: %s\n"
- (Formula.sprint (formula_of_tree phi));
- );
- (* }}} *)
+ LOG 3 "\npull-out_result: %s" (Formula.sprint (formula_of_tree phi));
loop (i+1) {x=Top; n=phi}
| None ->
let result = zip loc in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- printf "\nff_tnf-result: %s\n"...
[truncated message content] |
