;;;-*- Mode: Lisp; Package: XLE -*-

(in-package :XLE)

#||
Here is code for enumerating the justification for nogoods.  This only works 
on the unpacked f-structures.

      for (just = get_graph_prop(graph, "nogoods"); 
	   just; just = just->next) {
      }

/* (c) 2002-2005 by the Palo Alto Research Center.  All rights reserved */
/* (c) 1996-2001 by the Xerox Corporation.  All rights reserved */

/* Justifications are used to explicitly represent the deductions.  They */
/* are used for integrity checks and for grammar debugging. */

#ifndef JUSTIFICATIONS_H
#define JUSTIFICATIONS_H
||#

;; /* a Justified Fact is true IFF its Justifications are true */

;; struct JustifiedFact {
(ff:def-foreign-type JustifiedFact
    (:struct
     ;;  TypedValue fact; /* the fact justified */
     (fact :unsigned-long)
     ;;  Justification *justifications; /* its justifications */
     (justifications :unsigned-long)
     ;;  JustifiedFact *next;  /* this is a threaded list */
     (next :unsigned-long)
     ))
;;};

/* a Justification is a deduction that justifies some fact */

;; struct Justification {
(ff:def-foreign-type Justification
    (:struct
     ;;  unsigned int imported : 1; /* justification was imported from a daughter */
     (imported (:bit 1))
     ;;  unsigned int immutable : 1; /* next field cannot be modified; copy */
     ;;			      /* whole justification instead */
     (immutable (:bit 1))
     ;;  AVPair *avpair;       /* the AVPair where the deduction took place */
     (avpair :unsigned-long)

     ;;  Clause *context;      /* the context of the deduction */
     (context :unsigned-long)

     ;;  Rule *rule;           /* information about the rule used */
     (rule :unsigned-long)

     ;;  TypedValue ant1;      /* the antecedents of the rule used */
     (ant1-type :int)
     (ant1-val :unsigned-long)

     ;;  TypedValue ant2;
     (ant2-type :int)
     (ant2-val :unsigned-long)

     ;;  Justification *next;  /* this is a threaded list */
     (next :unsigned-long)
     ))	;;};

;; Justification *create_justification(Graph *graph, Clause *clause, AVPair *avp, 
;;				    ValueType type1, void *fact1,
;;				    ValueType type2, void *fact2);


:eof