From 5956a56d39d4de7cfe991e8592ce93a87d07022a Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 13 Apr 2016 03:03:14 +0200
Subject: [PATCH] First implementation of propagateUnsat
---
src/lib/CoAlgMisc.ml | 2 +
src/lib/CoAlgMisc.mli | 2 +
src/lib/CoAlgReasoner.ml | 127 +++++++++++++++++++++++++++++++++++++++
3 files changed, 131 insertions(+)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index ed0d2de..3358f6c 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -578,6 +578,8 @@ 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 setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
+let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
let setEmptyCnstr () = GHtS.create 128
let setAddState set state =
GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 9c25e6c..80a0eb8 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -267,6 +267,8 @@ val coreToDot : core -> string
val setEmptyState : unit -> setState
val setEmptyCore : unit -> setCore
+val setCopyState : setState -> setState
+val setCopyCore : setCore -> setCore
val setEmptyCnstr : unit -> setCnstr
val setAddState : setState -> state -> unit
val setAddCore : setCore -> core -> unit
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 91e04c7..ab63f46 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -411,6 +411,133 @@ let rec propagateUnsat = function
in
propagateUnsat tl1
+let propateUnsatMu () =
+ let setFinishingStates = setEmptyState () in
+ let setFinishingCores = setEmptyCore () in
+ let setStates = setEmptyState () in
+ let setCores = setEmptyCore () in
+ let emptySet = bsetMakeRealEmpty () in
+
+ (* Collect two sets of nodes. All nodes that may be unsatisfiable
+ * after this iteration are collected into setStates/setCores.
+ *
+ * Nodes reaching Points with empty focus as well as Expandable nodes
+ * (if not Unsat) can not be declared Unsat so we collect these into
+ * setFinishingStates/setFinishingCores.
+ *)
+ let stateCollector state =
+ match stateGetStatus state with
+ | Unsat -> ()
+ | Sat
+ | Expandable ->
+ setAddState setStates state;
+ setAddState setFinishingStates state
+ | Open ->
+ setAddState setStates state;
+ if bsetCompare (stateGetDeferral state) emptySet == 0
+ then begin
+ setAddState setFinishingStates state
+ end
+ else ()
+
+ and coreCollector core =
+ match coreGetStatus core with
+ | Unsat -> ()
+ | Expandable
+ | Sat ->
+ setAddCore setCores core;
+ setAddCore setFinishingCores core
+ | Open ->
+ setAddCore setCores core;
+ if bsetCompare (coreGetDeferral core) emptySet == 0
+ then begin
+ setAddCore setFinishingCores core
+ end
+ else ()
+ in
+ graphIterStates stateCollector;
+ graphIterCores coreCollector;
+
+ (* In a fixpoint the set called setFinishingStates/setFinishingCores
+ * is narrowed down
+ *
+ * In each iteration we start with all Nodes and remove all that can
+ * reach a finishing Node. We then remove all finishing Nodes from the
+ * respective set which are becoming Unsat and start with the next
+ * iteration until the fixpoint is reached
+ *
+ *
+ *)
+ let rec fixpointstep setPrevUnsatStates setPrevUnsatCores =
+ let setUnsatStates = setCopyState setStates in
+ let setUnsatCores = setCopyCore setCores in
+
+ let rec visitParentStates (core : core) : unit =
+ if setMemCore setUnsatCores core
+ then begin
+ setRemoveCore setUnsatCores core;
+ let verifyParent (state,_) =
+ let rules = stateGetRules state in
+ let ruleiter (dependencies, corelist) =
+ List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) || coreGetStatus core == Sat)
+ corelist
+ in
+ if List.for_all ruleiter rules
+ then visitParentCores state
+ in
+ List.iter verifyParent (coreGetParents core)
+ end
+
+ and visitParentCores (state : state) : unit =
+ if setMemState setUnsatStates state
+ then begin
+ setRemoveState setUnsatStates state;
+ let verifyParent core =
+ let acceptable =
+ List.exists (fun (state : state) -> not (setMemState setUnsatStates state) || stateGetStatus state == Sat)
+ (coreGetChildren core)
+ in
+ if acceptable
+ then visitParentStates core
+ in
+ List.iter verifyParent (stateGetParents state)
+ end
+ in
+
+ (* All rule applications need to still be potentially Sat for a
+ * finishing State to be a valid startingpoint for this fixpoint.
+ *)
+ let checkFinishingState (state : state) =
+ let ruleiter (dependencies, corelist) : bool =
+ List.for_all (fun (core : core) -> coreGetStatus core == Unsat || setMemCore setPrevUnsatCores core) corelist
+ in
+ if not (List.exists ruleiter (stateGetRules state)) then begin
+ visitParentCores state
+ end
+
+ (* There needs to be a State still potentially Sat for this core
+ * to be considered for the fixpoint
+ *)
+ and checkFinishingCore (core : core) =
+ if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state)
+ (coreGetChildren core))
+ then begin
+ visitParentStates core
+ end
+ in
+ setIterState checkFinishingState setFinishingStates;
+ setIterCore checkFinishingCore setFinishingCores;
+
+ if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
+ (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
+ then begin
+ setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
+ setIterCore (fun core -> coreSetStatus core Unsat; if core == graphGetRoot () then raise (CoAlg_finished false) else ()) setUnsatCores;
+ end else
+ fixpointstep setUnsatStates setUnsatCores
+ in
+ fixpointstep (setEmptyState ()) (setEmptyCore ())
+
(*****************************************************************************)
(* Propagation of Nominal Constraints *)
--
GitLab