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

[<si...@us...>]

Revision: 1594
          http://toss.svn.sourceforge.net/toss/?rev=1594&view=rev
Author:   simles
Date:     2011-10-13 13:36:15 +0000 (Thu, 13 Oct 2011)
Log Message:
-----------
updated ntype in WL, fixed index issue in Aux.array_replace

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Solver/WL.ml

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-10-13 12:28:21 UTC (rev 1593)
+++ trunk/Toss/Formula/Aux.ml	2011-10-13 13:36:15 UTC (rev 1594)
@@ -548,7 +548,7 @@
     with Not_found -> false
 
 let array_replace array i elem = 
-  let a = Array.copy array in a.(i-1) <- elem; a
+  let a = Array.copy array in a.(i) <- elem; a
 
 let neg f x = not (f x)
 

Modified: trunk/Toss/Solver/WL.ml
===================================================================
--- trunk/Toss/Solver/WL.ml	2011-10-13 12:28:21 UTC (rev 1593)
+++ trunk/Toss/Solver/WL.ml	2011-10-13 13:36:15 UTC (rev 1594)
@@ -13,40 +13,61 @@
 	else ( literal )))  
     listOfLiterals
 
-let rec existential index_l structure tuple k n =
-  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"
+let rec conj_b_ex_xmplus1_typesN structure tuple k n =
+  let elements = Structure.elements structure in
+  And(
+  List.map 
+    (fun x -> Ex ( [`FO ("x"^(string_of_int((Array.length tuple)+1)))],
+      (ntype structure (Array.append tuple [|x|]) k n))) 
+    elements)
 
-and universal index_l structure tuple k n =
-  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 all_xmplus1_disj_b_typesN structure tuple k n =
+  let elements = Structure.elements structure in
+  All ([`FO ("x"^(string_of_int((Array.length tuple)+1)))], 
+  ( Or  
+    (List.map 
+      (fun x -> (ntype structure (Array.append tuple [|x|]) k n)) 
+      elements ) ))
 
+and conj_b_ex_xi_typesN_replace_ai_by_b structure tuple k n i =
+  let elements = Structure.elements structure in
+  let substituted e = (Aux.array_replace tuple (i-1) e) in
+  And(
+    List.map
+      (fun x-> Ex( [`FO ("x"^(string_of_int i))],
+        (ntype structure (substituted x) k n)))
+      elements)
+
+and all_xi_disj_b_typesN_replace_ai_by_b structure tuple k n i=
+  let elements = Structure.elements structure in
+  let substituted e = (Aux.array_replace tuple (i-1) e) in
+  All ([`FO ("x"^(string_of_int i))],
+  ( Or
+    (List.map 
+      (fun x -> (ntype structure (substituted x) k n)) 
+      elements )))
+
+
 and ntype structure tuple k n =
+  let m = (Array.length tuple) in
   let variables = List.map (fun i -> "x"^string_of_int(i)) 
   (Aux.range k)  in
   let ats = FormulaOps.atoms (Structure.rel_signature structure)
-    (Aux.take_n (Array.length tuple) variables) in
+    (Aux.take_n m variables) in
   if n=0 then 
     Formula.flatten (And (atoms structure ats tuple (Array.of_list(List.map
     fo_var_of_string variables))))
   else
-    let indices = Aux.product [Structure.elements structure; Aux.range k] in
-    let formulas = 
-      List.map (fun x -> (
-        existential x structure tuple k (n-1))) indices in
-    let uformula =
-      List.map (fun x -> (universal x structure tuple k (n-1))) indices in
-    Formula.flatten (And (formulas))
+    if m < k then
+      Formula.flatten (And [ (ntype structure tuple k (n-1) );
+      (* conjunction b in A of ex x(m+1) (n-1)-type (tuple b) *)
+      (conj_b_ex_xmplus1_typesN structure tuple k (n-1));
+      (all_xmplus1_disj_b_typesN structure tuple k (n-1))])
+    else (*hard case, all variables already used*)
+      let indices = Aux.range k in
+      Formula.flatten (And [ (ntype structure tuple k (n-1));
+        (And ( (List.map 
+        (fun i ->(And 
+        [(conj_b_ex_xi_typesN_replace_ai_by_b structure tuple k (n-1) i);
+        (all_xi_disj_b_typesN_replace_ai_by_b structure tuple k (n-1) i)]))
+        indices )))])

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