Commit d9985960 authored by Simon Prucker's avatar Simon Prucker
Browse files

Eliminated duplicate implementation

parent 7e9ef18e
Pipeline #15204 failed with stages
in 23 minutes and 40 seconds
......@@ -953,7 +953,7 @@ let expandState state =
let getModalFormulaList state =
let filterTopLevelModalities state =
let filteredList = CoAlgMisc.bsetFilter (stateGetBs state) (fun lf -> CoAlgMisc.lfIsModality (stateGetSort state) lf) in
filteredList
......@@ -971,7 +971,7 @@ let expandStateOneStep state =
stateAddChild state core;
coreAddParent core state sort in
let formulaList = getModalFormulaList state in
let formulaList = filterTopLevelModalities state in
let powerset = CoAlgMisc.bsetNonEmptyPowersets formulaList in
List.iter createCore powerset;
stateSetStatus state Open
......
......@@ -8,6 +8,7 @@ open Cool
module CM = CoAlgMisc
module CF = CoAlgFormula
module CL = CoAlgLogics.Make(FocusTracking.PartialPermutationTracker)
module EA = EAFormula
module G = CoolGraph
module Reasoner = CoAlgReasonerOneStepTableau.Make(FocusTracking.PartialPermutationTracker)
......@@ -19,9 +20,6 @@ module FE = FunctorParsing
open CoolUtils
let a_list_functor_tableau_onestep =
["K", "ot"; "CL", "t"; "GML", "o"; "PML", ""]
(* A partial function mapping nominals to their sorts. *)
let nomTable name =
assert (CoAlgFormula.isNominal name);
......@@ -184,22 +182,23 @@ let printUsage name =
let counter = ref 0
exception Not_Implemented of string
let check_implementation logic onestep =
match (List.assoc logic a_list_functor_tableau_onestep) with
| "ot" | "to" -> onestep
| "o" -> let _ = (print_endline "\nOnly onestep implementation available") in true
| "t" -> let _ = (print_endline "\nOnly tableau implementation available") in false
| _ -> raise (Not_Implemented (logic ^ " is not implemented!"))
let choiceSat opts =
let verb = opts.verbose in
let onestep = check_implementation Sys.argv.(2) opts.onestep
let onestep = match (CM.functor_of_string Sys.argv.(2) []) with
| None -> false
| Some x -> match (List.assoc_opt x CL.implementationLookup) with
| None -> raise (Not_Implemented "This Functor is not implemented")
| Some x -> match x with
| These (_,_) -> let _ = (print_endline "\nBoth onestep and tableau implementation available") in opts.onestep
| That _ -> let _ = (print_endline "\nOnly onestep implementation available") in true
| This _ -> let _ = (print_endline "\nOnly tableau implementation available") in false
in
let sorts = (FE.sortTableFromString Sys.argv.(2)) in
(* test if GML or PML occurs in sort table *)
(* test if PML occurs in sort table *)
if Array.fold_left (fun x (func,_) -> x || func == CM.PML) false sorts then
raise (CF.CoAlgException "PML are currently not supported")
raise (CF.CoAlgException "PML is currently not supported")
else ();
let printRes sat =
......
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