diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index c7f4a376ed0cdaf01b58ecd44f4124dd3328321f..45d99f410094db6382f78851512fb86b9685003a 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -11,8 +11,8 @@ open Gmlmip
module S = MiscSolver
(** directly return a list of rules **)
-let mkRuleList_MultiModalK sort bs sl : rule list =
- (* arguments:
+let mkRuleList_MultiModalK sort bs defer sl : rule list =
+ (* arguments:
sort: type of formulae in bs (needed to disambiguate hashing)
sl: sorts functor arguments, e.g. type of argument formulae
bs: tableau sequent consisting of modal atoms
@@ -26,6 +26,13 @@ let mkRuleList_MultiModalK sort bs sl : rule list =
NB: propagating the whole premiss is always safe.
*)
assert (List.length sl = 1);
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+ let deferral =
+ if refocusing then
+ bsetCopy bs
+ else
+ defer
+ in
let dep f bsl = (* dependencies for formula f (f is a diamond) *)
assert (List.length bsl = 1); (* -+ *)
let bs1 = List.hd bsl in (* -+-> [bs1] := bsl *)
@@ -46,17 +53,27 @@ let mkRuleList_MultiModalK sort bs sl : rule list =
let getRules f acc =
if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *)
let bs1 = bsetMake () in
- bsetAdd bs1 (lfGetDest1 sort f); (* bs1 := { C } *)
+ let defer1 = bsetMakeRealEmpty () in
+ let nextf = (lfGetDest1 sort f) in
+ bsetAdd bs1 nextf; (* bs1 := { C } *)
+ if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ then
+ bsetAdd defer1 nextf;
let (role : int) = lfGetDest3 sort f in (* role := R *)
let filterFkt f1 =
if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
(* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
- bsetAdd bs1 (lfGetDest1 sort f1)
+ let nextf1 = (lfGetDest1 sort f1) in
+ bsetAdd bs1 nextf1;
+ (if (bsetMem defer f1) &&
+ (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1) then
+ bsetAdd defer1 nextf1;)
else ()
in
bsetIter filterFkt bs; (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
let s1 = List.hd sl in (* [s1] := sl *)
- let rle = (dep f, lazylistFromList [(s1, bs1)]) in
+ let rle = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
rle::acc
else acc
in
@@ -72,14 +89,14 @@ let mkRuleList_MultiModalK sort bs sl : rule list =
*)
bsetFold getRules bs []
-let mkRule_MultiModalK sort bs sl : stateExpander =
- let rules = mkRuleList_MultiModalK sort bs sl in
+let mkRule_MultiModalK sort bs defer sl : stateExpander =
+ let rules = mkRuleList_MultiModalK sort bs defer sl in
lazylistFromList rules
(* TODO: test it with:
make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True'
*)
-let mkRule_MultiModalKD sort bs sl : stateExpander =
+let mkRule_MultiModalKD sort bs defer sl : stateExpander =
assert (List.length sl = 1); (* functor has just one argument *)
let s1 = List.hd sl in (* [s1] = sl *)
let roles = S.makeBS () in
@@ -114,6 +131,7 @@ let mkRule_MultiModalKD sort bs sl : stateExpander =
res
in
let succs = bsetMake () in (* succs := {D | ∀r.D ∈ bs *)
+ let defer1 = bsetMake () in (* TODO: actually track deferrals *)
let f formula =
if lfGetType sort formula = AxF
&& lfGetDest3 sort formula = r
@@ -121,7 +139,7 @@ let mkRule_MultiModalKD sort bs sl : stateExpander =
else ()
in
bsetIter f bs;
- (dep r, lazylistFromList [(s1, succs)])::acc
+ (dep r, lazylistFromList [(s1, succs, defer1)])::acc
in
(*
mkRule_MultiModalKD sort bs [s1]
@@ -132,7 +150,7 @@ let mkRule_MultiModalKD sort bs sl : stateExpander =
}
∪ mkRule_MultiModalK sort bs [s1]
*)
- let rules = mkRuleList_MultiModalK sort bs sl in
+ let rules = mkRuleList_MultiModalK sort bs defer sl in
(* extend rules from K with enforcing of successors *)
let rules = S.foldBS getRules roles rules in
lazylistFromList rules
@@ -196,14 +214,15 @@ let compatible sort (a: bset) formula1 =
/ \i=1 a_i /\ b / \j=1 c_j
*)
-(* Not yet implemented: backjumping hooks.
+(* Not yet implemented: backjumping hooks.
E.g. in Rule 1, if a subset I of {a_1, ..., a_n} is unsat, then {[C_i] a_i : i \in I} is
already unsat.
*)
-let mkRule_CL sort bs sl : stateExpander =
+let mkRule_CL sort bs defer sl : stateExpander =
assert (List.length sl = 1); (* TODO: Why? *)
+ let defer1 = bsetMake () in (* TODO: track deferrals *)
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let boxes = bsetFilter bs (fun f -> lfGetType sort f = EnforcesF) in
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
@@ -242,7 +261,7 @@ let mkRule_CL sort bs sl : stateExpander =
let children = bsetMakeRealEmpty () in
List.iter (bsetAdd children) (b::c_j) ;
List.iter (bsetAdd children) (a_i) ;
- ((fun bs1 -> bs), lazylistFromList [(s1, children)])::acc
+ ((fun bs1 -> bs), lazylistFromList [(s1, children, defer1)])::acc
in
List.fold_left createSingleRule acc maxdisj
in
@@ -256,7 +275,7 @@ let mkRule_CL sort bs sl : stateExpander =
*)
let a_i : bset = bsetMakeRealEmpty () in
bsetIter (fun f -> bsetAdd a_i (lfGetDest1 sort f)) coalitions ;
- ((fun bs1 -> bs), lazylistFromList [(s1, a_i)])::acc
+ ((fun bs1 -> bs), lazylistFromList [(s1, a_i, defer1)])::acc
in
let rules = List.fold_left getRule1 rules disjoints in
(*
@@ -268,8 +287,9 @@ let mkRule_CL sort bs sl : stateExpander =
*)
lazylistFromList rules
-let mkRule_GML sort bs sl : stateExpander =
+let mkRule_GML sort bs defer sl : stateExpander =
assert (List.length sl = 1);
+ let defer1 = bsetMake () in (* TODO: track deferrals *)
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
let boxes = bsetFilter bs (fun f -> lfGetType sort f = MaxExceptF) in
@@ -305,7 +325,7 @@ let mkRule_GML sort bs sl : stateExpander =
in
bsetAdd res f)
conj;
- (s1,res)
+ (s1,res, defer1)
in
let rc = List.map handleConjunction rc in
((fun bs1 -> bs),lazylistFromList rc)::acc
@@ -314,8 +334,9 @@ let mkRule_GML sort bs sl : stateExpander =
let rules = S.foldBS addRule roles [] in
lazylistFromList rules
-let mkRule_PML sort bs sl : stateExpander =
+let mkRule_PML sort bs defer sl : stateExpander =
assert (List.length sl = 1);
+ let defer1 = bsetMake () in (* TODO: track deferrals *)
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AtLeastProbF) in
let boxes = bsetFilter bs (fun f -> lfGetType sort f = LessProbFailF) in
@@ -352,7 +373,7 @@ let mkRule_PML sort bs sl : stateExpander =
end
in
List.iter handleLiteral conj;
- (s1,res)
+ (s1,res, defer1)
in
let rc = List.map handleConjunction rc in
((fun bs1 -> bs),lazylistFromList rc)::acc
@@ -361,7 +382,7 @@ let mkRule_PML sort bs sl : stateExpander =
lazylistFromList rules
(* constant functor *)
-let mkRule_Const colors sort bs sl : stateExpander =
+let mkRule_Const colors sort bs defer sl : stateExpander =
assert (List.length sl = 1); (* just one (formal) argument *)
let helper (f:localFormula) (pos, neg) =
let col = lfGetDest3 sort f in
@@ -370,17 +391,18 @@ let mkRule_Const colors sort bs sl : stateExpander =
| ConstF -> ((col::pos), neg)
| _ -> (pos, neg)
in
- let (pos, neg) = bsetFold helper bs ([], []) in (* pos/neg literals *)
+ let (pos, neg) = bsetFold helper bs ([], []) in (* pos/neg literals *)
let clash = List.exists (fun l -> List.mem l pos) neg in (* =a /\ ~ = a *)
let allneg = List.length colors = List.length neg in
let twopos = List.length pos > 1 in
- let rules = if (clash || allneg || twopos)
+ let rules = if (clash || allneg || twopos)
then [((fun x -> bs), lazylistFromList [])] (* no backjumping *)
else []
- in
+ in
lazylistFromList rules
-let mkRule_Identity sort bs sl : stateExpander =
+let mkRule_Identity sort bs defer sl : stateExpander =
+ let defer1 = bsetMake () in (* TODO: track deferrals *)
assert (List.length sl = 1); (* Identity has one argument *)
let s1 = List.hd sl in
let dep bsl = (* return arguments prefixed with identity operator *)
@@ -398,19 +420,20 @@ let mkRule_Identity sort bs sl : stateExpander =
in
let bs1 = bsetMake () in
let getRule f =
- if lfGetType sort f = IdF
+ if lfGetType sort f = IdF
then bsetAdd bs1 (lfGetDest1 sort f)
else ()
in
bsetIter getRule bs;
- lazylistFromList [(dep, lazylistFromList [(s1, bs1)])]
+ lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1)])]
-let mkRule_DefaultImplication sort bs sl : stateExpander =
+let mkRule_DefaultImplication sort bs defer sl : stateExpander =
raise (CoAlgFormula.CoAlgException ("Default Implication Not yet implemented."))
-
-let mkRule_Choice sort bs sl : stateExpander =
+
+let mkRule_Choice sort bs defer sl : stateExpander =
assert (List.length sl = 2);
+ let defer1 = bsetMake () in (* TODO: track deferrals *)
let dep bsl =
assert (List.length bsl = 2);
let bs1 = List.nth bsl 0 in
@@ -436,11 +459,12 @@ let mkRule_Choice sort bs sl : stateExpander =
bsetIter getRule bs;
let s1 = List.nth sl 0 in
let s2 = List.nth sl 1 in
- lazylistFromList [(dep, lazylistFromList [(s1, bs1); (s2, bs2)])]
+ lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1); (s2, bs2, defer1)])]
-let mkRule_Fusion sort bs sl : stateExpander =
+let mkRule_Fusion sort bs defer sl : stateExpander =
assert (List.length sl = 2);
+ let defer1 = bsetMake () in (* TODO: track deferrals *)
let dep proj bsl =
assert (List.length bsl = 1);
let bs1 = List.hd bsl in
@@ -465,7 +489,7 @@ let mkRule_Fusion sort bs sl : stateExpander =
bsetIter getRule bs;
let s1 = List.nth sl 0 in
let s2 = List.nth sl 1 in
- lazylistFromList [(dep 0, lazylistFromList [(s1, bs1)]); (dep 1, lazylistFromList [(s2, bs2)])]
+ lazylistFromList [(dep 0, lazylistFromList [(s1, bs1, defer1)]); (dep 1, lazylistFromList [(s2, bs2, defer1)])]
(* Maps a logic represented by the type "functors" to the corresponding
diff --git a/src/lib/CoAlgLogics.mli b/src/lib/CoAlgLogics.mli
index 48d0958b68bceec89898bf9788866dea0e7084bc..dd5c9ad4230fb0ae152217bd8b8c7cf9755e113d 100644
--- a/src/lib/CoAlgLogics.mli
+++ b/src/lib/CoAlgLogics.mli
@@ -6,4 +6,4 @@
open CoAlgMisc
-val getExpandingFunctionProducer : functors -> sort -> bset -> sort list -> stateExpander
+val getExpandingFunctionProducer : functors -> sort -> bset -> bset -> sort list -> stateExpander
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 2ea83af44002edae8f2f5a581ac85bc3c1df01b3..071e169a6f60fe2cb0d21db6f51d401490608651 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -21,6 +21,17 @@ module BsSet = Set.Make(
(** An instantiation of a hash table (of the standard library) for bitsets.
*)
module GHt = Hashtbl.Make(
+ struct
+ type t = S.bitset * S.bitset
+ let equal ((bs1l, bs1r) : t) (bs2l, bs2r) =
+ (S.compareBS bs1l bs2l = 0) && (S.compareBS bs1r bs2r = 0)
+ let hash ((bsl, bsr) : t) = (S.hashBS bsl) lxor (S.hashBS bsr)
+ end
+ )
+
+(** An instantiation of a hash table (of the standard library) for bitsets.
+ *)
+module GHtS = Hashtbl.Make(
struct
type t = S.bitset
let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0
@@ -215,7 +226,7 @@ and setState = state GHt.t array
and setCore = core GHt.t array
-and setCnstr = unit GHt.t
+and setCnstr = unit GHtS.t
(*****************************************************************************)
@@ -237,7 +248,7 @@ and nodeStatus =
and dependencies = bset list -> bset
-and rule = (dependencies * (sort * bset) lazylist)
+and rule = (dependencies * (sort * bset * bset) lazylist)
and 'a lazyliststep =
| MultipleElements of 'a list
@@ -396,14 +407,14 @@ let doSatPropagation () =
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
-let graphCnstrs = ref (GHt.create 0 : constrnt GHt.t)
+let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
let graphRoot = ref (None : core option)
let graphInit () =
let size = Array.length !sortTable in
graphStates := Array.init size (fun _ -> GHt.create 128);
graphCores := Array.init size (fun _ -> GHt.create 128);
- graphCnstrs := GHt.create 128;
+ graphCnstrs := GHtS.create 128;
graphRoot := None
let graphIterStates fkt =
@@ -412,18 +423,18 @@ let graphIterStates fkt =
let graphIterCores fkt =
Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores
-let graphIterCnstrs fkt = GHt.iter fkt !graphCnstrs
+let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs
let graphClearCnstr () =
- let newGraph = GHt.create (GHt.length !graphCnstrs) in
+ let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
let copyCnstr cset cnstr =
match cnstr with
| UnsatC
- | SatC -> GHt.add newGraph cset cnstr
- | OpenC _ -> GHt.add newGraph cset (OpenC [])
- | UnexpandedC _ -> GHt.add newGraph cset (UnexpandedC [])
+ | SatC -> GHtS.add newGraph cset cnstr
+ | OpenC _ -> GHtS.add newGraph cset (OpenC [])
+ | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
in
- GHt.iter copyCnstr !graphCnstrs;
+ GHtS.iter copyCnstr !graphCnstrs;
graphCnstrs := newGraph
let graphFindState sort bs =
@@ -438,7 +449,7 @@ let graphFindCore sort bs =
let graphFindCnstr cset =
try
- Some (GHt.find !graphCnstrs cset)
+ Some (GHtS.find !graphCnstrs cset)
with Not_found -> None
let graphInsertState sort bs state =
@@ -450,17 +461,17 @@ let graphInsertCore sort bs core =
GHt.add !graphCores.(sort) bs core
let graphInsertCnstr cset cnstr =
- assert (not (GHt.mem !graphCnstrs cset));
- GHt.add !graphCnstrs cset cnstr
+ assert (not (GHtS.mem !graphCnstrs cset));
+ GHtS.add !graphCnstrs cset cnstr
let graphReplaceCnstr cset cnstr =
- GHt.replace !graphCnstrs cset cnstr
+ GHtS.replace !graphCnstrs cset cnstr
let graphSizeState () =
Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
let graphSizeCore () =
Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
-let graphSizeCnstr () = GHt.length !graphCnstrs
+let graphSizeCnstr () = GHtS.length !graphCnstrs
let graphAddRoot core =
if !graphRoot = None then graphRoot := Some core
@@ -559,19 +570,25 @@ let coreAddConstraintParent core cset =
let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
-let setEmptyCnstr () = GHt.create 128
-let setAddState set state = GHt.add set.(stateGetSort state) (stateGetBs state) state
-let setAddCore set core = GHt.add set.(coreGetSort core) (coreGetBs core) core
-let setAddCnstr set cset = GHt.add set cset ()
-let setMemState set state = GHt.mem set.(stateGetSort state) (stateGetBs state)
-let setMemCore set core = GHt.mem set.(coreGetSort core) (coreGetBs core)
-let setMemCnstr set cset = GHt.mem set cset
-let setRemoveState set state = GHt.remove set.(stateGetSort state) (stateGetBs state)
-let setRemoveCore set core = GHt.remove set.(coreGetSort core) (coreGetBs core)
-let setRemoveCnstr set cset = GHt.remove set cset
+let setEmptyCnstr () = GHtS.create 128
+let setAddState set state =
+ GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
+let setAddCore set core =
+ GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
+let setAddCnstr set cset = GHtS.add set cset ()
+let setMemState set state =
+ GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
+let setMemCore set core =
+ GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
+let setMemCnstr set cset = GHtS.mem set cset
+let setRemoveState set state =
+ GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
+let setRemoveCore set core =
+ GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
+let setRemoveCnstr set cset = GHtS.remove set cset
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
-let setIterCnstr fkt set = GHt.iter (fun cset () -> fkt cset) set
+let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
(*****************************************************************************)
@@ -613,6 +630,7 @@ let bsetMake () = S.makeBS ()
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 *)
@@ -723,6 +741,8 @@ let coreToString (core:core): string =
"Core "^(string_of_int core.idx)^" {\n"^
" Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
" " ^ bsetToString core.sortC core.bsC ^ "\n" ^
+ " Deferrals: \n" ^
+ " " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
" Constraints: { "^(String.concat
"\n " constraints)^" }\n"^
" Children: { "^(String.concat
@@ -751,6 +771,8 @@ let stateToString (state:state): string =
"State "^(string_of_int state.idx)^" {\n"^
" Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
" " ^ bsetToString state.sortS state.bsS ^ "\n" ^
+ " Deferrals: \n" ^
+ " " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
" Constraints: { "^(String.concat
"\n " constraints)^" }\n"^
" Children: { "^(String.concat
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 160222c47a9a95dff147e113dd8f00f3bb27453c..1dcbf77e7edb92dbe93a85d7e61fbdf4b1518baf 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -95,7 +95,7 @@ and nodeStatus =
and dependencies = bset list -> bset
-and rule = (dependencies * (sort * bset) lazylist)
+and rule = (dependencies * (sort * bset * bset) lazylist)
and 'a lazyliststep =
| MultipleElements of 'a list
@@ -180,11 +180,11 @@ val graphIterStates : (state -> unit) -> unit
val graphIterCores : (core -> unit) -> unit
val graphIterCnstrs : (cset -> constrnt -> unit) -> unit
val graphClearCnstr : unit -> unit
-val graphFindState : sort -> bset -> state option
-val graphFindCore : sort -> bset -> core option
+val graphFindState : sort -> (bset * bset) -> state option
+val graphFindCore : sort -> (bset * bset) -> core option
val graphFindCnstr : cset -> constrnt option
-val graphInsertState : sort -> bset -> state -> unit
-val graphInsertCore : sort -> bset -> core -> unit
+val graphInsertState : sort -> (bset * bset) -> state -> unit
+val graphInsertCore : sort -> (bset * bset) -> core -> unit
val graphInsertCnstr : cset -> constrnt -> unit
val graphReplaceCnstr : cset -> constrnt -> unit
val graphSizeState : unit -> int
@@ -311,6 +311,7 @@ val bsetMake : unit -> bset (* a new bset which only contains True *)
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
val bsetAdd : bset -> localFormula -> unit
val bsetMem : bset -> localFormula -> bool
+val bsetCompare : bset -> bset -> int
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
val bsetIter : (localFormula -> unit) -> bset -> unit
val bsetFilter : bset -> (localFormula -> bool) -> bset
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 4a13a6abaae9ae1ceaa1990939bbc8e988a5d994..e208997c1e8e69e5c58088e5c7f0fe73ead47130 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -413,7 +413,7 @@ let getLit sort fht solver f =
in
lit
-let newCore sort bs =
+let newCore sort bs defer =
(* when creating a now core from a set of formulas bs
bs = { x_1, ...., x_n }
= "x_1 /\ .... /\ x_n"
@@ -499,7 +499,7 @@ let newCore sort bs =
*)
in
bsetIter addClauses bs;
- coreMake sort bs bs solver fht
+ coreMake sort bs defer solver fht
let getNextState core =
(* Create a new state, which is obtained by a satisfying assignment of the
@@ -509,7 +509,13 @@ let getNextState core =
minisat calls.
*)
let bs = coreGetBs core in
- let deferralS = coreGetDeferral core in
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
+ let deferralS =
+ if refocusing then
+ bsetCopy bs
+ else
+ coreGetDeferral core
+ in
let fht = coreGetFht core in
let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
let solver = coreGetSolver core in
@@ -524,7 +530,7 @@ let getNextState core =
satisfiable.
*)
let newbs = bsetMake () in
- let newdefer = bsetMake () in
+ let newdefer = bsetMakeRealEmpty () in
(* if newbs = { l_1, .... l_n }, i.e.
newbs = l_1 /\ ... /\ l_n
@@ -571,15 +577,16 @@ let getNextState core =
(* ... to newbs *)
bsetAdd newbs f;
let defercandidate = lfGetDeferral sort f in
- (if deferral = defercandidate then
+ (if (defercandidate != (Hashtbl.hash "ε") &&
+ (refocusing || deferral = defercandidate)) then
bsetAdd newdefer f);
(* ... and to the new clause *)
(M.neg_lit (fhtMustFind fht f))::acc
in
let init_clause f acc =
let deferral =
- if bsetMem deferralS f then
- lfGetDeferral sort f
+ if bsetMem deferralS f then (
+ lfGetDeferral sort f)
else
(Hashtbl.hash "ε")
in
@@ -593,15 +600,15 @@ let getNextState core =
let newState sort bs defer =
let (func, sl) = !sortTable.(sort) in
let producer = CoAlgLogics.getExpandingFunctionProducer func in
- let exp = producer sort bs sl in
+ let exp = producer sort bs defer sl in
stateMake sort bs defer exp
let insertState parent sort bs defer =
let child =
- match graphFindState sort bs with
+ match graphFindState sort (bs, defer) with
| None ->
let s = newState sort bs defer in
- graphInsertState sort bs s;
+ graphInsertState sort (bs, defer) s;
queueInsertState s;
s
| Some s -> s
@@ -620,20 +627,20 @@ let expandCore core =
else coreSetStatus core Open
-let insertCore sort bs =
- match graphFindCore sort bs with
+let insertCore sort bs defer =
+ match graphFindCore sort (bs, defer) with
| None ->
- let c = newCore sort bs in
- graphInsertCore sort bs c;
- queueInsertCore c;
- c
+ let c = newCore sort bs defer in
+ graphInsertCore sort (bs, defer) c;
+ queueInsertCore c;
+ c
| Some c -> c
let insertRule state dep chldrn =
let chldrn = listFromLazylist chldrn in
- let insert (isUns, acc) (sort, bs) =
+ let insert (isUns, acc) (sort, bs, defer) =
let bs1 = bsetAddTBox sort bs in
- let core = insertCore sort bs1 in
+ let core = insertCore sort bs1 defer in
let isUns1 = if coreGetStatus core = Unsat then isUns else false in
(isUns1, core::acc)
in
@@ -681,7 +688,7 @@ let expandCnstr cset =
in
csetIter cset mkCores;
let inCores (sort, _) bs (isUns, acc) =
- let core = insertCore sort bs in
+ let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
coreAddConstraintParent core cset;
(coreGetStatus core = Unsat || isUns, core::acc)
in
@@ -744,9 +751,15 @@ let initReasoner sorts nomTable tbox sf =
let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
let sort = fst sf in
let bs1 = bsetAddTBox sort bs in
+ let deferrals = bsetMakeRealEmpty() in
+ let markDeferral f =
+ if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
+ bsetAdd deferrals f;)
+ in
+ bsetIter markDeferral bs;
graphInit ();
queueInit ();
- let root = insertCore sort bs1 in
+ let root = insertCore sort bs1 deferrals in
graphAddRoot root
let isRootSat () =