From 6aa0e444937dd8b9088ef16cf7c4a696ce9d283b Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 19 Apr 2016 18:57:17 +0200
Subject: [PATCH] Only deallocate solver for unsat nodes
We want to still have the solver for naive unsat propagation
---
src/lib/CoAlgReasoner.ml | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 08b5b31..c2fda8b 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -357,6 +357,7 @@ let rec propagateUnsat = function
in
coreSetBs core mbs;
coreSetStatus core Unsat;
+ coreDeallocateSolver core;
if core == graphGetRoot () then raise (CoAlg_finished false) else ();
let prop acc (state, idx) =
let turnsUnsat =
@@ -527,7 +528,7 @@ let propagateUnsatMu () =
(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;
+ setIterCore (fun core -> propagateUnsat [UCore (core, false)]) setUnsatCores;
end else
fixpointstep setUnsatStates setUnsatCores
in
@@ -902,9 +903,11 @@ let expandCore core =
queueInsertCore core
| None ->
let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
- if isUnsat then propagateUnsat [UCore (core, false)]
- else coreSetStatus core Open;
- coreDeallocateSolver core
+ if isUnsat
+ then
+ propagateUnsat [UCore (core, false)]
+ else
+ coreSetStatus core Open
let insertCore sort bs defer =
--
GitLab