[Toss-devel-svn] SF.net SVN: toss:[1685] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1685] trunk/Toss
|
From: <luk...@us...> - 2012-03-08 20:18:28
|
Revision: 1685
http://toss.svn.sourceforge.net/toss/?rev=1685&view=rev
Author: lukaszkaiser
Date: 2012-03-08 20:18:20 +0000 (Thu, 08 Mar 2012)
Log Message:
-----------
Optimizing and debugging JS playing.
Modified Paths:
--------------
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Client/JsHandler.ml
trunk/Toss/Client/Main.js
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/Sat/SatTest.ml
trunk/Toss/Solver/AssignmentSet.ml
trunk/Toss/Solver/AssignmentSet.mli
trunk/Toss/Solver/Assignments.ml
trunk/Toss/Solver/Solver.ml
trunk/Toss/Solver/Structure.ml
trunk/Toss/Solver/Structure.mli
trunk/Toss/Solver/StructureTest.ml
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Arena/DiscreteRule.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -296,8 +296,6 @@
List.map
(fun tp->List.map2 (fun v e->v,e) vars tp) tuples
| AssignmentSet.Empty -> []
- | AssignmentSet.FOUn _ as x ->
- enumerate_asgns all_elems vars (AssignmentSet.expand_unary x)
| AssignmentSet.FO (v, els) ->
let vars = list_remove v vars in
concat_map (fun (e,sub)->
Modified: trunk/Toss/Client/JsHandler.ml
===================================================================
--- trunk/Toss/Client/JsHandler.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Client/JsHandler.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -198,6 +198,16 @@
let _ = set_handle "make_move" make_move
+let precache time =
+ let game, _ = !cur_game.game_state in
+ let state = List.hd !play_states in
+ Play.set_timeout (Js.to_float time);
+ LOG 1 "precaching %f seconds" (Js.to_float time);
+ ignore (Play.maximax_unfold_choose 4 game state !cur_game.heuristic);
+ Play.cancel_timeout ()
+
+let _ = set_handle "precache" precache
+
(* When called in a different thread, we can't call continuation. So
arrange to do it from "outside". *)
let suggest player_name time =
@@ -215,6 +225,7 @@
game state !cur_game.heuristic) in
Play.cancel_timeout ();
let algo_iters = large_iters - !Play.latest_unfold_iters_left in
+ LOG 0 "iters: %i" algo_iters;
let move_id = Aux.array_argfind
(fun (_, m, _) -> m = move) !cur_all_moves in
let result =
Modified: trunk/Toss/Client/Main.js
===================================================================
--- trunk/Toss/Client/Main.js 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Client/Main.js 2012-03-08 20:18:20 UTC (rev 1685)
@@ -493,6 +493,7 @@
console.log ("new_play_do callback: play created");
PLAYS.push(p);
p.redraw ();
+ ASYNCH ("precache", [0.5], function () {});
//li = new_play_item (GAME_NAME, CUR_PLAY_I);
//document.getElementById ("plays-list-" + GAME_NAME).appendChild (li);
}
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Formula/BoolFormula.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -251,7 +251,7 @@
let get_conjunctions = function BAnd fl -> fl | f -> [f] in
let get_disjunctions = function BOr fl -> fl | f -> [f] in
let fold_acc f xl =
- List.fold_left (fun acc x -> (f x) @ acc) [] xl in
+ List.fold_left (fun acc x -> List.rev_append (List.rev (f x)) acc) [] xl in
let rev_collect_conj xl = fold_acc get_conjunctions xl in
let rev_collect_disj xl = fold_acc get_disjunctions xl in
match phi with
@@ -303,13 +303,14 @@
let unique_psis = Aux.unique (=) psis in
let lits = List.filter is_literal unique_psis in
if neg_occurrence lits then BAnd [] else
- BOr (List.map singularise unique_psis)
+ BOr (List.rev (List.rev_map singularise unique_psis))
| BAnd psis ->
let unique_psis = Aux.unique (=) psis in
let lits = List.filter is_literal unique_psis in
if neg_occurrence lits then BOr [] else
- BAnd (List.map singularise unique_psis) in
+ BAnd (List.rev (List.rev_map singularise unique_psis)) in
let rec subsumption phi =
+ LOG 2 "simplify: subsumption";
let subclause a b =
match (a,b) with
| (BOr psis, BOr thetas)
@@ -325,47 +326,51 @@
| BVar _ | BNot _ -> phi
| BAnd psis ->
let (disjnctns,non_disjnctns) = List.partition is_disjunction psis in
- BAnd(non_disjnctns @ List.filter
- (fun theta ->
- (List.for_all (fun phi -> phi=theta ||
- not (subformula phi theta)) non_disjnctns)
- && (List.for_all (fun phi -> phi=theta ||
- not (subclause phi theta)) disjnctns))
- disjnctns)
+ BAnd (List.rev_append (List.rev non_disjnctns) (
+ List.filter
+ (fun theta ->
+ (List.for_all (fun phi -> phi=theta ||
+ not (subformula phi theta)) non_disjnctns)
+ && (List.for_all (fun phi -> phi=theta ||
+ not (subclause phi theta)) disjnctns)
+ ) disjnctns))
| BOr psis ->
let (conjnctns,non_conjnctns) = List.partition is_conjunction psis in
- BOr(non_conjnctns @ List.filter
- (fun theta ->
- (List.for_all (fun phi -> phi=theta ||
- not (subformula phi theta)) non_conjnctns)
- && (List.for_all (fun phi -> phi=theta ||
- not (subclause phi theta)) conjnctns))
- conjnctns) in
+ BOr (List.rev_append (List.rev non_conjnctns) (
+ List.filter
+ (fun theta ->
+ (List.for_all (fun phi -> phi=theta ||
+ not (subformula phi theta)) non_conjnctns)
+ && (List.for_all (fun phi -> phi=theta ||
+ not (subclause phi theta)) conjnctns)
+ ) conjnctns)) in
let unit_propagation phi =
+ LOG 2 "simplify: unit_propagation";
(* beware that unit_propagation might introduce the subformula true,
and hence should be followed by neutral_absorbing before
starting the next fixed-point iteration *)
match phi with
| BAnd phis ->
- let units = List.map
- (function | BVar v -> v | _ -> failwith ("not a literal!"))
- (List.filter is_literal phis) in
+ let units = List.rev (List.rev_map (
+ function | BVar v -> v | _ -> failwith ("not a literal!")
+ ) (List.filter is_literal phis)) in
let rec propagate units phi =
match phi with
| BVar v ->
if List.exists (fun unit -> v=unit) units then BAnd [] else phi
| BNot psi -> BNot (propagate units psi)
- | BAnd psis -> BAnd (List.map (propagate units) psis)
- | BOr psis -> BOr (List.map (propagate units) psis) in
- BAnd ((List.map (fun v -> BVar v) units) @
- (List.map (propagate units) phis))
+ | BAnd psis -> BAnd (List.rev (List.rev_map (propagate units) psis))
+ | BOr psis-> BOr (List.rev (List.rev_map (propagate units) psis)) in
+ BAnd (List.rev_append (List.rev_map (fun v -> BVar v) units)
+ (List.rev (List.rev_map (propagate units) phis)))
| _ -> phi in
let rec resolution phi =
+ LOG 2 "simplify: resolution";
match phi with
| BVar v -> phi
| BNot psi -> BNot (resolution psi)
| BOr psis ->
- let res_psis = List.map resolution psis in
+ let res_psis = List.rev (List.rev_map resolution psis) in
let neg_phi = to_nnf (BNot (BOr res_psis)) in
let res_neg_phi = resolution neg_phi in
to_nnf (BNot res_neg_phi)
@@ -399,19 +404,20 @@
else (* construct a resolvent and mark it with the unused literal 0 *)
let lit = List.nth res_lits 0 in
(* construct resolvent of cl1 and cl2 using pivot-literal lit *)
- BOr ((lit_of_int 0) ::
- (List.map lit_of_int
- (List.filter (fun lit1 -> lit1 <> lit) cl1_lits
- @ List.filter (fun lit2 -> lit2 <> -lit) cl2_lits))
- @ cl1_rest @ cl2_rest) in
+ let flist = List.rev_map lit_of_int
+ (List.rev_append (List.rev (
+ List.filter (fun lit1 -> lit1 <> lit) cl1_lits))
+ (List.filter (fun lit2 -> lit2 <> -lit) cl2_lits)) in
+ BOr ((lit_of_int 0) :: (List.rev_append flist (
+ List.rev_append (List.rev cl1_rest) cl2_rest))) in
let res_clauses = ref [] in
let subsumed = ref [] in
- (* Construct all possible resolvents and check each new resolvent
- whether it is subsumed by some existing clause.
- In fact, the following does not work: If this is the case we can
- remove two initial clauses (ie add them to the list subsumed).
- Instead, we discard the resolved but subsumed clause directly.
- *)
+ (* Construct all possible resolvents and check each new resolvent
+ whether it is subsumed by some existing clause.
+ In fact, the following does not work: If this is the case we can
+ remove two initial clauses (ie add them to the list subsumed).
+ Instead, we discard the resolved but subsumed clause directly.
+ *)
List.iter (fun cl1 ->
(List.iter
(fun cl2 ->
@@ -434,22 +440,27 @@
then ( (* do nothing, since the resolvent is useless *) ) else
res_clauses := cl_res :: !res_clauses;
) clauses)) clauses;
+ LOG 2 "simplify: resolution: filtering; clauses: %i subsumed: %i"
+ (List.length clauses) (List.length !subsumed);
LOG 3 "Resolvents: %s\nSubsumed clauses: %s\nReduced Resolvents: %s"
- (String.concat ", " (List.map str !res_clauses))
- (String.concat ", " (List.map str !subsumed))
+ (String.concat ", " (List.rev (List.rev_map str !res_clauses)))
+ (String.concat ", " (List.rev (List.rev_map str !subsumed)))
(str (singularise (BAnd !res_clauses)));
- let total =
- (List.filter
- (fun clause ->
- not (List.exists (fun sub -> clause=sub) !subsumed)) clauses)
- @ !res_clauses @ non_clauses in
+ let filtered =
+ List.filter
+ (fun clause ->
+ not (List.exists (fun sub -> clause=sub) !subsumed)) clauses in
+ LOG 2 "simplify: resolution: computing total";
+ let total = List.rev_append (List.rev filtered)
+ (List.rev_append (List.rev !res_clauses) non_clauses) in
singularise (neutral_absorbing (BAnd total)) in
let choose_resolvents phi =
+ LOG 2 "simplify: choose_resolvents";
(* check the resolvents for "good" ones (at the moment these are clauses
that subsume clauses in the original formula) and discard the rest *)
let rec filter_by_subsumption = function
| BOr psis ->
- let filtered_psis = List.map filter_by_subsumption psis in
+ let filtered_psis= List.rev (List.rev_map filter_by_subsumption psis) in
let neg_phi = to_nnf (BNot (BOr filtered_psis)) in
let filtered_neg_phi = filter_by_subsumption neg_phi in
to_nnf (BNot filtered_neg_phi)
@@ -491,13 +502,14 @@
LOG 3 "Useful resolvents: %s"
(String.concat ", " (List.map str useful_resolvents));
let new_clauses =
- List.map (function
+ List.rev_map (function
| BOr lits ->
BOr (List.filter (fun lit -> lit <> (lit_of_int 0)) lits)
| _ -> failwith ("trying to remove literals from a non-clause!")
) useful_resolvents in
- BAnd (new_clauses @ non_resolvents @
- (List.map filter_by_subsumption non_clauses))
+ BAnd (List.rev_append new_clauses (
+ List.rev_append (List.rev non_resolvents)
+ (List.rev (List.rev_map filter_by_subsumption non_clauses))))
| BNot psi -> BNot (filter_by_subsumption psi)
| BVar v as lit ->
if v=0 then failwith "There should not be empty resolved clauses!" else
@@ -507,7 +519,7 @@
let simp_resolution = fun phi ->
if ((!simplification lsr 2) land 1) > 0 then
choose_resolvents (subsumption (resolution phi))
- else phi in
+ else phi in
let simp_fun = fun phi ->
(simp_resolution
(neutral_absorbing
@@ -655,13 +667,17 @@
let (ids, rev_ids, free_id) = (Hashtbl.create 7, Hashtbl.create 7, ref 1) in
let boolean_phi = bool_formula_of_formula_arg phi (ids, rev_ids, free_id) in
let cnf_llist = convert boolean_phi in
+ LOG 2 "formula_to_cnf: converted";
let bool_cnf =
- BAnd (List.map (fun literals -> BOr (List.map lit_of_int literals))
- cnf_llist) in
+ BAnd (List.rev (List.rev_map (
+ fun literals -> BOr (List.rev (List.rev_map lit_of_int literals))
+ ) cnf_llist)) in
+ LOG 2 "formula_to_cnf: bool_cnf";
let simplified =
if ((!simplification lsr 1) land 1) > 0 then
simplify bool_cnf
else bool_cnf in
+ LOG 2 "formula_to_cnf: simplified";
let formula_cnf =
formula_of_bool_formula_arg simplified (ids, rev_ids, free_id) in
formula_cnf
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Formula/FormulaOps.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -689,10 +689,10 @@
LOG 3 "comp. CNF: %s" (str f);
match BoolFormula.formula_to_cnf f with
| And flist ->
- LOG 3 "CNF: %s" (str (And flist));
+ LOG 2 "CNF: %s" (str (And flist));
flist
| psi ->
- LOG 3 "CNF: %s" (str psi);
+ LOG 2 "CNF: %s" (str psi);
[phi]
(* Convert an arbitrary boolean combination to DNF. *)
Modified: trunk/Toss/Formula/Sat/SatTest.ml
===================================================================
--- trunk/Toss/Formula/Sat/SatTest.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Formula/Sat/SatTest.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -69,7 +69,7 @@
[47; 5; 7; 8; 17]; [37; 5; 6; 8; 17]; [30; 5; 8; 17];
[52; 5; 6; 7; 17]; [53; 5; 6; 17]; [38; 5; 6; 7; 17];
[54; 5; 7; 17]; [55; 5; 6; 8; 9; 17]; [10; 5; 8; 9; 17];
- [48; 5; 6; 8; 9; 17]; [42; 5; 8; 9; 17];
+ [48; 5; 6; 8; 9; 17]; [42; 5; 8; 9; 17]; ] @ [
[56; 5; 6; 12; 7; 8; 9]; [57; 5; 6; 12; 7; 8];
[58; 5; 6; 12; 9]; [59; 5; 6; 12]; [44; 5; 6; 7; 8; 9];
[55; 5; 6; 8; 9]; [60; 5; 12; 7; 8; 9]; [51; 5; 12; 8; 9];
@@ -94,7 +94,7 @@
[62; 12; 7; 9]; [32; 12; 9]; [60; 12; 7; 8; 9];
[77; 12; 7; 9]; [51; 12; 8; 9]; [31; 12; 9]; [46; 7; 8; 17];
[61; 7; 17]; [10; 8; 9]; [30; 8]; [85; 9; 17]; [43; 17];
- [32; 9]; [63; 5; 6; 12; 7; 8; 9; 17];
+ [32; 9]; [63; 5; 6; 12; 7; 8; 9; 17]; ] @ [
[64; 5; 12; 7; 8; 9; 17]; [16; 5; 6; 12; 7; 8; 17];
[18; 5; 12; 7; 8; 17]; [34; 5; 6; 12; 7; 8];
[86; 5; 6; 7; 9]; [84; 5; 6; 9]; [39; 5; 6; 17];
@@ -121,7 +121,7 @@
[42; 6; 8; 17]; [110; 6; 12; 17]; [43; 6; 17]; [15; 6; 12; 8];
[111; 6; 12]; [112; 6; 12; 7; 8; 9]; [83; 6; 12; 8; 9];
[113; 6; 12; 7; 8; 9; 17]; [114; 6; 12; 8; 9; 17];
- [86; 6; 7; 8; 9]; [84; 6; 8; 9]; [44; 6; 7; 8; 9];
+ [86; 6; 7; 8; 9]; [84; 6; 8; 9]; [44; 6; 7; 8; 9]; ] @ [
[55; 6; 8; 9]; [13; 6; 12; 8]; [106; 6; 12]; [39; 6];
[112; 6; 12; 7; 9]; [86; 6; 7; 9]; [4; 12; 7; 8; 9];
[10; 12; 8; 9]; [14; 12; 7; 8]; [15; 12; 8]; [115; 12; 7];
@@ -190,7 +190,7 @@
[-79; -10; -9]; [-80; -10; -5]; [-81; -6; -10; -5; -9; -4; -8];
[-82; -14; -10; -4]; [-83; -14; -10; -5; -4; -8]; [-84; -6; -10; -8];
[-85; -6; -9; -8]; [-86; -6; -9]; [-87; -14; -4]; [-88;-14;-5;-4;-8];
- [-89; -14; -4; -8]; [-90; -14; -5; -8]; [-91; -14; -10; -9];
+ [-89; -14; -4; -8]; [-90; -14; -5; -8]; [-91; -14; -10; -9]; ] @ [
[-92; -6; -14; -10; -9; -8]; [-93; -6; -14; -9; -4; -8]; [-94; -9];
[-95; -9; -8]; [-96; -5]; [-97;-14;-10;-5;-4]; [-98;-14;-10;-5;-9;-4];
[-99; -14; -8]; [-100; -6; -10; -5; -9; -4]; [-101; -6; -10; -5; -9];
Modified: trunk/Toss/Solver/AssignmentSet.ml
===================================================================
--- trunk/Toss/Solver/AssignmentSet.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Solver/AssignmentSet.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -15,18 +15,11 @@
type assignment_set =
| Empty
| Any
- | FOUn of string * Bitvector.bitvector
| FO of string * (int * assignment_set) list
| MSO of string * ((Elems.t * Elems.t) * assignment_set) list
| Real of (Poly.polynomial * Formula.sign_op) list list
-let expand_unary = function
- | FOUn (v, bv) ->
- FO (v, List.rev_map (fun i -> (i, Any)) (Bitvector.to_rev_list bv))
- | x -> x
-
-
(* --------------------- PRINTING AND HELPER FUNCTIONS --------------------- *)
(* Variables assigned in an assignement set. *)
@@ -36,7 +29,6 @@
let rec assigned_vars acc = function
| Empty | Any -> acc
- | FOUn (v, _) -> (`FO v) :: acc
| FO (v, l) -> assigned_vars_list assigned_vars ((`FO v) :: acc) l
| MSO (v, l) -> assigned_vars_list assigned_vars ((`MSO v) :: acc) l
| _ -> failwith "AssignmentSet:assigned vars not implemented for reals"
@@ -58,7 +50,6 @@
let rec str = function
| Empty -> "{}"
| Any -> "T"
- | FOUn _ as x -> str (expand_unary x)
| FO (v, map) ->
let estr (e, a) =
if a = Any then v ^ "->" ^ (string_of_int e) else
@@ -79,7 +70,6 @@
let rec named_str struc = function
| Empty -> "{}"
| Any -> "T"
- | FOUn _ as x -> named_str struc (expand_unary x)
| FO (v, map) ->
let estr (e, a) =
if a = Any then v ^ "->" ^ (Structure.elem_str struc e) else
@@ -105,7 +95,6 @@
let rec choose_fo default = function
| Empty -> raise Not_found
| Any -> default
- | FOUn _ as x -> choose_fo default (expand_unary x)
| FO (v, []) when List.mem_assoc v default -> raise Not_found
| FO (v, (e, sub)::_) when e < 0 && List.mem_assoc v default ->
(v, List.assoc v default) :: choose_fo (List.remove_assoc v default) sub
@@ -124,7 +113,6 @@
List.rev_map Array.of_list
(Aux.product
(List.rev_map (fun _ -> Structure.Elems.elements elems) vars))
- | FOUn _ as x -> tuples elems vars (expand_unary x)
| FO (v, (e,other_aset)::asg_list) when e < 0 ->
let asg_list = List.map (fun e ->
e, try List.assoc e asg_list with Not_found -> other_aset)
@@ -155,7 +143,6 @@
let tuples = Aux.product elems in
List.map (List.combine vars) tuples
| Empty -> []
- | FOUn _ as x -> fo_assgn_to_list all_elems vars (expand_unary x)
| FO (v, (e,other_aset)::els) when e < 0 ->
let vars = Aux.list_remove (`FO v) vars in
let other_res =
Modified: trunk/Toss/Solver/AssignmentSet.mli
===================================================================
--- trunk/Toss/Solver/AssignmentSet.mli 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Solver/AssignmentSet.mli 2012-03-08 20:18:20 UTC (rev 1685)
@@ -11,15 +11,12 @@
type assignment_set =
| Empty
| Any
- | FOUn of string * Bitvector.bitvector
| FO of string * (int * assignment_set) list
| MSO of string *
((Structure.Elems.t * Structure.Elems.t) * assignment_set) list
| Real of (Poly.polynomial * Formula.sign_op) list list
-val expand_unary : assignment_set -> assignment_set
-
(** {2 Printing and small helper functions.} *)
(** Variables assigned in an assignement set. *)
Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Solver/Assignments.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -98,14 +98,6 @@
| (Empty, _) | (_, Empty) -> Empty
| (Any, a) -> a
| (a, Any) -> a
- | (FOUn (v1, bv1), FOUn (v2, bv2)) when v1 = v2 ->
- let bv = bv1 &&& bv2 in if is_empty bv then Empty else FOUn (v1, bv)
- | (FO (v1, map1), FOUn (v2, _)) when compare_vars v1 v2 < 0 ->
- fo_map v1 (join aset2) map1
- | (FOUn (v1, _), FO (v2, map2)) when compare_vars v1 v2 > 0 ->
- fo_map v2 (join aset1) map2
- | (FOUn _, _) -> join (expand_unary aset1) aset2
- | (_, FOUn _ ) -> join aset1 (expand_unary aset2)
| (FO (v1, map1), FO (v2, map2)) -> (
match compare_vars v1 v2 with
| 0 ->
@@ -163,11 +155,6 @@
(* Enforce [aset] and additionally that the FO variable [v] is set to [e]. *)
let rec set_equal uneq els v e = function
| Empty -> Empty
- | FOUn (u, b) when u = v ->
- let nb = if uneq then clear_bit b e else
- if get_bit b e then set_bit empty e else empty in
- if is_empty nb then Empty else FOUn (u, nb)
- | FOUn _ as x -> set_equal uneq els v e (expand_unary x)
| FO (u, map) as aset -> (
match compare_vars u v with
| 0 ->
@@ -193,7 +180,6 @@
(* Enforce that in [aset] the variable [u] is equal to [w]; assumes u < w. *)
let rec eq_vars uneq els u w = function
| Empty -> Empty
- | FOUn _ as x -> eq_vars uneq els u w (expand_unary x)
| FO (v, map) as aset -> (
match compare_vars v u with
| 0 ->
@@ -240,11 +226,6 @@
| (Any, _) | (_, Any) -> Any
| (Empty, a) -> a
| (a, Empty) -> a
- | (FOUn (v1, bv1), FOUn (v2, bv2)) when v1 = v2 ->
- let bv = bv1 ||| bv2 in
- if nbr_set_bits bv = sllen elems then Any else FOUn (v1, bv)
- | (FOUn _, _) -> sum elems (expand_unary aset1) aset2
- | (_, FOUn _) -> sum elems aset1 (expand_unary aset2)
| (FO (v1, map1), FO (v2, map2)) -> (
match compare_vars v1 v2 with
| 0 ->
@@ -321,7 +302,6 @@
let rec project elems v = function
| Empty -> Empty
| Any -> Any
- | FOUn (u, _) as x -> if u = v then Any else x
| FO (u, m) when u = v -> (* Sum the assignments below *)
List.fold_left (fun s (_, a) -> sum elems s a) Empty m
| FO (u, m) ->
@@ -364,8 +344,6 @@
let rec universal elems v = function
| Empty -> Empty
| Any -> Any
- | FOUn (u, b) as x ->
- if u <> v then x else if nbr_set_bits b < sllen elems then Empty else Any
| FO (u, m) when u = v -> (* Join the assignments below *)
if List.length m < sllen elems then Empty else
List.fold_left (fun s (_, a) -> join s a) Any m
@@ -412,7 +390,6 @@
let rec complement elems = function
| Empty -> Any
| Any -> Empty
- | FOUn _ as x -> complement elems (expand_unary x)
| FO (v, map) ->
let compl_map =
List.rev (complement_map_rev elems [] (slist elems, map)) in
@@ -470,8 +447,6 @@
| (Empty, _) | (_, Any) -> Empty
| (Any, a) -> complement elems a
| (a, Empty) -> a
- | (FOUn _ as x, y) -> complement_join elems (expand_unary x) y
- | (x, (FOUn _ as y)) -> complement_join elems x (expand_unary y)
| (FO (v1, map1), FO (v2, map2)) when v1 = v2 ->
let resm = List.rev (complement_join_map_rev elems [] (map1, map2)) in
if resm = [] then Empty else FO (v1, resm)
@@ -532,8 +507,6 @@
let rec join_rel aset vars tuples_set incidence_map all_elems =
match aset with (* TODO: better use of incidence map? *)
| Empty -> Empty
- | FOUn (v, _) when Aux.array_mem v vars ->
- join_rel (expand_unary aset) vars tuples_set incidence_map all_elems
| FO (v, map) when Aux.array_mem v vars ->
let tps e =
if e < Array.length incidence_map then incidence_map.(e) else
@@ -556,15 +529,8 @@
| (_, a1) :: (((_, a2) :: _) as r) when a1 = a2 -> same_asg r
| _ -> false
-let rec all_any = function
- | [] -> true
- | (_, a) :: rest when a = Any -> all_any rest
- | _ -> false
-
let rec compress no_elems = function
| FO (v, map) when List.length map = no_elems && same_asg map ->
compress no_elems (snd (List.hd map))
- | FO (v, map) when all_any map ->
- FOUn (v, Bitvector.of_list (List.rev_map fst map))
| FO (v, map) -> FO (v, map_snd (compress no_elems) map)
| x -> x
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Solver/Solver.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -136,12 +136,12 @@
if nxt = a then nxt else fixpnt v vs psi nxt in
let simp a = Assignments.compress (Assignments.sllen elems) a in
if aset = Empty then Empty else
- let foun_var = match aset with FOUn (v,_) -> v | _ -> "" in
+ let rec all_any = function
+ | [] -> true
+ | (_, a) :: rest when a = Any -> all_any rest
+ | _ -> false in
+ let foun_var = match aset with FO (v, map) when all_any map -> v | _-> "" in
match phi with
- | Rel (relname, [|v|]) ->
- let bv = Structure.pred_vector model relname in
- if Bitvector.is_empty bv then Empty else
- report (join aset (FOUn (var_str v, bv)))
| Rel (relname, vl) ->
let tuples_s = Structure.rel_graph relname model in
let inc_map = Structure.rel_incidence relname model in
@@ -170,8 +170,8 @@
| RealExpr (p, s) -> (* TODO: use aset directly as context for speed *)
report (join aset (assignment_of_real_expr fp model elems (p, s)))
| Not phi ->
- (*A intersect (complement B)=A intersect (complement(B intersect A))*)
- report (complement_join elems aset (eval fp model elems aset phi))
+ (*A intersect (complement B)=A intersect (complement(B intersect A))*)
+ report (complement_join elems aset (eval fp model elems aset phi))
| And [] -> aset
| And [phi] -> report (eval fp model elems aset phi)
| And fl -> report (List.fold_left (eval fp model elems) aset fl)
@@ -184,9 +184,9 @@
| Ex ([], phi) | All ([], phi) -> failwith "evaluating empty quantifier"
| Ex ([v], And (Rel (r1, v1):: Rel (r2, v2):: rest)) as ephi when
foun_var <> "" && ( let vfo = to_fo v in (* an often occurring join *)
- (v1 = [|vfo|] && v2 = [|vfo; `FO foun_var|]) ||
- (v1 = [|vfo|] && v2 = [|`FO foun_var; vfo|]) ||
- (v2 = [|vfo|] && v1 = [|vfo; `FO foun_var|]) ||
+ (v1 = [|vfo|] && v2 = [|vfo; `FO foun_var|]) || (* it isn't needed*)
+ (v1 = [|vfo|] && v2 = [|`FO foun_var; vfo|]) || (* but helps to *)
+ (v2 = [|vfo|] && v1 = [|vfo; `FO foun_var|]) || (* optimize here*)
(v2 = [|vfo|] && v1 = [|`FO foun_var; vfo|]) ) &&
not (List.mem (`FO foun_var) (FormulaSubst.free_vars (And rest)))->(
LOG 1 "special join on %s for %s" foun_var (str ephi);
@@ -194,15 +194,21 @@
if Array.length v1= 1 then r1, r2, v1, v2 else r2, r1, v2, v1 in
let othpos = if vpred.(0) = vbin.(0) then 0 else 1 in
let inc_map = Structure.rel_incidence rbin model in
- let av = match aset with FOUn (_, av) -> av | _-> failwith "av" in
- let add_to_bitvec b e =
- if e >= Array.length inc_map then b else
- Tuples.fold (fun t b -> set_bit b t.(othpos)) inc_map.(e) b in
- let b0 = List.fold_left add_to_bitvec Bitvector.empty
- (Bitvector.to_rev_list av) in
- let b = b0 &&& (Structure.pred_vector model pred) in
- if Bitvector.is_empty b then Empty else
- let r = eval fp model elems (FOUn (var_str v, b)) (And rest) in
+ let pred_map = Structure.rel_incidence pred model in
+ let is_in_pred e =
+ if e >= Array.length pred_map then false else
+ not (Tuples.is_empty pred_map.(e)) in
+ let am = match aset with FO (_, am) -> am | _ -> failwith "am" in
+ let add_to_map map (e, _) =
+ if e >= Array.length inc_map then map else
+ Tuples.fold (fun t m ->
+ if is_in_pred t.(othpos) then t.(othpos) :: m else m
+ ) inc_map.(e) map in
+ let newels = List.fold_left add_to_map [] am in
+ if newels = [] then Empty else
+ let newm = List.map (fun e -> (e, Any))
+ (Aux.unique_sorted newels) in
+ let r = eval fp model elems (FO (var_str v, newm)) (And rest) in
if r = Empty then Empty else
let ag = eval fp model elems r (Rel (rbin, vbin)) in
report (simp (join aset (project_list elems ag [var_str v])))
@@ -273,7 +279,7 @@
remove_dup_vars [] (List.sort compare_vars (fo_vars_r_rec re)) in
let rec sum_polys = function
| Empty -> Poly.Const 0.
- | Any | FOUn _ -> failwith "absolute assignement for sum,impossible to calc"
+ | Any -> failwith "absolute assignement for sum,impossible to calc"
| FO (_, alist) ->
let addp p (_, a) = Poly.Plus (p, sum_polys a) in
List.fold_left addp (Poly.Const 0.) alist
Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Solver/Structure.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -50,8 +50,7 @@
type structure = {
rel_signature : int StringMap.t ;
elements : Elems.t ;
- predicates : Bitvector.bitvector StringMap.t ; (* unary relations *)
- relations : Tuples.t StringMap.t ; (* binary (or more-ary) relations *)
+ relations : Tuples.t StringMap.t ;
functions : (float IntMap.t) StringMap.t ;
incidence : (TIntMap.t) StringMap.t ;
names : int StringMap.t ;
@@ -63,14 +62,12 @@
let compare s1 s2 =
if s1 == s2 then 0 else
- let c = Elems.compare s1.elements s2.elements in
+ let c = StringMap.compare Tuples.compare s1.relations s2.relations in
if c <> 0 then c else
- let d = StringMap.compare Tuples.compare s1.relations s2.relations in
+ let d = Elems.compare s1.elements s2.elements in
if d <> 0 then d else
- let e = StringMap.compare Pervasives.compare s1.predicates s2.predicates
- in if e <> 0 then e else
- StringMap.compare (IntMap.compare Pervasives.compare)
- s1.functions s2.functions
+ StringMap.compare (IntMap.compare Pervasives.compare)
+ s1.functions s2.functions
let equal s1 s2 = (compare s1 s2 = 0)
@@ -83,21 +80,15 @@
let inv_names s = s.inv_names
let replace_names s nms inms = { s with names = nms; inv_names = inms }
let functions s = s.functions
-let tuples_of_bitvec b =
- let append_sg tps e = Tuples.add [|e|] tps in
- List.fold_left append_sg Tuples.empty (Bitvector.to_rev_list b)
-let relations s = StringMap.fold (fun pred bv acc ->
- StringMap.add pred (tuples_of_bitvec bv) acc) s.predicates s.relations
+let relations s = s.relations
-
(* ----------------------- BASIC HELPER FUNCTIONS --------------------------- *)
(* Number of tuples in a relation. *)
let rel_size struc rel =
- try Tuples.cardinal (StringMap.find rel struc.relations)
- with Not_found ->
- try Bitvector.nbr_set_bits (StringMap.find rel struc.predicates)
- with Not_found -> 0
+ try
+ Tuples.cardinal (StringMap.find rel struc.relations)
+ with Not_found -> 0
(* Reverse a map: make a string IntMap from an int StringMap. *)
let rev_string_to_int_map map =
@@ -110,7 +101,6 @@
(* Return the empty structure. *)
let empty_structure () = {
elements = Elems.empty ;
- predicates = StringMap.empty ;
relations = StringMap.empty ;
functions = StringMap.empty ;
incidence = StringMap.empty ;
@@ -120,39 +110,28 @@
}
let rel_signature struc =
- StringMap.fold (fun r ar si -> (r,ar)::si) struc.rel_signature []
+ StringMap.fold (fun r ar si -> (r,ar)::si)
+ struc.rel_signature []
let rel_sizes struc =
- let rs = StringMap.fold (fun r tups si -> (r, Tuples.cardinal tups)::si)
- struc.relations [] in
- StringMap.fold (fun r bv si -> (r, Bitvector.nbr_set_bits bv)::si)
- struc.predicates rs
-
-let pred_vector struc pred =
- try StringMap.find pred struc.predicates with Not_found -> Bitvector.empty
+ StringMap.fold (fun r tups si -> (r,Tuples.cardinal tups)::si)
+ struc.relations []
+
(* Return the list of relation tuples incident to an element [e] in [struc]. *)
let incident struc e =
let acc_incident rname inc_map acc =
let tps = TIntMap.find e inc_map in
if Tuples.is_empty tps then acc else (rname, Tuples.elements tps) :: acc in
- let acc_inc_pred pred bv acc =
- if Bitvector.get_bit bv e then (pred, [[|e|]]) :: acc else acc in
- StringMap.fold acc_inc_pred struc.predicates
- (StringMap.fold acc_incident struc.incidence [])
+ StringMap.fold acc_incident struc.incidence []
(* Check if a relation holds for a tuple. *)
let check_rel struc rel tp =
- if Array.length tp > 1 then
- try
- let tups = StringMap.find rel struc.relations in
- Tuples.mem tp tups
- with Not_found -> false
- else
- try
- Bitvector.get_bit (StringMap.find rel struc.predicates) tp.(0)
- with Not_found -> false
+ try
+ let tups = StringMap.find rel struc.relations in
+ Tuples.mem tp tups
+ with Not_found -> false
(* Return the value of function [f] on [e] in [struc]. *)
let fun_val struc f e =
@@ -167,9 +146,7 @@
(* Find a relation in a model. *)
let rel_graph relname model =
try StringMap.find relname model.relations
- with Not_found ->
- try tuples_of_bitvec (StringMap.find relname model.predicates)
- with Not_found -> Tuples.empty
+ with Not_found -> Tuples.empty
(* Incidences of a relation in a model. *)
let rel_incidence relname model =
@@ -241,54 +218,53 @@
(* Ensure relation named [rn] exists in [struc], check arity, add the
relation if needed. *)
let add_rel_name rn arity struc =
- if arity = 1 then
- if StringMap.mem rn struc.predicates then struc else
- { struc with rel_signature = StringMap.add rn 1 struc.rel_signature;
- predicates = StringMap.add rn Bitvector.empty struc.predicates; }
+ if StringMap.mem rn struc.relations then
+ let old_arity = StringMap.find rn struc.rel_signature in
+ if arity <> old_arity then
+ raise (Structure_mismatch
+ (Printf.sprintf
+ "arity mismatch for %s: expected %d, given %d"
+ rn old_arity arity));
+ struc
else
- if StringMap.mem rn struc.relations then
- let old_arity = StringMap.find rn struc.rel_signature in
- if arity <> old_arity then
- raise (Structure_mismatch
- (Printf.sprintf "arity mismatch for %s: expected %d, given %d"
- rn old_arity arity));
- struc
- else
- { struc with
- rel_signature = StringMap.add rn arity struc.rel_signature;
- relations = StringMap.add rn Tuples.empty struc.relations;
- incidence = StringMap.add rn TIntMap.empty struc.incidence; }
+ { struc with
+ rel_signature = StringMap.add rn arity struc.rel_signature;
+ relations = StringMap.add rn Tuples.empty struc.relations;
+ incidence = StringMap.add rn TIntMap.empty struc.incidence; }
let empty_with_signat signat =
- List.fold_right (fun (rn, ar) -> add_rel_name rn ar) signat
+ List.fold_right (fun (rn,ar) -> add_rel_name rn ar) signat
(empty_structure ())
+(* Add empty relation named [rn] to [struc], with given arity,
+ regardless of whether it already existed. *)
+let force_add_rel_name rn arity struc =
+ { struc with
+ rel_signature = StringMap.add rn arity struc.rel_signature;
+ relations = StringMap.add rn Tuples.empty struc.relations;
+ incidence = StringMap.add rn TIntMap.empty struc.incidence; }
+
(* Add tuple [tp] to relation [rn] in structure [struc]. *)
let add_rel struc rn tp =
let new_struc =
Array.fold_left (fun struc e -> add_elem struc e)
(add_rel_name rn (Array.length tp) struc) tp in
- if Array.length tp = 1 then (
- let b = StringMap.find rn new_struc.predicates in
- let np = StringMap.add rn (Bitvector.set_bit b tp.(0)) new_struc.predicates
- in { new_struc with predicates = np; }
- ) else
- let add_to_relmap rmap =
- let tps = StringMap.find rn rmap in
- StringMap.add rn (Tuples.add tp tps) rmap in
- let new_rel = add_to_relmap new_struc.relations in
- let add_to_imap imap e =
- try
- TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
- with Not_found ->
- TIntMap.add e (Tuples.singleton tp) imap in
- let new_incidence_imap =
- try
- Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
- with Not_found ->
- Array.fold_left add_to_imap TIntMap.empty tp in
- let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence
- in { new_struc with relations = new_rel ; incidence = new_incidence }
+ let add_to_relmap rmap =
+ let tps = StringMap.find rn rmap in
+ StringMap.add rn (Tuples.add tp tps) rmap in
+ let new_rel = add_to_relmap new_struc.relations in
+ let add_to_imap imap e =
+ try
+ TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
+ with Not_found ->
+ TIntMap.add e (Tuples.singleton tp) imap in
+ let new_incidence_imap =
+ try
+ Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
+ with Not_found ->
+ Array.fold_left add_to_imap TIntMap.empty tp in
+ let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in
+ { new_struc with relations = new_rel ; incidence = new_incidence }
(* Add tuple [tp] to relation [rn] in structure [struc]. *)
let add_rel_named_elems struc rn tp =
@@ -298,31 +274,26 @@
struc, e::tp) tp
((add_rel_name rn (Array.length tp) struc), []) in
let tp = Array.of_list tp in
- if Array.length tp = 1 then (
- let b = StringMap.find rn new_struc.predicates in
- let np = StringMap.add rn (Bitvector.set_bit b tp.(0)) new_struc.predicates
- in { new_struc with predicates = np; }
- ) else
- let add_to_relmap rmap =
- let tps = StringMap.find rn rmap in
- StringMap.add rn (Tuples.add tp tps) rmap in
- let new_rel = add_to_relmap new_struc.relations in
- let add_to_imap imap e =
- try
- TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
- with Not_found ->
- TIntMap.add e (Tuples.singleton tp) imap in
- let new_incidence_imap =
- try
- Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
- with Not_found ->
- Array.fold_left add_to_imap TIntMap.empty tp in
- let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence
- in { new_struc with relations = new_rel ; incidence = new_incidence }
+ let add_to_relmap rmap =
+ let tps = StringMap.find rn rmap in
+ StringMap.add rn (Tuples.add tp tps) rmap in
+ let new_rel = add_to_relmap new_struc.relations in
+ let add_to_imap imap e =
+ try
+ TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
+ with Not_found ->
+ TIntMap.add e (Tuples.singleton tp) imap in
+ let new_incidence_imap =
+ try
+ Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
+ with Not_found ->
+ Array.fold_left add_to_imap TIntMap.empty tp in
+ let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in
+ { new_struc with relations = new_rel ; incidence = new_incidence }
-(* Return a structure with a single relation, over a single tuple,
- of different elements. *)
+(* Return a structure with a single relation, over a single tuple, of
+ different elements. *)
let free_for_rel rel arity =
let tup = Array.init arity (fun i->i+1) in
add_rel (empty_structure ()) rel tup
@@ -331,25 +302,20 @@
checking whether it and its elements already exist in the structure
and without checking arity. *)
let unsafe_add_rel struc rn tp =
- if Array.length tp = 1 then (
- let b = StringMap.find rn struc.predicates in
- let np = StringMap.add rn (Bitvector.set_bit b tp.(0)) struc.predicates
- in { struc with predicates = np; }
- ) else
- let new_rel =
+ let new_rel =
let tps = StringMap.find rn struc.relations in
StringMap.add rn (Tuples.add tp tps) struc.relations in
- let add_to_imap imap e =
- try
- TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
- with Not_found ->
- TIntMap.add e (Tuples.singleton tp) imap in
- let new_incidence_imap =
- try
- Array.fold_left add_to_imap (StringMap.find rn struc.incidence) tp
- with Not_found ->
- Array.fold_left add_to_imap TIntMap.empty tp in
- let new_incidence = StringMap.add rn new_incidence_imap struc.incidence in
+ let add_to_imap imap e =
+ try
+ TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
+ with Not_found ->
+ TIntMap.add e (Tuples.singleton tp) imap in
+ let new_incidence_imap =
+ try
+ Array.fold_left add_to_imap (StringMap.find rn struc.incidence) tp
+ with Not_found ->
+ Array.fold_left add_to_imap TIntMap.empty tp in
+ let new_incidence = StringMap.add rn new_incidence_imap struc.incidence in
{ struc with relations = new_rel ; incidence = new_incidence }
@@ -441,22 +407,17 @@
(* Remove the tuple [tp] from relation [rn] in structure [struc]. *)
let del_rel struc rn tp =
- if Array.length tp = 1 then (
- let b = StringMap.find rn struc.predicates in
- let np = StringMap.add rn (Bitvector.clear_bit b tp.(0)) struc.predicates
- in { struc with predicates = np; }
- ) else
- let del_rmap rmap =
- try StringMap.add rn (Tuples.remove tp (StringMap.find rn rmap)) rmap
- with Not_found -> rmap in
- let new_rel = del_rmap struc.relations in
- let del_imap imap e =
- try TIntMap.add e (Tuples.remove tp (TIntMap.find e imap)) imap
- with Not_found -> imap in
- let new_incidence =
- let imap=Array.fold_left del_imap (StringMap.find rn struc.incidence) tp
- in StringMap.add rn imap struc.incidence in
- { struc with relations = new_rel ; incidence = new_incidence }
+ let del_rmap rmap =
+ try StringMap.add rn (Tuples.remove tp (StringMap.find rn rmap)) rmap
+ with Not_found -> rmap in
+ let new_rel = del_rmap struc.relations in
+ let del_imap imap e =
+ try TIntMap.add e (Tuples.remove tp (TIntMap.find e imap)) imap
+ with Not_found -> imap in
+ let new_incidence =
+ let imap=Array.fold_left del_imap (StringMap.find rn struc.incidence) tp in
+ StringMap.add rn imap struc.incidence in
+ { struc with relations = new_rel ; incidence = new_incidence }
(* Remove the tuples [tps] from relation [rn] in structure [struc]. *)
let del_rels struc rn tps =
@@ -464,24 +425,26 @@
(* Remove the given relation [rn] in [struc]. *)
let clear_rel remove_from_sig struc rn =
- let new_rel_sig = if remove_from_sig then
+ let new_rels = StringMap.remove rn struc.relations in
+ let new_inc = StringMap.remove rn struc.incidence in
+ let new_rel_sig =
+ if remove_from_sig then
StringMap.remove rn struc.rel_signature
else struc.rel_signature in
- if StringMap.find rn struc.rel_signature = 1 then
- let np = StringMap.remove rn struc.predicates in
- { struc with predicates = np; rel_signature = new_rel_sig }
- else
- let new_rels = StringMap.remove rn struc.relations in
- let new_inc = StringMap.remove rn struc.incidence in
- { struc with relations = new_rels ; incidence = new_inc ;
- rel_signature = new_rel_sig }
+ { struc with relations = new_rels ; incidence = new_inc ;
+ rel_signature = new_rel_sig }
(* Remove all relations that meet predicate [p] in [struc]. *)
let clear_rels ?(remove_from_sig=true) struc p =
let p_rels = ref [] in
let _ = StringMap.iter (fun r _ -> if p r then p_rels := r :: !p_rels)
- struc.rel_signature in
+ struc.relations in
List.fold_left (clear_rel remove_from_sig) struc !p_rels
+(* {struc with
+ relations = StringMap.mapi (fun rel tups ->
+ if p rel then Tuples.empty else tups) struc.relations;
+ incidence = StringMap.mapi (fun rel inctups ->
+ if p rel then IntMap.empty else inctups) struc.incidence} *)
(* Remove the element [e] and all incident relation tuples from [struc]. *)
let del_elem struc e =
@@ -489,8 +452,8 @@
let del_rels_struc =
List.fold_left (fun s (rn, tps) -> del_rels s rn tps) struc rel_tuples in
let del_fun fmap = IntMap.remove e fmap in
- { del_rels_struc with elements = Elems.remove e del_rels_struc.elements ;
- functions = StringMap.map del_fun del_rels_struc.functions ; }
+ { del_rels_struc with elements = Elems.remove e del_rels_struc.elements ;
+ functions = StringMap.map del_fun del_rels_struc.functions ; }
(* Remove the elements [es] and all incident relation tuples from
[struc]; return the deleted relation tuples. *)
@@ -606,10 +569,10 @@
(fun rn ts ->
if show_empty || not (Tuples.is_empty ts) then
rel_s := !rel_s ^ "; " ^ rel_str struc rn ts)
- (relations struc);
+ struc.relations;
StringMap.iter
(fun fn vals -> fun_s := !fun_s ^ "; " ^ fun_str struc fn vals)
- (functions struc);
+ struc.functions;
"[" ^ elem_s ^ " | " ^ (omit 2 !rel_s) ^ " | " ^ (omit 2 !fun_s) ^ "]"
(** {2 Printing of rectangular boards.}
@@ -1001,8 +964,17 @@
let tup = [|elem|] in
let predicates = List.filter
(fun pred ->
- try Tuples.mem tup (StringMap.find pred (relations !ret))
- with Not_found -> false) all_predicates in
+ let tmap =
+ try StringMap.find pred !ret.relations
+ with Not_found -> Tuples.empty in
+ Tuples.mem tup tmap &&
+ let rmap =
+ try StringMap.find pred !ret.incidence
+ with Not_found -> TIntMap.empty in
+ not (Tuples.is_empty (
+ try TIntMap.find elem rmap
+ with Not_found -> Tuples.empty)))
+ all_predicates in
let up_line = String.make 3 ' '
and lo_line = String.make 3 ' ' in
if kind = `Plain then
@@ -1074,16 +1046,16 @@
else struc
with Not_found -> struc in
ret := List.fold_left clear_empty !ret ["x"; "y"; "vx"; "vy"];
- (* relations that are in the structure for the sake of
- signature, i.e. they're empty *)
+ (* relations that are in the structure for the sake of
+ signature, i.e. they're empty *)
let signat_rels =
StringMap.fold (fun rel tups acc ->
if Tuples.is_empty tups then rel::acc else acc)
- (relations struc) [] in
+ struc.relations [] in
ret := clear_rels !ret (fun rel ->
not (List.mem rel signat_rels) &&
(try List.assoc rel uniq_long = rel with Not_found -> true) &&
- try Tuples.is_empty (StringMap.find rel (relations !ret))
+ try Tuples.is_empty (StringMap.find rel !ret.relations)
with Not_found -> true);
span_rels ^ init_pos ^ dx_dy ^ "\"\n" ^
board ^ "\"",
@@ -1119,7 +1091,7 @@
StringMap.fold (fun k v acc ->
if show_empty || not (Tuples.is_empty v) then
(k,v)::acc
- else acc) (relations struc) [] in
+ else acc) struc.relations [] in
let funs =
StringMap.fold (fun k v acc -> (k,v)::acc) struc.functions [] in
let rels = List.rev rels and funs = List.rev funs in
@@ -1169,9 +1141,8 @@
with Not_found -> raise (Diff_result (
"Element "^name^" not found in the "^other^" structure")) in
Elems.iter (fun e -> ignore (map_elem e)) s1.elements;
- let s2_relations = relations s2 in
StringMap.iter (fun rel tups ->
- (let try tups2 = StringMap.find rel s2_relations in
+ (let try tups2 = StringMap.find rel s2.relations in
Tuples.iter (fun tup ->
let tup2 = Array.map map_elem tup in
if not (Tuples.mem tup2 tups2)
@@ -1184,7 +1155,7 @@
) tups
with Not_found -> raise (Diff_result (
"Relation "^rel^" not found in the "^other^" structure"))
- )) (relations s1);
+ )) s1.relations;
StringMap.iter (fun fn vals ->
(let try vals2 = StringMap.find fn s2.functions in
IntMap.iter (fun e v ->
@@ -1214,13 +1185,8 @@
let diff_elems s1 s2 =
let rels, _ = List.split (rel_signature s1) in
let elems = Elems.elements s1.elements in
- let inc s r e =
- try TIntMap.find e (StringMap.find r s.incidence) with Not_found ->
- try
- if Bitvector.get_bit (StringMap.find r s.predicates) e then
- Tuples.singleton [|e|]
- else Tuples.empty
- with Not_found -> Tuples.empty in
+ let inc s r e = try TIntMap.find e (StringMap.find r s.incidence) with
+ Not_found -> Tuples.empty in
let diff_elem_rel e r = not (Tuples.equal (inc s1 r e) (inc s2 r e)) in
let diff_rels e = (e, List.filter (diff_elem_rel e) rels) in
List.filter (fun (_, rs) -> rs <> []) (List.rev_map diff_rels elems)
@@ -1233,13 +1199,12 @@
try
Tuples.equal (StringMap.find rel map) tp
with Not_found -> false in
- let s1_relations, s2_relations = relations s1, relations s2 in
- let is_eq_in1, is_eq_in2 = is_eq_in s1_relations, is_eq_in s2_relations in
+ let is_eq_in1, is_eq_in2 = is_eq_in s1.relations, is_eq_in s2.relations in
let diffrels = ref [] in
let appdiff1 r tp = if not (is_eq_in1 r tp) then diffrels := r::!diffrels in
let appdiff2 r tp = if not (is_eq_in2 r tp) then diffrels := r::!diffrels in
- StringMap.iter appdiff1 s2_relations;
- StringMap.iter appdiff2 s1_relations;
+ StringMap.iter appdiff1 s2.relations;
+ StringMap.iter appdiff2 s1.relations;
LOG 2 "SOME DIFF: %s" (String.concat ", " !diffrels);
Some (Aux.unique_sorted !diffrels)
else None
Modified: trunk/Toss/Solver/Structure.mli
===================================================================
--- trunk/Toss/Solver/Structure.mli 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Solver/Structure.mli 2012-03-08 20:18:20 UTC (rev 1685)
@@ -45,8 +45,6 @@
(** Functions in the structure. *)
val functions : structure -> (float IntMap.t) StringMap.t
-(** The bitvector for a given predicate. *)
-val pred_vector : structure -> string -> Bitvector.bitvector
(** {3 Elements and their names.} *)
Modified: trunk/Toss/Solver/StructureTest.ml
===================================================================
--- trunk/Toss/Solver/StructureTest.ml 2012-03-08 01:17:02 UTC (rev 1684)
+++ trunk/Toss/Solver/StructureTest.ml 2012-03-08 20:18:20 UTC (rev 1685)
@@ -69,7 +69,7 @@
test_incident "[a, b | R (a, b) | ]"
["R {(a, b)}"; "R {(a, b)}"];
test_incident "[a, b | R { (a, b) }; P { a } | ]"
- ["P {(a)}; R {(a, b)}"; "R {(a, b)}"];
+ ["R {(a, b)}; P {(a)}"; "R {(a, b)}"];
);
"del" >::
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
