Skip to content
GitLab
Commit 88a4a2e4 authored by Merlin's avatar Merlin 💧
Browse files

Merge branch 'onestep' into 'master' 

Onestep

See merge request !9
parents 9ce630e3 fd1237b5
Pipeline #15211 passed with stages
in 22 minutes and 19 seconds
Expand all Hide whitespace changes
Inline Side-by-side
default.nix
View file @ 88a4a2e4
let
sources = import ./nix/sources.nix { };
withStatic = p: p.overrideAttrs (o: { dontDisableStatic = true; });
withoutTests = p: p.override { doCheck = false; };
nixpkgs = import sources.nixpkgs { };
versions = import ./nix/version.nix;
ocamline = nixpkgs.ocamlPackages.buildDunePackage {
......@@ -16,13 +17,17 @@ with nixpkgs; rec {
cool-lib = ocamlPackages.callPackage ./nix/cool-lib.nix {
inherit versions ocamline;
minisat = pkgs.minisat;
cool-generators = withoutTests cool-generators;
};
cool = ocamlPackages.callPackage ./nix/cool.nix {
inherit versions cool-lib cool-generators;
inherit versions;
minisat = pkgs.minisat;
cool-generators = withoutTests cool-generators;
cool-lib = withoutTests cool-lib;
};
cool-generators = ocamlPackages.callPackage ./nix/cool-generators.nix {
inherit versions cool-lib;
inherit versions;
cool-lib = withoutTests cool-lib;
};
cool-static = cool.override (o: {
doCheck = false;
......@@ -34,6 +39,6 @@ with nixpkgs; rec {
cool-devenv = mkShell {
inputsFrom = [ cool cool-lib cool-generators ];
packages = with ocamlPackages; [ ocaml-lsp ];
packages = with ocamlPackages; [ ocaml-lsp dune_2 ];
};
}
dune → dune-workspace
View file @ 88a4a2e4
(lang dune 2.8)
;; This disables a few warnings
;; 6: missing label applications as they most likely are intentional
;; 8: unused value as somethimes code is left over or for future use
......@@ -5,4 +6,4 @@
;; 32: unmatched values warnings are sometimes intentional
(env
(dev
(flags (:standard -w -6-8-24-32))))
\ No newline at end of file
(flags (:standard -w -6-8-24-32-67 -alert -all--all))))
lib/dune
View file @ 88a4a2e4
;; This disables a few warnings
;; 6: missing label applications as they most likely are intentional
;; 8: unused value as somethimes code is left over or for future use
;; 24: bad module name as our executables are not modules and we dont care
;; 32: unmatched values warnings are sometimes intentional
(env
(dev
(flags (:standard -w -6-8-24-32))))
\ No newline at end of file
lib/dune-project
View file @ 88a4a2e4
(lang dune 1.11)
(name cool-lib)
(version 2.0)
(version 2.1)
lib/src/CoAlgFormula.ml
View file @ 88a4a2e4
......@@ -3,7 +3,6 @@
@author Florian Widmann
*)
module HC = HashConsing
module A = AltGenlex
module L = List
......@@ -86,7 +85,6 @@ type sortedFormula = sort * formula
*)
let isNominal s = String.contains s '\''
(** Determines the size of a formula.
@param f A formula.
@return The size of f.
......@@ -412,18 +410,18 @@ let rec exportFormula_buffer sb f =
Buffer.add_string sb "}";
prio 4 f1
| MORETHAN (n, s, f1) ->
Buffer.add_string sb "{>";
Buffer.add_string sb "<";
Buffer.add_string sb (string_of_int n);
Buffer.add_string sb " ";
Buffer.add_string sb s;
Buffer.add_string sb "}";
Buffer.add_string sb ">";
prio 4 f1
| MAXEXCEPT (n, s, f1) ->
Buffer.add_string sb "{<=";
Buffer.add_string sb "[";
Buffer.add_string sb (string_of_int n);
Buffer.add_string sb " ~ ";
Buffer.add_string sb " ";
Buffer.add_string sb s;
Buffer.add_string sb "}";
Buffer.add_string sb "]";
prio 4 f1 (* actually is prio of ~ and not of <= *)
| ID (f1) ->
Buffer.add_string sb "O ";
......@@ -969,41 +967,63 @@ and parse_cimp symtab ts =
@raise CoAlgException if ts does not represent a formula.
*)
and parse_rest symtab ts =
let boxinternals noNo es =
let n =
if noNo then 0
else
match Stream.next ts with
| A.Int n when n >= 0 -> n
| t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: "
in
let (s,denominator) =
match Stream.peek ts with
| Some (A.Ident s1) -> Stream.junk ts; (s1,0)
| Some (A.Kwd c) when c = es -> ("", 0)
| Some (A.Kwd "/") -> begin
Stream.junk ts;
match Stream.next ts with
| A.Int denom when denom > 0 -> ("", denom)
| t -> A.printError mk_exn ~t ~ts "<positive number> (the denominator) expected: "
end
| _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
in
if (denominator < n) then begin
let explanation =
("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator))
in
A.printError mk_exn ~ts ("Nominator must not be larger than the denominator "
^"("^explanation^") at: "
)
end;
let _ =
let boxinternals noNo es =
let n =
if noNo then -1
else
match Stream.next ts with
| A.Kwd c when c = es -> ()
| t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ")
in
(n, denominator, s)
| A.Int n when n >= 0 -> n
| t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: "
in
let (s,denominator) =
match Stream.peek ts with
| Some (A.Ident s1) -> Stream.junk ts; (s1,-1)
| Some (A.Kwd c) when c = es -> ("", -1)
| Some (A.Int i) -> begin
if i < 0 then
A.printError mk_exn ~ts "grade has to be >= 0"
else
(Stream.junk ts ;
match Stream.peek ts with
| Some (A.Ident s1) -> Stream.junk ts ; (s1, i)
| Some (A.Kwd c) when c = es -> ("", i)
| _ -> A.printError
mk_exn ~ts ("action or " ^ es ^ " expected:"))
end
| Some (A.Kwd "/") ->
begin
let check_for_action denom =
match Stream.peek ts with
| Some x -> begin
match x with
| A.Ident c -> Stream.junk ts ; (c, denom)
| _ -> ("", denom)
end
| None -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
in
Stream.junk ts;
match Stream.next ts with
| A.Int denom when denom > 0 -> check_for_action denom
| t -> A.printError mk_exn ~t ~ts "<positive number> (the denominator) expected: "
end
| _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
in
if (denominator < n) then begin
let explanation =
("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator))
in
A.printError mk_exn ~ts ("Nominator must not be larger than the denominator "
^"("^explanation^") at: "
)
end;
let _ =
match Stream.next ts with
| A.Kwd c when c = es -> ()
| t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ")
in
(n, denominator, s)
in
let rec agentlist es =
let allAgents = CoolUtils.cl_get_agents () in
match Stream.next ts with
......@@ -1040,13 +1060,20 @@ and parse_rest symtab ts =
let f = parse_rest symtab ts in
AT (s, f)
| A.Kwd "<" ->
let (_, _, s) = boxinternals true ">" in
let (_, d, s) = boxinternals true ">" in
let f1 = parse_rest symtab ts in
EX (s, f1)
if d = -1 then
EX (s, f1)
else
MORETHAN (d, s, f1)
| A.Kwd "[" ->
let (_, _, s) = boxinternals true "]" in
let (_, d, s) = boxinternals true "]" in
let f1 = parse_rest symtab ts in
AX (s, f1)
if d = -1 then
AX (s, f1)
else
MAXEXCEPT (d, s, f1)
| A.Kwd "[{" ->
let ls = agentlist "}]" in
let f1 = parse_rest symtab ts in
......@@ -2510,4 +2537,80 @@ module HcFHt = Hashtbl.Make(
end
)
let rec parseFormulaToTree formula =
let open CoolUtils.Tree in
match formula with
| TRUE -> Leaf TRUE
| FALSE -> Leaf FALSE
| AP a -> Leaf (AP a)
| NOT f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> NOT (List.hd fList)), (getHeight child) + 1)
| AT (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> AT (s, List.hd fList)), (getHeight child) + 1)
| OR (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> OR (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| AND (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> AND (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| EQU (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> EQU (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| IMP (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> IMP (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| EX (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> EX (s, List.hd fList)), (getHeight child) + 1)
| AX (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> AX (s, List.hd fList)), (getHeight child) + 1)
| ENFORCES (iL, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> ENFORCES (iL, List.hd fList)), (getHeight child) + 1)
| ALLOWS (iL, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> ALLOWS (iL, List.hd fList)), (getHeight child) + 1)
| MIN (i, s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MIN (i, s, List.hd fList)), (getHeight child) + 1)
| MAX (i, s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MAX (i, s, List.hd fList)), (getHeight child) + 1)
| MORETHAN (i, s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MORETHAN (i, s, List.hd fList)), (getHeight child) + 1)
| MAXEXCEPT (i, s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MAXEXCEPT (i, s, List.hd fList)), (getHeight child) + 1)
| ATLEASTPROB (r, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> ATLEASTPROB (r, List.hd fList)), (getHeight child) + 1)
| LESSPROBFAIL (r, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> LESSPROBFAIL (r, List.hd fList)), (getHeight child) + 1)
| CONST s -> Leaf (CONST s)
| CONSTN s -> Leaf (CONSTN s)
| ID f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> ID (List.hd fList)), (getHeight child) + 1)
| NORM (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> NORM (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| NORMN (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> NORMN (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| CHC (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> CHC (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| FUS (b, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> FUS (b, List.hd fList)), (getHeight child) + 1)
| MU (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> MU (s, List.hd fList)), (getHeight child) + 1)
| NU (s, f) -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> NU (s, List.hd fList)), (getHeight child) + 1)
| VAR s -> Leaf (VAR s)
| AF f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> AF (List.hd fList)), (getHeight child) + 1)
| EF f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> EF (List.hd fList)), (getHeight child) + 1)
| AG f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> AG (List.hd fList)), (getHeight child) + 1)
| EG f -> let child = parseFormulaToTree f in
Node ([child], (fun fList -> EG (List.hd fList)), (getHeight child) + 1)
| AU (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> AU (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| EU (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> EU (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| AR (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> AR (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| ER (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> ER (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| AB (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> AB (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
| EB (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> EB (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
(* vim: set et sw=2 sts=2 ts=8 : *)
lib/src/CoAlgFormula.mli
View file @ 88a4a2e4
......@@ -188,4 +188,9 @@ val hc_freeIn2 : string -> hcFormula -> bool
module HcFHt : (Hashtbl.S with type key = hcFormula)
(**
Parses a formula into a tree representation, where each node contains a connective. The tree structure then supports simplification and recombination of formulae.
**)
val parseFormulaToTree: formula -> formula CoolUtils.Tree.tree
(* vim: set et sw=2 sts=2 ts=8 : *)
lib/src/CoAlgLogics.ml
View file @ 88a4a2e4
......@@ -7,6 +7,8 @@ open CoAlgMisc
open CoolUtils
open CoAlgLogicUtils
module O = Option
module S = MiscSolver
module type S = sig
......@@ -16,8 +18,11 @@ module type S = sig
type rule = (dependencies * (sort * bset * focus) lazylist)
type stateExpander = rule lazylist
type ruleEnumeration = rule lazyliststep
type implementation = ((sort -> bset -> focus -> sort list -> stateExpander), (bset list -> (sort * bset) -> bool)) these
val getExpandingFunctionProducer : functors -> sort -> bset -> focus -> sort list -> stateExpander
val oneStepSatisfiability : functors -> (bset list -> (sort * bset) -> bool)
val implementationLookup : (functors * implementation) list
end
module Make (T: FocusTracking.FocusTracker) = struct
......@@ -30,6 +35,12 @@ type ruleEnumeration = rule lazyliststep
module Focus = T
type implementation = ((sort -> bset -> focus -> sort list -> stateExpander), (bset list -> (sort * bset) -> bool)) these
let getTableau = These.fst
let getOneStepFun = These.snd
(** directly return a list of rules **)
let mkRuleList_MultiModalK sort bs focus sl : rule list =
(* arguments:
......@@ -433,11 +444,6 @@ let mkRule_CL sort bs focus sl : stateExpander =
The implementation can still be found in the git history.
*)
let mkRule_GML _sort _bs _defer _sl : stateExpander =
raise (CoAlgFormula.CoAlgException "GML is currently not implemented.")
let mkRule_PML _sort _bs _defer _sl : stateExpander =
raise (CoAlgFormula.CoAlgException "PML is currently not implemented.")
(* constant functor *)
let mkRule_Const colors sort bs _defer sl : stateExpander =
......@@ -490,9 +496,6 @@ let mkRule_Identity sort bs focus sl : stateExpander =
lazylistFromList [(dep, lazylistFromList [(s1, bs1, Focus.finalize focus1)])]
let mkRule_DefaultImplication _sort _bs _defer _sl : stateExpander =
raise (CoAlgFormula.CoAlgException ("Default Implication Not yet implemented."))
let mkRule_Choice sort bs focus sl : stateExpander =
assert (List.length sl = 2);
let dep bsl =
......@@ -568,21 +571,99 @@ let mkRule_Fusion sort bs focus sl : stateExpander =
(dep 1, lazylistFromList [(s2, bs2, Focus.finalize focus2)])]
(* Maps a logic represented by the type "functors" to the corresponding
"plug-in" function.
*)
let getExpandingFunctionProducer = function
| MultiModalK -> mkRule_MultiModalK
| MultiModalKD -> mkRule_MultiModalKD
| Monotone -> mkRule_Monotone
| CoalitionLogic -> mkRule_CL
| GML -> mkRule_GML
| PML -> mkRule_PML
| Constant colors -> mkRule_Const colors
| Identity -> mkRule_Identity
| DefaultImplication -> mkRule_DefaultImplication
| Choice -> mkRule_Choice
| Fusion -> mkRule_Fusion
let oneStepSat_MultiModalK (u: bset list) sv =
let (sort, v) = sv in
let boxes = bsetFilter v (fun lf -> (lfGetType sort lf) = AxF) in
let diamonds = bsetFilter v (fun lf -> (lfGetType sort lf) = ExF) in
let boxargsForRel rel = bsetMap (lfGetDest1 sort) (bsetFilter boxes (fun r -> (lfGetDest3 sort r) = rel)) in
(*Make reduced U. Will be applied for each relation*)
let redU args = List.filter (fun bs -> bsetIsSubOrEqual args bs) u in
(*check if reducedU contains formula for every diamond per relation*)
let existsInU rel lf = List.exists (fun bs -> bsetMem bs lf) (redU (boxargsForRel rel)) in
bsetForall diamonds (fun lf -> existsInU (lfGetDest3 sort lf) (lfGetDest1 sort lf))
(**
Recursive helper function for handling One-Step satisfiability of GML formulae for one individual relation.
**)
let rec oneStepGMLRec counters sort v currentU =
let isExceedingBox lf = (lfGetType sort lf = MaxExceptF) && ((lfGetDestNum sort lf) < (Hashtbl.find counters lf)) in
if (bsetExists v isExceedingBox)
then false
else
let filterUnsatDiamond lf = (lfGetType sort lf = MoreThanF) && ((lfGetDestNum sort lf) >= (Hashtbl.find counters lf)) in
let filteredV = bsetFilter v filterUnsatDiamond in
if (bsetIsSubOrEqual filteredV (bsetMake())) then true
else
let filterCoreLabels bset =
bsetExists filteredV (fun lf -> bsetMem bset (lfGetDest1 sort lf)) in
let filteredU = List.filter filterCoreLabels currentU in
if filteredU = [] then false (* ensures early termination and guards the List.hd below *)
else
let u = List.hd filteredU in
let updateCountersAdd lf =
let modalArg = lfGetDest1 sort lf in
let newVal = (Hashtbl.find counters lf) + 1 in
match lfGetType sort lf with
| MoreThanF -> if bsetMem u modalArg then Hashtbl.add counters lf newVal
| MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.add counters lf newVal
| _ -> ()
in
let updateCountersRem lf =
let modalArg = lfGetDest1 sort lf in
match lfGetType sort lf with
| MoreThanF -> if bsetMem u modalArg then Hashtbl.remove counters lf
| MaxExceptF -> if not (bsetMem u modalArg) then Hashtbl.remove counters lf
| _ -> ()
in
bsetIter updateCountersAdd v;
if ((oneStepGMLRec counters sort v filteredU)) then true
else begin
bsetIter updateCountersRem v;
if (oneStepGMLRec counters sort v (List.tl filteredU)) then true
else false
end
(**
Checks One-Step satisfaction for GML formulae by setting up counters for each relation and then recursively handling all boxes and diamonds for one relation independently.
**)
let oneStepSat_GML u sv =
let (sort, v) = sv in
let rels = bsetFold (fun lf accu -> let role = lfGetDest3 sort lf in role :: accu) v [] in
let reled_v = List.map (fun rel -> (rel, bsetFilter v (fun lf -> lfGetDest3 sort lf = rel))) rels in
List.for_all (fun (_rel, sub_v) ->
let counters = Hashtbl.create (bsetLen sub_v) in
bsetIter (fun lf -> Hashtbl.add counters lf 0) v;
oneStepGMLRec counters sort sub_v u
) reled_v
(**
Records the available sat-checking mechanisms for the individual functors, first tableau, second one-step.
**)
let implementationLookup = [ (MultiModalK, These (mkRule_MultiModalK, oneStepSat_MultiModalK))
; (MultiModalKD, This mkRule_MultiModalKD)
; (Monotone, This mkRule_Monotone)
; (CoalitionLogic, This mkRule_CL)
(* ; (Constant colors, ost mkRule_Const colors) *) (* this is an issue because we can't bind this here... *)
; (Identity, This mkRule_Identity)
; (Choice, This mkRule_Choice)
; (Fusion, This mkRule_Fusion)
; (GML, That oneStepSat_GML)
]
let oval o d = match o with
| None -> d ()
| Some v -> v
let obind o f = match o with
| None -> None
| Some v -> f v
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)))
end
......
lib/src/CoAlgLogics.mli
View file @ 88a4a2e4
......@@ -4,6 +4,7 @@
open CoAlgMisc
open CoolUtils
module type S = sig
type focus
......@@ -12,8 +13,11 @@ module type S = sig
type rule = (dependencies * (sort * bset * focus) lazylist)
type stateExpander = rule lazylist
type ruleEnumeration = rule lazyliststep
type implementation = ((sort -> bset -> focus -> sort list -> stateExpander), (bset list -> (sort * bset) -> bool)) these
val getExpandingFunctionProducer : functors -> sort -> bset -> focus -> sort list -> stateExpander
val oneStepSatisfiability : functors -> bset list -> (sort * bset) -> bool
val implementationLookup : (functors * implementation) list
end
module Make (T: FocusTracking.FocusTracker) : S with type focus = T.t
......
lib/src/CoAlgMisc.ml
View file @ 88a4a2e4
......@@ -7,6 +7,7 @@ module S = MiscSolver
module L = List
module C = CoAlgFormula
module HC = HashConsing
open CoolUtils
(** An instantiation of a set (of the standard library) for bitsets.
*)
......@@ -93,6 +94,7 @@ let unaryfunctor2name : (functorName*string) list =
; (NPa Identity, "Identity")
]
let functor2name : (functorName*string) list =
L.append unaryfunctor2name
[ (NPa Choice , "Choice")
......@@ -139,7 +141,7 @@ type formulaType =
| TrueFalseF (* constant true or false *)
| AndF
| OrF
| AtF
| AtF (* Atomic Formula *)
| NomF
| ExF (* Existential / diamond *)
| AxF (* Universal / box *)
......@@ -263,6 +265,11 @@ let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function
| Conjunctive l -> (l, fun x -> Conjunctive x)
let formulaTypeIsModality ftype =
match ftype with
| ExF | AxF | EnforcesF | AllowsF | MoreThanF | MaxExceptF | AtLeastProbF | LessProbFailF -> true
| Other | TrueFalseF | AndF | OrF | AtF | NomF | ConstF | ConstnF | IdF | NormF | NormnF | ChcF | FusF | MuF | NuF -> false
(*****************************************************************************)
(* "Module type" and a specific implementation of the mapping *)
(* between (local) formulae and literals of the sat solver, *)
......@@ -275,6 +282,10 @@ let lhtFind lht lit =
try
Some (LHt.find lht lit)
with Not_found -> None
let lhtMustFind lht l =
match lhtFind lht l with
| Some f -> f
| None -> assert false
let fhtInit () = FHt.create 16
let fhtAdd fht f lit = FHt.add fht f lit
......@@ -282,6 +293,10 @@ let fhtFind fht f =
try
Some (FHt.find fht f)
with Not_found -> None
let fhtMustFind fht f =
match fhtFind fht f with
| Some l -> l
| None -> assert false
let fhtReset fht = FHt.reset fht
let nhtInit () = NHt.create 8
......@@ -304,10 +319,9 @@ let bsetAdd bs lf = S.addBSNoChk bs lf
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 () =
let res = bsetMake () in
bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
res
let bsetMakeRealEmpty () = S.makeEmptyBS ()
let bsetSingleton lf =
let res = bsetMakeRealEmpty () in
bsetAdd res lf;
......@@ -315,11 +329,22 @@ let bsetSingleton lf =
let bsetCopy bs = S.copyBS bs
let bsetFold fkt bs init = S.foldBS fkt bs init
let bsetIter fkt bset = S.iterBS fkt bset
let bsetMap fkt bset = S.endoMapBS fkt bset
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
let res = bsetMakeRealEmpty () in
bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
res
let bsetNonEmptyPowersets bset =