From 86948faead24639a17981d64b497c6bd475cc051 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 13 Apr 2016 21:33:21 +0200
Subject: [PATCH] Switch to only unsat propagation for testing
---
src/lib/CoAlgReasoner.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index efb958d..b21350b 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -994,7 +994,7 @@ let expandNodesLoop (recursiveAction: unit -> unit) =
expandState state;
if doNominalPropagation () then begin
propagateNominals ();
- if doSatPropagation () then propagateSatMu ()
+ if doSatPropagation () then propagateUnsatMu ()
end else ()
end else ();
recursiveAction ()
@@ -1003,7 +1003,7 @@ let expandNodesLoop (recursiveAction: unit -> unit) =
expandCore core;
if doNominalPropagation () then begin
propagateNominals ();
- if doSatPropagation () then propagateSatMu ()
+ if doSatPropagation () then propagateUnsatMu ()
end else ()
end else ();
recursiveAction ()
@@ -1050,7 +1050,7 @@ let isRootSat () =
| Expandable -> None
| Unsat -> Some false
| Sat -> Some true
- | Open -> if (queueIsEmpty()) then Some false else None
+ | Open -> if (queueIsEmpty()) then Some true else None
let reasonerFinished () =
match coreGetStatus (graphGetRoot ()) with
--
GitLab