#include "just.h"
This page has information from files
just.h and just.c.
Contents
Public Routines in File just.c
Index
Details
Just append_just(Just j1, Just j2);
This appends two justifications. No copying occurs.
Just back_demod_just(Topform c);
This routine builds and returns a justification list for back_demod.
Just back_unit_deletion_just(Topform c);
This routine builds and returns a justification list for back_unit_deletion.
Just binary_res_just(Topform c1, int n1, Topform c2, int n2);
This routine builds and returns a justification list for binary resolution.
(Binary res justifications may also be constructed in resolve(), along
with hyper and UR.)
Just binary_res_just_by_id(int c1, int n1, int c2, int n2);
Similar to binary_res_just, except that IDs are given instead of clauses.
int clause_level(Topform c);
Return the level of a clause. Input clauses have level=0, and
a derived clause has level 1 more than the max of the levels of its parents.
Just clausify_just(Topform tf);
This routine builds and returns a justification list for clausify.
Just copy_just(Topform c);
This routine builds and returns a justification list for copy.
Just copy_justification(Just j);
Copy a justification.
Just demod_just(I3list steps);
This routine builds and returns a justification for a demodulation.
Just deny_just(Topform tf);
This routine builds and returns a justification list for deny.
Just expand_def_just(Topform tf, Topform def);
This routine builds and returns a justification list for expand_def.
Just factor_just(Topform c, int lit1, int lit2);
This routine builds and returns a justification list for a factorization.
Topform first_negative_parent(Topform c);
Just flip_just(int n);
This routine builds and returns a justification for equality flipping.
void fprint_just_mem(FILE *fp, BOOL heading);
This routine prints (to FILE *fp) memory usage statistics for data types
associated with the just package.
The Boolean argument heading tells whether to print a heading on the table.
Plist get_clause_ancestors(Topform c);
This routine returns the Plist of clauses that are ancestors of Topform c,
including clause c. The result is sorted (increasing) by ID.
If any of the ancestors are compressed, they are uncompressed
(in place) and left uncompressed.
Instancejust get_instancejust(void);
Just get_just(void);
Parajust get_parajust(void);
Ilist get_parents(Just just, BOOL all);
This routine returns an Ilist of parent IDs.
If (all), get parents from the whole justification; otherwise
get parents from the first node only.
Just goal_just(void);
This routine builds and returns a justification list for goal.
BOOL has_copy_flip_just(Topform c);
Does a clause have justification "copy, flip", and nothing else?
BOOL has_copy_just(Topform c);
Does a clause have justification "copy"?
BOOL has_input_just(Topform c);
Does a clause have justtification "input"?
Just input_just(void);
This routine builds and returns a justification list for input.
Just instance_just(Topform parent, Plist pairs);
This routine builds and returns a justification list for an instance
inference. The list of pairs is not copied.
Just ivy_just(Just_type type,
int parent1, Ilist pos1,
int parent2, Ilist pos2,
Plist pairs);
int jmap1(I3list map, int i);
A jmap maps ints to pairs of ints. This returns the first.
If i is not in the map, i is returned.
char *jmap2(I3list map, int i, char *a);
A jmap maps ints to pairs of ints. This returns a string
representation of the second. If i is not in the map, or
if the int value of is INT_MIN, "" is returned.
Starting with 0, the strings are "A" - "Z", "A26", "A27", ... .
The argument *a must point to available space for the result.
The result is returned.
char *jstring(Just j);
What is the string, e.g., "resolve" associated with a justification node?
int just_count(Just j);
Return the number of justification elements in a justtification.
void map_just(Just just, I2list map);
Update the clause IDs in a justification according to the map.
void mark_parents_as_used(Topform c);
Just merge_just(int n);
This routine builds and returns a justification for the merging
a literal. The n-th literal has been removed because it is
identical to another literal.
Just new_symbol_just(Topform c);
This routine builds and returns a justification list for new_symbol inference.
void p_just(Just j);
void p_just_mem();
This routine prints (to stdout) memory usage statistics for data types
associated with the just package.
Just para_just(Just_type rule,
Topform from, Ilist from_vec,
Topform into, Ilist into_vec);
This routine builds and returns a justification list for a paramodulation
inference. The position vectors are not copied.
Just para_just_rev_copy(Just_type rule,
Topform from, Ilist from_vec,
Topform into, Ilist into_vec);
This routine builds and returns a justification list for a paramodulation
inference. The position vectors are copied and reversed.
BOOL primary_just_type(Topform c, Just_type t);
Does a clause have justtification "input"?
int proof_length(Plist proof);
Just propositional_just(Topform c);
This routine builds and returns a justification list for propositional.
Just resolve_just(Ilist g, Just_type type);
This routine builds and returns a justification for resolution rules.
This handles binary, hyper, ur, and maybe others.
void sb_append_id(String_buf sb, int id, I3list map);
void sb_write_ids(String_buf sb, Ilist p, I3list map);
void sb_write_just(String_buf sb, Just just, I3list map);
This routine writes (to a String_buf) a clause justification.
No whitespace is printed before or after.
void sb_xml_write_just(String_buf sb, Just just, I3list map);
Just term_to_just(Term lst);
Just unit_del_just(Topform deleter, int literal_num);
This routine builds and returns a justification list for a factorization.
Just xx_just(int n);
This routine builds and returns a justification for the XX rule,
which removes literals that are instances of x!=x.
Just xxres_just(Topform c, int lit);
This routine builds and returns a justification list for resolution with x=x.
void zap_just(Just just);
This routine frees a justification list, including any sublists.
Public Definitions in File just.h
typedef enum {
INPUT_JUST, /* Primary */
GOAL_JUST, /* Primary */
DENY_JUST, /* Primary int (ID) */
CLAUSIFY_JUST, /* Primary int (ID) */
COPY_JUST, /* Primary int (ID) */
BACK_DEMOD_JUST, /* Primary int (ID) */
BACK_UNIT_DEL_JUST, /* Primary int (ID) */
NEW_SYMBOL_JUST, /* Primary int (ID) */
EXPAND_DEF_JUST, /* Primary Ilist (ID,def-ID) */
BINARY_RES_JUST, /* Primary Ilist */
HYPER_RES_JUST, /* Primary Ilist */
UR_RES_JUST, /* Primary Ilist */
FACTOR_JUST, /* Primary Ilist (ID,lit1,lit2) */
XXRES_JUST, /* Primary Ilist (ID,lit) */
PARA_JUST, /* Primary Parajust */
PARA_FX_JUST, /* Primary Parajust */
PARA_IX_JUST, /* Primary Parajust */
PARA_FX_IX_JUST, /* Primary Parajust */
INSTANCE_JUST, /* Primary Instancejust */
PROPOSITIONAL_JUST, /* Primary int (ID) */
DEMOD_JUST, /* Secondary I3list */
UNIT_DEL_JUST, /* Secondary Ilist (lit,ID) */
FLIP_JUST, /* Secondary int (lit) */
XX_JUST, /* Secondary int (lit) */
MERGE_JUST, /* Secondary int (lit) */
IVY_JUST, /* Primary Ivyjust */
UNKNOWN_JUST /* probably an error */
} Just_type;
typedef struct parajust * Parajust;
struct parajust {
int from_id;
int into_id;
Ilist from_pos;
Ilist into_pos;
};
typedef struct instancejust * Instancejust;
struct instancejust {
int parent_id;
Plist pairs;
};
typedef struct ivyjust * Ivyjust;
struct ivyjust {
Just_type type; /* input,resolve,paramod,instantiate,flip,propositional */
int parent1;
int parent2;
Ilist pos1;
Ilist pos2;
Plist pairs; /* for instantiate */
};
typedef struct just * Just;
struct just {
Just_type type;
Just next;
union {
int id;
Ilist lst;
Parajust para;
I3list demod;
Instancejust instance;
Ivyjust ivy;
} u;
};
/* A justification starts with a Primary part and then
has a sequence (maybe none) of Secondary parts.
Each type has some data, an integer or Ilist (integer
list) giving clause IDs, or positions of literals or
subterms.
*/
Introduction