scyther/src/match_clp.c
ccremers 1bdaf7b5d9 - Large rewrite of switch code. Instead of having switch parameters in
the (monstrously large) system structure, there is now a global
  'switchdata' structure originating in switches.c. This makes it much
  easier to see what's happening.
  * Note: although this code has been tested, there might be some
    hiccups, because doing multiple search&replace actions over all
    files is bound to cause some problems.
2005-06-07 15:02:27 +00:00

532 lines
12 KiB
C

/*!\file match_clp.c
*\brief Implements the match function.
*
* The match function here is integrated here with an enabled() function.
* It is the constraint-logic based match.
*
*\warning Some code is obsolete, as there hasn't been any development on the CL version for a while.
*/
#include <stdlib.h>
#include <stdio.h>
#include "match_clp.h"
#include "system.h"
#include "memory.h"
#include "constraint.h"
#include "mgu.h"
#include "memory.h"
#include "debug.h"
#include "match_clp.h"
#include "modelchecker.h"
#include "switches.h"
struct solvepass
{
int (*solution) ();
System sys;
int run;
int (*proceed) (System, int);
};
int
solve (const struct solvepass sp, Constraintlist solvecons)
{
Constraintlist activecl, cl, beforecl;
Constraint activeco;
int flag;
flag = 0;
/* locate first non-variable constraint */
activecl = firstNonVariable (solvecons);
if (activecl == NULL)
{
/* no such thing, so that's nice */
if (sp.solution != NULL)
sp.solution (sp, solvecons);
return 1;
}
/* there is an active constraint */
/* detach it from the list, but retain */
beforecl = activecl->prev;
solvecons = constraintlistUnlink (activecl);
activeco = activecl->constraint;
if (isTermTuple (activeco->term))
{
/* it's a tuple, so we unfold it first */
Constraintlist oldcl = solvecons;
cl = constraintlistDuplicate (solvecons);
cl =
constraintlistAdd (cl,
makeConstraint (TermOp1 (deVar (activeco->term)),
activeco->know));
cl =
constraintlistAdd (cl,
makeConstraint (TermOp2 (deVar (activeco->term)),
activeco->know));
solvecons = cl;
flag = solve (sp, solvecons) || flag;
constraintlistDestroy (solvecons);
solvecons = oldcl;
if (flag && sp.solution == NULL)
return 1;
}
else
{
/* not a tuple. does it unify? */
//TODO or remove: termNormalize(activeco->term);
void examine (Termlist tl)
{
Termlist tlres, tlscan;
int goodsubst;
while (tl != NULL)
{
//TODO or remove: termNormalize(tl->term);
tlres = termMguTerm (activeco->term, tl->term);
/* check whether this is a valid
* substitution */
goodsubst = 1;
tlscan = tlres;
while (tlscan != NULL && tlres != MGUFAIL)
{
if (validSubst (switches.match, tlscan->term))
{
tlscan = tlscan->next;
}
else
{
goodsubst = 0;
tlscan = NULL;
}
}
if (tlres != MGUFAIL && goodsubst)
{
/* maybe this has modified current and previous knowledge! */
/* modify and copy _all_ knowledge instances, if needed, that is
all constraints as well as all agent knowledge! */
Constraintlist oldcl = NULL;
int copied = 0;
if (tlres != NULL)
{
Constraintlist cl;
copied = 1;
/* sometimes not needed, when no substitutions took place */
oldcl = solvecons;
solvecons = constraintlistDuplicate (solvecons);
cl = solvecons;
while (cl != NULL)
{
cl->constraint->know =
knowledgeSubstDo (cl->constraint->know);
cl = cl->next;
}
}
/* explore this new state */
flag = solve (sp, solvecons) || flag;
/* undo changes */
if (copied)
{
Constraintlist cl;
cl = solvecons;
while (cl != NULL)
{
knowledgeDelete (cl->constraint->know);
cl = cl->next;
}
constraintlistDestroy (solvecons);
solvecons = oldcl;
cl = solvecons;
while (cl != NULL)
{
knowledgeSubstUndo (cl->constraint->know);
cl = cl->next;
}
}
}
else
{
/* unification failed */
}
if (tlres != MGUFAIL)
{
tlscan = tlres;
while (tlscan != NULL)
{
tlscan->term->subst = NULL;
tlscan = tlscan->next;
}
termlistDelete (tlres);
}
/* abort if necessary */
if (flag && sp.solution == NULL)
return;
tl = tl->next;
}
}
examine (activeco->know->basic);
if (flag && sp.solution == NULL)
return 1;
examine (activeco->know->encrypt);
if (flag && sp.solution == NULL)
return 1;
if (isTermEncrypt (activecl->constraint->term))
{
/* shouldn't this be a branch? TODO */
Constraintlist oldcl = solvecons;
cl = constraintlistDuplicate (oldcl);
cl =
constraintlistAdd (cl,
makeConstraint (TermOp (activeco->term),
activeco->know));
cl =
constraintlistAdd (cl,
makeConstraint (TermKey (activeco->term),
activeco->know));
solvecons = cl;
flag = solve (sp, solvecons) || flag;
constraintlistDestroy (solvecons);
solvecons = oldcl;
if (flag && sp.solution == NULL)
return 1;
}
}
/* relink detached link */
if (beforecl == NULL)
{
solvecons = constraintlistConcat (activecl, solvecons);
}
else
{
activecl->prev = beforecl;
activecl->next = beforecl->next;
beforecl->next = activecl;
if (activecl->next != NULL)
activecl->next->prev = activecl;
}
return flag;
}
int
matchRead_clp (const System sys, const int run, int (*proceed) (System, int))
{
Constraintlist oldcl, newcl;
Constraint co;
Roledef runPoint;
int flag;
struct solvepass sp;
/* check solvability */
int solution (const struct solvepass sp, const Constraintlist cl)
{
Knowledge oldknow;
int flag;
int copied;
Constraintlist oldcl;
oldknow = NULL;
flag = 0;
copied = 0;
oldcl = sys->constraints;
sys->constraints = cl;
if (knowledgeSubstNeeded (sys->know))
{
copied = 1;
oldknow = sys->know;
sys->know = knowledgeSubstDo (sys->know);
}
flag = sp.proceed (sys, run);
if (copied)
{
knowledgeDelete (sys->know);
sys->know = oldknow;
knowledgeSubstUndo (sys->know);
}
sys->constraints = oldcl;
return flag;
}
/* save old state */
oldcl = sys->constraints;
newcl = constraintlistShallow (oldcl);
/* creat new state */
runPoint = runPointerGet (sys, run);
/* we know this is a read */
co = makeConstraint (runPoint->message, sys->know);
newcl = constraintlistAdd (newcl, co);
sys->constraints = newcl;
#ifdef DEBUG
if (DEBUGL (5))
{
constraintlistPrint (newcl);
}
#endif
sp.solution = solution;
sp.sys = sys;
sp.run = run;
sp.proceed = proceed;
flag = solve (sp, sys->constraints);
/* restore memory allocation */
constraintDestroy (co);
constraintlistDelete (newcl);
sys->constraints = oldcl;
return flag;
}
int
enabled_clp (const System sys, const int run)
{
return 1;
}
int
block_clp (const System sys, const int run)
{
return 1;
}
int
secret_clp (const System sys, const Term t)
{
Constraintlist oldcl, newcl;
Constraint co;
int flag;
struct solvepass sp;
/* save old state */
oldcl = sys->constraints;
newcl = constraintlistShallow (oldcl);
/* we know this is a read */
co = makeConstraint (t, sys->know);
newcl = constraintlistAdd (newcl, co);
sys->constraints = newcl;
/* check solvability */
sp.solution = NULL;
sp.sys = sys;
flag = !solve (sp, sys->constraints);
/* restore memory allocation */
constraintDestroy (co);
constraintlistDelete (newcl);
sys->constraints = oldcl;
return flag;
}
void
sendAdd_clp (const System sys, const int run, const Termlist tl)
{
Term t;
Termlist tl2;
if (tl == NULL)
{
/* TODO because the constraints might have changed, we can try to solve them again... */
explorify (sys, run);
return;
}
t = deVar (tl->term);
if (realTermLeaf (t))
{
/* leaf: simply add it */
knowledgeAddTerm (sys->know, t);
sendAdd_clp (sys, run, tl->next);
return;
}
else
{
/* node */
if (realTermTuple (t))
{
/* tuple */
tl2 = termlistShallow (tl->next);
tl2 = termlistAdd (tl2, TermOp1 (t));
tl2 = termlistAdd (tl2, TermOp2 (t));
sendAdd_clp (sys, run, tl2);
termlistDelete (tl2);
}
else
{
/* encrypt */
Term invkey;
invkey = inverseKey (sys->know->inverses, TermKey (t));
if (!hasTermVariable (invkey))
{
/* simple case: no variable inside */
knowledgeAddTerm (sys->know, t);
tl2 = termlistShallow (tl->next);
if (inKnowledge (sys->know, invkey)
&& hasTermVariable (TermOp (t)))
tl2 = termlistAdd (tl2, TermOp (t));
sendAdd_clp (sys, run, tl2);
termlistDelete (tl2);
}
else
{
/* difficult case: variable in inverse
* key. We have to branch. */
Knowledge oldknow;
Constraint co;
Constraintlist clold, clbuf;
/* branch 1 : invkey not in knowledge */
/* TODO this yields a negative constraint, which we omit for the time being */
oldknow = knowledgeDuplicate (sys->know);
knowledgeAddTerm (sys->know, t);
sendAdd_clp (sys, run, tl->next);
knowledgeDelete (sys->know);
sys->know = oldknow;
/* branch 2 : invkey in knowledge */
oldknow = knowledgeDuplicate (sys->know);
clold = sys->constraints;
clbuf = constraintlistShallow (clold);
tl2 = termlistShallow (tl->next);
co = makeConstraint (invkey, sys->know);
sys->constraints = constraintlistAdd (clbuf, co);
/* we _could_ explore first if this is solveable */
knowledgeAddTerm (sys->know, t);
tl2 = termlistAdd (tl2, TermOp (t));
sendAdd_clp (sys, run, tl2);
termlistDelete (tl2);
constraintDestroy (co);
constraintlistDelete (clbuf);
sys->constraints = clold;
knowledgeDelete (sys->know);
sys->know = oldknow;
}
}
}
}
int
send_clp (const System sys, const int run)
{
Roledef rd = runPointerGet (sys, run);
/* execute send, push knowledge? */
if (inKnowledge (sys->know, rd->message))
{
/* no new knowledge, so this remains */
explorify (sys, run);
}
else
{
/* new knowledge, must store old state */
Knowledge oldknow;
Termlist tl;
oldknow = sys->know;
sys->know = knowledgeDuplicate (sys->know);
tl = termlistAdd (NULL, rd->message);
sendAdd_clp (sys, run, tl);
termlistDelete (tl);
knowledgeDelete (sys->know);
sys->know = oldknow;
}
return 1;
}
int
isPossible_clp (const System sys, const int run, int
(*proceed) (System, int), const Term t, const Knowledge k)
{
Constraintlist oldcl, newcl;
Constraint co;
Roledef runPoint;
int flag;
struct solvepass sp;
/* check solvability */
int solution (const struct solvepass sp, const Constraintlist cl)
{
Knowledge oldknow;
Constraintlist oldcl;
int flag;
int copied;
oldknow = NULL;
oldcl = sys->constraints;
flag = 0;
copied = 0;
sys->constraints = cl;
if (knowledgeSubstNeeded (sys->know))
{
copied = 1;
oldknow = sys->know;
sys->know = knowledgeSubstDo (sys->know);
}
flag = sp.proceed (sys, run);
if (copied)
{
knowledgeDelete (sys->know);
sys->know = oldknow;
knowledgeSubstUndo (sys->know);
}
sys->constraints = oldcl;
return flag;
}
/* save old state */
oldcl = sys->constraints;
newcl = constraintlistShallow (oldcl);
/* creat new state */
runPoint = runPointerGet (sys, run);
/* add the new constraint */
co = makeConstraint (t, k);
newcl = constraintlistAdd (newcl, co);
sys->constraints = newcl;
sp.solution = solution;
sp.sys = sys;
sp.run = run;
sp.proceed = proceed;
flag = solve (sp, sys->constraints);
/* restore memory allocation */
constraintDestroy (co);
constraintlistDelete (newcl);
sys->constraints = oldcl;
return flag;
}