From 6bbde09cdaeed9163dff9d4c31bbfaaaf1e3091a Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Thu, 7 Apr 2016 02:35:46 +0200
Subject: [PATCH] =?UTF-8?q?preliminary=20propafateSat=20for=20=CE=BC-Calcu?=
=?UTF-8?q?lus?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
This still produces wrong results: It assumes every node with empty
focus to be sat.
---
src/lib/CoAlgReasoner.ml | 96 ++++++++++++++++++++++++++++++++++++++++
1 file changed, 96 insertions(+)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 75de2ac..a040b9f 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -113,6 +113,102 @@ let propagateSat () =
setIterCnstr (fun cset -> graphReplaceCnstr cset SatC) setCnstr
+let propagateSatMu () =
+ let setFinishingStates = setEmptyState () in
+ let setFinishingCores = setEmptyCore () in
+ let setStates = setEmptyState () in
+ let setCores = setEmptyCore () in
+ let emptySet = bsetMakeRealEmpty () in
+
+ let stateCollector state =
+ match stateGetStatus state with
+ | Unsat
+ | Sat -> ()
+ | Expandable
+ | Open ->
+ setAddState setStates state;
+ if bsetCompare (stateGetDeferral state) emptySet == 0
+ then begin
+ print_endline (stateToString state);
+ setAddState setFinishingStates state
+ end
+ else ()
+ in
+ let coreCollector core =
+ match coreGetStatus core with
+ | Unsat
+ | Sat -> ()
+ | Expandable
+ | Open ->
+ setAddCore setCores core;
+ if bsetCompare (coreGetDeferral core) emptySet == 0
+ then begin
+ print_endline (coreToString core);
+ setAddCore setFinishingCores core
+ end
+ else ()
+ in
+ graphIterStates stateCollector;
+ graphIterCores coreCollector;
+
+ (*
+ In a fixpoint the set called setStates / setCores is narrowed down.
+
+ In each step only those states and cores are retained in setStates
+ / setCores which reach one of setFinishing{States,Cores} in
+ finitely many steps. This new set of States / Cores is collected
+ as allowed{States,Cores} during each fixpoint iteration.
+
+ Only those finishing nodes are retained that have allowed or
+ Successfull Children.
+ *)
+
+ let rec fixpointstep setStates setCores =
+ let allowedStates = setFinishingStates in
+ let allowedCores = setFinishingCores in
+
+ let rec visitParentStates (core : core) : unit =
+ if setMemCore allowedCores core then () else begin
+ let children = coreGetChildren core in
+ let acceptable = List.exists (fun (state) -> setMemState allowedStates state) children in
+ if acceptable then begin
+ print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed");
+ setAddCore allowedCores core;
+ List.iter (fun (state, _) -> visitParentCores state)
+ (coreGetParents core)
+ end
+ end
+
+ and visitParentCores (state : state) : unit =
+ if setMemState allowedStates state then () else begin
+ let rules = stateGetRules state in
+ let ruleiter (dependencies, corelist) =
+ List.exists (fun (core) -> setMemCore allowedCores core) corelist
+ in
+ let acceptable = List.for_all ruleiter rules in
+ if acceptable then begin
+ print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as allowed");
+ setAddState allowedStates state;
+ List.iter (fun core -> visitParentStates core)
+ (stateGetParents state)
+ end
+ end
+ in
+
+ setIterState visitParentCores setFinishingStates;
+ setIterCore visitParentStates setFinishingCores;
+
+ if (setLengthState setStates) = (setLengthState allowedStates) &&
+ (setLengthCore setCores) = (setLengthCore allowedCores)
+ then begin
+ setIterState (fun state -> stateSetStatus state Sat) setStates;
+ setIterCore (fun core -> coreSetStatus core Sat) setCores;
+ end else
+ fixpointstep allowedStates allowedCores
+ in
+ fixpointstep setStates setCores
+
+
(*****************************************************************************)
(* Propagation of Unsatisfiability *)
(*****************************************************************************)
--
GitLab