From e1489b0d68130957559baf0321b34ee6bdf737cb Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 13 Apr 2016 21:54:43 +0200
Subject: [PATCH] Expandable states are always acceptable Finishing states for
Unsat propagation
---
src/lib/CoAlgReasoner.ml | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index b21350b..9534330 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -511,7 +511,7 @@ let propateUnsatMu () =
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
+ if not (List.exists ruleiter (stateGetRules state)) || stateGetStatus state == Expandable then begin
visitParentCores state
end
@@ -520,7 +520,8 @@ let propateUnsatMu () =
*)
and checkFinishingCore (core : core) =
if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state)
- (coreGetChildren core))
+ (coreGetChildren core)) ||
+ coreGetStatus core == Expandable
then begin
visitParentStates core
end
--
GitLab