From 371cb823ca3c6a87d0fda717f25741f04d973e06 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Tue, 21 Mar 2017 00:24:58 +0100
Subject: [PATCH] Perform sat propagation in debugger step
Otherwise, the debugger would report the reasoner result to be "Sat"
when it should really be "Unsat".
---
src/debugger/debugger.ml | 8 +++++---
src/lib/CoAlgReasoner.ml | 1 +
src/lib/CoAlgReasoner.mli | 6 ++++++
3 files changed, 12 insertions(+), 3 deletions(-)
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index c51625a..b2366bd 100644
--- a/src/debugger/debugger.ml
+++ b/src/debugger/debugger.ml
@@ -52,9 +52,11 @@ let doStep args =
let action() =
if Reasoner.reasonerFinished ()
then print_endline "Reasoner already finished!"
- else try
- Reasoner.runReasonerStep ()
- with CoAlgMisc.CoAlg_finished _ -> printResult()
+ else
+ try
+ Reasoner.runReasonerStep ();
+ if (Reasoner.reasonerFinished ()) then printResult();
+ with CoAlgMisc.CoAlg_finished _ -> printResult()
in
let steps = match args with
| (str::_) -> (int_of_string str)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 93d7761..fca69aa 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -1035,6 +1035,7 @@ let expandNodesLoop (recursiveAction: unit -> unit) =
let runReasonerStep () =
let void () = () in
expandNodesLoop void; (* expand at most one node *)
+ propagateUnsatMu ();
(* if this emptied the queue *)
if queueIsEmpty () then begin
(* then check whether the nominals would add further queue elements *)
diff --git a/src/lib/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli
index b63083d..a30ed93 100644
--- a/src/lib/CoAlgReasoner.mli
+++ b/src/lib/CoAlgReasoner.mli
@@ -20,7 +20,13 @@ val isSat : ?verbose:bool -> sortTable -> (string -> CoAlgFormula.sort option) -
val initReasoner : sortTable -> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> unit
+(** Run a single step of the reasoner. That is: Expand one node and perform sat
+ * propagation.
+ *
+ * This is used in the debugger.
+ *)
val runReasonerStep : unit -> unit
+
val reasonerFinished : unit -> bool
val isRootSat : unit -> bool option
--
GitLab