scyther/src/terms.c

796 lines
16 KiB
C
Raw Normal View History

2004-05-15 13:39:49 +01:00
/**
* @file terms.c
* \brief Term related base functions.
*
* Intended to be a standalone file, however during development it turned out that a termlist structure was needed
* to define term types, so there is now a dependency loop with termlists.c.
*/
#include <strings.h>
2004-04-23 11:58:43 +01:00
#include <stdlib.h>
#include <stdio.h>
#include <limits.h>
#include "terms.h"
#include "debug.h"
#include "memory.h"
#include "ctype.h"
/* external definitions */
extern Term TERM_Function;
extern int inTermlist (); // suppresses a warning, but at what cost?
extern int globalLatex;
/* forward declarations */
void indent (void);
/* useful macros */
#define RID_UNDEF MIN_INT
/* main code */
/* Two types of terms: general, and normalized. Normalized rewrites all
tuples to (x,(y,z))..NULL form, making list traversal easy. */
2004-05-15 13:33:01 +01:00
//! Initialization of terms code.
2004-04-23 11:58:43 +01:00
void
termsInit (void)
{
return;
}
2004-05-15 13:33:01 +01:00
//! Cleanup of terms code.
2004-04-23 11:58:43 +01:00
void
termsDone (void)
{
return;
}
2004-05-15 13:33:01 +01:00
//! Allocate memory for a term.
/**
*@return A pointer to the new term memory, which is not yet initialised.
*/
2004-04-23 11:58:43 +01:00
Term
makeTerm ()
{
return (Term) memAlloc (sizeof (struct term));
}
2004-05-15 13:33:01 +01:00
//! Create a fresh encrypted term from two existing terms.
/**
*@return A pointer to the new term.
*/
2004-04-23 11:58:43 +01:00
Term
makeTermEncrypt (Term t1, Term t2)
{
Term term = makeTerm ();
term->type = ENCRYPT;
term->stype = NULL;
term->left.op = t1;
term->right.key = t2;
2004-04-23 11:58:43 +01:00
return term;
}
2004-05-15 13:33:01 +01:00
//! Create a fresh term tuple from two existing terms.
/**
*@return A pointer to the new term.
*/
2004-04-23 11:58:43 +01:00
Term
makeTermTuple (Term t1, Term t2)
{
2004-05-26 09:52:15 +01:00
Term tt;
2004-04-23 11:58:43 +01:00
if (t1 == NULL)
{
if (t2 == NULL)
{
#ifdef DEBUG
debug (5, "Trying to make a tuple node with an empty term.");
#endif
return NULL;
}
else
2004-05-26 13:17:09 +01:00
{
return t2;
}
2004-04-23 11:58:43 +01:00
}
if (t2 == NULL)
{
return t1;
}
2004-05-26 09:52:15 +01:00
tt = makeTerm ();
2004-04-23 11:58:43 +01:00
tt->type = TUPLE;
tt->stype = NULL;
tt->left.op1 = t1;
tt->right.op2 = t2;
2004-04-23 11:58:43 +01:00
return tt;
}
2004-05-15 13:33:01 +01:00
//! Make a term of the given type with run identifier and symbol.
/**
*@return A pointer to the new term.
*\sa GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE
*/
2004-04-23 11:58:43 +01:00
Term
makeTermType (const int type, const Symbol symb, const int runid)
{
Term term = makeTerm ();
term->type = type;
term->stype = NULL;
term->subst = NULL;
term->left.symb = symb;
term->right.runid = runid;
2004-04-23 11:58:43 +01:00
return term;
}
2004-05-15 13:33:01 +01:00
//! Unwrap any substitutions.
/**
* For speed, it is also a macro. Sometimes it will call
2004-04-23 11:58:43 +01:00
* deVarScan to do the actual unwinding.
2004-05-15 13:33:01 +01:00
*@return A term that is either not a variable, or has a NULL substitution.
*\sa deVar()
2004-04-23 11:58:43 +01:00
*/
Term
deVarScan (Term t)
{
while (realTermVariable (t) && t->subst != NULL)
t = t->subst;
return t;
}
2004-05-15 13:33:01 +01:00
//! Determine whether a term contains an unsubstituted variable as subterm.
/**
*@return True iff there is an open variable as subterm.
*/
2004-04-23 11:58:43 +01:00
int
hasTermVariable (Term term)
{
if (term == NULL)
return 0;
term = deVar (term);
if (realTermLeaf (term))
return realTermVariable (term);
else
{
if (realTermTuple (term))
return (hasTermVariable (term->left.op1) || hasTermVariable (term->right.op2));
2004-04-23 11:58:43 +01:00
else
return (hasTermVariable (term->left.op) || hasTermVariable (term->right.key));
2004-04-23 11:58:43 +01:00
}
}
2004-05-15 13:33:01 +01:00
//!Tests whether two terms are completely identical.
/**
* This also includes
* variables. This is the recursive function.
* We assume the term is normalized, e.g. no tupling has direct
* subtupling.
*@return True iff the terms are equal.
*\sa isTermEqual()
*/
2004-04-23 11:58:43 +01:00
int
isTermEqualFn (Term term1, Term term2)
{
term1 = deVar (term1);
term2 = deVar (term2);
if (term1 == term2)
return 1;
if ((term1 == NULL) || (term2 == NULL))
return 0;
if (term1->type != term2->type)
{
return 0;
}
if (realTermLeaf (term1))
{
return (term1->left.symb == term2->left.symb && term1->right.runid == term2->right.runid);
2004-04-23 11:58:43 +01:00
}
else
{
/* ENCRYPT or TUPLE */
if (realTermEncrypt (term1))
{
/* for optimization of encryption equality, we compare
operator 2 first (we expect it to be a smaller term)
*/
return (isTermEqualFn (term1->right.key, term2->right.key) &&
isTermEqualFn (term1->left.op, term2->left.op));
2004-04-23 11:58:43 +01:00
}
else
{
/* tuple */
return (isTermEqualFn (term1->left.op1, term2->left.op1) &&
isTermEqualFn (term1->right.op2, term2->right.op2));
2004-04-23 11:58:43 +01:00
}
}
}
2004-05-15 13:33:01 +01:00
//! See if a term is a subterm of another.
/**
*@param t Term to be checked for a subterm.
*@param tsub Subterm.
*@return True iff tsub is a subterm of t.
*/
2004-04-23 11:58:43 +01:00
int
termOccurs (Term t, Term tsub)
{
t = deVar (t);
tsub = deVar (tsub);
if (isTermEqual (t, tsub))
return 1;
if (realTermLeaf (t))
return 0;
if (realTermTuple (t))
return (termOccurs (t->left.op1, tsub) || termOccurs (t->right.op2, tsub));
2004-04-23 11:58:43 +01:00
else
return (termOccurs (t->left.op, tsub) || termOccurs (t->right.key, tsub));
2004-04-23 11:58:43 +01:00
}
2004-05-15 13:33:01 +01:00
//! Print a term to stdout.
2004-05-19 09:39:39 +01:00
/**
* The tuple printing only works correctly for normalized terms.
* If not, they might are displayed as "((x,y),z)". Maybe that is even
* desirable to distinguish them.
*\sa termTuplePrint()
*/
2004-04-23 11:58:43 +01:00
void
termPrint (Term term)
{
if (term == NULL)
{
printf ("Empty term");
return;
}
#ifdef DEBUG
if (!DEBUGL (1))
{
term = deVar (term);
}
#else
term = deVar (term);
#endif
if (realTermLeaf (term))
{
symbolPrint (term->left.symb);
2004-04-23 11:58:43 +01:00
if (realTermVariable (term))
printf ("V");
if (term->right.runid >= 0)
2004-04-23 11:58:43 +01:00
{
if (globalLatex)
printf ("\\sharp%i", term->right.runid);
2004-04-23 11:58:43 +01:00
else
printf ("#%i", term->right.runid);
2004-04-23 11:58:43 +01:00
}
if (term->subst != NULL)
{
if (globalLatex)
printf ("\\rightarrow");
else
printf ("->");
termPrint (term->subst);
}
}
if (realTermTuple (term))
{
printf ("(");
2004-05-19 09:39:39 +01:00
termTuplePrint(term);
2004-04-23 11:58:43 +01:00
printf (")");
return;
}
if (realTermEncrypt (term))
{
if (isTermLeaf (term->right.key)
&& inTermlist (term->right.key->stype, TERM_Function))
2004-04-23 11:58:43 +01:00
{
/* function application */
termPrint (term->right.key);
2004-04-23 11:58:43 +01:00
printf ("(");
termTuplePrint (term->left.op);
2004-04-23 11:58:43 +01:00
printf (")");
}
else
{
/* normal encryption */
if (globalLatex)
{
printf ("\\{");
termTuplePrint (term->left.op);
2004-04-23 11:58:43 +01:00
printf ("\\}_{");
termPrint (term->right.key);
2004-04-23 11:58:43 +01:00
printf ("}");
}
else
{
printf ("{");
termTuplePrint (term->left.op);
2004-04-23 11:58:43 +01:00
printf ("}");
termPrint (term->right.key);
2004-04-23 11:58:43 +01:00
}
}
}
}
2004-05-19 09:39:39 +01:00
//! Print an inner (tuple) term to stdout, without brackets.
/**
* The tuple printing only works correctly for normalized terms.
* If not, they might are displayed as "((x,y),z)". Maybe that is even
* desirable to distinguish them.
*/
void
termTuplePrint (Term term)
{
if (term == NULL)
{
printf ("Empty term");
return;
}
term = deVar(term);
while (realTermTuple (term))
{
// To remove any brackets, change this into termTuplePrint.
termPrint (term->left.op1);
2004-05-19 09:39:39 +01:00
printf (",");
term = deVar(term->right.op2);
2004-05-19 09:39:39 +01:00
}
termPrint(term);
return;
}
2004-04-23 11:58:43 +01:00
2004-05-15 13:33:01 +01:00
//! Make a deep copy of a term.
/**
* Leaves are not copied.
*@return If the original was a leaf, then the pointer is simply returned. Otherwise, new memory is allocated and the node is copied recursively.
*\sa termDuplicateDeep()
*/
2004-04-23 11:58:43 +01:00
Term
termDuplicate (const Term term)
{
Term newterm;
if (term == NULL)
return NULL;
if (realTermLeaf (term))
return term;
newterm = (Term) memAlloc (sizeof (struct term));
newterm->type = term->type;
if (realTermEncrypt (term))
{
newterm->left.op = termDuplicate (term->left.op);
newterm->right.key = termDuplicate (term->right.key);
2004-04-23 11:58:43 +01:00
}
else
{
newterm->left.op1 = termDuplicate (term->left.op1);
newterm->right.op2 = termDuplicate (term->right.op2);
2004-04-23 11:58:43 +01:00
}
return newterm;
}
2004-05-15 13:33:01 +01:00
//! Make a true deep copy of a term.
/**
* Currently, it this function is not to be used, so we can be sure leaf nodes occur only once in the system.
*@return New memory is allocated and the node is copied recursively.
*\sa termDuplicate()
*/
2004-04-23 11:58:43 +01:00
Term
termDuplicateDeep (const Term term)
{
Term newterm;
if (term == NULL)
return NULL;
newterm = (Term) memAlloc (sizeof (struct term));
if (realTermLeaf (term))
{
memcpy (newterm, term, sizeof (struct term));
}
else
{
newterm->type = term->type;
if (realTermEncrypt (term))
{
newterm->left.op = termDuplicateDeep (term->left.op);
newterm->right.key = termDuplicateDeep (term->right.key);
2004-04-23 11:58:43 +01:00
}
else
{
newterm->left.op1 = termDuplicateDeep (term->left.op1);
newterm->right.op2 = termDuplicateDeep (term->right.op2);
2004-04-23 11:58:43 +01:00
}
}
return newterm;
}
2004-05-15 13:33:01 +01:00
//! Make a copy of a term, but remove substituted variable nodes.
/**
2004-04-23 11:58:43 +01:00
* Remove all instantiated variables on the way down.
2004-05-15 13:33:01 +01:00
*\sa termDuplicate()
2004-04-23 11:58:43 +01:00
*/
Term
termDuplicateUV (Term term)
{
Term newterm;
if (term == NULL)
return NULL;
term = deVar (term);
if (realTermLeaf (term))
return term;
newterm = (Term) memAlloc (sizeof (struct term));
newterm->type = term->type;
if (realTermEncrypt (term))
{
newterm->left.op = termDuplicateUV (term->left.op);
newterm->right.key = termDuplicateUV (term->right.key);
2004-04-23 11:58:43 +01:00
}
else
{
newterm->left.op1 = termDuplicateUV (term->left.op1);
newterm->right.op2 = termDuplicateUV (term->right.op2);
2004-04-23 11:58:43 +01:00
}
return newterm;
}
/*
realTermDuplicate
make a deep copy of a term, also of leaves.
*/
Term
realTermDuplicate (const Term term)
{
Term newterm;
if (term == NULL)
return NULL;
newterm = (Term) memAlloc (sizeof (struct term));
if (realTermLeaf (term))
{
memcpy (newterm, term, sizeof (struct term));
}
else
{
newterm->type = term->type;
if (realTermEncrypt (term))
{
newterm->left.op = realTermDuplicate (term->left.op);
newterm->right.key = realTermDuplicate (term->right.key);
2004-04-23 11:58:43 +01:00
}
else
{
newterm->left.op1 = realTermDuplicate (term->left.op1);
newterm->right.op2 = realTermDuplicate (term->right.op2);
2004-04-23 11:58:43 +01:00
}
}
return newterm;
}
2004-05-15 13:33:01 +01:00
//!Removes a term and deallocates memory.
/**
* Is meant to remove terms make with termDuplicate. Only deallocates memory
* of nodes, not of leaves.
*\sa termDuplicate(), termDuplicateUV()
*/
2004-04-23 11:58:43 +01:00
void
termDelete (const Term term)
{
if (term != NULL && !realTermLeaf (term))
{
if (realTermEncrypt (term))
{
termDelete (term->left.op);
termDelete (term->right.key);
2004-04-23 11:58:43 +01:00
}
else
{
termDelete (term->left.op1);
termDelete (term->right.op2);
2004-04-23 11:58:43 +01:00
}
memFree (term, sizeof (struct term));
}
}
2004-05-15 13:33:01 +01:00
//! Normalize a term with respect to tupling.
/**
* Avoids problems with associativity by rewriting every ((x,y),z) to
* (x,(y,z)), i.e. a normal form for terms, after which equality is
* okay. No memory was allocated or deallocated, as only pointers are swapped.
*
*@return After execution, the term pointed at has been normalized. */
2004-04-23 11:58:43 +01:00
void
termNormalize (Term term)
{
term = deVar (term);
if (term == NULL || realTermLeaf (term))
return;
if (realTermEncrypt (term))
{
termNormalize (term->left.op);
termNormalize (term->right.key);
2004-04-23 11:58:43 +01:00
}
else
{
/* normalize left hand first,both for tupling and for
encryption */
termNormalize (term->left.op1);
2004-04-23 11:58:43 +01:00
/* check for ((x,y),z) construct */
if (realTermTuple (term->left.op1))
2004-04-23 11:58:43 +01:00
{
/* temporarily store the old terms */
Term tx = (term->left.op1)->left.op1;
Term ty = (term->left.op1)->right.op2;
Term tz = term->right.op2;
2004-04-23 11:58:43 +01:00
/* move node */
term->right.op2 = term->left.op1;
2004-04-23 11:58:43 +01:00
/* construct (x,(y,z)) version */
term->left.op1 = tx;
(term->right.op2)->left.op1 = ty;
(term->right.op2)->right.op2 = tz;
2004-04-23 11:58:43 +01:00
}
termNormalize (term->right.op2);
2004-04-23 11:58:43 +01:00
}
}
2004-05-15 13:33:01 +01:00
//! Copy a term, and ensure all run identifiers are set to the new value.
/**
* Strange code. Only to be used on locals, as is stupidly replaces all run identifiers.
*@return The new term.
*\sa termDuplicate()
*/
2004-04-23 11:58:43 +01:00
Term
termRunid (Term term, int runid)
{
if (term == NULL)
return NULL;
if (realTermLeaf (term))
{
/* leaf */
if (term->right.runid == runid)
2004-04-23 11:58:43 +01:00
return term;
else
{
Term newt = termDuplicate (term);
newt->right.runid = runid;
2004-04-23 11:58:43 +01:00
return newt;
}
}
else
{
/* anything else, recurse */
if (realTermEncrypt (term))
{
return makeTermEncrypt (termRunid (term->left.op, runid),
termRunid (term->right.key, runid));
2004-04-23 11:58:43 +01:00
}
else
{
return makeTermTuple (termRunid (term->left.op1, runid),
termRunid (term->right.op2, runid));
2004-04-23 11:58:43 +01:00
}
}
}
2004-05-15 13:33:01 +01:00
//! Determine tuple width of a given term.
/**
*\sa tupleProject()
*/
2004-04-23 11:58:43 +01:00
int
tupleCount (Term tt)
{
if (tt == NULL)
{
return 0;
}
else
{
deVar (tt);
if (!realTermTuple (tt))
{
return 1;
}
else
{
return (tupleCount (tt->left.op1) + tupleCount (tt->right.op2));
2004-04-23 11:58:43 +01:00
}
}
}
2004-05-15 13:33:01 +01:00
//! Yield the projection Pi(n) of a term.
/**
*@param tt Term
*@param n The index in the tuple.
*@return Returns either a pointer to a term, or NULL if the index is out of range.
*\sa tupleCount()
*/
2004-04-23 11:58:43 +01:00
Term
tupleProject (Term tt, int n)
{
if (tt == NULL)
{
return NULL;
}
deVar (tt);
if (!realTermTuple (tt))
{
if (n > 0)
{
/* no tuple, adressing error */
return NULL;
}
else
{
/* no tuple */
return tt;
}
}
else
{
/* there is a tuple to traverse */
int left = tupleCount (tt->left.op1);
2004-04-23 11:58:43 +01:00
if (n >= left)
{
/* it's in the right hand side */
return tupleProject (tt->right.op2, n - left);
2004-04-23 11:58:43 +01:00
}
else
{
/* left hand side */
return tupleProject (tt->left.op1, n);
2004-04-23 11:58:43 +01:00
}
}
}
2004-05-15 13:33:01 +01:00
//! Determine size of term.
/**
* Determines the size of a term according to some heuristic.
2004-04-23 11:58:43 +01:00
* Currently, the encryption operator is weighed as well.
2004-05-15 13:33:01 +01:00
*@return Returns a nonnegative integer.
*\sa termDistance()
2004-04-23 11:58:43 +01:00
*/
int
termSize(Term t)
{
if (t == NULL)
{
return 0;
}
t = deVar(t);
if (realTermLeaf(t))
{
return 1;
}
else
{
if (realTermEncrypt(t))
{
return 1 + termSize(t->left.op) + termSize(t->right.key);
2004-04-23 11:58:43 +01:00
}
else
{
return termSize(t->left.op1) + termSize(t->right.op2);
2004-04-23 11:58:43 +01:00
}
}
}
2004-05-15 13:33:01 +01:00
//! Determine distance between two terms.
/**
*@return A float value between 0, completely dissimilar, and 1, equal.
*\sa termSize()
2004-04-23 11:58:43 +01:00
*/
float
termDistance(Term t1, Term t2)
{
int t1s;
int t2s;
2004-04-23 11:58:43 +01:00
/* First the special cases: no equal subterms, completely equal */
if (isTermEqual(t1,t2))
return 1;
t1 = deVar(t1);
t2 = deVar(t2);
t1s = termSize(t1);
t2s = termSize(t2);
2004-04-23 11:58:43 +01:00
if (t1 == NULL || t2 == NULL)
{
return 0;
}
if (t1->type != t2->type)
{
/* unequal type, maybe one is a subterm of the other? */
if (t1s > t2s && termOccurs(t1,t2))
{
return (float) t2s / t1s;
}
if (t2s > t1s && termOccurs(t2,t1))
{
return (float) t1s / t2s;
}
return 0;
}
else
{
/* equal types */
if (isTermLeaf(t1))
{
/* we had established before that they are not equal */
return 0;
}
else
{
/* non-leaf recurse */
if (isTermEncrypt(t1))
{
/* encryption */
return (termDistance(t1->left.op, t2->left.op) + termDistance(t1->right.key, t2->right.key)) / 2;
2004-04-23 11:58:43 +01:00
}
else
{
return (termDistance(t1->left.op1, t2->left.op1) + termDistance(t1->right.op2, t2->right.op2)) / 2;
2004-04-23 11:58:43 +01:00
}
}
}
}
/**
* Enforce a (arbitrary) ordering on basic terms
* <0 means a<b, 0 means a=b, >0 means a>b.
*/
int termOrder (Term t1, Term t2)
{
char* name1;
char* name2;
t1 = deVar (t1);
t2 = deVar (t2);
if (!(realTermLeaf (t1) && realTermLeaf (t2)))
{
error ("'termOrder' can only be applied to two basic terms.");
}
if (isTermEqual (t1,t2))
{
/* equal terms */
return 0;
}
if (t1->type != t2->type)
{
/* unequal types (can this even occur?) */
if (t1->type < t2->type)
return -1;
else
return 1;
}
/* same type, compare names */
name1 = t1->left.symb->text;
name2 = t2->left.symb->text;
return strcmp (name1,name2);
}