From e8afbb675067c93f2fd0eaa0850f1bc464c1741d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Fri, 11 Jul 2014 02:59:39 +0200
Subject: [PATCH] Make insertRule more disjunctive-aware
---
src/lib/CoAlgReasoner.ml | 13 ++++++++-----
1 file changed, 8 insertions(+), 5 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 81eb2ff..202a29f 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -538,14 +538,17 @@ let insertRule state dep (chldrn: (sort * bset) list junction) : bool option =
in
junctionEvalBoolOption (junc (List.map child2satState children))
in
- let isUnsat = (satStateChildren = Some false) in
(* find out satisfiability *)
let idx = stateAddRule state dep (List.rev children) in
List.iter (fun c -> coreAddParent c state idx) children;
- if isUnsat then begin
- propagateUnsat [UState (state, Some idx)];
- Some false
- end else None
+ match satStateChildren with
+ | Some false -> (* definitely unsat *)
+ propagateUnsat [UState (state, Some idx)];
+ Some false
+ | Some true ->
+ (* TODO: propagateSat ? *)
+ Some true
+ | None -> None
(* tells whether it is satisfiable:
Some true -> surely satisfiable
--
GitLab