#include "clash.h"

This page has information from files clash.h and clash.c.

Public Routines
Public Definitions
Introduction

Public Routines in File clash.c

Index

append_clash	atom_to_literal	fprint_clash_mem	zap_clash
apply_lit	clash	p_clash_mem

Details

Clash append_clash(Clash p);

This routine simply allocates a new clash node, links it in after the given node, and returns the new node.

Literals apply_lit(Literals lit, Context c);

This routine applies a substitution to a literal and returns the instance. The given literal is not changed.

Literals atom_to_literal(Term atom);

This routine takes an atom and returns its parent literal.

void clash(Clash c,
	   BOOL (*sat_test) (Literals),
	   Just_type rule,
	   void (*proc_proc) (Topform));

This routine takes a complete clash list and computes the resolvents.

clash -- a complete clash list corresponding to the nucleus.
sat_test -- a Boolean function on clauses which identifies potential satellites (e.g., positive clauses for hyperresolution).
rule -- the name of the inference rule for the justification list (see just.h).
proc_proc -- procedure for processing resolvents.

void fprint_clash_mem(FILE *fp, BOOL heading);

This routine prints (to FILE *fp) memory usage statistics for data types associated with the clash package. The Boolean argument heading tells whether to print a heading on the table.

void p_clash_mem();

This routine prints (to stdout) memory usage statistics for data types associated with the clash package.

void  zap_clash(Clash p);

Free a clash list. Contexts in clashable nodes (which are assumed to exist and be empty) are freed as well.

Public Definitions in File clash.h

typedef struct clash  * Clash;

struct clash {
  BOOL       clashable;
  BOOL       clashed;
  BOOL       flipped;  /* Is nuc_lit or sat_lit a flipped equality? */
  Literals    nuc_lit;
  Context    nuc_subst;
  Literals    sat_lit;
  Context    sat_subst;
  Mindex     mate_index;
  Mindex_pos mate_pos;
  Clash      next;
};

Introduction