From b395c870c6174b1717ab00b7798e95c0c4e14b24 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 9 Feb 2016 11:45:36 +0100
Subject: [PATCH] track deferrals across propositional reasoning
---
src/lib/CoAlgReasoner.ml | 52 +++++++++++++++++++++++++---------------
1 file changed, 33 insertions(+), 19 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 45ef0dc..4a13a6a 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -509,6 +509,7 @@ let getNextState core =
minisat calls.
*)
let bs = coreGetBs core in
+ let deferralS = coreGetDeferral core in
let fht = coreGetFht core in
let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
let solver = coreGetSolver core in
@@ -523,6 +524,7 @@ let getNextState core =
satisfiable.
*)
let newbs = bsetMake () in
+ let newdefer = bsetMake () in
(* if newbs = { l_1, .... l_n }, i.e.
newbs = l_1 /\ ... /\ l_n
@@ -534,7 +536,7 @@ let getNextState core =
By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
*)
- let rec mkExclClause f acc =
+ let rec mkExclClause deferral f acc =
(* f is a formula that is true in the current satisfying assignment *)
match lfGetType sort f with
| OrF ->
@@ -543,50 +545,62 @@ let getNextState core =
let lf1 = fhtMustFind fht f1 in
(* if the first disjunct f1 is true, then we need to add subformulas
of f1 to newbs&clause *)
- if M.literal_status solver lf1 = M.LTRUE then mkExclClause f1 acc
+ if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
else
(* otherwise f2 must be true *)
let f2 = lfGetDest2 sort f in
let lf2 = fhtMustFind fht f2 in
assert (M.literal_status solver lf2 = M.LTRUE);
- mkExclClause f2 acc
+ mkExclClause deferral f2 acc
| AndF ->
(* if the true f is a conjuction, then both conjunctions must be true *)
let f1 = lfGetDest1 sort f in
let lf1 = fhtMustFind fht f1 in
assert (M.literal_status solver lf1 = M.LTRUE);
- let acc1 = mkExclClause f1 acc in
+ let acc1 = mkExclClause deferral f1 acc in
let f2 = lfGetDest2 sort f in
let lf2 = fhtMustFind fht f2 in
assert (M.literal_status solver lf2 = M.LTRUE);
- mkExclClause f2 acc1
+ mkExclClause deferral f2 acc1
| MuF
| NuF ->
let f1 = lfGetDest1 sort f in
- mkExclClause f1 acc
+ mkExclClause deferral f1 acc
| _ ->
- (* if f is a trivial formula or modality, then add it ... *)
- (* ... to newbs *)
- bsetAdd newbs f;
- (* ... and to the new clause *)
- (M.neg_lit (fhtMustFind fht f))::acc
+ (* if f is a trivial formula or modality, then add it ... *)
+ (* ... to newbs *)
+ bsetAdd newbs f;
+ let defercandidate = lfGetDeferral sort f in
+ (if deferral = defercandidate then
+ bsetAdd newdefer f);
+ (* ... and to the new clause *)
+ (M.neg_lit (fhtMustFind fht f))::acc
in
- let clause = bsetFold mkExclClause bs [] in
+ let init_clause f acc =
+ let deferral =
+ if bsetMem deferralS f then
+ lfGetDeferral sort f
+ else
+ (Hashtbl.hash "ε")
+ in
+ mkExclClause deferral f acc
+ in
+ let clause = bsetFold init_clause bs [] in
let okay = M.add_clause solver clause in
assert (okay);
- Some (sort, newbs)
+ Some (sort, newbs, newdefer)
-let newState sort bs =
+let newState sort bs defer =
let (func, sl) = !sortTable.(sort) in
let producer = CoAlgLogics.getExpandingFunctionProducer func in
let exp = producer sort bs sl in
- stateMake sort bs bs exp
+ stateMake sort bs defer exp
-let insertState parent sort bs =
+let insertState parent sort bs defer =
let child =
match graphFindState sort bs with
| None ->
- let s = newState sort bs in
+ let s = newState sort bs defer in
graphInsertState sort bs s;
queueInsertState s;
s
@@ -597,8 +611,8 @@ let insertState parent sort bs =
let expandCore core =
match getNextState core with
- | Some (sort, bs) ->
- insertState core sort bs;
+ | Some (sort, bs, defer) ->
+ insertState core sort bs defer;
queueInsertCore core
| None ->
let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
--
GitLab