[Toss-devel-svn] SF.net SVN: toss:[1187] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1187] trunk/Toss
|
From: <luk...@us...> - 2010-11-21 20:45:53
|
Revision: 1187
http://toss.svn.sourceforge.net/toss/?rev=1187&view=rev
Author: lukstafi
Date: 2010-11-21 20:45:43 +0000 (Sun, 21 Nov 2010)
Log Message:
-----------
Cleanup of Aux: removed unused functions, some functions used once moved to their use site. AuxTest test suite.
Modified Paths:
--------------
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/FFTNF.ml
trunk/Toss/Play/Game.ml
trunk/Toss/Play/Heuristic.ml
trunk/Toss/Solver/AssignmentSet.ml
trunk/Toss/Solver/Assignments.ml
trunk/Toss/Solver/FFSolver.ml
trunk/Toss/Solver/Structure.ml
trunk/Toss/TossTest.ml
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Arena/DiscreteRule.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -209,10 +209,7 @@
let enumerate_matchings model rule matches =
let all_elems = Structure.Elems.elements model.Structure.elements in
let assgns =
- (* Aux.drop_repeating (
- List.sort Pervasives.compare ( *)
- enumerate_assgns all_elems rule.lhs_elem_vars matches
- (* )) *) in
+ enumerate_assgns all_elems rule.lhs_elem_vars matches in
List.map (assignment_to_embedding rule) assgns
(* Helpers for special relations. *)
@@ -228,6 +225,12 @@
Some (String.sub rel 1 (String.index_from rel 1 '_' - 1))
with Not_found -> None
+(* Return the result of the first index [i] that passes the
+ given test, and [i+1]. *)
+let rec first_i n gen test =
+ let res = gen n in
+ if test res then n+1, res else first_i (n+1) gen test
+
(* Rewrite the model [given_model], allowing the elements to be
cloned and deleted. Also change the "trace" of rewritten
elements.
@@ -251,7 +254,7 @@
let _, alloc_elems, rmmap =
List.fold_left (fun (next, alloc_elems, rmmap) evar ->
let next, nelem =
- Aux.first_i next (fun i->i) (fun i-> not (Els.mem i elems)) in
+ first_i next (fun i->i) (fun i-> not (Els.mem i elems)) in
next, nelem::alloc_elems, (evar, nelem)::rmmap)
(1, [], []) rule_obj.rhs_elem_vars in
(* Select a nice name in case elements in the model are named. In
@@ -470,6 +473,44 @@
module STups = Structure.Tuples
+(** Return the nth dimensional "triangle matrix", as the set of [n]
+ element subsets of [l]. *)
+let triang_product n l =
+ let rec mult1 = function
+ | [],[] -> []
+ | [_],[_] -> []
+ | e::es,(_::rs) -> List.map (fun r->e::r) rs::mult1 (es, rs)
+ | _ -> failwith "triang_product: impossible" in
+ let rec mult2 = function
+ (*| [],[] -> []*)
+ | [_],[] -> []
+ | [_;_],[_] -> []
+ | e::es,(_::rs) -> List.map (List.map (fun r->e::r)) rs::mult2 (es, rs)
+ | _ -> failwith "triang_product: impossible" in
+ let rec multn = function
+ | _,[] -> []
+ | _,[_] -> []
+ | _,[_;[[]]] -> []
+ | e::es,(_::rs) ->
+ List.map (concat_map (List.map (fun r->e::r))) rs::multn (es, rs)
+ | _ -> failwith "triang_product: impossible" in
+ let ls = List.map (fun e->[e]) l in
+ match n with
+ | 0 -> []
+ | 1 -> ls
+ | 2 -> List.flatten (mult1 (l,ls))
+ | 3 ->
+ let lls = mult1 (l,ls) in
+ List.flatten (List.flatten (mult2 (l,lls)))
+ | n ->
+ let rec aux n acc =
+ if n=0 then acc
+ else aux (n-1) (multn (l,acc)) in
+ let lls = mult1 (l,ls) in
+ let llls = mult2 (l,lls) in
+ List.flatten (List.flatten (aux (n-3) llls))
+
+
(** Translate a rule specification into a processed form. Note that
when a relation is in $\tau_h$, and is present in the LHS but not
in the RHS, it is still not removed by a rewrite.
@@ -598,8 +639,8 @@
(* check if the map is a total 1-1 onto, if so, [rlmap=None], optimize *)
let rlmap =
let rimg, ldom = List.split rule_src.rule_s in
- let rimg = Aux.drop_repeating (List.sort Pervasives.compare rimg)
- and ldom = Aux.drop_repeating (List.sort Pervasives.compare ldom) in
+ let rimg = Aux.unique (=) rimg
+ and ldom = Aux.unique (=) ldom in
let nimg = List.length rimg and ndom = List.length ldom in
if nimg = Els.cardinal rule_src.rhs_struc.Structure.elements &&
ndom = Els.cardinal rule_src.lhs_struc.Structure.elements &&
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Formula/Aux.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -30,15 +30,6 @@
in
List.rev (maps_f [] l)
-let rec map_some2 f l1 l2 =
- match (l1, l2) with
- ([], []) -> []
- | (a1::l1, a2::l2) ->
- (match f a1 a2 with
- | None -> map_some2 f l1 l2
- | Some r -> r :: map_some2 f l1 l2)
- | (_, _) -> invalid_arg "map_some2"
-
let map_reduce mapf redf red0 l =
match List.sort (fun x y -> compare (fst x) (fst y))
(List.map mapf l) with
@@ -50,38 +41,19 @@
List.rev (List.map (fun (k,vs) -> k, List.fold_left redf red0 vs)
((k0,vs)::l))
-let rec drop_repeating = function
- | hd::(nk::tl as rest) when hd = nk -> drop_repeating rest
- | hd::tl -> hd::drop_repeating tl
- | tl -> tl
-
-let rec has_repeating = function
- | [] -> false
- | hd::tl when List.mem hd tl -> true
- | hd::tl -> has_repeating tl
-
let list_remove v l = List.filter (fun w->v<>w) l
-let list_existsi p l =
- let rec aux i = function
- | [] -> false
- | a::l -> p i a || aux (i+1) l in
- aux 0 l
-
let rec rev_assoc l x = match l with
[] -> raise Not_found
- | (a,b)::l -> if compare b x = 0 then a else rev_assoc l x
+ | (a,b)::l -> if b = x then a else rev_assoc l x
let rev_assoc_all l x =
let rec aux acc = function
| [] -> acc
| (a,b)::l ->
- if compare b x = 0 then aux (a::acc) l else aux acc l in
+ if b = x then aux (a::acc) l else aux acc l in
aux [] l
-let replace_assoc k v l =
- (k, v)::(List.remove_assoc k l)
-
let rec replace_assoc k v = function
| [] -> [k, v]
| (a, b as pair) :: l ->
@@ -95,53 +67,10 @@
else aux (pair :: acc) l in
aux [] l
-
-let find_max cmp l =
- let rec find acc = function
- | hd::tl ->
- if cmp hd acc <= 0 then find acc tl
- else find hd tl
- | [] -> acc in
- match l with
- | [] -> invalid_arg "find_max: empty list"
- | hd::tl -> find hd tl
-
-let find_all_max cmp l =
- let rec find best acc = function
- | hd::tl ->
- let rel = cmp hd best in
- if rel < 0 then find best acc tl
- else if rel = 0 then find best (hd::acc) tl
- else find hd [hd] tl
- | [] -> acc in
- match l with
- | [] -> invalid_arg "find_all_max: empty list"
- | hd::tl -> find hd [hd] tl
-
-let insert_ordered cmp e l =
- let rec aux = function
- | [] -> [e]
- | hd::_ as l when cmp e hd <= 0 -> e::l
- | hd::tl -> hd::aux tl in
- aux l
-
let unsome = function
| Some v -> v
| None -> raise (Invalid_argument "unsome")
-let rev_map_choose f l =
- let rec rmap_f accu = function
- | [] -> None, accu, []
- | a::tl ->
- match f a with
- | Left r -> rmap_f (r :: accu) tl
- | Right r -> Some r, accu, tl in
- rmap_f [] l
-
-let rec try_find f = function
- | [] -> raise Not_found
- | hd::tl -> try f hd with Not_found -> try_find f tl
-
let rec map_try f = function
| [] -> []
| hd::tl ->
@@ -155,75 +84,21 @@
concat_map (fun el -> List.map (fun tup -> el::tup) prod) set)
l [[]]
-let gproduct f r0 l =
- List.fold_right (fun set prod ->
- concat_map (fun el -> List.map (fun tup -> f el tup) prod) set)
- l [r0]
+let all_tuples_for args elems =
+ List.fold_left (fun tups _ ->
+ concat_map (fun e -> (List.map (fun tup -> e::tup) tups))
+ elems) [[]] args
-let triang_product n l =
- let rec mult1 = function
- | [],[] -> []
- | [_],[_] -> []
- | e::es,(_::rs) -> List.map (fun r->e::r) rs::mult1 (es, rs)
- | _ -> failwith "triang_product: impossible" in
- let rec mult2 = function
- (*| [],[] -> []*)
- | [_],[] -> []
- | [_;_],[_] -> []
- | e::es,(_::rs) -> List.map (List.map (fun r->e::r)) rs::mult2 (es, rs)
- | _ -> failwith "triang_product: impossible" in
- let rec multn = function
- | _,[] -> []
- | _,[_] -> []
- | _,[_;[[]]] -> []
- | e::es,(_::rs) ->
- List.map (concat_map (List.map (fun r->e::r))) rs::multn (es, rs)
- | _ -> failwith "triang_product: impossible" in
- let ls = List.map (fun e->[e]) l in
- match n with
- | 0 -> []
- | 1 -> ls
- | 2 -> List.flatten (mult1 (l,ls))
- | 3 ->
- let lls = mult1 (l,ls) in
- List.flatten (List.flatten (mult2 (l,lls)))
- | n ->
- let rec aux n acc =
- if n=0 then acc
- else aux (n-1) (multn (l,acc)) in
- let lls = mult1 (l,ls) in
- let llls = mult2 (l,lls) in
- List.flatten (List.flatten (aux (n-3) llls))
-
let rec remove_one e = function
| hd::tl when hd = e -> tl
| hd::tl -> hd::(remove_one e tl)
| [] -> []
-let rec remove_nth n = function
- | [] -> invalid_arg "remove_nth"
- | hd::tl when n<=0 -> tl
- | hd::tl -> hd::(remove_nth (n-1) tl)
+let rec insert_nth n e = function
+ | l when n<=0 -> e::l
+ | [] -> raise Not_found
+ | hd::tl -> hd::(insert_nth (n-1) e tl)
-
-let rec extract_nth n = function
- | [] -> invalid_arg "extract_nth"
- | hd::tl when n<=0 -> hd, tl
- | hd::tl ->
- let e, tl = extract_nth (n-1) tl in
- e, hd::tl
-
-let rec replace_nth n e = function
- | [] -> invalid_arg "replace_nth"
- | hd::tl when n<=0 -> e::tl
- | hd::tl -> hd::(replace_nth (n-1) e tl)
-
-
-let rec add_nth n e = function
- | [] -> [e]
- | hd::tl when n<=0 -> e::hd::tl
- | hd::tl -> hd::(add_nth (n-1) e tl)
-
let find_index v l =
let rec aux n = function
| [] -> raise Not_found
@@ -231,20 +106,6 @@
| _::tl -> aux (n+1) tl in
aux 0 l
-let sample n l =
- let s = List.length l in
- let rec samp n =
- if n=0 then []
- else (List.nth l (Random.int s))::samp (n-1) in
- samp n
-
-let rec first_i n gen test =
- let res = gen n in
- if test res then n+1, res else first_i (n+1) gen test
-
-let rec map_for b n f =
- if b < n then (f b)::(map_for (b+1) n f) else []
-
let maximal cmp l =
let rec aux acc = function
| hd::tl when
@@ -257,13 +118,10 @@
(* TODO: that's quadratic, perhaps (sort |> drop_repeating)
would be faster in practice *)
-let unique cmp l =
- let rec aux acc = function
- | hd::tl when not (List.exists (fun x->cmp hd x) acc) ->
- aux (hd::acc) tl
- | hd::tl -> aux acc tl
- | [] -> acc in
- List.rev (aux [] l)
+let rec unique eq = function
+ | [] -> []
+ | x :: xs ->
+ x :: unique eq (List.filter (fun y -> not (eq y x)) xs)
let take_n n l =
let rec aux n acc = function
@@ -272,36 +130,6 @@
| _ -> acc in
List.rev (aux n [] l)
-let take_n_unique n l =
- let rec aux n acc = function
- | hd::tl when n > 0 && not (List.mem hd acc) ->
- aux (n-1) (hd::acc) tl
- | hd::tl when n > 0 -> aux n acc tl
- | _ -> acc in
- List.rev (aux n [] l)
-
-let concat_unique ls =
- let rec conc acc = function
- | [] -> acc
- | []::rest -> conc acc rest
- | (hd::tl)::rest when List.mem hd acc -> conc acc (tl::rest)
- | (hd::tl)::rest -> conc (hd::acc) (tl::rest) in
- List.rev (conc [] ls)
-
-let prefix_free ls =
- let rec prefix = function
- | [],[] -> false
- | [],_ -> true
- | hd1::tl1, hd2::tl2 when hd1=hd2 -> prefix (tl1,tl2)
- | _ -> false in
- let rec aux acc = function
- | hd::tl when not (List.exists (fun x->hd=x) acc) &&
- not (List.exists (fun l2->prefix (l2,hd)) ls) ->
- aux (hd::acc) tl
- | hd::tl -> aux acc tl
- | [] -> acc in
- List.rev (aux [] ls)
-
let array_map2 f a b =
let l = Array.length a in
if l <> Array.length b then
@@ -317,58 +145,9 @@
r
end
-let array_mapi2 f a b =
- let l = Array.length a in
- if l <> Array.length b then
- raise (Invalid_argument "Aux.array_mapi2")
- else
- if l = 0 then [||] else begin
- let r = Array.create l
- (f 0 (Array.unsafe_get a 0) (Array.unsafe_get b 0)) in
- for i = 1 to l - 1 do
- Array.unsafe_set r i
- (f i (Array.unsafe_get a i) (Array.unsafe_get b i))
- done;
- r
- end
-
-let array_fold_map f acc a =
- let l = Array.length a in
- if l = 0 then acc, [||] else begin
- let acc, e = f acc (Array.unsafe_get a 0) in
- let prev = ref acc in
- let r = Array.create l e in
- for i = 1 to l - 1 do
- let acc, e = f !prev (Array.unsafe_get a i) in
- prev := acc;
- Array.unsafe_set r i e
- done;
- !prev, r
- end
-
let array_combine a b =
- let l = Array.length a in
- if l <> Array.length b then
- raise (Invalid_argument "Aux.array_combine")
- else
- if l = 0 then [||] else begin
- let r = Array.create l
- (Array.unsafe_get a 0, Array.unsafe_get b 0) in
- for i = 1 to l - 1 do
- Array.unsafe_set r i
- (Array.unsafe_get a i, Array.unsafe_get b i)
- done;
- r
- end
+ array_map2 (fun x y->x,y) a b
-let array_exists p a =
- let res = ref false in
- let i = ref 0 in
- while !i < Array.length a && not !res do
- res := p (Array.unsafe_get a !i);
- incr i
- done; !res
-
let array_existsi p a =
let res = ref false in
let i = ref 0 in
@@ -378,7 +157,7 @@
done; !res
let array_mem e a =
- array_exists (fun x -> e=x) a
+ array_existsi (fun _ x -> e=x) a
let array_from_assoc l =
match l with
@@ -401,54 +180,6 @@
| hd::tl -> Array.unsafe_set a i (f hd); fill (i+1) tl in
fill 1 tl
-(* Same as [Array.of_list (List.concat (List.map (fun x-> List.map (g
- x) (f x)) l))] *)
-let array_concat_map_of_list f g = function
- [] -> [||]
- | hd::tl as l ->
- let ls = List.map f l in
- let len =
- List.fold_left (fun acc l->acc + List.length l) 0 ls in
- if len = 0 then [||] else
- let org = ref l in
- let rec seek = function
- | [] -> assert false
- | []::tl -> org := List.tl !org; seek tl
- | (hd::_)::_ -> hd in
- let e = seek ls in
- let a = Array.make len (g (List.hd !org) e) in
- let hd = ref (List.hd ls) and tl = ref (List.tl ls) in
- while !hd=[] do
- hd := List.hd !tl; tl := List.tl !tl
- done;
- let e = ref (List.hd !org) in
- hd := List.tl !hd;
- for i=1 to len-1 do
- while !hd=[] do
- hd := List.hd !tl; tl := List.tl !tl;
- org := List.tl !org; e := List.hd !org
- done;
- Array.unsafe_set a i (g !e (List.hd !hd));
- hd := List.tl !hd
- done;
- a
-
-let array_fold_while p f x a =
- let r = ref x and i = ref 0 in
- let n = Array.length a in
- while !i < n && p (Array.unsafe_get a !i) do
- r := f !r (Array.unsafe_get a !i); incr i
- done;
- !r
-
-let array_find f a =
- let i = ref 0 in
- let n = Array.length a in
- while !i < n && not (f (Array.unsafe_get a !i)) do
- incr i done;
- if !i >= n then raise Not_found
- else Array.unsafe_get a !i
-
let array_argfind f a =
let i = ref 0 in
let n = Array.length a in
@@ -473,37 +204,6 @@
done;
!r
-let array_for_all f a =
- try
- for i = 0 to Array.length a - 1 do
- if not (f (Array.unsafe_get a i)) then
- raise Not_found
- done;
- true
- with Not_found -> false
-
-let array_for_all2 f a b =
- let len = min (Array.length a) (Array.length b) in
- try
- for i = 0 to len - 1 do
- if not (f (Array.unsafe_get a i) (Array.unsafe_get b i)) then
- raise Not_found
- done;
- true
- with Not_found -> false
-
-let array_argfind_max cmp a =
- let n = Array.length a in
- if n=0 then failwith "array_argfind_max: empty array"
- else
- let best = ref (Array.unsafe_get a 0)
- and besti = ref 0 in
- for i = 1 to n-1 do
- let e = Array.unsafe_get a i in
- if cmp e !best > 0 then (best := e; besti := i)
- done;
- !besti
-
let array_argfind_all_max cmp a =
let n = Array.length a in
if n=0 then []
@@ -517,12 +217,34 @@
else if res = 0 then besti := i:: !besti
done;
!besti
+
+let array_for_all f a =
+ try
+ for i = 0 to Array.length a - 1 do
+ if not (f (Array.unsafe_get a i)) then
+ raise Not_found
+ done;
+ true
+ with Not_found -> false
+let array_for_all2 f a b =
+ let len = Array.length a in
+ if len <> Array.length b then
+ raise (Invalid_argument "Aux.array_for_all2")
+ else
+ try
+ for i = 0 to len - 1 do
+ if not (f (Array.unsafe_get a i) (Array.unsafe_get b i)) then
+ raise Not_found
+ done;
+ true
+ with Not_found -> false
+
let neg f x = not (f x)
let partition_choice l =
let rec split laux raux = function
- | [] -> laux, raux
+ | [] -> List.rev laux, List.rev raux
| Left e::tl -> split (e::laux) raux tl
| Right e::tl -> split laux (e::raux) tl in
split [] [] l
@@ -536,11 +258,6 @@
| Right e -> split laux (e::raux) tl in
split [] [] l
-let rec split_triples = function
- [] -> ([], [], [])
- | (x,y,z)::l ->
- let (rx, ry, rz) = split_triples l in (x::rx, y::ry, z::rz)
-
let transpose_lists lls =
let rec aux acc = function
| [] -> List.map List.rev acc
@@ -551,28 +268,17 @@
| hd::tl ->
aux (List.map (fun e->[e]) hd) tl
-let all_tuples_for args elems =
- List.fold_left (fun tups _ ->
- concat_map (fun e -> (List.map (fun tup -> e::tup) tups))
- elems) [[]] args
-
let rec fold_n f accu n =
if n <= 0 then accu
else fold_n f (f accu) (n-1)
-let rec foldi_n f accu n =
- let accu = ref accu in
- for i=1 to n do
- accu := f i !accu
- done; !accu
+(* Return the result of the first index [i] that passes the
+ given test, and [i+1]. *)
+let rec first_i n gen test =
+ let res = gen n in
+ if test res then n+1, res else first_i (n+1) gen test
-let all_tuples_n arity elems =
- fold_n (fun tups ->
- concat_map (fun e -> (List.map (fun tup -> e::tup) tups))
- elems) [[]] arity
-
-
let new_filename basename suffix =
if not (Sys.file_exists (basename^suffix))
then basename^suffix else
@@ -585,34 +291,13 @@
snd (first_i 0 (fun i -> s^(string_of_int i))
(fun v -> not (Strings.mem v names)))
-let not_conflicting_name_cands names cands =
- let _ = if cands = [] then
- failwith "not_conflicting_name: no candidates" in
- if List.exists (fun s->not (Strings.mem s names)) cands
- then List.find (fun s->not (Strings.mem s names)) cands
- else
- let ncands = List.map (fun s->
- first_i 0 (fun i -> s^(string_of_int i))
- (fun v -> not (Strings.mem v names))) cands in
- snd (List.hd (List.stable_sort (fun (a,_) (b,_) -> a-b) ncands))
-
let not_conflicting_names s names n =
- snd (List.fold_left (fun (i,res) _ ->
+ List.rev (snd (List.fold_left (fun (i,res) _ ->
let i', v =
first_i i (fun i -> s^(string_of_int i))
(fun v -> not (Strings.mem v names)) in
- i', v::res) (0,[]) n)
+ i', v::res) (0,[]) n))
-let rec split_table columns rows =
- let rec collect = function
- | [], rest -> [], rest
- | hd::tl, e::more ->
- let cols, rest = collect (tl, more) in
- (e::hd)::cols, rest
- | cols, [] -> cols, [] in
- let columns, rest = collect (columns, rows) in
- if rest = [] then columns else split_table columns rest
-
(* Character classes. *)
let is_uppercase c = c >= 'A' && c <= 'Z'
let is_lowercase c = c >= 'a' && c <= 'z'
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Formula/Aux.mli 2010-11-21 20:45:43 UTC (rev 1187)
@@ -15,109 +15,59 @@
(** Map a list filtering out some elements. *)
val map_some : ('a -> 'b option) -> 'a list -> 'b list
-val map_some2 : ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
-
(** Map elements into key-value pairs, and fold values with the same
- key. *)
+ key. Uses {!List.fold_left}, therefore reverses the order. The
+ resulting keys are sorted in the {!Pervasives.compare} order. *)
val map_reduce :
('a -> 'b * 'c) -> ('d -> 'c -> 'd) -> 'd -> 'a list -> ('b * 'd) list
-(** Return a list of unique elements (using structural equality) for a
- *sorted* input list. *)
-val drop_repeating : 'a list -> 'a list
-
-(** Check if an element of a list repeats, using structural
- equality. *)
-val has_repeating : 'a list -> bool
-
(** Remove all elements equal to the argument, using structural
inequality. *)
val list_remove : 'a -> 'a list -> 'a list
-(** Check if at least one element and its position satisfies the predicate. *)
-val list_existsi : (int -> 'a -> bool) -> 'a list -> bool
-
-(** Return first key with the given value from the key-value pairs. *)
+(** Return first key with the given value from the key-value pairs,
+ using structural equality. *)
val rev_assoc : ('a * 'b) list -> 'b -> 'a
-(** Inverse image of an association: return all keys with a given value. *)
+(** Inverse image of an association: return all keys with a given
+ value (using structural equality). Returns elements in reverse order. *)
val rev_assoc_all : ('a * 'b) list -> 'b -> 'a list
-(** Replace the value of a first occurrence of a key. *)
+(** Replace the value of a first occurrence of a key, or place it at
+ the end of the assoc list. *)
val replace_assoc : 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list
(** Find the value associated with the first occurrence of the key and
remove them from the list. *)
val pop_assoc : 'a -> ('a * 'b) list -> 'b * ('a * 'b) list
-(** Find the first maximal element. Comparison is by [cmp a b <= 0]
- iff [a <= b]. *)
-val find_max : ('a -> 'a -> int) -> 'a list -> 'a
-
-(** Find all maximal elements. *)
-val find_all_max : ('a -> 'a -> int) -> 'a list -> 'a list
-
-(** Insert an element (without repeating it) into an
- increasing-ordered list. *)
-val insert_ordered : ('a -> 'a -> int) -> 'a -> 'a list -> 'a list
-
(** unConstructors. *)
val unsome : 'a option -> 'a
-(** Map a prefix of [Left] elements (returned in reverse order) till
- the first [Right] element (if any), also return the unmapped tail
- of the list. *)
-val rev_map_choose :
- ('a -> ('b, 'c) choice) -> 'a list -> 'c option * 'b list * 'a list
-
-(** Find the first result of [f] on [l] that does not raise [Not_found]. *)
-val try_find : ('a -> 'b) -> 'a list -> 'b
-
(** Map [f] on the list collecting results whose computation does not
raise [Not_found]. Therefore [map_try] call cannot raise [Not_found]. *)
val map_try : ('a -> 'b) -> 'a list -> 'b list
-(** Cartesian product of lists. *)
+(** Cartesian product of lists. Not tail recursive. *)
val product : 'a list list -> 'a list list
-(** Generalized product. [product l = gproduct (fun x y->x::y) [] l]. *)
-val gproduct : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
+(** An [n]th cartesian power of the second list, where [n] is the
+ length of the first list. Tail recursive. *)
+val all_tuples_for : 'a list -> 'b list -> 'b list list
-(** Return the nth dimensional "triangle matrix", as the set of [n]
- element subsets of [l]. *)
-val triang_product : int -> 'a list -> 'a list list
-
(** Remove an occurrence of a value (uses structural equality). *)
val remove_one : 'a -> 'a list -> 'a list
-(** Remove [n+1]th element of a list ([n]th counting from zero). *)
-val remove_nth : int -> 'a list -> 'a list
+(** Insert as [n]th element of a list (counting from zero). Raise
+ [Not_found] if the list has less than [n] elements (e.g. inserting
+ 0th element to empty list is OK). *)
+val insert_nth : int -> 'a -> 'a list -> 'a list
-(** At once access an element as by {!List.nth}, and delete as by
- {!remove_nth}. *)
-val extract_nth : int -> 'a list -> 'a * 'a list
-
-(** Replace [n+1]th element of a list ([n]th counting from zero). *)
-val replace_nth : int -> 'a -> 'a list -> 'a list
-
-(** Add as [n]th element of a list (counting from zero). *)
-val add_nth : int -> 'a -> 'a list -> 'a list
-
(** Find the index of the first occurrence of a value in a list,
counting from zero. *)
val find_index : 'a -> 'a list -> int
-(** Sample from a list with repetitions. *)
-val sample : int -> 'a list -> 'a list
-
-(** Return the result of the first index [i] that passes the
- given test, and [i+1]. *)
-val first_i : int -> (int -> 'a) -> ('a -> bool) -> int * 'a
-
-(** Map the numbers [b..n]. *)
-val map_for : int -> int -> (int -> 'a) -> 'a list
-
(** Return the list of maximal elements, under the given less-or-equal
comparison (the input does not need to be sorted). (Currently, of
equal elements only the last one is preserved.) *)
@@ -126,41 +76,26 @@
(** Return the list of unique elements, under the given comparison
(the input does not need to be sorted). (Currently uses a
straightforward [n^2] algorithm, a sorting-based would reduce it to
- [n log n].) *)
+ [n log n]. Currently not tail-recursive.) *)
val unique : ('a -> 'a -> bool) -> 'a list -> 'a list
(** Take [n] elements of the given list, or less it the list does not
contain enough values. *)
val take_n : int -> 'a list -> 'a list
-(** Take [n] nonrepeating elements of the given list, or less it the
- list does not contain enough values. *)
-val take_n_unique : int -> 'a list -> 'a list
-
-(** Concatenate lists without repeating the elements. *)
-val concat_unique : 'a list list -> 'a list
-
-(** All lists from [l] that are not initial parts of other lists from [l]. *)
-val prefix_free : 'a list list -> 'a list list
-
(** Make an array from an association from indices to values. The
indices must cover the [0..length-1] range; raises
- [Invalid_argument] otherwise. *)
+ [Invalid_argument "Aux.array_from_assoc"] otherwise. *)
val array_from_assoc : (int * 'a) list -> 'a array
(** Map a function over two arrays index-wise. Raises
[Invalid_argument] if the arrays are of different lengths. *)
val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
-val array_mapi2 : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
-(** Map a function over an array threading an accumulator. *)
-val array_fold_map :
- ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
-
-(** Zip two arrays into an array of pairs. *)
+(** Zip two arrays into an array of pairs. Raises [Invalid_argument
+ "Aux.array_map2"] if the arrays are of different lengths. *)
val array_combine : 'a array -> 'b array -> ('a * 'b) array
-val array_exists : ('a -> bool) -> 'a array -> bool
val array_existsi : (int -> 'a -> bool) -> 'a array -> bool
val array_mem : 'a -> 'a array -> bool
@@ -168,20 +103,6 @@
(** Same as [Array.of_list (List.map f l)] *)
val array_map_of_list : ('a -> 'b) -> 'a list -> 'b array
-(** Same as [Array.of_list (List.concat (List.map (fun x-> List.map (g
- x) (f x)) l))]. The first function generates the results and the
- second postprocesses them. *)
-val array_concat_map_of_list
- : ('a -> 'b list) -> ('a -> 'b -> 'c) -> 'a list -> 'c array
-
-(** Like {!Array.fold_left}, but only for the initial elements for
- which the predicate holds. *)
-val array_fold_while :
- ('a -> bool) -> ('b -> 'a -> 'b) -> 'b -> 'a array -> 'b
-
-(** Find the first element that satisfies a predicate. Raises [Not_found]. *)
-val array_find : ('a -> bool) -> 'a array -> 'a
-
val array_argfind : ('a -> bool) -> 'a array -> int
(** Find all elements for which [f] holds. *)
@@ -192,12 +113,11 @@
(** Find if a predicate holds for all elements. *)
val array_for_all : ('a -> bool) -> 'a array -> bool
-(** Find if a predicate holds for all elements of two arrays pointwise. *)
+(** Find if a predicate holds for all elements of two arrays
+ pointwise. Raises [Invalid_argument "Aux.array_for_all2"] if
+ arrays are of different lengths. *)
val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
-(** Find the index of the first maximal element in an array. *)
-val array_argfind_max : ('a -> 'a -> int) -> 'a array -> int
-
(** Find indices of all maximal elements in an array. *)
val array_argfind_all_max : ('a -> 'a -> int) -> 'a array -> int list
@@ -212,42 +132,23 @@
also {!partition_choice}). *)
val partition_map : ('a -> ('b, 'c) choice) -> 'a list -> 'b list * 'c list
-(** Transpose a list of triples into a triple of lists. *)
-val split_triples : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
-
-(** Transpose a rectangular matrix represented by lists. *)
+(** Transpose a rectangular matrix represented by lists. Raises
+ [Invalid_argument "List.map2"] when matrix is not rectangular. *)
val transpose_lists : 'a list list -> 'a list list
-(** An [n]th cartesian power of the second list, where [n] is the
- length of the first list. *)
-val all_tuples_for : 'a list -> 'b list -> 'b list list
-
(** Iterate a function [n] times: [f^n(x)]. *)
val fold_n : ('a -> 'a) -> 'a -> int -> 'a
-(** Fold a function over the [1..n] sequence: [f(n,f(...f(1,x)...))]. *)
-val foldi_n : (int -> 'a -> 'a) -> 'a -> int -> 'a
-
-(** An [n]th cartesian power of a list. *)
-val all_tuples_n : int -> 'a list -> 'a list list
-
(** Generate a fresh filename of the form [base ^ n ^ suffix]. *)
val new_filename : string -> string -> string
(** Returns a string proloning [s] and not appearing in [names]. *)
val not_conflicting_name : Strings.t -> string -> string
-(** Returns a string proloning one of [cands] and not appearing in
- [names]. *)
-val not_conflicting_name_cands : Strings.t -> string list -> string
-
(** Returns [n] strings proloning [s] and not appearing in [names]. *)
val not_conflicting_names :
string -> Strings.t -> 'a list -> string list
-(** Collect columns of a table given by concatenation of rows. *)
-val split_table : 'a list list -> 'a list -> 'a list list
-
(** Character classes. *)
val is_uppercase : char -> bool
val is_lowercase : char -> bool
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Formula/BoolFormula.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -261,9 +261,6 @@
then (BOr []) else BAnd (List.map neutral_absorbing filtered) in
let rec singularise unsorted_phi =
let phi = sort unsorted_phi in (* this should be done more elegantly!!! *)
- let rec unique = function (* remove duplicate subformulas *)
- [] -> []
- | x :: xs -> [x] @ (unique (List.filter (fun y -> y<>x) xs)) in
let rec neg_occurrence = function
(* check whether a _sorted_ "uniqued" list contains a pair (phi,not phi)
at the moment this only works for literals due to the implementation of compare! *)
@@ -272,10 +269,10 @@
match phi with
BVar _ -> phi
| BNot psi -> BNot (singularise psi)
- | BOr psis -> let unique_psis = unique psis in
+ | BOr psis -> 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)
- | BAnd psis -> let unique_psis = unique psis in
+ | 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
let rec subsumption phi =
Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Formula/FFTNF.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -1073,6 +1073,18 @@
(* build will flatten the formula *)
evs, build false phi
+(* Map a prefix of [Left] elements (returned in reverse order) till
+ the first [Right] element (if any), also return the unmapped tail
+ of the list. *)
+let rev_map_choose f l =
+ let rec rmap_f accu = function
+ | [] -> None, accu, []
+ | a::tl ->
+ match f a with
+ | Left r -> rmap_f (r :: accu) tl
+ | Right r -> Some r, accu, tl in
+ rmap_f [] l
+
(* Step 4. Search depth-first since it's simpler, perhaps results in less
duplication, and there are no clear advantages of breadth-first. *)
let find_active frels evs t =
Modified: trunk/Toss/Play/Game.ml
===================================================================
--- trunk/Toss/Play/Game.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Play/Game.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -477,6 +477,19 @@
v1+.v2) sum table) hd tl in
Array.map (fun v -> v /. n) sum
+(* Find all maximal elements. *)
+let find_all_max cmp l =
+ let rec find best acc = function
+ | hd::tl ->
+ let rel = cmp hd best in
+ if rel < 0 then find best acc tl
+ else if rel = 0 then find best (hd::acc) tl
+ else find hd [hd] tl
+ | [] -> acc in
+ match l with
+ | [] -> invalid_arg "find_all_max: empty list"
+ | hd::tl -> find hd [hd] tl
+
(* Maximaxing: find the best among subtrees for a player. Pick a best
entry in the lexicographic product of: maximal [scores] value for
[player], minimal/maximal sum of [scores] values (resp. competitive
@@ -503,14 +516,14 @@
then fun (_,x) (_,y) -> compare x y
else fun (_,x) (_,y) -> compare y x in
let bestsc =
- Aux.find_all_max cmp_sums sc_sums in
+ find_all_max cmp_sums sc_sums in
match bestsc with
| [] -> failwith "impossible"
| [bestsc,_] -> scores.(bestsc), bestsc
| _ ->
(* pick ones from biggest subtrees *)
let bestsc =
- Aux.find_all_max
+ find_all_max
(fun (b1,_) (b2,_) -> subt_sizes.(b1) - subt_sizes.(b2))
bestsc in
match bestsc with
Modified: trunk/Toss/Play/Heuristic.ml
===================================================================
--- trunk/Toss/Play/Heuristic.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Play/Heuristic.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -307,6 +307,10 @@
List.map (fun v ->
List.map (List.assoc v) substs) vars in
(* TODO: optimizable *)
+ let rec has_repeating = function
+ | [] -> false
+ | hd::tl when List.mem hd tl -> true
+ | hd::tl -> has_repeating tl in
if has_repeating vs_insts
then
[], true, []
@@ -317,6 +321,16 @@
exception Outside_subst of (fo_var * int) list
+let find_max cmp l =
+ let rec find acc = function
+ | hd::tl ->
+ if cmp hd acc <= 0 then find acc tl
+ else find hd tl
+ | [] -> acc in
+ match l with
+ | [] -> invalid_arg "find_max: empty list"
+ | hd::tl -> find hd tl
+
let expanded_descr max_alt_descr elems rels struc
all_vars xvars xsubsts =
let alt_descr = ref 0 in
@@ -633,6 +647,12 @@
(* ********** Heuristic of Payoff Expression ********** *)
+(* Generalized product. [product l = gproduct (fun x y->x::y) [] l]. *)
+let gproduct f r0 l =
+ List.fold_right (fun set prod ->
+ concat_map (fun el -> List.map (fun tup -> f el tup) prod) set)
+ l [r0]
+
let rec limited_dnf neg = function
| (Rel _
| Eq _
@@ -640,7 +660,7 @@
| RealExpr _) as psi -> [[if neg then Not psi else psi]]
| Not psi -> limited_dnf (not neg) psi
| And conjs ->
- Aux.gproduct List.append [] (List.map (limited_dnf neg) conjs)
+ gproduct List.append [] (List.map (limited_dnf neg) conjs)
| Or disjs -> Aux.concat_map (limited_dnf neg) disjs
| Ex (vs, psi) as phi ->
[[if neg then All (vs, Not psi) else phi]]
Modified: trunk/Toss/Solver/AssignmentSet.ml
===================================================================
--- trunk/Toss/Solver/AssignmentSet.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Solver/AssignmentSet.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -93,7 +93,8 @@
(Aux.product (List.rev_map (fun _ -> Structure.Elems.elements elems) vars))
| FO (`FO v, asg_list) ->
let (idx, vs) = (Aux.find_index v vars, Aux.remove_one v vars) in
- let prolong e asg = Array.of_list (Aux.add_nth idx e (Array.to_list asg)) in
+ let prolong e asg =
+ Array.of_list (Aux.insert_nth idx e (Array.to_list asg)) in
List.concat (List.rev_map (fun (e, asg) ->
List.rev_map (prolong e) (tuples elems vs asg)) asg_list)
| _ -> failwith "listing tuples in non first-order assignment set"
Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Solver/Assignments.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -292,24 +292,10 @@
(* ---------------------- UNIVERSAL PROJECTION ------------------------------ *)
-let concat_map f l =
- let rec cmap_f accu = function
- | [] -> accu
- | a::l -> cmap_f (List.rev_append (f a) accu) l
- in
- List.rev (cmap_f [] l)
-
-let product l =
- if List.mem [] l then []
- else
- List.fold_right (fun set prod ->
- concat_map (fun el -> List.map (fun tup -> el::tup) prod) set)
- l [[]]
-
let negate_real_disj poly_disj =
let neg_sign (p, s) = (p, SignTable.neg_sign_op s) in
let ndisj = List.rev_map (fun l -> List.rev_map neg_sign l) poly_disj in
- List.filter RealQuantElim.sat (product ndisj)
+ List.filter RealQuantElim.sat (Aux.product ndisj)
(* Project assignments on a given universal variable. We assume that [elems]
are all elements and are sorted. Corresponds to the for-all v quantifier. *)
Modified: trunk/Toss/Solver/FFSolver.ml
===================================================================
--- trunk/Toss/Solver/FFSolver.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Solver/FFSolver.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -156,6 +156,12 @@
let debug_count = ref 0
+let list_existsi p l =
+ let rec aux i = function
+ | [] -> false
+ | a::l -> p i a || aux (i+1) l in
+ aux 0 l
+
(* We assume that for every "not ex
psi" subformula, "ex psi" is ground, and that every other
occurrence of negation is in a literal (it is guaranteed by
@@ -289,7 +295,7 @@
if List.mem_assoc x sb then 1, y else 0, x in
let oldvars =
List.filter (fun v->List.mem_assoc v sb) vtup in
- let multi_unkn = Aux.list_existsi
+ let multi_unkn = list_existsi
(fun i v->i>nvi && not (List.mem v oldvars)) vtup in
if multi_unkn && (conj_cont <> [] || delayed1 <> [])
then (* delay *)
@@ -401,7 +407,7 @@
if List.mem_assoc x sb then 1, y else 0, x in
let oldvars =
List.filter (fun v->List.mem_assoc v sb) vtup in
- let multi_unkn = Aux.list_existsi
+ let multi_unkn = list_existsi
(fun i v->i>nvi && not (List.mem v oldvars)) vtup in
if multi_unkn && (conj_cont <> [] || delayed1 <> [])
then (* delay *)
Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/Solver/Structure.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -254,6 +254,21 @@
(* ------------ GLOBAL FUNCTIONS TO CREATE STRUCTURES FROM LISTS ------------ *)
+(** Map a function over an array threading an accumulator. *)
+let array_fold_map f acc a =
+ let l = Array.length a in
+ if l = 0 then acc, [||] else begin
+ let acc, e = f acc (Array.unsafe_get a 0) in
+ let prev = ref acc in
+ let r = Array.create l e in
+ for i = 1 to l - 1 do
+ let acc, e = f !prev (Array.unsafe_get a i) in
+ prev := acc;
+ Array.unsafe_set r i e
+ done;
+ !prev, r
+ end
+
(* Add to a named structure elements, relations and functions from the lists. *)
let add_from_lists struc els rels funs =
List.fold_left (fun s (fn, assgns) ->
@@ -271,7 +286,7 @@
| Some ar -> ar in
let s = add_rel_name rn arity s in
List.fold_left (fun s tp ->
- let s, tp = Aux.array_fold_map find_or_new_elem s tp in
+ let s, tp = array_fold_map find_or_new_elem s tp in
add_rel s rn tp) s tps)
(List.fold_left (fun s ne ->
fst (find_or_new_elem s ne)) struc els) rels) funs
@@ -335,31 +350,12 @@
{ del_rels_struc with elements = Elems.remove e del_rels_struc.elements ;
functions = StringMap.map del_fun del_rels_struc.functions ; }
-(* Copied from Server/Aux.ml *)
-let map_reduce mapf redf red0 l =
- match List.sort (fun x y -> Pervasives.compare (fst x) (fst y))
- (List.map mapf l) with
- | [] -> []
- | (k0, v0)::tl ->
- let k0, vs, l = List.fold_left (fun (k0, vs, l) (kn, vn) ->
- if k0 = kn then k0, vn::vs, l else kn, [vn], (k0,vs)::l)
- (k0, [v0], []) tl in
- List.rev (List.map (fun (k,vs) -> k, List.fold_left redf red0 vs)
- ((k0,vs)::l))
-
-let concat_map f l =
- let rec cmap_f accu = function
- | [] -> accu
- | a::l -> cmap_f (List.rev_append (f a) accu) l
- in
- List.rev (cmap_f [] l)
-
(* Remove the elements [es] and all incident relation tuples from
[struc]; return the deleted relation tuples. *)
let del_elems struc es =
let rel_tuples =
- map_reduce (fun x->x) List.rev_append []
- (concat_map (incident struc) es) in
+ Aux.map_reduce (fun x->x) List.rev_append []
+ (Aux.concat_map (incident struc) es) in
let del_rels_struc =
List.fold_left (fun s (rn, tps) -> del_rels s rn tps) struc rel_tuples in
let del_fun fmap =
Modified: trunk/Toss/TossTest.ml
===================================================================
--- trunk/Toss/TossTest.ml 2010-11-21 17:16:38 UTC (rev 1186)
+++ trunk/Toss/TossTest.ml 2010-11-21 20:45:43 UTC (rev 1187)
@@ -1,6 +1,7 @@
open OUnit
let formula_tests = "Formula" >::: [
+ AuxTest.tests;
FormulaTest.tests;
FormulaOpsTest.tests;
FFTNFTest.tests;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
