diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml index b1795e25581870280f46dadbbe680aec2af2ce0f..f06bde32d14471a0a77261d94a882e905fa22a48 100644 --- a/src/coalg/coalg.ml +++ b/src/coalg/coalg.ml @@ -22,15 +22,16 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm type options = { verbose : bool + ; fragment : CM.fragment_spec } -let defaultOpts = { verbose = false } +let defaultOpts = { verbose = false; fragment = CM.Auto } let options = [ { Args.long = "verbose" ; Args.short = Some 'v' ; Args.description = "print verbose output with statistics" - ; Args.argument = Args.No_arg (fun a -> { verbose = true }) + ; Args.argument = Args.No_arg (fun a -> { a with verbose = true }) } ; { Args.long = "agents" ; Args.short = None @@ -44,6 +45,21 @@ let options = in Args.Required_arg ("AGLIST", fun s a -> parse_agents s; a) } + ; { Args.long = "fragment" + ; Args.short = None + ; Args.description = "Use reasoner algorithm specialized to FRAGMENT.\n" + ^ "Possible values are: auto, altfree, altfreeaconj\n" + ^ "where \"auto\" detects the fragment from the given formulas" + ; Args.argument = + let parse_fragment s = match s with + | "auto" -> CM.Auto + | "altfree" -> CM.Fragment CM.AlternationFree + | "altfreeaconj" -> CM.Fragment CM.AconjunctiveAltFree + | _ -> raise (Args.ParseError ("Unknown fragment " ^ s)) + in + Args.Required_arg + ("FRAGMENT", fun s a -> { a with fragment = parse_fragment s }) + } ] let printUsage name = @@ -109,7 +125,7 @@ let choiceSat opts = incr counter; print_string ("\nFormula " ^ (string_of_int !counter) ^ ": "); flush stdout; - printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox f) + printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox f) else () done with End_of_file -> () @@ -134,7 +150,7 @@ let choiceProvable opts = incr counter; print_string ("\nFormula " ^ (string_of_int !counter) ^ ": "); flush stdout; - printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox fneg) + printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox fneg) else () done with End_of_file -> () @@ -187,7 +203,7 @@ let choiceGraph opts = let input = read_line () in let (tbox, f) = CoAlgFormula.importQuery input in - ignore(CoAlgReasoner.isSat sorts nomTable tbox f); + ignore(CoAlgReasoner.isSat opts.fragment sorts nomTable tbox f); print_endline (CM.graphToDot ()) let choiceVerify opts = diff --git a/src/coalgcompare/coalgcompare.ml b/src/coalgcompare/coalgcompare.ml index 8ef8daa3451454ad8076a0e07f69e30f716d3229..548b6bd34deded1400f872e46d48175169064358 100644 --- a/src/coalgcompare/coalgcompare.ml +++ b/src/coalgcompare/coalgcompare.ml @@ -124,7 +124,7 @@ let exportALCQuery tbox (_, f) = let solvCoalg sortTable args = - G.evaluateFkt (fun (tbox, sf) -> CoAlgReasoner.isSat sortTable nomTable tbox sf) args + G.evaluateFkt (fun (tbox, sf) -> CoAlgReasoner.isSat CoAlgMisc.Auto sortTable nomTable tbox sf) args let solvALC (tbox, sf) = let args = exportALCQuery tbox sf in diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml index 7f75b176ecf945dc43933b068ad087c6582b80b3..7efe4f585456a60d7e247914612b9b0e535dc973 100644 --- a/src/debugger/debugger.ml +++ b/src/debugger/debugger.ml @@ -100,7 +100,7 @@ let _ = let formula = Sys.argv.(2) in let sorts = (FE.sortTableFromString Sys.argv.(1)) in let (tbox, f) = CoAlgFormula.importQuery formula in - Reasoner.initReasoner sorts nomTable tbox f; + Reasoner.initReasoner CoAlgMisc.Auto sorts nomTable tbox f; let session = { Repl.prompt = "> "; Repl.bindings = Repl.addHelpBinding [ diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml index fd6ff8496d85c2838bbf19e2a373b376969ccc58..447c4427138564f63ecbd09bf8d0c87391b1ef2f 100644 --- a/src/lib/CoAlgMisc.ml +++ b/src/lib/CoAlgMisc.ml @@ -896,6 +896,7 @@ let lfToAt _ lf = lf type fragment = AlternationFree | AconjunctiveAltFree +type fragment_spec = Auto | Fragment of fragment let fragment = ref AlternationFree let getFragment () = !fragment @@ -1217,7 +1218,7 @@ let initTablesAt hcF htF name sort = in C.HcFHt.iter addAt htF.(sort) -let ppFormulae nomTbl tbox (s, f) = +let ppFormulae fragSpec nomTbl tbox (s, f) = let card = Array.length !sortTable in if card <= 0 then raise (C.CoAlgException "Number of sorts must be positive.") @@ -1278,10 +1279,27 @@ let ppFormulae nomTbl tbox (s, f) = if size2 > !size then size := size2 else () done; - if C.isMuAconjunctive f then - fragment := AconjunctiveAltFree - else - fragment := AlternationFree; + begin match fragSpec with + | Auto -> if C.isMuAconjunctive f then + fragment := AconjunctiveAltFree + else + fragment := AlternationFree + | Fragment AconjunctiveAltFree -> + if not (C.isMuAconjunctive f) then + raise (CoAlgFormula.CoAlgException "Formula not in required fragment") + else fragment := AconjunctiveAltFree + | Fragment AlternationFree -> + if C.isMuAconjunctive f then + raise (CoAlgFormula.CoAlgException "Formula not in required fragment") + else fragment := AlternationFree + end; + + (* if (fragSpec = Auto || fragSpec = Fragment AconjunctiveAltFree) && C.isMuAconjunctive f then *) + (* fragment := AconjunctiveAltFree; *) + (* else if (fragSpec = Auto || fragSpec = Fragment AlternationFree) && (not (C.isMuAconjunctive f)) *) + (* fragment := AlternationFree; *) + (* else *) + (* raise (CoAlgFormula.CoAlgException "Formula not in required fragment"); *) arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE); arrayType := Array.init card (fun _ -> Array.make !size Other); diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli index 8c82cad00bb7effed6cfe004a82825bd9c356cea..d03a537d35dc9b5117cbb6015295ba997c1c364e 100644 --- a/src/lib/CoAlgMisc.mli +++ b/src/lib/CoAlgMisc.mli @@ -376,16 +376,19 @@ val lfToAt : sort -> localFormula -> atFormula *) type fragment = AlternationFree | AconjunctiveAltFree +type fragment_spec = Auto | Fragment of fragment + (** Return the fragment of the mu-calculus that the original formula uses *) val getFragment : unit -> fragment -(** [ppFormulae nomTbl tbox sf] initializes the array representation and various +(** [ppFormulae fragment nomTbl tbox sf] initializes the array representation and various tables for the formula. @return (simplified NNF of f, simplified nnf of tbox, bitset containing f) *) -val ppFormulae : (string -> sort option) -> CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> - CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset +val ppFormulae : fragment_spec -> (string -> sort option) -> CoAlgFormula.sortedFormula list + -> CoAlgFormula.sortedFormula + -> CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset (* vim: set et sw=2 sts=2 ts=8 : *) diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml index 6844973a071d3e583524650edefcc427b5ad1e7d..583153fdd09eab0d0b3989142858d9c85ca2c775 100644 --- a/src/lib/CoAlgReasoner.ml +++ b/src/lib/CoAlgReasoner.ml @@ -1070,9 +1070,9 @@ let rec buildGraphLoop () = (* if propagating nominals added some more queue members, do all again.. *) if queueIsEmpty () then () else buildGraphLoop () -let initReasoner sorts nomTable tbox sf = +let initReasoner fragSpec sorts nomTable tbox sf = sortTable := Array.copy sorts; - let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in + let (tbox1, sf1, bs) = ppFormulae fragSpec nomTable tbox sf in let sort = fst sf in let bs1 = bsetAddTBox sort bs in let deferrals = bsetMakeRealEmpty() in @@ -1114,9 +1114,9 @@ let reasonerFinished () = @return True if sf is satisfiable wrt tbox, false otherwise. *) -let isSat ?(verbose = false) sorts nomTable tbox sf = +let isSat ?(verbose = false) fragSpec sorts nomTable tbox sf = let start = if verbose then Unix.gettimeofday () else 0. in - initReasoner sorts nomTable tbox sf; + initReasoner fragSpec sorts nomTable tbox sf; let sat = try buildGraphLoop (); diff --git a/src/lib/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli index 52bb178a7fca3ea8b51d142e4282b4b5087d87ad..506af70642ac0269d51226a36d28585eb52aea5a 100644 --- a/src/lib/CoAlgReasoner.mli +++ b/src/lib/CoAlgReasoner.mli @@ -13,12 +13,15 @@ type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula exception ReasonerError of string -val isSat : ?verbose:bool -> sortTable -> (string -> CoAlgFormula.sort option) -> - CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool +val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable + -> (string -> CoAlgFormula.sort option) -> + CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool -val initReasoner : sortTable -> (string -> CoAlgFormula.sort option) -> - CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> unit +val initReasoner : CoAlgMisc.fragment_spec -> sortTable + -> (string -> CoAlgFormula.sort option) -> + CoAlgFormula.sortedFormula list + -> CoAlgFormula.sortedFormula -> unit (** Run a single step of the reasoner. That is: Expand one node and perform sat propagation. diff --git a/src/lib/CoolUtils.mli b/src/lib/CoolUtils.mli index 438c4042fee2e2f011c21993fe97c151b31f6073..df6a0b2519191697f8b648a5efbb71d2872f6253 100644 --- a/src/lib/CoolUtils.mli +++ b/src/lib/CoolUtils.mli @@ -31,7 +31,9 @@ module Args : sig (** Specifies whether the option takes an addition paramter. *) type 'a argument = Required_arg of string * (string -> 'a param_parser) - (** name of the argument and parser. *) + (** name of the argument and parser. + Parser can throw ParseErrors + *) | No_arg of 'a param_parser type 'a description = @@ -41,6 +43,8 @@ module Args : sig ; argument : 'a argument } + exception ParseError of string + type 'a result = Ok of 'a | Error of string (** parses command line options. diff --git a/src/owl/cool-owl.ml b/src/owl/cool-owl.ml index 55a25b6cfe4f559b58c33c247529776982bcef49..87a2ad2f435de4dc59f0076afffb78cd70e7384c 100644 --- a/src/owl/cool-owl.ml +++ b/src/owl/cool-owl.ml @@ -45,7 +45,7 @@ let consistency () = | (_, []) -> raise (Exception "File needs to contain at least one ontology") in let (sorts,nomTable,axioms) = OWL.to_coalg ontology in - let cons = CR.isSat sorts nomTable axioms (0,CF.TRUE) in + let cons = CR.isSat CoAlgMisc.Auto sorts nomTable axioms (0,CF.TRUE) in let cons = if cons then "yes" else "no" in let (ontoname, _) = ontology in Printf.printf "%s consistent: %s\n" ontoname cons diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml index e84db2a2368daac6788a1dcca2683a793ca65aef..1cddc01131fdf9055dee5f884cca272ae99c06f5 100644 --- a/src/testsuite/Testsuite.ml +++ b/src/testsuite/Testsuite.ml @@ -41,7 +41,7 @@ let runSatCheck (_,logic,input) = (* isSat leaks tons of memory. Call it in new process to allow the OS to reclaim that memory between calls. *) match Unix.fork () with - | 0 -> let res = CoAlgReasoner.isSat logic nomTable tbox f in + | 0 -> let res = CoAlgReasoner.isSat CoAlgMisc.Auto logic nomTable tbox f in if res then exit 0 else exit 1 | -1 -> raise (CoAlgFormula.CoAlgException "fork() failed") | _ -> match Unix.wait () with