From f4498ed12e9d9b64d00f68fa662674d79ff6aaa0 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 5 Apr 2016 02:55:23 +0200
Subject: [PATCH] Add documentation on dependencies
---
src/lib/CoAlgMisc.ml | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index c465ec0..6981601 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -246,8 +246,16 @@ and nodeStatus =
| Sat
| Unsat
+(* In K, given the singleton list [bs] returns the list of all Ax'es
+ responsible for the individual members of bs being part of the core
+ as well as the Ex.
+
+ So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
+ dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
+*)
and dependencies = bset list -> bset
+(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
and rule = (dependencies * (sort * bset * bset) lazylist)
and 'a lazyliststep =
--
GitLab