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

(in-package :XLE)

#||
/* (c) 1996 by the Xerox Corporation.  All rights reserved */

/* The check_* procedures verify that everything is working right.  They */
/* haven't been used in a while, and so may not be still working. */

/* These procedures perform integrity checks on different structures. */
void check_subtree_justifications(Graph *graph, Graph *edgeGraph, 
			       Graph *partial, Graph *complete);
void check_edge_justifications(Graph *graph);
void check_graph(Graph *graph);
void check_avpair(Graph *graph, AVPair *attr);
void check_cvpairs(Graph *graph, AVPair *avp, CVPair *values);
void find_spurious_facts(Graph *graph, AVPair *avp);

/* these procedures supplement the existing deduction functions */
void check_equal(Graph *graph, AVPair *avp);
void check_equal_v(Graph *graph, AVPair *avp);
void check_sub_c(Graph *graph, AVPair *avp);
void check_negation(Graph *graph, AVPair *avp);
void check_lazy(Graph *graph, AVPair *avp);

/* these procedures evaluate the justifications produced elsewhere */
void check_justifications(Graph *graph, Graph *edgeGraph);
void check_lazy_justifications(Graph *graph, JustifiedFact *fact,
			       JustifiedFact *facts);
int check_nogoods(Graph *graph, JustifiedFact *false, Graph *edgeGraph);
void check_solutions(Graph *graph, int nogood);
int evaluate_fact(TypedValue fact);
int evaluate_justification(Justification *justification);

/* these procedures report justification errors */
void spurious_fact(Graph *graph, JustifiedFact *fact);
void spurious_nogood(Graph *graph, Clause *clause);
void deduction_failed(Graph *graph, JustifiedFact *fact, 
		      Justification *justification);
AVPair *find_value(Graph *graph, CVPair *value, AVPair *avp);

/* these procedures parallel the assert-* relations */
Justification *conjoin_facts2(Graph* graph, 
			      CVPair *fact1, CVPair *fact2);
Justification *conjoin_facts3(Graph* graph, 
			      CVPair *fact1, AVPair *fact2);
int lazy_avpair(AVPair *avp);
void assert_relation2(Graph *graph, RelID relID, 
		      TypedValue tv1, TypedValue tv2, 
		      Justification *justification, CVProps props, Rule *rule);
void assert_indexed_relation(Graph *graph, RelID relID, 
		      AVPair *avp, TypedValue tv2, 
		      Justification *justification, CVProps props, 
		      Rule *rule, int vertical);
void assert_equality2(Graph *graph, 
		      AVPair *avp1, AVPair *avp2, 
		      Justification *justification, CVProps props, Rule *rule);
AVPair *assert_attr2(Graph *graph, AVPair *avp, AttrID attr,
		  Justification *justification, Rule *rule);
void assert_nogood2(Graph *graph, Justification *justification,
		    int inconsistent, Rule *rule);
int compare_typed_values_v(TypedValue value1, TypedValue value2);

CVPair *find_relation(Graph *graph, RelID relID, 
		      TypedValue tv1, TypedValue tv2, CVProps props);
CVPair *find_equality(Graph *graph, 
		      TypedValue tv1, TypedValue tv2, CVProps props);

/* these procedures manage justifications */
void clear_justifications();
int edge_visited(struct Edge *edge);
void add_justification(Graph *graph, TypedValue data, 
		       Justification *justification, Rule *rule);
||#
;; JustifiedFact *get_justified_facts(Graph *graph);
(define-foreign-function "get_justified_facts"
    ((graph :unsigned-long)
     )
  :unsigned-long
  :lisp-name get_justified_facts
  :module +xle-module-path+)

;; JustifiedFact *get_justified_fact(JustifiedFact *facts, TypedValue fact);

:eof