- Added functions to globally check variable substitution consistency.
This commit is contained in:
parent
2452a34671
commit
2e495099bb
315
src/type.c
315
src/type.c
@ -14,6 +14,7 @@
|
||||
#include "specialterm.h"
|
||||
|
||||
extern Protocol INTRUDER;
|
||||
extern Termlist TERMLISTERROR;
|
||||
|
||||
//! Report a bad substitution, if needed
|
||||
void
|
||||
@ -42,6 +43,44 @@ reportBadSubst (const Term tvar, const Term tsubst)
|
||||
#endif
|
||||
}
|
||||
|
||||
//! Say whether a typelist is 'generic' or should be taken per item.
|
||||
int
|
||||
isTypelistGeneric (const Termlist typelist)
|
||||
{
|
||||
if (typelist == NULL)
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
return inTermlist (typelist, TERM_Ticket);
|
||||
}
|
||||
}
|
||||
|
||||
//! Check whether a single type constant matches a typelist
|
||||
/**
|
||||
* Understands semantics of NULL and TERM_Ticket
|
||||
*/
|
||||
int
|
||||
matchSingleType (Termlist typelist, Term type)
|
||||
{
|
||||
if (typelist == TERMLISTERROR)
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (isTypelistGeneric (typelist))
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
return inTermlist (typelist, type);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//! Check whether a single variable term is instantiated correctly.
|
||||
/**
|
||||
* Check whether a single variable term is instantiated correctly in this
|
||||
@ -59,11 +98,7 @@ checkTypeTerm (const int mgumode, const Term tvar)
|
||||
// Non-instantiated terms are fine.
|
||||
if (tvar->subst != NULL)
|
||||
{
|
||||
// NULL type is always fine
|
||||
if (tvar->stype != NULL)
|
||||
{
|
||||
// Tickets are always fine too
|
||||
if (!inTermlist (tvar->stype, TERM_Ticket))
|
||||
if (!isTypelistGeneric (tvar->stype))
|
||||
{
|
||||
// So there is a specific (non-ticket) type, and the var is instantiated, match mode 0 or 1
|
||||
// Is it really a leaf?
|
||||
@ -103,7 +138,6 @@ checkTypeTerm (const int mgumode, const Term tvar)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
@ -141,3 +175,272 @@ checkTypeLocals (const System sys)
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
//! Check whether a typelist is a strict agent type list
|
||||
int
|
||||
isAgentType (Termlist typelist)
|
||||
{
|
||||
return (termlistLength (typelist) == 1 &&
|
||||
inTermlist (typelist, TERM_Agent));
|
||||
}
|
||||
|
||||
//! Helper function to determine whether a list is compatible with an agent var.
|
||||
int
|
||||
agentCompatible (Termlist tl)
|
||||
{
|
||||
if (isTypelistGeneric (tl))
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
return inTermlist (tl, TERM_Agent);
|
||||
}
|
||||
}
|
||||
|
||||
//! Check whether two type lists are compatible for variables
|
||||
/**
|
||||
* Depends on some input:
|
||||
*
|
||||
* mgumode type of matching
|
||||
* agentcheck true if agent type is always restrictive
|
||||
*
|
||||
* returns the new type list (needs to be deleted!) or TERMLISTERROR (should
|
||||
* not be deleted!)
|
||||
*/
|
||||
Termlist
|
||||
typelistConjunct (Termlist typelist1, Termlist typelist2, const int mgumode,
|
||||
const int agentcheck)
|
||||
{
|
||||
if (typelist1 != TERMLISTERROR && typelist2 != TERMLISTERROR)
|
||||
{
|
||||
|
||||
/* In the restricted agent case, we check whether agent list occurs in
|
||||
* either set. If so, the result can only be an agent-restrictive list.
|
||||
*/
|
||||
|
||||
if (agentcheck)
|
||||
{
|
||||
if (isAgentType (typelist1) || isAgentType (typelist2))
|
||||
{
|
||||
/* Now, the result must surely accept agents. Thus, it must be
|
||||
* NULL or accept agents.
|
||||
*/
|
||||
|
||||
if (!
|
||||
(agentCompatible (typelist1)
|
||||
&& agentCompatible (typelist2)))
|
||||
{
|
||||
// Not good: one of them cannot
|
||||
return TERMLISTERROR;
|
||||
}
|
||||
else
|
||||
{
|
||||
// Good: but because an agent is involved, the type reduces to the simple Agent type only.
|
||||
return termlistAdd (NULL, TERM_Agent);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
/* Not the simple agent variable case. Now other things come in to play.
|
||||
*/
|
||||
if (mgumode == 0)
|
||||
{
|
||||
/*
|
||||
* Strict match: (-m0) conjunct of the types must be non-empty.
|
||||
*/
|
||||
|
||||
// Generic exceptions
|
||||
if (isTypelistGeneric (typelist1))
|
||||
{
|
||||
// Copy for later deletion
|
||||
return termlistShallow (typelist2);
|
||||
}
|
||||
else
|
||||
{
|
||||
if (isTypelistGeneric (typelist2))
|
||||
{
|
||||
// Copy for later deletion
|
||||
return termlistShallow (typelist1);
|
||||
}
|
||||
else
|
||||
{
|
||||
/* Apparently neither is generic, and we can take the real conjunct.
|
||||
* However, this conjunct must not be empty (because that implies that the types cannot match).
|
||||
*/
|
||||
Termlist conjunct;
|
||||
|
||||
conjunct = termlistConjunct (typelist1, typelist2);
|
||||
if (conjunct == NULL)
|
||||
{
|
||||
// Empty, and thus the variables cannot be instantiated without causing a type flaw.
|
||||
return TERMLISTERROR;
|
||||
}
|
||||
else
|
||||
{
|
||||
// Non-empty, which is good in this case.
|
||||
return conjunct;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
/*
|
||||
* Not so strict: (-m1 or -m2)
|
||||
*
|
||||
* Because the variable is not bound, there is certainly no
|
||||
* binding yet to tuples or crypted terms, and thus any
|
||||
* typing will do.
|
||||
*/
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return TERMLISTERROR;
|
||||
}
|
||||
|
||||
//! Check a single ground variable
|
||||
/**
|
||||
* Check whether all variables that map to this one have a possible valid substitution
|
||||
*/
|
||||
int
|
||||
checkGroundVariable (const System sys, const Term groundvar)
|
||||
{
|
||||
int allvalid;
|
||||
|
||||
allvalid = 1;
|
||||
if (realTermVariable (groundvar))
|
||||
{
|
||||
Termlist tl;
|
||||
Termlist typelist;
|
||||
|
||||
// Check
|
||||
typelist = termlistShallow (groundvar->stype);
|
||||
tl = sys->variables;
|
||||
while (allvalid == 1 && tl != NULL)
|
||||
{
|
||||
Term term;
|
||||
|
||||
term = tl->term;
|
||||
|
||||
// Not actually the same, of course
|
||||
if (term != groundvar)
|
||||
{
|
||||
// Does this term map to the same variable?
|
||||
if (isTermEqual (term, groundvar))
|
||||
{
|
||||
Termlist tlprev;
|
||||
|
||||
// Maps to same ground term
|
||||
// Take conjunct
|
||||
tlprev = typelist;
|
||||
typelist =
|
||||
typelistConjunct (tlprev, term->stype, switches.match,
|
||||
switches.agentTypecheck);
|
||||
termlistDelete (tlprev);
|
||||
|
||||
if (typelist == TERMLISTERROR)
|
||||
{
|
||||
// And this is not valid...
|
||||
allvalid = 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
tl = tl->next;
|
||||
}
|
||||
if (typelist != TERMLISTERROR)
|
||||
{
|
||||
termlistDelete (typelist);
|
||||
}
|
||||
}
|
||||
return allvalid;
|
||||
}
|
||||
|
||||
|
||||
//! Global check of the system, for all variables.
|
||||
/**
|
||||
* Returns true if all variables are okay.
|
||||
*
|
||||
* This version checks all substitutions, and thus takes over all the functions
|
||||
* that are now in mgu.c. However, we have left them in for speed purposes,
|
||||
* because pruning early is good.
|
||||
*/
|
||||
int
|
||||
checkAllSubstitutions (const System sys)
|
||||
{
|
||||
int allvalid;
|
||||
Termlist groundvars;
|
||||
Termlist tl;
|
||||
|
||||
/* We scan all unbound variables for so called 'ground variables', which are
|
||||
* the root of a substitution tree. Such variables are checked for
|
||||
* satisfyability, i.e. the conjunction of their type lists must not be
|
||||
* empty.
|
||||
*
|
||||
* At the same time, we check also bound variables for their mappings.
|
||||
*/
|
||||
groundvars = NULL;
|
||||
allvalid = 1;
|
||||
tl = sys->variables;
|
||||
while ((allvalid == 1) && (tl != NULL))
|
||||
{
|
||||
Term tvar;
|
||||
|
||||
tvar = tl->term;
|
||||
if (realTermVariable (tvar))
|
||||
{
|
||||
Term tsubst;
|
||||
|
||||
tsubst = deVar (tvar);
|
||||
|
||||
if (tvar != tsubst)
|
||||
{
|
||||
// Substitution going on, check
|
||||
|
||||
if (realTermVariable (tsubst))
|
||||
{
|
||||
/* Variable -> Variable (unbound)
|
||||
*
|
||||
* Check whether we already scanned for this one, because we
|
||||
* don't want to scan for this ground variable more than once.
|
||||
*/
|
||||
if (!inTermlist (groundvars, tsubst))
|
||||
{
|
||||
/* Not done before, add now.
|
||||
*/
|
||||
groundvars = termlistAdd (groundvars, tsubst);
|
||||
|
||||
/* Check whether there exists a valid substitution for
|
||||
* everything mapping to this ground variable.
|
||||
*/
|
||||
allvalid = allvalid
|
||||
&& checkGroundVariable (sys, tsubst);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
/* Variable -> term (bound)
|
||||
*/
|
||||
|
||||
if (switches.agentTypecheck && isAgentType (tvar->stype))
|
||||
{
|
||||
// *Must* include agent type, regardless of match
|
||||
allvalid = allvalid && agentCompatible (tsubst->stype);
|
||||
}
|
||||
else
|
||||
{
|
||||
// Consider match
|
||||
allvalid = allvalid
|
||||
&& checkTypeTerm (switches.match, tvar);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
tl = tl->next;
|
||||
}
|
||||
|
||||
termlistDelete (groundvars);
|
||||
return allvalid;
|
||||
}
|
||||
|
@ -7,5 +7,8 @@
|
||||
int checkTypeTerm (const int mgumode, const Term t);
|
||||
int checkTypeTermlist (const int mgumode, Termlist tl);
|
||||
int checkTypeLocals (const System sys);
|
||||
Termlist typelistConjunct (Termlist typelist1, Termlist Typelist2);
|
||||
int checkAllSubstitutions (const System sys);
|
||||
int isAgentType (Termlist typelist);
|
||||
|
||||
#endif
|
||||
|
Loading…
Reference in New Issue
Block a user