[Toss-devel-svn] SF.net SVN: toss:[1593] trunk/Toss

[<luk...@us...>]

Revision: 1593
          http://toss.svn.sourceforge.net/toss/?rev=1593&view=rev
Author:   lukaszkaiser
Date:     2011-10-13 12:28:21 +0000 (Thu, 13 Oct 2011)
Log Message:
-----------
Improvements to the assignments and structure interfaces.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Solver/Assignments.ml
    trunk/Toss/Solver/Assignments.mli
    trunk/Toss/Solver/AssignmentsTest.ml
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/Structure.mli
    trunk/Toss/Solver/WL.ml
    trunk/Toss/Solver/WLTest.ml

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Formula/Aux.ml	2011-10-13 12:28:21 UTC (rev 1593)
@@ -547,6 +547,9 @@
       true
     with Not_found -> false
 
+let array_replace array i elem = 
+  let a = Array.copy array in a.(i-1) <- elem; a
+
 let neg f x = not (f x)
 
 let is_right = function Right _ -> true | Left _ -> false

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Formula/Aux.mli	2011-10-13 12:28:21 UTC (rev 1593)
@@ -260,6 +260,9 @@
     arrays are of different lengths. *)
 val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
 
+(** Return a copy of [array] with the [i]th element replaced by [elem]. *)
+val array_replace : 'a array -> int -> 'a -> 'a array
+
 (** Find all maximal elements in a list. *)
 val list_find_all_max : ('a -> 'a -> int) -> 'a list -> 'a list
 (** Find all maximal elements in an array. *)

Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Solver/Assignments.ml	2011-10-13 12:28:21 UTC (rev 1593)
@@ -42,6 +42,10 @@
 (* Helper type to represent a set or a list of elements with length. *)
 type set_list = List of int * int list | Set  of int * Elems.t
 
+(* Create a set_list out of a set. *)
+let set_to_set_list set = ref (Set ((Elems.cardinal set), set))
+let list_to_set_list list = ref (List ((List.length list), list))
+
 (* List a set or list ref; changes from set to list if required. *)
 let slist slr = 
   match !slr with 
@@ -447,34 +451,43 @@
 
 (* -------- CREATING ASSIGNMENTS FROM VARIABLES AND ELEMENT TUPLES  --------- *)
 
-(* Helper function to remove duplicate assignments to variables and append.*)
-let remove_dup_append assgn_list asgn =
-  let rec remove_dup acc = function
-    | [] -> acc :: assgn_list
-    | [x] -> (x :: acc) :: assgn_list
-    | (v1, e1) :: (v2, e2) :: xs when v1 = v2 ->
-	if e1 = e2 then remove_dup acc ((v2, e2) :: xs) else assgn_list
-  | (v1, e1) :: (v2, e2) :: xs -> remove_dup ((v1, e1)::acc) ((v2, e2) :: xs)
-  in
-    remove_dup [] asgn
 
+(* Helper function for assignment creation below. *)
+let make_assign vl tuple =
+  let compare_asvs (v1, e1) (v2, e2) = 
+    let c = compare_vars (v1 :> Formula.var) (v2 :> Formula.var) in
+      if c != 0 then -c else compare_elems e1 e2 in
+  List.sort compare_asvs (Array.to_list (Aux.array_combine vl tuple))
 
 (* Create an assignment set out of a list of variables and assigned tuples. *)
 let assignments_of_list elems vl tl =
-  let compare_asvs (v1, e1) (v2, e2) = 
-    let c = compare_vars (v1 :> Formula.var) (v2 :> Formula.var) in
-      if c != 0 then -c else compare_elems e1 e2 in
-  let make_assign tuple =
-    List.sort compare_asvs (Array.to_list (Aux.array_combine vl tuple)) in
-  let make_append l t = remove_dup_append l (make_assign t) in
+  (* Helper function to remove duplicate assignments to variables and append.*)
+  let remove_dup_append assgn_list asgn =
+    let rec remove_dup acc = function
+      | [] -> acc :: assgn_list
+      | [x] -> (x :: acc) :: assgn_list
+      | (v1, e1) :: (v2, e2) :: xs when v1 = v2 ->
+	if e1 = e2 then remove_dup acc ((v2, e2) :: xs) else assgn_list
+      | (v1, e1) :: (v2, e2) :: xs ->
+	remove_dup ((v1, e1)::acc) ((v2, e2) :: xs) in
+    remove_dup [] asgn in
+  let make_append l t = remove_dup_append l (make_assign vl t) in
   let asgn_list = List.fold_left make_append [] tl in
   let rec set_of_single = function
     | [] -> Empty
     | [(v, e)] -> FO (v, [(e, Any)])
