- Introduced termInTerm (bigterm, smallterm)
This commit is contained in:
parent
a2cc46bb34
commit
bb78c71c90
@ -254,7 +254,7 @@ create_intruder_goal (Term t)
|
||||
int run;
|
||||
Roledef rd;
|
||||
|
||||
roleInstance (sys, INTRUDER, I_GOAL, NULL, NULL);
|
||||
roleInstance (sys, INTRUDER, NULL, NULL, NULL);
|
||||
run = sys->maxruns - 1;
|
||||
rd = sys->runs[run].start;
|
||||
sys->runs[run].length = 1;
|
||||
|
@ -144,7 +144,7 @@ termMguTerm (Term t1, Term t2)
|
||||
/* symmetrical tests for single variable */
|
||||
if (realTermVariable (t2))
|
||||
{
|
||||
if (termOccurs (t1, t2) || !goodsubst (t2, t1))
|
||||
if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
|
||||
return MGUFAIL;
|
||||
else
|
||||
{
|
||||
@ -157,7 +157,7 @@ termMguTerm (Term t1, Term t2)
|
||||
}
|
||||
if (realTermVariable (t1))
|
||||
{
|
||||
if (termOccurs (t2, t1) || !goodsubst (t1, t2))
|
||||
if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
|
||||
return MGUFAIL;
|
||||
else
|
||||
{
|
||||
|
@ -539,7 +539,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
|
||||
* case we forget it */
|
||||
if (sys->switchForceChoose
|
||||
|| !(rd->type == READ
|
||||
&& termOccurs (rd->message, scanfrom->term)))
|
||||
&& termSubTerm (rd->message, scanfrom->term)))
|
||||
{
|
||||
/* this term is forced as a choose, or it does not occur in the (first) read event */
|
||||
/* TODO scan might be more complex, but
|
||||
|
35
src/term.c
35
src/term.c
@ -265,7 +265,7 @@ isTermEqualFn (Term term1, Term term2)
|
||||
*@return True iff tsub is a subterm of t.
|
||||
*/
|
||||
int
|
||||
termOccurs (Term t, Term tsub)
|
||||
termSubTerm (Term t, Term tsub)
|
||||
{
|
||||
t = deVar (t);
|
||||
tsub = deVar (tsub);
|
||||
@ -275,10 +275,33 @@ termOccurs (Term t, Term tsub)
|
||||
if (realTermLeaf (t))
|
||||
return 0;
|
||||
if (realTermTuple (t))
|
||||
return (termOccurs (t->left.op1, tsub)
|
||||
|| termOccurs (t->right.op2, tsub));
|
||||
return (termSubTerm (t->left.op1, tsub)
|
||||
|| termSubTerm (t->right.op2, tsub));
|
||||
else
|
||||
return (termOccurs (t->left.op, tsub) || termOccurs (t->right.key, tsub));
|
||||
return (termSubTerm (t->left.op, tsub) || termSubTerm (t->right.key, tsub));
|
||||
}
|
||||
|
||||
//! See if a term is an interm of another.
|
||||
/**
|
||||
*@param t Term to be checked for a subterm.
|
||||
*@param tsub interm.
|
||||
*@return True iff tsub is an interm of t.
|
||||
*/
|
||||
int
|
||||
termInTerm (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 (termInTerm (t->left.op1, tsub)
|
||||
|| termInTerm (t->right.op2, tsub));
|
||||
else
|
||||
return 0;
|
||||
}
|
||||
|
||||
//! Print a term to stdout.
|
||||
@ -772,11 +795,11 @@ termDistance (Term t1, Term t2)
|
||||
if (t1->type != t2->type)
|
||||
{
|
||||
/* unequal type, maybe one is a subterm of the other? */
|
||||
if (t1s > t2s && termOccurs (t1, t2))
|
||||
if (t1s > t2s && termSubTerm (t1, t2))
|
||||
{
|
||||
return (float) t2s / t1s;
|
||||
}
|
||||
if (t2s > t1s && termOccurs (t2, t1))
|
||||
if (t2s > t1s && termSubTerm (t2, t1))
|
||||
{
|
||||
return (float) t1s / t2s;
|
||||
}
|
||||
|
@ -153,7 +153,8 @@ int isTermEqualDebug (Term t1, Term t2);
|
||||
|
||||
int hasTermVariable (Term term);
|
||||
int isTermEqualFn (Term term1, Term term2);
|
||||
int termOccurs (Term t, Term tsub);
|
||||
int termSubTerm (Term t, Term tsub);
|
||||
int termInTerm (Term t, Term tsub);
|
||||
void termPrint (Term term);
|
||||
void termTuplePrint (Term term);
|
||||
Term termDuplicate (const Term term);
|
||||
|
Loading…
Reference in New Issue
Block a user