From d9f4e4afdd31b1e8930d127812b714fd518f84d6 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 26 Jan 2016 16:32:28 +0100
Subject: [PATCH] Add deferrals to reasoner array

---
 src/lib/CoAlgMisc.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 106569f..e3536b1 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -666,6 +666,7 @@ let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
 let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1)))  (* first subformula *)
 let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1)))  (* second subformula *)
 let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1)))  (* a role *)
+let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1)))  (* deferral at point *)
 let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
 let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1)))  (* another integer *)
 let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
@@ -922,8 +923,9 @@ let detClosureAt hcF atset name f () =
 
 (** Initialises the arrays for a formula and its integer representation.
  *)
-let initTables nomTbl hcF htF htR s f n =
+let initTables nomTbl hcF htF htR vset s f n =
   !arrayFormula.(s).(n) <- f.HC.fml;
+  !arrayDeferral.(s).(n) <- Hashtbl.hash (C.HcFHt.find vset.(s) f);
   let fneg = f.HC.neg in
   if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg;
   let (_, sortlst) = !sortTable.(s) in
@@ -1149,12 +1151,13 @@ let ppFormulae nomTbl tbox (s, f) =
   arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
   arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
   arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
+  arrayDeferral := Array.init card (fun _-> Array.make !size(-1));
   arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
   arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
   arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1));
   arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
   let htR = Hashtbl.create 128 in
-  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR s) ht) htF;
+  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
   arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
   Hashtbl.iter (initTablesAt hcF htF) nomset;
 
-- 
GitLab