From bb78c71c90bc669d0605fb2e6c015b3cc67adf6d Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 17 Aug 2004 14:11:25 +0000
Subject: [PATCH] - Introduced termInTerm (bigterm, smallterm)

---
 src/arachne.c |  2 +-
 src/mgu.c     |  4 ++--
 src/system.c  |  2 +-
 src/term.c    | 35 +++++++++++++++++++++++++++++------
 src/term.h    |  3 ++-
 5 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index 0e8dda7..22fb8e1 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -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;
diff --git a/src/mgu.c b/src/mgu.c
index c69d34b..c88a398 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -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
 	{
diff --git a/src/system.c b/src/system.c
index d394e63..111ac66 100644
--- a/src/system.c
+++ b/src/system.c
@@ -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
diff --git a/src/term.c b/src/term.c
index 7928e83..44bcfd8 100644
--- a/src/term.c
+++ b/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;
 	}
diff --git a/src/term.h b/src/term.h
index f687a35..4d75cd1 100644
--- a/src/term.h
+++ b/src/term.h
@@ -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);