# #include "ac_redun.h"

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

## Contents

- Public Routines
- Public Definitions
- Introduction

## Public Routines in File ac_redun.c

#### Index

associativity | associativity4 | cac_redundancy | commutativity
associativity3 | c_associativity | cac_tautology | same_top

#### Details

    int associativity(Term atom);

If the atom is associativity, f(f(x,y),z) = f(x,f(y,z)), return the symnum of the operation; otherwise return 0 (which is never a symnum).

    int associativity3(Term atom);

If the atom is any of the following (ab)c = a(bc) (ab)c = a(cb) (ab)c = b(ac) (ab)c = b(ca) return the symnum of the operation; otherwise return 0 (which is never a symnum).

    int associativity4(Term atom);

If the atom is any of the following a(bc) = b(ac) a(bc) = b(ca) a(bc) = c(ab) a(bc) = c(ba) return the symnum of the operation; otherwise return 0 (which is never a symnum).

    int c_associativity(Term atom);

If the atom is c_associativity, f(x,f(y,z)) = f(y,f(x,z)), return the symnum of the operation; otherwise return 0 (which is never a symnum).

    BOOL cac_redundancy(Topform c, BOOL print);

This routine checks if the clause is commutativity or "c-associativity" x(yz)=y(xz); if so, it stores that information for later calls to cac_redundancy(). If an operation is found to C or AC, return TRUE; if found to be just A, return FALSE;

Otherwise, if any positive literal is an instance of x=x (mod C and AC as previously noted), it is rewritten to $T. Then return FALSE.

Motivation: If we know that * is commutative, and we derive an equation f(a,b*c)=f(a,c*b), we can delete that equation, because commutativity can do anything that equation can do. The same goes for AC operations.

    BOOL cac_tautology(Literals lits);

    int commutativity(Term atom);

If the atom is commutativity, return the symnum of the operation; otherwise return 0 (which is never a symnum).

    BOOL same_top(Term t1, Term t2);

Do the two terms have the same top symbol?

## Public Definitions in File ac_redun.h

## Introduction