Commit 1853b71b authored by Simon Prucker's avatar Simon Prucker
Browse files

Trying two modules for onestep and tableau reasoner, with shared types

parent 53cd2d0f
Pipeline #13685 waiting for manual action with stages
......@@ -682,7 +682,7 @@ let obind o f = match o with
let getExpandingFunctionProducer func = oval (obind (List.assoc_opt func implementationLookup) getTableau) (fun _ -> raise (CoAlgFormula.CoAlgException ("one-step tableau based satisfiability is not implemented for " ^ string_of_functor func)))
let oneStepSatisfiability func = oval (obind (List.assoc_opt func implementationLookup) getOneStepFun) (fun _ -> raise (CoAlgFormula.CoAlgException ("one-step function based satisfiability is not implemented for " ^ string_of_functor func)))
let oneStepSatisfiability func = print_endline "\nonestep\n" ;oval (obind (List.assoc_opt func implementationLookup) getOneStepFun) (fun _ -> raise (CoAlgFormula.CoAlgException ("one-step function based satisfiability is not implemented for " ^ string_of_functor func)))
end
......
......@@ -312,6 +312,8 @@ let bsetMem bs lf = S.memBS bs lf
let bsetRem bs lf = S.remBS bs lf
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
let bsetMakeRealEmpty () = S.makeEmptyBS ()
let bsetSingleton lf =
let res = bsetMakeRealEmpty () in
bsetAdd res lf;
......@@ -373,6 +375,10 @@ let bsetIsSubset (a: bset) (b: bset) : bool =
let csetCompare cs1 cs2 = S.compareBS cs1 cs2
let csetMake () = S.makeBS ()
let csetAdd cs lf = S.addBSNoChk cs lf
......
......@@ -8,7 +8,7 @@ open FocusTracking
module M = Minisat_cool
module CU = CoolUtils
module PG = Paritygame
module C = CoAlgFormula
module R_com = CoAlgReasoner_common
type sortTable = CoAlgMisc.sortTable
......@@ -23,20 +23,14 @@ exception ReasonerError of string
module type S = sig
module G : CoolGraph.S
type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
val isSat : ?verbose:bool -> ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver
-> propagation_rate -> sortTable
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> R_com.game_solver
-> R_com.propagation_rate -> sortTable
-> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
val initReasoner : ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver -> propagation_rate
val initReasoner : CoAlgMisc.fragment_spec -> R_com.game_solver -> R_com.propagation_rate
-> sortTable -> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list
-> CoAlgFormula.sortedFormula -> unit
......@@ -75,7 +69,7 @@ module HashSet = struct
Hashtbl.iter f_intern set
end
let propagateSatMu ?(onestep = false) () =
let propagateSatMu () =
let maxPrio = graphMaxPriority () in
let setStates = setEmptyState () in
......@@ -127,8 +121,7 @@ end
(* All rule applications need to still be potentially won by Eloise for a
* State to be a valid startingpoint for this fixpoint.
*)
(*Copied function from the master for tableaux*)
let onestepFunctionState_master resultStates (state : state) =
let onestepFunctionState resultStates (state : state) =
let ruleiter (_dependencies, corelist) : bool =
List.exists (fun (core : core) -> coreGetStatus core == Sat ||
(setMemCore (Array.get setsFPVarsCores (T.priority (stateGetFocus state)) ) core)) corelist
......@@ -136,29 +129,11 @@ end
if (List.for_all ruleiter (stateGetRules state)) then begin
setAddState resultStates state
end
in
let onestepFunctionState_onestep resultStates (state : state) =
let stateSort = stateGetSort state in
let stateLabel = stateGetBs state in
let statePriority = T.priority (stateGetFocus state) in
let x_i = Array.get setsFPVarsCores statePriority in
let usableCores = List.filter (fun core -> ((setMemCore x_i core) || (coreGetStatus core = Sat))) (stateGetChildren state) in
let usableCoreLabels = CU.TList.safe_map coreGetBs usableCores in
let (func, _) = !sortTable.(stateSort) in
if (Logics.oneStepSatisfiability func usableCoreLabels (stateSort, stateLabel)) then begin
setAddState resultStates state
end
in
let onestepFunctionState =
if onestep (*somehow access onestep flag from options*)
then onestepFunctionState_onestep
else onestepFunctionState_master
in
(* There needs to be a State still potentially Sat for this core
* to be considered for the fixpoint.
*)
in
let onestepFunctionCore resultCores (core : core) =
if (List.exists (fun (state : state) -> stateGetStatus state == Sat ||
(setMemState (Array.get setsFPVarsStates (T.priority (coreGetFocus core))) state))) (coreGetChildren core)
......@@ -363,7 +338,7 @@ let rec propagateUnsat = function
in
propagateUnsat tl1
let propagateUnsatMu ?(onestep = false) () =
let propagateUnsatMu () =
let maxPrio = graphMaxPriority () in
(* Partition set of nodes according to their priorities
......@@ -409,33 +384,15 @@ let rec propagateUnsat = function
let setsFPVarsCores = initializeFPCores (maxPrio+1) in
let resetLevel = ref 0 in
if (maxPrio mod 2 == 0) then resetLevel := maxPrio + 1 else resetLevel := maxPrio;
(*Copied function from the master for tableaux*)
let onestepFunctionState_master resultStates (state : state) =
let ruleiter (_dependencies, corelist) : bool =
List.for_all (fun (core : core) -> (coreGetStatus core <> Sat) && ( (coreGetStatus core == Unsat) ||
(setMemCore (Array.get setsFPVarsCores (T.priority (stateGetFocus state)) ) core) )) corelist
in
if (List.exists ruleiter (stateGetRules state)) then begin
setAddState resultStates state
end
in
let onestepFunctionState_onestep resultStates (state : state) =
let stateSort = stateGetSort state in
let stateLabel = stateGetBs state in
let statePriority = T.priority (stateGetFocus state) in
let x_i = Array.get setsFPVarsCores statePriority in
let usableCores = List.filter (fun core -> (not (setMemCore x_i core)) && (coreGetStatus core <> Unsat)) (stateGetChildren state) in
let usableCoreLabels = CU.TList.safe_map coreGetBs usableCores in
let (func, _) = !sortTable.(stateSort) in
if (not (Logics.oneStepSatisfiability func usableCoreLabels (stateSort, stateLabel))) then begin
let onestepFunctionState resultStates (state : state) =
let ruleiter (_dependencies, corelist) : bool =
List.for_all (fun (core : core) -> (coreGetStatus core <> Sat) && ( (coreGetStatus core == Unsat) ||
(setMemCore (Array.get setsFPVarsCores (T.priority (stateGetFocus state)) ) core) )) corelist
in
if (List.exists ruleiter (stateGetRules state)) then begin
setAddState resultStates state
end
in
let onestepFunctionState =
if onestep (*access onestep flag from options*)
then onestepFunctionState_onestep
else onestepFunctionState_master
in
let onestepFunctionCore resultCores (core : core) =
if (List.for_all (fun (state : state) -> (stateGetStatus state <> Sat) && ((stateGetStatus state == Unsat) ||
(setMemState (Array.get setsFPVarsStates (T.priority (coreGetFocus core))) state)))) (coreGetChildren core)
......@@ -985,7 +942,7 @@ let insertCore sort bs focus =
*
* @return true if all new cores are already unsatisfiable, false otherwise
*)
let insertRule state dep chldrn =
let insertRule state dep chldrn =
let chldrn = listFromLazylist chldrn in
let mkCores (sort, bs, defer) =
let bs1 = bsetAddTBox sort bs in
......@@ -1039,34 +996,6 @@ let expandState state =
| NoMoreElements ->
setSatOrOpen ()
let getModalFormulaList state =
let filteredList = CoAlgMisc.bsetFilter (stateGetBs state) (fun lf -> CoAlgMisc.lfIsModality (stateGetSort state) lf) in
filteredList
let expandStateOneStep state =
let sort = stateGetSort state in
let old_focus = stateGetFocus state in
let createCore subset =
let transient_focus = T.make_transient old_focus in
let extractAndTrack formula =
let new_formula = lfGetDest1 sort formula in
T.track sort formula new_formula old_focus transient_focus;
new_formula in
let core_bset = bsetMap extractAndTrack subset in
let core = insertCore sort (bsetAddTBox sort core_bset) (T.finalize transient_focus) in
stateAddChild state core;
coreAddParent core state sort in
let formulaList = getModalFormulaList state in
let powerset = CoAlgMisc.bsetNonEmptyPowersets formulaList in (* empty cores are always sat and hence excluded *)
List.iter createCore powerset;
stateSetStatus state Open
let expandStateWrapper state =
expandStateOneStep state
let expandCnstr cset =
let nht = nhtInit () in
let mkCores f =
......@@ -1102,16 +1031,16 @@ let expandCnstr cset =
(* The Main Loop *)
(*****************************************************************************)
let propagateMu ?(_onestep=false) () = propagateSatMu ~onestep:_onestep (); propagateUnsatMu ~onestep:_onestep ()
let propagateMu () = propagateSatMu (); propagateUnsatMu ()
(* Solver to use. Will be set by initReasoner. *)
let solver = ref (propagateMu ~_onestep: false)
let solver = ref propagateMu
let expandNodesLoop (recursiveAction: unit -> unit) =
match queueGetElement () with
| QState state ->
if stateGetStatus state = Expandable then begin
expandStateWrapper state;
expandState state;
if doSatPropagation () then begin !solver () end;
end else ();
recursiveAction ()
......@@ -1143,7 +1072,7 @@ type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
let initReasoner ?(onestep=false) fragSpec game_solver propagation_rate sorts nomTable tbox sf =
let initReasoner fragSpec game_solver propagation_rate sorts nomTable tbox sf =
sortTable := Array.copy sorts;
let (_tbox1, _sf1, bs) = ppFormulae fragSpec nomTable tbox sf in
let sort = fst sf in
......@@ -1151,7 +1080,7 @@ let initReasoner ?(onestep=false) fragSpec game_solver propagation_rate sorts no
let focus = T.init sort bs in
begin
match game_solver with
| Cool -> solver := propagateMu ~_onestep: onestep
| Cool -> solver := propagateMu
| PGSolver algo -> solver := fun () -> solveGameWithPGsolver algo
| PGSolverLocal algo -> solver := fun () -> solveGameWithPGsolverLocal algo
end;
......@@ -1190,9 +1119,9 @@ type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
@return True if sf is satisfiable wrt tbox, false otherwise.
*)
let isSat ?(verbose = false) ?(onestep = false)fragSpec game_solver propagation_rate sorts nomTable tbox sf =
let isSat ?(verbose = false) fragSpec game_solver propagation_rate sorts nomTable tbox sf =
let start = if verbose then Unix.gettimeofday () else 0. in
initReasoner ~onestep: onestep fragSpec game_solver propagation_rate sorts nomTable tbox sf;
initReasoner fragSpec game_solver propagation_rate sorts nomTable tbox sf;
let sat =
try
buildGraphLoop ();
......
......@@ -14,28 +14,27 @@ type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
exception ReasonerError of string
module R_com = CoAlgReasoner_common
module type S = sig
module G : CoolGraph.S
(** Specifies when cool propagates sat/unsat information. *)
type propagation_rate = G.propagation_rate =
(*type propagation_rate = G.propagation_rate =
| Once (** Propagate only when the tableaux is fully expanded *)
| Adaptive (** Automatic mode based on the number of open states *)
| Fixed of int (** Propagate after this many expansion steps *)
type game_solver = PGSolver of Paritygame.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
| Cool*)
val isSat : ?verbose:bool -> ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver
-> propagation_rate -> sortTable
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> R_com.game_solver
-> R_com.propagation_rate -> sortTable
-> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
val initReasoner : ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver -> propagation_rate
val initReasoner : CoAlgMisc.fragment_spec -> R_com.game_solver -> R_com.propagation_rate
-> sortTable -> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list
-> CoAlgFormula.sortedFormula -> unit
......
This diff is collapsed.
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
@author Florian Widmann
*)
open FocusTracking
type sortTable = (CoAlgMisc.functors * int list) array
type nomTable = string -> CoAlgFormula.sort option
type assumptions = CoAlgFormula.sortedFormula list
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
exception ReasonerError of string
module type S = sig
module G : CoolGraph.S
(** Specifies when cool propagates sat/unsat information. *)
type propagation_rate = G.propagation_rate =
| Once (** Propagate only when the tableaux is fully expanded *)
| Adaptive (** Automatic mode based on the number of open states *)
| Fixed of int (** Propagate after this many expansion steps *)
type game_solver = PGSolver of Paritygame.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
val isSat : ?verbose:bool -> ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver
-> propagation_rate -> sortTable
-> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
val initReasoner : ?onestep:bool
-> CoAlgMisc.fragment_spec -> game_solver -> propagation_rate
-> 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.
This is used in the debugger.
*)
val runReasonerStep : unit -> unit
val reasonerFinished : unit -> bool
val isRootSat : unit -> bool option
end
module Make (T : FocusTracker) : S
(* vim: set et sw=2 sts=2 ts=8 : *)
module PG = Paritygame
(*module type S = sig
module G : CoolGraph.S*)
type game_solver = PGSolver of PG.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
(*Hier noch G.propagation_rate einfügen, siehe git*)
type propagation_rate (*= G.propagation_rate*) = Once | Adaptive | Fixed of int
This diff is collapsed.
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
@author Florian Widmann
*)
open FocusTracking
type sortTable = (CoAlgMisc.functors * int list) array
type nomTable = string -> CoAlgFormula.sort option
type assumptions = CoAlgFormula.sortedFormula list
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
exception ReasonerError of string
module R_com = CoAlgReasoner_common
module type S = sig
module G : CoolGraph.S
(** Specifies when cool propagates sat/unsat information. *)
(* type propagation_rate = G.propagation_rate =
| Once (** Propagate only when the tableaux is fully expanded *)
| Adaptive (** Automatic mode based on the number of open states *)
| Fixed of int (** Propagate after this many expansion steps *)
type game_solver = PGSolver of Paritygame.global_solver
| PGSolverLocal of Paritygame.partial_solver
| Cool
*)
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> R_com.game_solver
-> R_com.propagation_rate -> sortTable
-> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
val initReasoner : CoAlgMisc.fragment_spec -> R_com.game_solver -> R_com.propagation_rate
-> 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.
This is used in the debugger.
*)
val runReasonerStep : unit -> unit
val reasonerFinished : unit -> bool
val isRootSat : unit -> bool option
end
module Make (T : FocusTracker) : S
(* vim: set et sw=2 sts=2 ts=8 : *)
......@@ -129,14 +129,14 @@ let ctl_fast_testcases =
use_functor "KD" nop CTL.fastTests
let testcases =
[ "DL98" >::: dl98_testcases
; "CTL" >::: ctl_fast_testcases
[ (*"DL98" >::: dl98_testcases;*)
"CTL" >::: ctl_fast_testcases
; "K" >::: k_testcases
; "KD" >::: kd_testcases
; "K*K" >::: kAndK_testcases
; "K*KD" >::: kAndKd_testcases
; "K+KD" >::: kOrKd_testcases
; "Nominals" >::: nominal_testcases
(*;"Nominals" >::: nominal_testcases*)
; "CL" >::: cl_testcases
; "CL" >::: cl_testcases_2agents
; "PML" >::: pml_testcases (* PML is currently disabled. See CoAlgLogics.ml *)
......
......@@ -10,6 +10,8 @@ module CM = CoAlgMisc
module CF = CoAlgFormula
module EA = EAFormula
module Reasoner = CoAlgReasoner.Make(FocusTracking.PartialPermutationTracker)
module O_Reasoner = CoAlgReasoner_onestep.Make(FocusTracking.PartialPermutationTracker)
module R_com = CoAlgReasoner_common
module NF = Nom2fix
module FE = FunctorParsing
......@@ -30,16 +32,16 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
type options =
{ verbose : bool
; fragment : CM.fragment_spec
; prop_rate : Reasoner.propagation_rate
; game_solver : Reasoner.game_solver
; prop_rate : R_com.propagation_rate
; game_solver : R_com.game_solver
; onestep : bool
}
let defaultOpts =
{ verbose = false
; fragment = CM.Auto
; prop_rate = Reasoner.Adaptive
; game_solver = Reasoner.Cool
; prop_rate = R_com.Adaptive
; game_solver = R_com.Cool
; onestep = false
}
......@@ -90,9 +92,9 @@ let options =
^ " INTEGER: Propagate after this many expansion steps"
; Args.argument =
let parse_prop_rate s = match s with
| "once" -> Reasoner.Once
| "adaptive" -> Reasoner.Adaptive
| _ -> try Reasoner.Fixed (int_of_string s) with
| "once" -> R_com.Once
| "adaptive" -> R_com.Adaptive
| _ -> try R_com.Fixed (int_of_string s) with
| Failure _ -> raise (Args.ParseError ("Invalid integer: " ^ s))
in
Args.Required_arg
......@@ -107,9 +109,9 @@ let options =
^ " \"cool\": Use cool's own game solving implementation (default)"
; Args.argument =
let parse_solver s = match s with
| "cool" -> Reasoner.Cool
| "pgsolver" -> Reasoner.PGSolver Recursive.solve
| "pgsolverlocal" -> Reasoner.PGSolverLocal Stratimprlocal2.partially_solve
| "cool" -> R_com.Cool
| "pgsolver" -> R_com.PGSolver Recursive.solve
| "pgsolverlocal" -> R_com.PGSolverLocal Stratimprlocal2.partially_solve
| _ ->
let splitPrefix str =
try begin
......@@ -125,13 +127,13 @@ let options =
try Solvers.find_solver algo with
| Not_found -> raise (Args.ParseError ("Unknown pgsolver algorithm " ^ algo))
in
Reasoner.PGSolver (solver_factory (Array.of_list []))
R_com.PGSolver (solver_factory (Array.of_list []))
| Some ("pgsolverlocal:", algo) ->
let (solver_factory,_,_) =
try Solvers.find_partial_solver algo with
| Not_found -> raise (Args.ParseError ("Unknown local pgsolver algorithm " ^ algo))
in
Reasoner.PGSolverLocal (solver_factory (Array.of_list []))
R_com.PGSolverLocal (solver_factory (Array.of_list []))
| Some _ | None -> raise (Args.ParseError ("Unknown game solver " ^ s))
in
Args.Required_arg
......@@ -190,7 +192,7 @@ let check_implementation logic onestep =
let choiceSat opts =
let verb = opts.verbose in
let onestep = check_implementation Sys.argv.(2) opts.onestep
let _onestep = check_implementation Sys.argv.(2) opts.onestep
in
let sorts = (FE.sortTableFromString Sys.argv.(2)) in
......@@ -212,7 +214,9 @@ let choiceSat opts =
incr counter;
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
flush stdout;
printRes (Reasoner.isSat ~onestep:onestep ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f)
if _onestep
then printRes (O_Reasoner.isSat ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f)
else printRes (Reasoner.isSat ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f)
else ()
done
with End_of_file -> ()
......@@ -358,7 +362,7 @@ let _ =
| Args.Error e -> Printf.printf "%s\n\n" e; printUsage (Sys.argv.(0))
| Args.Ok opts ->
match opts.game_solver with
| Reasoner.PGSolverLocal _ when opts.prop_rate <> Reasoner.Once ->
| R_com.PGSolverLocal _ when opts.prop_rate <> R_com.Once ->
Printf.printf "Error: pgsolverlocal can not be used with intermediate propagation\n"
| _ ->
match choice with
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment