From a2ec2dfcd06a3055e5d1798d726f8b86cb2a3f29 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Fri, 14 Apr 2017 11:22:39 +0200
Subject: [PATCH] Set states without children to Sat early
We can set states without children to Sat right after we expand them.
---
src/lib/CoAlgReasoner.ml | 12 ++++++++++--
1 file changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index cae46fb..4049c1c 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -1114,14 +1114,22 @@ let rec insertAllRules state rules =
List.mem true (List.map (fun (dep, children) -> insertRule state dep children) rules)
let expandState state =
+ let setSatOrOpen () =
+ if CU.TList.empty (stateGetRules state) then
+ stateSetStatus state Sat
+ else
+ stateSetStatus state Open
+ in
+
match stateNextRule state with
| MultipleElements rules ->
let unsat = insertAllRules state rules in
- if not unsat then stateSetStatus state Open
+ if not unsat then setSatOrOpen ()
| SingleElement (dep, chldrn) ->
let unsat = insertRule state dep chldrn in
if not unsat then queueInsertState state else ()
- | NoMoreElements -> stateSetStatus state Open
+ | NoMoreElements ->
+ setSatOrOpen ()
let expandCnstr cset =
--
GitLab