-    | (v, e) :: rest -> FO (v, [(e, set_of_single rest)])
-  in
-    List.fold_left (fun s t -> sum elems s (set_of_single t)) Empty asgn_list
+    | (v, e) :: rest -> FO (v, [(e, set_of_single rest)]) in
+  List.fold_left (fun s t -> sum elems s (set_of_single t)) Empty asgn_list
 
+(* Create an assignment out of a list of variables and a tuple. 
+   WRONG THIS WAY
+let assignment_of_list vl t =
+  let rec set_of_single = function
+    | [] -> Empty
+    | [(v, e)] -> FO (v, [(e, Any)])
+    | (v, e) :: rest -> FO (v, [(e, set_of_single rest)]) in
+  set_of_single (make_assign vl t)
+*)
 
 (* ----------------- JOIN A RELATION WITH AN ASSIGNMENT  -------------------- *)
 

Modified: trunk/Toss/Solver/Assignments.mli
===================================================================
--- trunk/Toss/Solver/Assignments.mli	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Solver/Assignments.mli	2011-10-13 12:28:21 UTC (rev 1593)
@@ -18,14 +18,17 @@
 
 
 (** Helper type to represent a set or a list of elements with length. *)
-type set_list = List of int * int list | Set  of int * Structure.Elems.t
+type set_list
 
+(** Create a set_list *)
+val set_to_set_list : Structure.Elems.t -> set_list ref
+val list_to_set_list : int list -> set_list ref
+
 (** List a set or list ref; changes from set to list if required. *)
 val slist : set_list ref -> int list
 val sset  : set_list ref -> Structure.Elems.t
 val sllen : set_list ref -> int
 
-
 (** {2 Join} *)
 
 
@@ -86,12 +89,10 @@
 
 (** {2 Creating Assignments from Variables and Element Tuples} *)
 
-
 (** Create an assignment set out of an array of variables and a list of
-   assigned tuples. *)
+    assigned tuples. The first argument are elements of the structure. *)
 val assignments_of_list : set_list ref ->
-  Formula.fo_var array -> int array list ->
-  assignment_set
+  Formula.fo_var array -> int array list -> assignment_set
 
 
 (** {2 Join a Relation with an Assignment} *)

Modified: trunk/Toss/Solver/AssignmentsTest.ml
===================================================================
--- trunk/Toss/Solver/AssignmentsTest.ml	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Solver/AssignmentsTest.ml	2011-10-13 12:28:21 UTC (rev 1593)
@@ -23,21 +23,20 @@
 let test_join = test2 "Join" join str
 
 let test_join_tup elems_l (vns1, tps1) (vns2, tps2) =
-  let elems = ref (List (List.length elems_l, elems_l)) in
+  let elems = list_to_set_list elems_l in
   let vs1 = List.map (fun s -> Formula.fo_var_of_string s) vns1 in
   let vs2 = List.map (fun s -> Formula.fo_var_of_string s) vns2 in
   let as1 = assignments_of_list elems (Array.of_list vs1) tps1 in
   let as2 = assignments_of_list elems (Array.of_list vs2) tps2 in
     test_join as1 as2
 
-let test_sum elems = 
-  test2 "Sum" (sum (ref (List (List.length elems, elems)))) str
+let test_sum elems = test2 "Sum" (sum (list_to_set_list elems)) str
 
 let test_complement elems = 
-  test1 "Complement" (complement (ref (List (List.length elems, elems)))) str
+  test1 "Complement" (complement (list_to_set_list elems)) str
 
 let test_project elems v = 
-  test1 "Project" (project (ref (List (List.length elems, elems))) v) str
+  test1 "Project" (project (list_to_set_list elems) v) str
 
 
 (* ------ Some constants used in tests ------ *)

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Solver/Solver.ml	2011-10-13 12:28:21 UTC (rev 1593)
@@ -283,9 +283,7 @@
 
 (* Evaluate with assignment, no cache. *)
 let evaluate_partial_aset solver ~formula struc fo_aset =
-  let elems =
-    ref (Set (Elems.cardinal (Structure.elems struc),
-	      (Structure.elems struc))) in
+  let elems = Assignments.set_to_set_list (Structure.elems struc) in
   let phi = Hashtbl.find solver.formulas_eval formula in
   incr eval_counter;
   eval [] struc elems fo_aset phi
