From 246c0c1c23414f630f64d91f2766c0652cd4a9d9 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 9 Aug 2004 21:22:24 +0000
Subject: [PATCH] - Added termMguSubTerm and termMguInTerm

---
 src/mgu.c | 70 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/mgu.h |  3 +++
 2 files changed, 73 insertions(+)

diff --git a/src/mgu.c b/src/mgu.c
index 8b3ad19..be6fc89 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -159,3 +159,73 @@ termMguTerm (Term t1, Term t2)
     }
   return MGUFAIL;
 }
+
+//! Most general interm unifiers of t1 interm t2
+/**
+ * Try to determine the most general interm unifiers of two terms.
+ *@returns Nothing. Iteration gets void.
+ */
+void
+termMguInTerm (Term t1, Term t2, void (*iterator) ())
+{
+  Termlist tl;
+
+  t2 = deVar (t2);
+  if (t2 != NULL && isTermTuple (t2))
+    {
+      // t2 is a tuple, consider interm options as well.
+      termMguInTerm (t1, t2->left.op1, iterator);
+      termMguInTerm (t1, t2->right.op2, iterator);
+    }
+  // simple clause or combined
+  tl = termMguTerm (t1, t2);
+  // Iterate
+  iterator ();
+  // Reset variables
+  termlistSubstReset (tl);
+}
+
+//! Most general subterm unifiers of t1 subterm t2
+/**
+ * Try to determine the most general subterm unifiers of two terms.
+ *@returns Nothing. Iteration gets list of keys needed to decrypt.
+ */
+void
+termMguSubTerm (Term t1, Term t2, void (*iterator) (),
+		const Termlist inverses, Termlist keylist)
+{
+  Termlist tl;
+  t2 = deVar (t2);
+  if (t2 != NULL && !isTermLeaf (t2))
+    {
+      if (isTermTuple (t2))
+	{
+	  // 'simple' tuple
+	  termMguSubTerm (t1, t2->left.op1, iterator, inverses, keylist);
+	  termMguSubTerm (t1, t2->right.op2, iterator, inverses, keylist);
+	}
+      else
+	{
+	  // Must be encryption
+	  // So, we need the key, and try to get the rest
+	  Termlist keylist_new;
+	  Term newkey;
+
+	  keylist_new = termlistShallow (keylist);
+	  newkey = inverseKey (inverses, t2->right.key);
+	  keylist_new = termlistAdd (keylist_new, newkey);
+
+	  // Recurse
+	  termMguSubTerm (t1, t2->left.op, iterator, inverses, keylist_new);
+
+	  termlistDelete (keylist_new);
+	  termDelete (newkey);
+	}
+    }
+  // simple clause or combined
+  tl = termMguTerm (t1, t2);
+  // Iterate
+  iterator (keylist);
+  // Reset variables
+  termlistSubstReset (tl);
+}
diff --git a/src/mgu.h b/src/mgu.h
index 045902f..0cb636b 100644
--- a/src/mgu.h
+++ b/src/mgu.h
@@ -15,5 +15,8 @@
 #define MGUFAIL (Termlist) -1
 
 Termlist termMguTerm (Term t1, Term t2);
+void termMguInTerm (Term t1, Term t2, void (*iterator) ());
+void termMguSubTerm (Term t1, Term t2, void (*iterator) (),
+		     const Termlist inverses, Termlist keylist);
 
 #endif