# #include "subsume.h"

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

## Contents

- Public Routines
- Public Definitions
- Introduction

## Public Routines in File subsume.c

#### Index

back_subsume | forward_subsume | subsumes | unit_delete
back_subsume_one | nonunit_subsumption_tests | subsumes_bt |
back_unit_del_by_index | simplify_literals | try_unit_conflict |
eq_removable_literal | simplify_literals2 | unit_conflict_by_index |

#### Details

    Plist back_subsume(Topform c, Lindex idx);

Look in the index and return the list of clauses subsumed by c.

    Topform back_subsume_one(Topform c, Lindex idx);

Look in the index for a clause subsumed by c. The first one found is returned. (It is not necessarily the first of the subsumees that was inserted into the index.)

    Plist back_unit_del_by_index(Topform unit, Lindex idx);

Given a unit clause and a literal index, return the Plist of clauses containing literals that are instances of the negation of the unit clause.

Such clauses can be "back unit deleted".

    BOOL eq_removable_literal(Topform c, Literals lit);

Can a literal in a clause be removed by resolution with x=x without instantiating any other literal in the clause?

If so, instantiate any inheritable (e.g., answer) attributes with the corresponding substitution.

    Topform forward_subsume(Topform d, Lindex idx);

    int nonunit_subsumption_tests(void);

    void simplify_literals(Topform c);

Remove any literals t!=t.

    void simplify_literals2(Topform c);

1. If there are any literals t=t, the clause becomes true_sym(). 2. Remove any literals t!=t. 3. If there are any literals s!=t, where unify(s,t), without instantiating any other literals, remove the literal.

    BOOL subsumes(Topform c, Topform d);

This routine checks if Topform c subsumes Topform d. Ordinary unification is used; in particular, symmetry of equality is not built in.

    BOOL subsumes_bt(Topform c, Topform d);

This routine checks if Topform c subsumes Topform d. Backtrack unification is used; in particular, AC and commutative/symmetric matching are applied where appropriate.

    Topform try_unit_conflict(Topform a, Topform b);

    void unit_conflict_by_index(Topform c, Lindex idx, void (*empty_proc) (Topform));

Look in idx for unit conflicts

    void unit_delete(Topform c, Lindex idx);

Given a clause and a literal index, remove the literals that can be removed by "unit deletion" with units in the index. Update the clause's justification for each removed literal.

## Public Definitions in File subsume.h

## Introduction