@@ -364,21 +362,14 @@
       res
     with Not_found ->
       if !debug_level > 0 then print_endline ("Eval_m " ^ (str phi));    
-      let els = Set (Elems.cardinal (Structure.elems struc),
-		     (Structure.elems struc)) in
+      let els = Assignments.set_to_set_list (Structure.elems struc) in
       check_timeout "Solver.eval_m.not_found";
-      let asg = eval [] struc (ref els) Any phi in
+      let asg = eval [] struc els Any phi in
       incr eval_counter;
       Hashtbl.add !cache_results phi (asg, phi_rels phi);
       asg
   )
 
-(* Helper function, assignment of tuple. *)
-let asg_of_tuple struc vars tuple =
-  let els = Set (Elems.cardinal (Structure.elems struc),
-		 (Structure.elems struc)) in
-  assignments_of_list (ref els) (Array.of_list vars) [tuple]
-
 (* Evaluate real expressions. Result is represented as assignments with
    real-valued polynomials using variable [rvar] to represent [expr]. 
    We assume that [rvar] does not occur in [expr]. *)
@@ -456,7 +447,8 @@
       let tps = tuples (Structure.elems struc) 
 	(List.map var_str all_vs) asg_gd in
       let add_val acc tp = 
-	let tp_asg = asg_of_tuple struc all_vs tp in
+	let tp_asg = assignments_of_list 
+	  (set_to_set_list(Structure.elems struc))(Array.of_list all_vs) [tp] in
 	acc +. (get_real_val solver tp_asg r struc) in
       List.fold_left add_val 0. tps
     | _ ->

Modified: trunk/Toss/Solver/Structure.mli
===================================================================
--- trunk/Toss/Solver/Structure.mli	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Solver/Structure.mli	2011-10-13 12:28:21 UTC (rev 1593)
@@ -1,6 +1,6 @@
-(** Representing Structures *)
+(** Representing Relational Structures with Real-Valued Functions *)
 
-val debug_level : int ref
+(** {2 Modules used in structure representation.} *)
 
 module IntMap : Map.S with type key = int (** Maps from int to 'alpha *)
 
@@ -10,31 +10,59 @@
 val add_elems : int list -> Elems.t -> Elems.t
 val elems_of_list : int list -> Elems.t
 
-module Tuples : Set.S with type elt = int array
+module Tuples : Set.S with type elt = int array (** Sets of tuples of ints *)
 val add_tuples : int array list -> Tuples.t -> Tuples.t
 val tuples_of_list : int array list -> Tuples.t
 
-(** No element is named by a decimal numeral other than its
-   number. Elements not appearing in [names] are assumed to be named
-   by their decimal numeral. *)
+(** {2 Structure type and basic getters.} *)
+
+(** Elements are internally represented by integers, bu the structure
+    also stores a naming of elements. No element is named by a decimal
+    numeral other than its number to prevent misunderstandings.
+    Elements not appearing in [names] are assumed to be named
+    by their decimal numeral. *)
 type structure
 
+(** Comparison function for elements. *)
 val compare_elems : int -> int -> int
+(** Comparison function for structures. *)
 val compare : structure -> structure -> int
+(** Equality check on structures. *)
 val equal : structure -> structure -> bool
 
+(** Return the list of elements in a structure. *)
 val elements : structure -> int list
+
+(** Return the set of elements in a structure. *)
 val elems : structure -> Elems.t
+
+(** Number of elements in a structure. *)
 val nbr_elems : structure -> int
 
+(** Relations in the structure. *)
+val relations : structure -> Tuples.t StringMap.t
+
+(** Functions in the structure. *)
+val functions : structure -> (float IntMap.t) StringMap.t
+
+(** {3 Elements and their names.} *)
+
+(** The integer corresponding to a given element name. *)
 val elem_nbr : structure -> string -> int
+
+(** The element name of an element (given by integers) *)
 val elem_name : structure -> int -> string
+
+(** The map containing element names. *)
 val names : structure -> int StringMap.t
+
+(** The inverse map of element names. *)
 val inv_names : structure -> string IntMap.t
+
+(** Replace the names of elements by new maps. *)
 val replace_names : structure -> int StringMap.t -> string IntMap.t -> structure
-val functions : structure -> (float IntMap.t) StringMap.t
-val relations : structure -> Tuples.t StringMap.t
 
+
 (** {2 Basic helper functions} *)
 
 (** Size of a relation, i.e. number of tuples in it. *)
@@ -251,3 +279,9 @@
   ?pos_initial:float * float ->
   ?pos_increment:float * float ->
   ?struc:structure -> string -> structure
+
+
+(** {2 Debugging} *)
+
+val debug_level : int ref
+

Modified: trunk/Toss/Solver/WL.ml
===================================================================
--- trunk/Toss/Solver/WL.ml	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Solver/WL.ml	2011-10-13 12:28:21 UTC (rev 1593)
@@ -4,40 +4,35 @@
   let variables = (Array.sub variable 0 (Array.length tuple)) in
   let eval structure literal assignment =
     (Solver.M.evaluate_partial structure assignment literal) in
-  let set_listS = Assignments.Set (Structure.Elems.cardinal (Structure.elems structure),
-                 (Structure.elems structure)) in
-  let assignment = Assignments.assignments_of_list (ref
-    set_listS) variables [tuple] in
+  let elems = Assignments.set_to_set_list (Structure.elems structure) in
+  let assignment = Assignments.assignments_of_list elems variables [tuple] in
   List.map 
     ( fun literal ->
-      ( if (( eval structure literal assignment )=AssignmentSet.Empty ) then (Not literal)
-      else ( literal )))  
+      ( if (( eval structure literal assignment )=AssignmentSet.Empty ) then
+	  (Not literal)
+	else ( literal )))  
     listOfLiterals
 
 let rec existential index_l structure tuple k n =
