From e0f199997cfc885926f7fa471563b325e242f8fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Tue, 24 Nov 2015 12:52:34 +0100
Subject: [PATCH] Add a lot of comments about cores
---
src/lib/CoAlgMisc.ml | 27 ++++++++++++---
src/lib/CoAlgReasoner.ml | 72 ++++++++++++++++++++++++++++++++++++++++
2 files changed, 95 insertions(+), 4 deletions(-)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index c103bb7..00174a7 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -177,14 +177,33 @@ type lht = localFormula LHt.t
type fht = Minisat.lit FHt.t
type nht = bset NHt.t
-type state = { sortS : sort; mutable bsS : bset; mutable statusS : nodeStatus;
+type state = { sortS : sort;
+ mutable bsS : bset; (* a set of formulas who are either literals or
+ modalities (TODO: also @-formulas?).
+ the state is satisfiable if /\bsS is satisfiable.
+ *)
+ mutable statusS : nodeStatus;
mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
mutable constraintsS : csetSet; expandFkt : stateExpander;
idx: int }
-and core = { sortC : sort; mutable bsC : bset; mutable statusC : nodeStatus;
- mutable parentsC : (state * int) list; mutable childrenC : state list;
- mutable constraintsC : csetSet; solver : Minisat.solver; fht : fht;
+and core = { (* for details, see documentation of newCore *)
+ sortC : sort;
+ mutable bsC : bset; (* a set of arbitrary formulas.
+ the present core is satisfiable if /\ bsC is satisfiable *)
+ mutable statusC : nodeStatus;
+ mutable parentsC : (state * int) list;
+ mutable childrenC : state list;
+ mutable constraintsC : csetSet;
+ solver : Minisat.solver; (* a solver to find satisfying assignemnts for bsC.
+ the solver returns "satisfiable" iff
+ there is a satisfying assignment of
+ bsC which is not represented by some state from the
+ childrenC yet.
+ *)
+ fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals
+ of the Minisat solver
+ *)
mutable constraintParents : cset list;
idx : int }
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index a17d10e..034d6f2 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -414,58 +414,127 @@ let getLit sort fht solver f =
lit
let newCore sort bs =
+ (* when creating a now core from a set of formulas bs
+ bs = { x_1, ...., x_n }
+ = "x_1 /\ .... /\ x_n"
+ Then we do this by:
+
+ 1. creating a new literal in the sat solver for each
+ "boolean subformula" from the x_i. "boolean subformula" means that
+ this subformula is not hidden under modalities but only under
+ boolean connectives (/\, \/).
+ 2. encoding the relation between a formula and its intermediate boolean
+ subformulas by a clause:
+ *)
let fht = fhtInit () in
let solver = M.new_solver () in
let rec addClauses f =
+ (* step 1: create a literal in the satsolver representing the formula f *)
let lf = getLit sort fht solver f in
+ (* step 2: encode relation to possible subformulas *)
match lfGetType sort f with
| OrF ->
+ (*
+ case 2.(a) f = f1 \/ f2
+ fill fht such that it says:
+
+ f |---> lf
+ f1 |---> lf1
+ f2 |---> lf2
+ *)
let f1 = lfGetDest1 sort f in
let f2 = lfGetDest2 sort f in
addClauses f1;
addClauses f2;
let lf1 = fhtMustFind fht f1 in
let lf2 = fhtMustFind fht f2 in
+ (*
+ encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
+ *)
let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
assert (okay)
| AndF ->
+ (*
+ case 2.(b) f = f1 /\ f2
+ fill fht such that it says:
+
+ f |---> lf
+ f1 |---> lf1
+ f2 |---> lf2
+ *)
let f1 = lfGetDest1 sort f in
let f2 = lfGetDest2 sort f in
addClauses f1;
addClauses f2;
let lf1 = fhtMustFind fht f1 in
let lf2 = fhtMustFind fht f2 in
+ (*
+ encode the structure of f by adding the clauses
+ (lf -> lf1) /\ (lf -> lf2)
+ *)
let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
assert (okay1);
let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
assert (okay2)
| _ -> ()
+ (* case 2.(c)
+ We don't need to do anything except adding f to the fht
+ *)
in
bsetIter addClauses bs;
coreMake sort bs solver fht
let getNextState core =
+ (* Create a new state, which is obtained by a satisfying assignment of the
+ literals of the minisat solver.
+ In addition to that, feed the negation of the satisfying assignment back
+ to the minisat solver in order to obtain different solutions on successive
+ minisat calls.
+ *)
let bs = coreGetBs core in
let fht = coreGetFht core in
let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
let solver = coreGetSolver core in
let isSat = M.invoke_solver solver litset in
+ (* Clearly, if the current core is unsatisfiable, no further child state can
+ be created *)
if not isSat then None
else
let sort = coreGetSort core in
+ (* create a new set of formulas newbs with the property:
+ if the conjunction of newbs is satisfiable, then the present core is
+ satisfiable.
+ *)
let newbs = bsetMake () in
+ (* if newbs = { l_1, .... l_n }, i.e.
+
+ newbs = l_1 /\ ... /\ l_n
+
+ then we can get essentially different satisfying assignments of bs by
+ adding another clause
+
+ clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
+
+ By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
+ *)
let rec mkExclClause f acc =
+ (* f is a formula that is true in the current satisfying assignment *)
match lfGetType sort f with
| OrF ->
+ (* if f is true and a disjunction, then one of its disjuncts is true *)
let f1 = lfGetDest1 sort f in
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
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
| 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);
@@ -475,7 +544,10 @@ let getNextState core =
assert (M.literal_status solver lf2 = M.LTRUE);
mkExclClause f2 acc1
| _ ->
+ (* 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
in
let clause = bsetFold mkExclClause bs [] in
--
GitLab