From b36e57bcf10aed57d5ec8dfcc3069895e4c74ceb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Tue, 15 Jul 2014 21:33:59 +0200
Subject: [PATCH] Remove Disjunctive ruleEnumerations
Propagation of satisfiability and unsatisfiability does not cover
disjunctions and I don't get how propagation works, so I won't touch it
yet. So this reverts the only partially implemented Disjunctive
ruleEnumerations,
---
src/lib/CoAlgLogics.ml | 23 +++++++++++------------
src/lib/CoAlgMisc.ml | 2 +-
src/lib/CoAlgMisc.mli | 4 ++--
src/lib/CoAlgReasoner.ml | 29 ++++++++++-------------------
4 files changed, 24 insertions(+), 34 deletions(-)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 1b89a2b..d1e3785 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -63,11 +63,11 @@ let mkRule_MultiModalK sort bs sl : stateExpander =
let rules = mkRuleList_MultiModalK sort bs sl in
let res = ref (Some rules) in
fun () ->
- Conjunctive (match !res with
+ match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules)
+ AllInOne rules
(* TODO: test it with:
make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True'
@@ -131,12 +131,11 @@ let mkRule_MultiModalKD sort bs sl : stateExpander =
(* TODO: replace cannonical wrapper by helper function *)
let res = ref (Some rules) in
fun () ->
- Conjunctive (match !res with
+ match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
AllInOne rules
- )
(* CoalitionLogic: helper functions *)
@@ -264,11 +263,11 @@ let mkRule_CL sort bs sl : stateExpander =
(* standard return procedure *)
let res = ref (Some rules) in
fun () ->
- Conjunctive (match !res with
+ match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules)
+ AllInOne rules
let mkRule_GML sort bs sl : stateExpander =
assert (List.length sl = 1);
@@ -317,11 +316,11 @@ let mkRule_GML sort bs sl : stateExpander =
(* standard return procedure *)
let res = ref (Some rules) in
fun () ->
- Conjunctive (match !res with
+ match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules)
+ AllInOne rules
let mkRule_Choice sort bs sl : stateExpander =
assert (List.length sl = 2);
@@ -352,11 +351,11 @@ let mkRule_Choice sort bs sl : stateExpander =
let s2 = List.nth sl 1 in
let res = ref (Some [(dep, [(s1, bs1); (s2, bs2)])]) in
fun () ->
- Conjunctive (match !res with
+ match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules)
+ AllInOne rules
let mkRule_Fusion sort bs sl : stateExpander =
@@ -387,11 +386,11 @@ let mkRule_Fusion sort bs sl : stateExpander =
let s2 = List.nth sl 1 in
let res = ref (Some [(dep 0, [(s1, bs1)]); (dep 1, [(s2, bs2)])]) in
fun () ->
- Conjunctive (match !res with
+ match !res with
| None -> NoMoreRules
| Some rules ->
res := None;
- AllInOne rules)
+ AllInOne rules
(* Maps a logic represented by the type "functors" to the corresponding
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 995698d..4cb56c6 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -124,7 +124,7 @@ and setCnstr = unit GHt.t
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
| Conjunctive of 'a (*specifies that all of the 'a need to be satifsfied *)
-and stateExpander = unit -> ruleEnumeration junction
+and stateExpander = unit -> ruleEnumeration
and sort = C.sort
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 15fdb34..c21a8a1 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -62,7 +62,7 @@ type setCnstr
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
| Conjunctive of 'a (*specifies that all of the 'a need to be satifsfied *)
-and stateExpander = unit -> ruleEnumeration junction
+and stateExpander = unit -> ruleEnumeration
and sort = CoAlgFormula.sort
@@ -192,7 +192,7 @@ val stateGetRules : state -> (dependencies * core list) list
val stateAddRule : state -> dependencies -> core list -> int
val stateGetConstraints : state -> csetSet
val stateSetConstraints : state -> csetSet -> unit
-val stateNextRule : state -> ruleEnumeration junction
+val stateNextRule : state -> ruleEnumeration
(*****************************************************************************)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index fb11c4f..ffc28c2 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -582,8 +582,7 @@ let insertCore sort bs =
Some false -> surely unsat
None -> Not known yet
*)
-let insertRule state dep (chldrn: (sort * bset) list junction) : bool option =
- let (chldrn, junc) = junctionExtract chldrn in
+let insertRule state dep (chldrn: (sort * bset) list) : bool option =
let insert (sort, bs) = (* checks if the given child node has some sat-state *)
let bs1 = bsetAddTBox sort bs in
insertCore sort bs1
@@ -598,7 +597,7 @@ let insertRule state dep (chldrn: (sort * bset) list junction) : bool option =
| Expandable -> None (* unknown state *)
| Open -> None (* unknown state *)
in
- junctionEvalBoolOption (junc (List.map child2satState children))
+ junctionEvalBoolOption (Conjunctive (List.map child2satState children))
in
(* find out satisfiability *)
let idx = stateAddRule state dep (List.rev children) in
@@ -617,30 +616,22 @@ let insertRule state dep (chldrn: (sort * bset) list junction) : bool option =
Some false -> surely unsat
None -> Not known yet
*)
-let rec insertAllRules state : rule list junction -> bool option = function
- | Conjunctive [] -> Some true
- | Disjunctive [] -> Some false
- | Conjunctive ((dep, chldrn)::tl) ->
- let satState = insertRule state dep (Conjunctive chldrn) in
+let rec insertAllRules state : rule list -> bool option = function
+ | [] -> Some true
+ | ((dep, chldrn)::tl) ->
+ let satState = insertRule state dep chldrn in
if satState <> Some false (* if notUnsat*)
- then insertAllRules state (Conjunctive tl)
+ then insertAllRules state tl
else Some false
- | Disjunctive ((dep, chldrn)::tl) ->
- let satState = insertRule state dep (Disjunctive chldrn) in
- if satState <> Some true (* if not Sat *)
- then insertAllRules state (Disjunctive tl)
- else Some true
let expandState state =
- let (rules, _) = junctionExtract (stateNextRule state) in
+ let rules = stateNextRule state in
match rules with
| AllInOne rules ->
- let (_, junction) = junctionExtract (stateNextRule state) in
- let satState = insertAllRules state (junction rules) in
+ let satState = insertAllRules state rules in
if satState <> Some false (* i.e. if not Unsat *) then stateSetStatus state Open
| NextRule (dep, chldrn) ->
- let (_, junction) = junctionExtract (stateNextRule state) in
- let satState = insertRule state dep (junction chldrn) in
+ let satState = insertRule state dep chldrn in
if satState <> Some false (* if notUnsat *) then queueInsertState state else ()
| NoMoreRules -> stateSetStatus state Open
--
GitLab