-  match index_l with [element; index] ->
-    let replace array i elem = 
-      let a = Array.copy array in 
-      if (i-1) < (Array.length tuple) then
-        (a.(i-1) <- elem;
-        a)
-      else Array.append a [|elem|]
-    in
-    Ex ([`FO ("x" ^ string_of_int(index))],
-	ntype structure (replace tuple index element) k n)
-    | _ -> failwith "wrong index list"
+  match index_l with 
+    | [element; index] ->
+      let substituted = 
+	if (index-1) < (Array.length tuple) then
+	  Aux.array_replace tuple index element
+	else Array.append (Array.copy tuple) [|element|] in
+      Ex ([`FO ("x" ^ string_of_int(index))],
+	  ntype structure substituted k n)
+    | _ -> failwith "existential: wrong index list"
 
 and universal index_l structure tuple k n =
-  match index_l with [element; index] ->
-    let replace array i elem = 
-      let a = Array.copy array in 
-      if (i-1) < (Array.length tuple) then
-        (a.(i-1) <- elem;
-        a)
-      else Array.append a [|elem|]
-    in
-	ntype structure (replace tuple index element) k n
-    | _ -> failwith "wrong index list"
+  match index_l with 
+    | [element; index] ->
+      let substituted = 
+	if (index-1) < (Array.length tuple) then
+	  Aux.array_replace tuple index element
+	else Array.append (Array.copy tuple) [|element|] in
+      ntype structure substituted k n
+    | _ -> failwith "universal: wrong index list"
 
 and ntype structure tuple k n =
   let variables = List.map (fun i -> "x"^string_of_int(i)) 

Modified: trunk/Toss/Solver/WLTest.ml
===================================================================
--- trunk/Toss/Solver/WLTest.ml	2011-10-13 10:10:15 UTC (rev 1592)
+++ trunk/Toss/Solver/WLTest.ml	2011-10-13 12:28:21 UTC (rev 1593)
@@ -7,21 +7,20 @@
   StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
 
 let tests = "WL" >::: [
-  "klist" >::
-    (fun () ->
-      assert_equal ~printer:(fun x -> string_of_int x)
-	6 (List.length (Aux.range 6));
-    );
   "atoms" >::
     (fun () ->
       let variables = ["x1";"x2"] in
       let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
       assert_equal ~printer:(fun x -> x)
-        "(not R(x1, x1) and R(x1, x2) and not R(x2, x1) and not R(x2, x2))" (Formula.str (Formula.And (WL.atoms structure
-        (FormulaOps.atoms (Structure.rel_signature structure) variables) 
-        [|2; 3|] 
-        (Array.of_list(List.map Formula.fo_var_of_string variables))
-        )));
+        "(not R(x1, x1) and R(x1, x2) and not R(x2, x1) and not R(x2, x2))" 
+	(Formula.str (Formula.And 
+			(WL.atoms structure
+			   (FormulaOps.atoms (Structure.rel_signature structure)
+			      variables) 
+			   [|2; 3|] 
+			   (Array.of_list 
+			      (List.map Formula.fo_var_of_string variables))
+			)));
     );
   "ntype1" >::
     ( fun () ->

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.