From: ian <ian>
Date: Thu, 27 Mar 2008 23:58:14 +0000 (+0000)
Subject: wip hostside resolver continues; still startup.c not checked in here; before remove... 
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ijackson/git?a=commitdiff_plain;h=0bbb027611fe278014940fd8ea8e6907338a70b7;p=trains.git

wip hostside resolver continues; still startup.c not checked in here; before remove aggregation of proof elements
---

diff --git a/hostside/common.h b/hostside/common.h
index c27ba14..ef4d3e7 100644
--- a/hostside/common.h
+++ b/hostside/common.h
@@ -128,4 +128,8 @@ void nmra_addchecksum(Nmra *packet);
 void nmra_encodeforpic(const Nmra *packet, PicInsn *pi_out);
 
 
+#define ARRAY_SIZE(a) (sizeof((a))/sizeof(*(a)))
+#define ARRAY_END(a) ((a) + ARRAY_SIZE((a)))
+
+
 #endif /*COMMON_H*/
diff --git a/hostside/resolve.c b/hostside/resolve.c
index e471163..4c27aaa 100644
--- a/hostside/resolve.c
+++ b/hostside/resolve.c
@@ -178,24 +178,37 @@ void resolve_begin(void) {
   TrainNum t##n= (tra) - trains;		\
   TrainResolution *t##r= rx + t##n;
 
-#define APPENDING(array, variable, isreal)				\
-  typeof(*array) variable;						\
-  for ((variable)=(array);						\
-       ;								\
-       (variable)++) {							\
-    assert((variable) < (array)+sizeof((array))/sizeof(*(array)));	\
-    if (!(isreal)) break;						\
-  }
+#define BLANKREASONS(array, sentinelmember)	\
+    ((*(SegmentNum*)(array))= NOTA(Segment))
+
+#define ADDREASON(array, newvalue) do{			\
+    typeof(*(array)) addreason_i;			\
+    for (addreason_i=(array);				\
+         ;						\
+         addreason_i++) {				\
+      assert(addreason_i < ARRAY_END(array));		\
+      if (!SOMEP(*(SegmentNum*)(addreason_i))) {	\
+	*addreason_i++= newvalue;			\
+        *(SegmentNum*)addreason_i= NOTA(Segment);	\
+        assert(addreason_i < ARRAY_END(array));		\
+	break;						\
+      }							\
+      if (*addreason_i == newvalue)			\
+	break;						\
+    }							\
+  }while(0)
+
+#define FOR_TRAIN_R(t)  FOR_TRAIN(t, t##r=rx, t##r++)
 
 int resolve_complete(void) {
   int problems;
   SEG_IV;
 
   rx= mmalloc(sizeof(*rx) * n_trains);
-  FOR_TRA {
-    rx[tran].r= RR_N;
-    rx[tran].why_eh.d= NOTA(Segment);
-    rx[tran].whynot_e.d1= NOTA(Segment);
+  FOR_TRAIN_R(t) {
+    tr->r= RR_N;
+    BLANKREASONS(tr->why_eh);
+    BLANKREASONS(tr->whynot_e);
   }
 
   while 1 {
@@ -212,18 +225,30 @@ int resolve_complete(void) {
 	continue;
       /* 3. we have a violation of D \subset U, namely d */
 
+      ProofElement why_h;
+      why_h.d= d;
+      why_h.t= NOTA(Train);
+      
       if (d->owner) { /* 3a perhaps */
 	TRAIN(t, d->owner);  /* t st d \elem E(t) */
-	if (tr->r == RR_H || SOMEP(tr->whynot_e[0]))
+	why_h.t= tn;
+	if (tr->r == RR_H)
 	  goto not_3a;
 
+	if (tr->r == RR_E)
+	  /* we added it in this sweep and have found another d */
+	  goto already_3a;
+	assert(tr->r == RR_N);
+
 	/* check E(t) \disjoint U */
-	Clash clash;
-	FOR_SEGMENT(clash.d1, NOOP, NOOP) {
-	  if (clash.d1->owner == t && clash.d1->tr_updated) {
-	    FOR_TRAIN(clash.t2, NOOP, NOOP) {
-	      if (clash.t2r->r == HH_H && clash.d1->owner == clash.t2) {
-		ADDREASON(tr->whynot_e, clash, SOMEP(clash->clash.d1));
+	FOR_SEGMENT(d1, NOOP, NOOP) {
+	  if (d1->owner == t && d1->tr_updated) {
+	    FOR_TRAIN(t2, NOOP, NOOP) {
+	      if (t2r->r == HH_H && d1->owner == t2) {
+		Clash clash;
+		clash.d1= d1;
+		clash.t2= t2;
+		ADDREASON(tr->whynot_e, clash);
 	      }
 	    }
 	  }
@@ -232,8 +257,48 @@ int resolve_complete(void) {
 	  goto not_3a;
 
 	/* Yay! 3a. */
+	tr->r= RR_E;
+      already_3a:
+	ProofElement why_e;
+	why_e.d= d;
+	why_e.t= NOTA(Train);
+	ADDREASON(tr->why_eh, why_e);
+	continue;
+      }
+
+    not_3a:
+      if (d->home) { /* 3b then */
+	TRAIN(t1, d->home); /* t' st d \elem H(t') */
 	
+	if (tr->r == RR_H)
+	  /* added in this sweep, have found another d */
+	  goto already_3b;
+
+	FOR_SEGMENT(dplus, NOOP, NOOP) {
+	  if (!dplus->owner) continue;
+	  TRAIN(tplus, dplus->owner);
+	  if (tplusr->r != HH_E) continue;
+	  dplus->tr_updated= 0;
+	}
+	FOR_TRAIN_R(tplus) {
+	  BLANKREASONS(tplusr->whynot_e);
+	  if (tplusr->r == HH_E) {
+	    tplusr->r= HH_N;
+	    BLANKREASONS(tplusr->why_eh);
+	  }
+	}
+
+	tr->r= RR_H;
+	BLANKREASONS(tr->why_eh);
 
+      already_3b:
+	ADDREASON(tr->why_eh, why_h);
+	fixme /* need to make us scan for case 3a first, so that
+		 when we report a problem we report as reasons
+		 for some H only those ds which would not have
+		 been satisfied by E.  perhaps scan for Es
+	         and then only for Hs, each time ? */
+	
 	  /* tr->whynot_e is already filled in */
 	  goto not_3a;
 	assert(tr->r == RR_N);