From 8a2ae84f35e20fef9d774f59d3bb8fc0338cf90f Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Mon, 17 Sep 2007 16:54:17 +0200
Subject: [PATCH] Added incompleteness marker for the untyped variables and
 MGDU set problem.

---
 src/arachne.h |  1 +
 src/mgu.c     | 22 ++++++++++++++++++++++
 src/type.c    | 10 ++++++++++
 src/type.h    |  1 +
 4 files changed, 34 insertions(+)

diff --git a/src/arachne.h b/src/arachne.h
index 2b50132..95b1abb 100644
--- a/src/arachne.h
+++ b/src/arachne.h
@@ -35,5 +35,6 @@ void arachneOutputAttack ();
 void printSemiState ();
 int countIntruderActions ();
 void role_name_print (const int run);
+void markNoFullProof ();
 
 #endif
diff --git a/src/mgu.c b/src/mgu.c
index 11b02e2..93a706e 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -26,6 +26,7 @@
 #include "debug.h"
 #include "specialterm.h"
 #include "switches.h"
+#include "arachne.h"
 
 /*
    Most General Unifier
@@ -569,6 +570,27 @@ termMguSubTerm (Term smallterm, Term bigterm,
 	      termDelete (keyneeded);
 	    }
 	}
+      else
+	{
+	  // The big term is a leaf
+	  /**
+	   * In this case we really need to consider the problematic Athena case for untyped variables.
+	   */
+	  if (isTermVariable (bigterm))
+	    {
+	      // Check the type: can it contain tuples, encryptions?
+	      if (isOpenVariable (bigterm))
+		{
+		  // This one needs to be pursued by further constraint adding
+		    /**
+		     * Currently, this is not implemented yet. TODO.
+		     * This is actually the main Athena problem that we haven't solved yet.
+		     */
+		  // Mark that we don't have a full proof.
+		  markNoFullProof ();
+		}
+	    }
+	}
       // simple clause or combined
       tl = termMguTerm (smallterm, bigterm);
       if (tl != MGUFAIL)
diff --git a/src/type.c b/src/type.c
index b42471e..ed68b60 100644
--- a/src/type.c
+++ b/src/type.c
@@ -76,6 +76,16 @@ isTypelistGeneric (const Termlist typelist)
     }
 }
 
+//! Say whether this variable can contain tuples and/or encryptions
+/**
+ * Precondition: tvar should be a variable
+ */
+int
+isOpenVariable (const Term tvar)
+{
+  return isTypelistGeneric (tvar->stype);
+}
+
 //! Check whether a single variable term is instantiated correctly.
 /**
  * Check whether a single variable term is instantiated correctly in this
diff --git a/src/type.h b/src/type.h
index 4a50a7d..e6b56d6 100644
--- a/src/type.h
+++ b/src/type.h
@@ -30,5 +30,6 @@ Termlist typelistConjunct (Termlist typelist1, Termlist Typelist2);
 int checkAllSubstitutions (const System sys);
 int isAgentType (Termlist typelist);
 int goodAgentType (Term agent);
+int isOpenVariable(const Term tvar);
 
 #endif