[Toss-devel-svn] SF.net SVN: toss:[1594] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
From: <si...@us...> - 2011-10-13 13:36:24
|
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. |