#include "topform.h"

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

Public Routines
Public Definitions
Introduction

Public Routines in File topform.c

Index

append_label_attribute	fprint_topform_mem	p_clause	term_to_topform
check_upward_clause_links	fsym_set_in_topforms	p_topform_mem	topform_properties
cl_id_compare	function_symbols_in_topform	relation_symbols_in_topform	topform_to_term
cl_wt_id_compare	function_symbols_in_topforms	relation_symbols_in_topforms	topform_to_term_without_attributes
clause_set_variables	get_topform	renum_vars_map	upward_clause_links
copy_clause	inherit_attributes	renumber_variables	zap_topform
copy_clause_with_flag	initial_clause	rsym_set_in_topforms
copy_clause_with_flags	min_depth	term_renumber_variables
fprint_clause	negative_clause_possibly_compressed	term_to_clause

Details

void append_label_attribute(Topform tf, char *s);

BOOL check_upward_clause_links(Topform c);

In the given Topform c, check that the "container" field of each subterm point to c.

Ordertype cl_id_compare(Topform c1, Topform c2);

Ordertype cl_wt_id_compare(Topform c1, Topform c2);

void clause_set_variables(Topform c, int max_vars);

This routine traverses a clause and changes the constants that should be variables, into variables. On input, the clause should have no variables. The new variables are numbered 0, 1, 2 ... according the the first occurrence, reading from the left.

A fatal error occurs if there are more than max_vars variables.

The intended is use is for input clauses that are built without regard to variable/constant distinction.

Topform copy_clause(Topform c);

This routine builds and returns a copy of a clause. The container field of each nonvariable subterm points to the clause.

Topform copy_clause_with_flag(Topform c, int flag);

This routine builds and returns a copy of a clause. The given termflag is copied for all subterms (including atoms, excluding variables).

Topform copy_clause_with_flags(Topform c);

This routine builds and returns a copy of a clause. All termflags are copied for all subterms (including atoms, excluding variables).

void fprint_clause(FILE *fp, Topform c);

This routine prints a clause to a file.

void fprint_topform_mem(FILE *fp, int heading);

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

Ilist fsym_set_in_topforms(Plist lst);

I2list function_symbols_in_topform(Topform c, I2list g);

Collect the multiset of function symbols in a clause.

I2list function_symbols_in_topforms(Plist lst);

Collect the multiset of function symbols (including constants) in clauses in a Plist. An I2list of SYMNUMs is returned.

Topform get_topform(void);

void inherit_attributes(Topform par1, Context s1,
			Topform par2, Context s2,
			Topform child);

This takes two parent clauses and their associated substitutions, and a child clause. All inheritable attributes on the parents are instantiated and appended to the child's attributes.

Either parent can be NULL.

BOOL initial_clause(Topform c);

Is (was) the clause part of the initial sos (after processing input clauses, before starting search)/

BOOL min_depth(Literals lit);

Does the Literals have minimum depth of all literals the containing clause?

BOOL negative_clause_possibly_compressed(Topform c);

Is (was) the clause part of the initial sos (after processing input clauses, before starting search)/

void p_clause(Topform c);

This routine prints a clause to stdout.

void p_topform_mem();

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

I2list relation_symbols_in_topform(Topform c, I2list g);

Collect the multiset of relation symbols in a clause.

I2list relation_symbols_in_topforms(Plist lst);

Collect the multiset of relation symbols (including propositional constants) in clauses in a Plist. An I2list of SYMNUMs is returned.

Plist renum_vars_map(Topform c);

void renumber_variables(Topform c, int max_vars);

This routine renumbers the variables of a clause. The variables are renumbered 0, 1, 2 ... according the the first occurrence, reading from the left.

If there are more than max_vars distinct variables, a fatal error occurs.

The intended is use is for inferred clauses that may contain variable indexes greater than max_vars.

Ilist rsym_set_in_topforms(Plist lst);

void term_renumber_variables(Term t, int max_vars);

This routine renumbers the variables of a term. The variables are renumbered 0, 1, 2 ... according the the first occurrence, reading from the left.

If there are more than max_vars distinct variables, a fatal error occurs.

Do not use this to renumber variables of a clause (see renumber_variables).

Topform term_to_clause(Term t);

This routine takes a Term t (presumably a disjunction with binary symbol or_sym()), and constructs a Topform. The Topform is entirely new.

The main use of this routine is intended to be as follows: a Term representing a clause is parsed (using mixfix notation) from the input, then here it is copied translated into a Topform data structure.

Topform term_to_topform(Term t, BOOL is_formula);

Term topform_properties(Topform c);

Construct a term containing a list of miscellaneous properties of a Topform. This is meant to be used as an attribute on Topforms for debugging.

Term topform_to_term(Topform tf);

This routine takes a Topform and returns an entirely new Term which represents the clause. The disjunction symbol for the term is binary or_sym(), and the negation symbols is not_sym(). The attributes are included, but not the id or justifiction.

Term topform_to_term_without_attributes(Topform tf);

void upward_clause_links(Topform c);

In the given Topform c, make the "container" field of each subterm point to c.

void zap_topform(Topform tf);

This routine frees a Topform (but not any justification list). The caller should make sure that nothing (e.g., indexes) refer to the clause or any of its subterms.

If the clause has a justification or an official ID, use the higher-level routine delete_clause(c) instead.

Public Definitions in File topform.h

typedef struct topform * Topform;

struct topform {

  /* for both clauses and formulas */

  int              id;
  struct clist_pos *containers;     /* Clists that contain the Topform */
  Attribute        attributes;
  struct just      *justification;
  int              weight;
  char             *compressed;     /* if nonNULL, a compressed form */

  /* for clauses only */

  Literals         literals;        /* NULL can mean the empty clause */

  /* for formulas only */

  Formula          formula;

  int   semantics;        /* evaluation in interpretations */

  /* The rest of the fields are flags.  These could be bits. */

  char   is_formula;      /* is this really a formula? */
  char   normal_vars;     /* variables have been renumbered */
  char   used;            /* used to infer a clause that was kept */
  char   official_id;     /* Topform is in the ID table */
  char   initial;         /* existed at the start of the search */
  char   neg_compressed;  /* negative and compressed */
  char   matches_hint;    /* does this clause match a hint? */
  char   subsumer;        /* has this clause back subsumed anything? */

};

Introduction

A Topform can be used to store a formula or a clause. The field is_formula says which it is.

In earlier versions of LADR, this data structure was called Clause. When we decided to put non-clausal formulas in proofs, they needed to have IDs, attributes, and justifications, so we elevated the data structure to include non-clausal formulas and changed the name to Topform (top formula).

In many cases, when we say "clause", we mean a list of Literals. For example, most of the functions that tell the properties of clauses (positive_clause, number_of_literals, etc.) take a list of Literals, not a Topform.