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

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

Revision: 1590
          http://toss.svn.sourceforge.net/toss/?rev=1590&view=rev
Author:   lukaszkaiser
Date:     2011-10-12 15:57:24 +0000 (Wed, 12 Oct 2011)
Log Message:
-----------
Adding a placeholder file for WL stuff.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOps.mli
    trunk/Toss/Formula/FormulaOpsTest.ml
    trunk/Toss/Server/Tests.ml
    trunk/Toss/Solver/Makefile

Added Paths:
-----------
    trunk/Toss/Solver/WL.ml
    trunk/Toss/Solver/WL.mli
    trunk/Toss/Solver/WLTest.ml

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-10-11 10:33:28 UTC (rev 1589)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-10-12 15:57:24 UTC (rev 1590)
@@ -102,7 +102,7 @@
 
 (* --- AType with variables over given relations, no repetition, equality --- *)
 
-let atp rels vars_in =
+let atoms ?(repetitions=true) rels vars_in =
   if vars_in = [] then [] else
     let vars = List.rev_map fo_var_of_string vars_in in
     let rec rept i l = if i < 1 then [] else l :: (rept (i-1) l) in
@@ -110,12 +110,18 @@
       if i < 1 then [] else if i = 1 then 
 	  List.map (fun v -> [|v|]) vars
 	else let arr l = 
-	       if List.length (Aux.unique_sorted l) = i then
-		 Some (Array.of_list l)
-	       else None in
+	       if repetitions then Some (Array.of_list l) else
+		 if List.length (Aux.unique_sorted l) = i then
+		   Some (Array.of_list l)
+		 else None in
 	     Aux.map_some arr (Aux.product (rept i vars)) in
     let atom (rel, i) = List.rev_map (fun vs -> Rel (rel, vs)) (prod i) in
-    let atoms = Array.of_list (List.concat (List.map atom rels)) in
+    List.concat (List.map atom rels)
+
+let atp rels vars_in =
+  if vars_in = [] then [] else
+    let rec rept i l = if i < 1 then [] else l :: (rept (i-1) l) in
+    let atoms = Array.of_list (atoms ~repetitions:false rels vars_in) in
     let choices = Aux.product (rept (Array.length atoms) [true; false]) in
     let atom_choice i c = if c then atoms.(i) else Not (atoms.(i)) in
     let tp_of_choice l = And (Array.to_list (Array.mapi atom_choice l)) in

Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli	2011-10-11 10:33:28 UTC (rev 1589)
+++ trunk/Toss/Formula/FormulaOps.mli	2011-10-12 15:57:24 UTC (rev 1590)
@@ -22,6 +22,10 @@
 
 (** {2 Type generating functions.} *)
 
+(** All atoms over given signature and variables. *)
+val atoms : ?repetitions: bool -> (string * int) list ->
+  string list -> formula list
+
 (** AType with variables over given relations, no repetition, equality. *)
 val atp : (string * int) list -> string list -> formula list
 

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-10-11 10:33:28 UTC (rev 1589)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-10-12 15:57:24 UTC (rev 1590)
@@ -247,7 +247,7 @@
             ((not Succ(t, s)) or (t in X) or (not (s in C))))))"
      );
 
-   "atp, mintp" >::
+   "atoms, atp, mintp" >::
      (fun () ->
        let report phis = 
 	 (* List.iter (fun f -> Format.printf "\n%!"; Formula.print f) phis; *)
@@ -269,6 +269,9 @@
 
        let phis = report (FormulaOps.mintp (nv 2) [("R", 2); ("P", 1)] []) in
        assert_equal ~printer:string_of_int 16 (List.length phis);
+
+       let phis = report (FormulaOps.atoms [("R", 2); ("P", 1)] ["x"; "y"]) in
+       assert_equal ~printer:string_of_int 6 (List.length phis);
      );
 
    "remove_redundant default" >::

Modified: trunk/Toss/Server/Tests.ml
===================================================================
--- trunk/Toss/Server/Tests.ml	2011-10-11 10:33:28 UTC (rev 1589)
+++ trunk/Toss/Server/Tests.ml	2011-10-12 15:57:24 UTC (rev 1590)
@@ -17,6 +17,7 @@
   "AssignmentsTest", [AssignmentsTest.tests];
   "SolverTest",      [SolverTest.tests; SolverTest.bigtests];
   "ClassTest",       [ClassTest.tests; ClassTest.bigtests];
+  "WLTest",          [WLTest.tests];
 ]
 
 let arena_tests = "Arena", [

Modified: trunk/Toss/Solver/Makefile
===================================================================
--- trunk/Toss/Solver/Makefile	2011-10-11 10:33:28 UTC (rev 1589)
+++ trunk/Toss/Solver/Makefile	2011-10-12 15:57:24 UTC (rev 1590)
@@ -9,6 +9,7 @@
 FFSolverTest:
 ClassTest:
 PresbTest:
+WLTest:
 
 tests:
 	make -C .. SolverTestsVerbose

Added: trunk/Toss/Solver/WL.ml
===================================================================
--- trunk/Toss/Solver/WL.ml	                        (rev 0)
+++ trunk/Toss/Solver/WL.ml	2011-10-12 15:57:24 UTC (rev 1590)
@@ -0,0 +1,27 @@
+open Formula
+
+let rec klist ?(i=1) k =
+  if i>=k then [k]
+  else i :: klist ~i:(i+1) k 
+
+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 
+      a.(i) <- elem; 
+      a
+    in
+    Ex ([`FO ("x" ^ string_of_int(index))],
+	ntype structure (replace tuple index element) k n)
+    | _ -> failwith "wrong index list"
+
+and ntype structure tuple k n =
+  if n=0 then 
+    And (FormulaOps.atoms (Structure.rel_signature structure)
+	     (Array.to_list (Array.map string_of_int tuple)))
+  else
+    let eq = Eq(`FO "x", `FO "x") in
+    let indices = Aux.product [Structure.elements structure; klist k] in
+    let formulas = 
+      List.map (fun x -> (existential x structure tuple k n)) indices in
+    And (eq :: formulas)

Added: trunk/Toss/Solver/WL.mli
===================================================================
--- trunk/Toss/Solver/WL.mli	                        (rev 0)
+++ trunk/Toss/Solver/WL.mli	2011-10-12 15:57:24 UTC (rev 1590)
@@ -0,0 +1,3 @@
+(* The WL algorithm and related tests. *)
+
+val klist: ?i : int -> int -> int list

Added: trunk/Toss/Solver/WLTest.ml
===================================================================
--- trunk/Toss/Solver/WLTest.ml	                        (rev 0)
+++ trunk/Toss/Solver/WLTest.ml	2011-10-12 15:57:24 UTC (rev 1590)
@@ -0,0 +1,12 @@
+open OUnit
+
+let tests = "WL" >::: [
+  "klist" >::
+    (fun () ->
+      assert_equal ~printer:(fun x -> string_of_int x)
+	6 (List.length (WL.klist 6));
+    );
+]
+
+
+let exec = Aux.run_test_if_target "WLTest" tests

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