andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Added some useful macros to term.h to address subparts (e.g.

Browse Source 
TermOp1(t)). Renamed all uses.
This commit is contained in:
ccremers 2004-11-16 12:06:36 +00:00
parent 343314896b
commit a38925c9c2
15 changed files with 235 additions and 225 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/arachne.c
View File

@ -200,9 +200,9 @@ getTermFunction (Term t)
t = deVar (t); t = deVar (t);
if (t != NULL) if (t != NULL)
{ {
if (realTermEncrypt (t) && isTermFunctionName (t->right.key)) if (realTermEncrypt (t) && isTermFunctionName (TermKey(t)))
{ {
return t->right.key; return TermKey(t);
} }
} }
return NULL; return NULL;
@ -304,7 +304,7 @@ determine_unification_run (Termlist tl)
while (tl != NULL) while (tl != NULL)
{ {
//! Again, hardcoded reference to compiler.c. Level -3 means a local constant for a role. //! Again, hardcoded reference to compiler.c. Level -3 means a local constant for a role.
if (tl->term->type != VARIABLE && tl->term->right.runid == -3) if (tl->term->type != VARIABLE && TermRunid(tl->term) == -3)
{ {
Term t; Term t;
@ -320,12 +320,12 @@ determine_unification_run (Termlist tl)
if (run == -2) if (run == -2)
{ {
// Any run // Any run
run = t->right.runid; run = TermRunid(t);
} }
else else
{ {
// Specific run: compare // Specific run: compare
if (run != t->right.runid) if (run != TermRunid(t))
{ {
return -1; return -1;
} }
@ -553,7 +553,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
if (realTermEncrypt (tl->term)) if (realTermEncrypt (tl->term))
{ {
/* the key is a construction itself */ /* the key is a construction itself */
if (inKnowledge (sys->know, tl->term->right.key)) if (inKnowledge (sys->know, TermKey(tl->term)))
{ {
/* the key is constructed by a public thing */ /* the key is constructed by a public thing */
/* typically, this is a public key, so we postpone it */ /* typically, this is a public key, so we postpone it */
@ -1361,8 +1361,8 @@ bind_goal_new_encrypt (const Binding b)
} }
// must be encryption // must be encryption
t1 = term->left.op; t1 = TermOp(term);
t2 = term->right.key; t2 = TermKey(term);
if (t2 != TERM_Hidden) if (t2 != TERM_Hidden)
{ {

4
src/binding.c
View File

@ -177,7 +177,7 @@ goal_graph_create ()
Term t; Term t;
t = tl->term; t = tl->term;
if (t->type == VARIABLE && t->right.runid == run if (t->type == VARIABLE && TermRunid(t) == run
&& t->subst != NULL) && t->subst != NULL)
{ {
// t is a variable of run // t is a variable of run
@ -190,7 +190,7 @@ goal_graph_create ()
t2 = tl2->term; t2 = tl2->term;
if (realTermLeaf (t2) && t2->type != VARIABLE if (realTermLeaf (t2) && t2->type != VARIABLE
&& t2->right.runid == run2) && TermRunid(t2) == run2)
{ {
// t2 is a constant of run2 // t2 is a constant of run2
if (isTermEqual (t, t2)) if (isTermEqual (t, t2))

8
src/compiler.c
View File

@ -241,7 +241,7 @@ levelFind (Symbol s, int level)
{ {
if (isTermLeaf (tl->term)) if (isTermLeaf (tl->term))
{ {
if (tl->term->left.symb == s) if (TermSymb(tl->term) == s)
{ {
return tl->term; return tl->term;
} }
@ -505,7 +505,7 @@ commEvent (int event, Tac tc)
else else
{ {
/* n parameters */ /* n parameters */
msg = deVar (claimbig)->right.op2; msg = TermOp2(deVar (claimbig));
if (tupleCount (msg) != n) if (tupleCount (msg) != n)
{ {
error ("Problem with claim tuple unfolding at line %i.", error ("Problem with claim tuple unfolding at line %i.",
@ -690,7 +690,7 @@ runInstanceCreate (Tac tc)
/* first, locate the protocol */ /* first, locate the protocol */
psym = tc->t1.tac->t1.sym; psym = tc->t1.tac->t1.sym;
p = sys->protocols; p = sys->protocols;
while (p != NULL && p->nameterm->left.symb != psym) while (p != NULL && TermSymb(p->nameterm) != psym)
p = p->next; p = p->next;
if (p == NULL) if (p == NULL)
{ {
@ -703,7 +703,7 @@ runInstanceCreate (Tac tc)
/* locate the role */ /* locate the role */
rsym = tc->t1.tac->t2.sym; rsym = tc->t1.tac->t2.sym;
r = p->roles; r = p->roles;
while (r != NULL && r->nameterm->left.symb != rsym) while (r != NULL && TermSymb(r->nameterm) != rsym)
r = r->next; r = r->next;
if (r == NULL) if (r == NULL)
{ {

22
src/knowledge.c
View File

@ -154,8 +154,8 @@ knowledgeAddTerm (Knowledge know, Term term)
{ {
int status; int status;
status = knowledgeAddTerm (know, term->left.op1); status = knowledgeAddTerm (know, TermOp1(term));
return knowledgeAddTerm (know, term->right.op2) || status; return knowledgeAddTerm (know, TermOp2(term)) || status;
} }
/* test whether we knew it before */ /* test whether we knew it before */
@ -172,12 +172,12 @@ knowledgeAddTerm (Knowledge know, Term term)
} }
if (term->type == ENCRYPT) if (term->type == ENCRYPT)
{ {
Term invkey = inverseKey (know->inverses, term->right.key); Term invkey = inverseKey (know->inverses, TermKey(term));
if (inKnowledge (know, invkey)) if (inKnowledge (know, invkey))
{ {
/* we can decrypt it */ /* we can decrypt it */
knowledgeAddTerm (know, term->left.op); knowledgeAddTerm (know, TermOp(term));
if (!inKnowledge (know, term->right.key)) if (!inKnowledge (know, TermKey(term)))
{ {
/* we know the op now, but not the key, so add it anyway */ /* we know the op now, but not the key, so add it anyway */
know->encrypt = termlistAdd (know->encrypt, term); know->encrypt = termlistAdd (know->encrypt, term);
@ -208,9 +208,9 @@ knowledgeSimplify (Knowledge know, Term key)
while (scan != NULL) while (scan != NULL)
{ {
if (isTermEqual ((scan->term)->right.key, invkey)) if (isTermEqual (TermKey(scan->term), invkey))
{ {
tldecrypts = termlistAdd (tldecrypts, (scan->term)->left.op); tldecrypts = termlistAdd (tldecrypts, TermOp(scan->term));
know->encrypt = termlistDelTerm (scan); know->encrypt = termlistDelTerm (scan);
scan = know->encrypt; scan = know->encrypt;
} }
@ -285,14 +285,14 @@ inKnowledge (const Knowledge know, Term term)
if (term->type == ENCRYPT) if (term->type == ENCRYPT)
{ {
return inTermlist (know->encrypt, term) || return inTermlist (know->encrypt, term) ||
(inKnowledge (know, term->right.key) (inKnowledge (know, TermKey(term))
&& inKnowledge (know, term->left.op)); && inKnowledge (know, TermOp(term)));
} }
if (term->type == TUPLE) if (term->type == TUPLE)
{ {
return (inTermlist (know->encrypt, term) || return (inTermlist (know->encrypt, term) ||
(inKnowledge (know, term->left.op1) && (inKnowledge (know, TermOp1(term)) &&
inKnowledge (know, term->right.op2))); inKnowledge (know, TermOp2(term))));
} }
return 0; /* unrecognized term type, weird */ return 0; /* unrecognized term type, weird */
} }

24
src/latex.c
View File

@ -117,12 +117,12 @@ latexTermPrint (Term term, Termlist highlight)
{ {
if (inTermlist (highlight, term)) if (inTermlist (highlight, term))
printf ("\\mathbf{"); printf ("\\mathbf{");
symbolPrint (term->left.symb); symbolPrint (TermSymb(term));
if (realTermVariable (term)) if (realTermVariable (term))
printf ("V"); printf ("V");
if (term->right.runid >= 0) if (TermRunid(term) >= 0)
{ {
printf ("\\sharp%i", term->right.runid); printf ("\\sharp%i", TermRunid(term));
} }
if (term->subst != NULL) if (term->subst != NULL)
{ {
@ -141,22 +141,22 @@ latexTermPrint (Term term, Termlist highlight)
} }
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
if (isTermLeaf (term->right.key) if (isTermLeaf (TermKey(term))
&& inTermlist (term->right.key->stype, TERM_Function)) && inTermlist (TermKey(term)->stype, TERM_Function))
{ {
/* function application */ /* function application */
latexTermPrint (term->right.key, highlight); latexTermPrint (TermKey(term), highlight);
printf ("("); printf ("(");
latexTermTuplePrint (term->left.op, highlight); latexTermTuplePrint (TermOp(term), highlight);
printf (")"); printf (")");
} }
else else
{ {
/* normal encryption */ /* normal encryption */
printf ("\\{"); printf ("\\{");
latexTermTuplePrint (term->left.op, highlight); latexTermTuplePrint (TermOp(term), highlight);
printf ("\\}_{"); printf ("\\}_{");
latexTermPrint (term->right.key, highlight); latexTermPrint (TermKey(term), highlight);
printf ("}"); printf ("}");
} }
} }
@ -180,9 +180,9 @@ latexTermTuplePrint (Term term, Termlist hl)
while (realTermTuple (term)) while (realTermTuple (term))
{ {
// To remove any brackets, change this into latexTermTuplePrint. // To remove any brackets, change this into latexTermTuplePrint.
latexTermPrint (term->left.op1, hl); latexTermPrint (TermOp1(term), hl);
printf (","); printf (",");
term = deVar (term->right.op2); term = deVar (TermOp2(term));
} }
latexTermPrint (term, hl); latexTermPrint (term, hl);
return; return;
@ -966,7 +966,7 @@ attackDisplayLatex (const System sys)
{ {
/* detect whether it's really local to this run */ /* detect whether it's really local to this run */
Term t = deVar (tl->term); Term t = deVar (tl->term);
if (isTermLeaf (t) && t->right.runid == i) if (isTermLeaf (t) && TermRunid(t) == i)
{ {
if (first) if (first)
{ {

4
src/main.c
View File

@ -772,14 +772,14 @@ timersPrint (const System sys)
{ {
/* modern version: claim label is tuple (protocname, label) */ /* modern version: claim label is tuple (protocname, label) */
/* first print protocol.role */ /* first print protocol.role */
termPrint (cl_scan->label->left.op1); termPrint (TermOp1(cl_scan->label));
eprintf ("\t"); eprintf ("\t");
termPrint (cl_scan->rolename); termPrint (cl_scan->rolename);
eprintf ("\t"); eprintf ("\t");
/* second print event_label */ /* second print event_label */
termPrint (cl_scan->type); termPrint (cl_scan->type);
eprintf ("_"); eprintf ("_");
termPrint (cl_scan->label->right.op2); termPrint (TermOp2(cl_scan->label));
eprintf ("\t"); eprintf ("\t");
} }
else else

20
src/match_clp.c
View File

@ -60,11 +60,11 @@ solve (const struct solvepass sp, Constraintlist solvecons)
cl = constraintlistDuplicate (solvecons); cl = constraintlistDuplicate (solvecons);
cl = cl =
constraintlistAdd (cl, constraintlistAdd (cl,
makeConstraint (deVar (activeco->term)->left.op1, makeConstraint (TermOp1(deVar (activeco->term)),
activeco->know)); activeco->know));
cl = cl =
constraintlistAdd (cl, constraintlistAdd (cl,
makeConstraint (deVar (activeco->term)->right.op2, makeConstraint (TermOp2(deVar (activeco->term)),
activeco->know)); activeco->know));
solvecons = cl; solvecons = cl;
flag = solve (sp, solvecons) || flag; flag = solve (sp, solvecons) || flag;
@ -192,11 +192,11 @@ solve (const struct solvepass sp, Constraintlist solvecons)
cl = constraintlistDuplicate (oldcl); cl = constraintlistDuplicate (oldcl);
cl = cl =
constraintlistAdd (cl, constraintlistAdd (cl,
makeConstraint (activeco->term->left.op, makeConstraint (TermOp(activeco->term),
activeco->know)); activeco->know));
cl = cl =
constraintlistAdd (cl, constraintlistAdd (cl,
makeConstraint (activeco->term->right.key, makeConstraint (TermKey(activeco->term),
activeco->know)); activeco->know));
solvecons = cl; solvecons = cl;
flag = solve (sp, solvecons) || flag; flag = solve (sp, solvecons) || flag;
@ -368,8 +368,8 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
{ {
/* tuple */ /* tuple */
tl2 = termlistShallow (tl->next); tl2 = termlistShallow (tl->next);
tl2 = termlistAdd (tl2, t->left.op1); tl2 = termlistAdd (tl2, TermOp1(t));
tl2 = termlistAdd (tl2, t->right.op2); tl2 = termlistAdd (tl2, TermOp2(t));
sendAdd_clp (sys, run, tl2); sendAdd_clp (sys, run, tl2);
termlistDelete (tl2); termlistDelete (tl2);
} }
@ -378,15 +378,15 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
/* encrypt */ /* encrypt */
Term invkey; Term invkey;
invkey = inverseKey (sys->know->inverses, t->right.key); invkey = inverseKey (sys->know->inverses, TermKey(t));
if (!hasTermVariable (invkey)) if (!hasTermVariable (invkey))
{ {
/* simple case: no variable inside */ /* simple case: no variable inside */
knowledgeAddTerm (sys->know, t); knowledgeAddTerm (sys->know, t);
tl2 = termlistShallow (tl->next); tl2 = termlistShallow (tl->next);
if (inKnowledge (sys->know, invkey) if (inKnowledge (sys->know, invkey)
&& hasTermVariable (t->left.op)) && hasTermVariable (TermOp(t)))
tl2 = termlistAdd (tl2, t->left.op); tl2 = termlistAdd (tl2, TermOp(t));
sendAdd_clp (sys, run, tl2); sendAdd_clp (sys, run, tl2);
termlistDelete (tl2); termlistDelete (tl2);
} }
@ -418,7 +418,7 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
sys->constraints = constraintlistAdd (clbuf, co); sys->constraints = constraintlistAdd (clbuf, co);
/* we _could_ explore first if this is solveable */ /* we _could_ explore first if this is solveable */
knowledgeAddTerm (sys->know, t); knowledgeAddTerm (sys->know, t);
tl2 = termlistAdd (tl2, t->left.op); tl2 = termlistAdd (tl2, TermOp(t));
sendAdd_clp (sys, run, tl2); sendAdd_clp (sys, run, tl2);
termlistDelete (tl2); termlistDelete (tl2);

20
src/mgu.c
View File

@ -183,14 +183,14 @@ termMguTerm (Term t1, Term t2)
{ {
Termlist tl1, tl2; Termlist tl1, tl2;
tl1 = termMguTerm (t1->right.key, t2->right.key); tl1 = termMguTerm (TermKey(t1), TermKey(t2));
if (tl1 == MGUFAIL) if (tl1 == MGUFAIL)
{ {
return MGUFAIL; return MGUFAIL;
} }
else else
{ {
tl2 = termMguTerm (t1->left.op, t2->left.op); tl2 = termMguTerm (TermOp(t1), TermOp(t2));
if (tl2 == MGUFAIL) if (tl2 == MGUFAIL)
{ {
termlistSubstReset (tl1); termlistSubstReset (tl1);
@ -210,14 +210,14 @@ termMguTerm (Term t1, Term t2)
{ {
Termlist tl1, tl2; Termlist tl1, tl2;
tl1 = termMguTerm (t1->left.op1, t2->left.op1); tl1 = termMguTerm (TermOp1(t1), TermOp1(t2));
if (tl1 == MGUFAIL) if (tl1 == MGUFAIL)
{ {
return MGUFAIL; return MGUFAIL;
} }
else else
{ {
tl2 = termMguTerm (t1->right.op2, t2->right.op2); tl2 = termMguTerm (TermOp2(t1), TermOp2(t2));
if (tl2 == MGUFAIL) if (tl2 == MGUFAIL)
{ {
termlistSubstReset (tl1); termlistSubstReset (tl1);
@ -251,8 +251,8 @@ termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist))
if (realTermTuple (t2)) if (realTermTuple (t2))
{ {
// t2 is a tuple, consider interm options as well. // t2 is a tuple, consider interm options as well.
flag = flag && termMguInTerm (t1, t2->left.op1, iterator); flag = flag && termMguInTerm (t1, TermOp1(t2), iterator);
flag = flag && termMguInTerm (t1, t2->right.op2, iterator); flag = flag && termMguInTerm (t1, TermOp2(t2), iterator);
} }
// simple clause or combined // simple clause or combined
tl = termMguTerm (t1, t2); tl = termMguTerm (t1, t2);
@ -300,10 +300,10 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
{ {
// 'simple' tuple // 'simple' tuple
flag = flag =
flag && termMguSubTerm (t1, t2->left.op1, iterator, inverses, flag && termMguSubTerm (t1, TermOp1(t2), iterator, inverses,
keylist); keylist);
flag = flag =
flag && termMguSubTerm (t1, t2->right.op2, iterator, inverses, flag && termMguSubTerm (t1, TermOp2(t2), iterator, inverses,
keylist); keylist);
} }
else else
@ -312,7 +312,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
// So, we need the key, and try to get the rest // So, we need the key, and try to get the rest
Term newkey; Term newkey;
newkey = inverseKey (inverses, t2->right.key); newkey = inverseKey (inverses, TermKey(t2));
// We can never produce the TERM_Hidden key, thus, this is not a valid iteration. // We can never produce the TERM_Hidden key, thus, this is not a valid iteration.
if (!isTermEqual (newkey, TERM_Hidden)) if (!isTermEqual (newkey, TERM_Hidden))
{ {
@ -323,7 +323,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
// Recurse // Recurse
flag = flag =
flag && termMguSubTerm (t1, t2->left.op, iterator, inverses, flag && termMguSubTerm (t1, TermOp(t2), iterator, inverses,
keylist_new); keylist_new);
termlistDelete (keylist_new); termlistDelete (keylist_new);

6
src/modelchecker.c
View File

@ -1147,7 +1147,7 @@ claimSecrecy (const System sys, const Term t)
{ {
t = deVar (t); t = deVar (t);
if (isTermTuple (t)) if (isTermTuple (t))
return csScan (t->left.op1) && csScan (t->right.op2); return csScan (TermOp1(t)) && csScan (TermOp2(t));
else else
return isTermSecret (sys, t); return isTermSecret (sys, t);
} }
@ -1171,8 +1171,8 @@ secrecyUnfolding (Term t, const Knowledge know)
{ {
t = deVar (t); t = deVar (t);
if (isTermTuple (t)) if (isTermTuple (t))
return termlistConcat (secrecyUnfolding (t->left.op1, know), return termlistConcat (secrecyUnfolding (TermOp1(t), know),
secrecyUnfolding (t->right.op2, know)); secrecyUnfolding (TermOp2(t), know));
else else
{ {
if (inKnowledge (know, t)) if (inKnowledge (know, t))

2
src/role.c
View File

@ -61,7 +61,7 @@ roledefPrintGeneric (Roledef rd, int print_actor)
if (protocolCount < 2 && realTermTuple (label)) if (protocolCount < 2 && realTermTuple (label))
{ {
// Only one protocol, so we don't need to show the extra label info // Only one protocol, so we don't need to show the extra label info
label = label->right.op2; label = TermOp2(label);
} }
//! Print latex/normal //! Print latex/normal

8
src/substitution.c
View File

@ -64,14 +64,14 @@ termSubstitute (Term term, Substitution subs)
{ {
if (isTermEncrypt (term)) if (isTermEncrypt (term))
{ {
return makeTermEncrypt (termSubstitute (term->left.op, subs), return makeTermEncrypt (termSubstitute (TermOp(term), subs),
termSubstitute (term->right.key, subs)); termSubstitute (TermKey(term), subs));
} }
else else
{ {
return return
makeTermTuple (termSubstitute (term->left.op1, subs), makeTermTuple (termSubstitute (TermOp1(term), subs),
termSubstitute (term->right.op2, subs)); termSubstitute (TermOp2(term), subs));
} }
} }
else else

6
src/system.c
View File

@ -563,7 +563,7 @@ create_new_local (const Term t, const int rid)
{ {
Term newt; Term newt;
newt = makeTermType (t->type, t->left.symb, rid); newt = makeTermType (t->type, TermSymb(t), rid);
newt->stype = t->stype; newt->stype = t->stype;
return newt; return newt;
@ -667,7 +667,7 @@ roleInstanceArachne (const System sys, const Protocol protocol,
if (realTermVariable (newt)) if (realTermVariable (newt))
{ {
// Make new var for this run // Make new var for this run
newt = makeTermType (VARIABLE, newt->left.symb, rid); newt = makeTermType (VARIABLE, TermSymb(newt), rid);
artefacts = termlistAdd (artefacts, newt); artefacts = termlistAdd (artefacts, newt);
newt->stype = oldt->stype; newt->stype = oldt->stype;
// Copy substitution // Copy substitution
@ -808,7 +808,7 @@ roleInstanceModelchecker (const System sys, const Protocol protocol,
/* There is a TYPE constant in the parameter list. /* There is a TYPE constant in the parameter list.
* Generate a new local variable for this run, with this type */ * Generate a new local variable for this run, with this type */
newvar = makeTermType (VARIABLE, scanfrom->term->left.symb, rid); newvar = makeTermType (VARIABLE, TermSymb(scanfrom->term), rid);
artefacts = termlistAdd (artefacts, newvar); artefacts = termlistAdd (artefacts, newvar);
sys->variables = termlistAdd (sys->variables, newvar); sys->variables = termlistAdd (sys->variables, newvar);
newvar->stype = termlistAdd (NULL, scanto->term); newvar->stype = termlistAdd (NULL, scanto->term);

242
src/term.c
View File

@ -75,8 +75,8 @@ makeTermEncrypt (Term t1, Term t2)
Term term = makeTerm (); Term term = makeTerm ();
term->type = ENCRYPT; term->type = ENCRYPT;
term->stype = NULL; term->stype = NULL;
term->left.op = t1; TermOp(term) = t1;
term->right.key = t2; TermKey(term) = t2;
return term; return term;
} }
@ -111,8 +111,8 @@ makeTermTuple (Term t1, Term t2)
tt = makeTerm (); tt = makeTerm ();
tt->type = TUPLE; tt->type = TUPLE;
tt->stype = NULL; tt->stype = NULL;
tt->left.op1 = t1; TermOp1(tt) = t1;
tt->right.op2 = t2; TermOp2(tt) = t2;
return tt; return tt;
} }
@ -128,8 +128,8 @@ makeTermType (const int type, const Symbol symb, const int runid)
term->type = type; term->type = type;
term->stype = NULL; term->stype = NULL;
term->subst = NULL; term->subst = NULL;
term->left.symb = symb; TermSymb(term) = symb;
term->right.runid = runid; TermRunid(term) = runid;
return term; return term;
} }
@ -163,11 +163,11 @@ hasTermVariable (Term term)
else else
{ {
if (realTermTuple (term)) if (realTermTuple (term))
return (hasTermVariable (term->left.op1) return (hasTermVariable (TermOp1(term))
|| hasTermVariable (term->right.op2)); || hasTermVariable (TermOp2(term)));
else else
return (hasTermVariable (term->left.op) return (hasTermVariable (TermOp(term))
|| hasTermVariable (term->right.key)); || hasTermVariable (TermKey(term)));
} }
} }
@ -206,8 +206,8 @@ isTermEqualFn (Term term1, Term term2)
} }
if (realTermLeaf (term1)) if (realTermLeaf (term1))
{ {
return (term1->left.symb == term2->left.symb return (TermSymb(term1) == TermSymb(term2)
&& term1->right.runid == term2->right.runid); && TermRunid(term1) == TermRunid(term2));
} }
else else
{ {
@ -218,15 +218,15 @@ isTermEqualFn (Term term1, Term term2)
/* for optimization of encryption equality, we compare /* for optimization of encryption equality, we compare
operator 2 first (we expect it to be a smaller term) operator 2 first (we expect it to be a smaller term)
*/ */
return (isTermEqualFn (term1->right.key, term2->right.key) && return (isTermEqualFn (TermKey(term1), TermKey(term2)) &&
isTermEqualFn (term1->left.op, term2->left.op)); isTermEqualFn (TermOp(term1), TermOp(term2)));
} }
else else
{ {
/* tuple */ /* tuple */
return (isTermEqualFn (term1->left.op1, term2->left.op1) && return (isTermEqualFn (TermOp1(term1), TermOp1(term2)) &&
isTermEqualFn (term1->right.op2, term2->right.op2)); isTermEqualFn (TermOp2(term1), TermOp2(term2)));
} }
} }
} }
@ -248,11 +248,11 @@ termSubTerm (Term t, Term tsub)
if (realTermLeaf (t)) if (realTermLeaf (t))
return 0; return 0;
if (realTermTuple (t)) if (realTermTuple (t))
return (termSubTerm (t->left.op1, tsub) return (termSubTerm (TermOp1(t), tsub)
|| termSubTerm (t->right.op2, tsub)); || termSubTerm (TermOp2(t), tsub));
else else
return (termSubTerm (t->left.op, tsub) return (termSubTerm (TermOp(t), tsub)
|| termSubTerm (t->right.key, tsub)); || termSubTerm (TermKey(t), tsub));
} }
//! See if a term is an interm of another. //! See if a term is an interm of another.
@ -272,8 +272,8 @@ termInTerm (Term t, Term tsub)
if (realTermLeaf (t)) if (realTermLeaf (t))
return 0; return 0;
if (realTermTuple (t)) if (realTermTuple (t))
return (termInTerm (t->left.op1, tsub) return (termInTerm (TermOp1(t), tsub)
|| termInTerm (t->right.op2, tsub)); || termInTerm (TermOp2(t), tsub));
else else
return 0; return 0;
} }
@ -303,15 +303,15 @@ termPrint (Term term)
#endif #endif
if (realTermLeaf (term)) if (realTermLeaf (term))
{ {
symbolPrint (term->left.symb); symbolPrint (TermSymb(term));
if (term->type == VARIABLE) if (term->type == VARIABLE)
eprintf ("V"); eprintf ("V");
if (term->right.runid >= 0) if (TermRunid(term) >= 0)
{ {
if (globalLatex && globalError == 0) if (globalLatex && globalError == 0)
eprintf ("\\sharp%i", term->right.runid); eprintf ("\\sharp%i", TermRunid(term));
else else
eprintf ("#%i", term->right.runid); eprintf ("#%i", TermRunid(term));
} }
if (term->subst != NULL) if (term->subst != NULL)
{ {
@ -331,13 +331,13 @@ termPrint (Term term)
} }
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
if (isTermLeaf (term->right.key) if (isTermLeaf (TermKey(term))
&& inTermlist (term->right.key->stype, TERM_Function)) && inTermlist (TermKey(term)->stype, TERM_Function))
{ {
/* function application */ /* function application */
termPrint (term->right.key); termPrint (TermKey(term));
eprintf ("("); eprintf ("(");
termTuplePrint (term->left.op); termTuplePrint (TermOp(term));
eprintf (")"); eprintf (")");
} }
else else
@ -346,17 +346,17 @@ termPrint (Term term)
if (globalLatex) if (globalLatex)
{ {
eprintf ("\\{"); eprintf ("\\{");
termTuplePrint (term->left.op); termTuplePrint (TermOp(term));
eprintf ("\\}_{"); eprintf ("\\}_{");
termPrint (term->right.key); termPrint (TermKey(term));
eprintf ("}"); eprintf ("}");
} }
else else
{ {
eprintf ("{"); eprintf ("{");
termTuplePrint (term->left.op); termTuplePrint (TermOp(term));
eprintf ("}"); eprintf ("}");
termPrint (term->right.key); termPrint (TermKey(term));
} }
} }
} }
@ -380,9 +380,9 @@ termTuplePrint (Term term)
while (realTermTuple (term)) while (realTermTuple (term))
{ {
// To remove any brackets, change this into termTuplePrint. // To remove any brackets, change this into termTuplePrint.
termPrint (term->left.op1); termPrint (TermOp1(term));
eprintf (","); eprintf (",");
term = deVar (term->right.op2); term = deVar (TermOp2(term));
} }
termPrint (term); termPrint (term);
return; return;
@ -409,13 +409,13 @@ termDuplicate (const Term term)
memcpy (newterm, term, sizeof (struct term)); memcpy (newterm, term, sizeof (struct term));
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
newterm->left.op = termDuplicate (term->left.op); TermOp(newterm) = termDuplicate (TermOp(term));
newterm->right.key = termDuplicate (term->right.key); TermKey(newterm) = termDuplicate (TermKey(term));
} }
else else
{ {
newterm->left.op1 = termDuplicate (term->left.op1); TermOp1(newterm) = termDuplicate (TermOp1(term));
newterm->right.op2 = termDuplicate (term->right.op2); TermOp2(newterm) = termDuplicate (TermOp2(term));
} }
return newterm; return newterm;
} }
@ -464,13 +464,13 @@ termDuplicateDeep (const Term term)
{ {
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
newterm->left.op = termDuplicateDeep (term->left.op); TermOp(newterm) = termDuplicateDeep (TermOp(term));
newterm->right.key = termDuplicateDeep (term->right.key); TermKey(newterm) = termDuplicateDeep (TermKey(term));
} }
else else
{ {
newterm->left.op1 = termDuplicateDeep (term->left.op1); TermOp1(newterm) = termDuplicateDeep (TermOp1(term));
newterm->right.op2 = termDuplicateDeep (term->right.op2); TermOp2(newterm) = termDuplicateDeep (TermOp2(term));
} }
} }
return newterm; return newterm;
@ -497,13 +497,13 @@ termDuplicateUV (Term term)
memcpy (newterm, term, sizeof (struct term)); memcpy (newterm, term, sizeof (struct term));
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
newterm->left.op = termDuplicateUV (term->left.op); TermOp(newterm) = termDuplicateUV (TermOp(term));
newterm->right.key = termDuplicateUV (term->right.key); TermKey(newterm) = termDuplicateUV (TermKey(term));
} }
else else
{ {
newterm->left.op1 = termDuplicateUV (term->left.op1); TermOp1(newterm) = termDuplicateUV (TermOp1(term));
newterm->right.op2 = termDuplicateUV (term->right.op2); TermOp2(newterm) = termDuplicateUV (TermOp2(term));
} }
return newterm; return newterm;
} }
@ -534,13 +534,13 @@ realTermDuplicate (const Term term)
newterm->type = term->type; newterm->type = term->type;
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
newterm->left.op = realTermDuplicate (term->left.op); TermOp(newterm) = realTermDuplicate (TermOp(term));
newterm->right.key = realTermDuplicate (term->right.key); TermKey(newterm) = realTermDuplicate (TermKey(term));
} }
else else
{ {
newterm->left.op1 = realTermDuplicate (term->left.op1); TermOp1(newterm) = realTermDuplicate (TermOp1(term));
newterm->right.op2 = realTermDuplicate (term->right.op2); TermOp2(newterm) = realTermDuplicate (TermOp2(term));
} }
} }
return newterm; return newterm;
@ -560,13 +560,13 @@ termDelete (const Term term)
{ {
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
termDelete (term->left.op); termDelete (TermOp(term));
termDelete (term->right.key); termDelete (TermKey(term));
} }
else else
{ {
termDelete (term->left.op1); termDelete (TermOp1(term));
termDelete (term->right.op2); termDelete (TermOp2(term));
} }
memFree (term, sizeof (struct term)); memFree (term, sizeof (struct term));
} }
@ -589,29 +589,29 @@ termNormalize (Term term)
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
termNormalize (term->left.op); termNormalize (TermOp(term));
termNormalize (term->right.key); termNormalize (TermKey(term));
} }
else else
{ {
/* normalize left hand first,both for tupling and for /* normalize left hand first,both for tupling and for
encryption */ encryption */
termNormalize (term->left.op1); termNormalize (TermOp1(term));
/* check for ((x,y),z) construct */ /* check for ((x,y),z) construct */
if (realTermTuple (term->left.op1)) if (realTermTuple (TermOp1(term)))
{ {
/* temporarily store the old terms */ /* temporarily store the old terms */
Term tx = (term->left.op1)->left.op1; Term tx = TermOp1(TermOp1(term));
Term ty = (term->left.op1)->right.op2; Term ty = TermOp2(TermOp1(term));
Term tz = term->right.op2; Term tz = TermOp2(term);
/* move node */ /* move node */
term->right.op2 = term->left.op1; TermOp2(term) = TermOp1(term);
/* construct (x,(y,z)) version */ /* construct (x,(y,z)) version */
term->left.op1 = tx; TermOp1(term) = tx;
(term->right.op2)->left.op1 = ty; TermOp1(TermOp2(term)) = ty;
(term->right.op2)->right.op2 = tz; TermOp2(TermOp2(term)) = tz;
} }
termNormalize (term->right.op2); termNormalize (TermOp2(term));
} }
} }
@ -629,12 +629,12 @@ termRunid (Term term, int runid)
if (realTermLeaf (term)) if (realTermLeaf (term))
{ {
/* leaf */ /* leaf */
if (term->right.runid == runid) if (TermRunid(term) == runid)
return term; return term;
else else
{ {
Term newt = termDuplicate (term); Term newt = termDuplicate (term);
newt->right.runid = runid; TermRunid(newt) = runid;
return newt; return newt;
} }
} }
@ -643,13 +643,13 @@ termRunid (Term term, int runid)
/* anything else, recurse */ /* anything else, recurse */
if (realTermEncrypt (term)) if (realTermEncrypt (term))
{ {
return makeTermEncrypt (termRunid (term->left.op, runid), return makeTermEncrypt (termRunid (TermOp(term), runid),
termRunid (term->right.key, runid)); termRunid (TermKey(term), runid));
} }
else else
{ {
return makeTermTuple (termRunid (term->left.op1, runid), return makeTermTuple (termRunid (TermOp1(term), runid),
termRunid (term->right.op2, runid)); termRunid (TermOp2(term), runid));
} }
} }
} }
@ -674,7 +674,7 @@ tupleCount (Term tt)
} }
else else
{ {
return (tupleCount (tt->left.op1) + tupleCount (tt->right.op2)); return (tupleCount (TermOp1(tt)) + tupleCount (TermOp2(tt)));
} }
} }
} }
@ -710,16 +710,16 @@ tupleProject (Term tt, int n)
else else
{ {
/* there is a tuple to traverse */ /* there is a tuple to traverse */
int left = tupleCount (tt->left.op1); int left = tupleCount (TermOp1(tt));
if (n >= left) if (n >= left)
{ {
/* it's in the right hand side */ /* it's in the right hand side */
return tupleProject (tt->right.op2, n - left); return tupleProject (TermOp2(tt), n - left);
} }
else else
{ {
/* left hand side */ /* left hand side */
return tupleProject (tt->left.op1, n); return tupleProject (TermOp1(tt), n);
} }
} }
} }
@ -749,11 +749,11 @@ termSize (Term t)
{ {
if (realTermEncrypt (t)) if (realTermEncrypt (t))
{ {
return 1 + termSize (t->left.op) + termSize (t->right.key); return 1 + termSize (TermOp(t)) + termSize (TermKey(t));
} }
else else
{ {
return termSize (t->left.op1) + termSize (t->right.op2); return termSize (TermOp1(t)) + termSize (TermOp2(t));
} }
} }
} }
@ -811,13 +811,13 @@ termDistance (Term t1, Term t2)
if (isTermEncrypt (t1)) if (isTermEncrypt (t1))
{ {
/* encryption */ /* encryption */
return (termDistance (t1->left.op, t2->left.op) + return (termDistance (TermOp(t1), TermOp(t2)) +
termDistance (t1->right.key, t2->right.key)) / 2; termDistance (TermKey(t1), TermKey(t2))) / 2;
} }
else else
{ {
return (termDistance (t1->left.op1, t2->left.op1) + return (termDistance (TermOp1(t1), TermOp1(t2)) +
termDistance (t1->right.op2, t2->right.op2)) / 2; termDistance (TermOp2(t1), TermOp2(t2))) / 2;
} }
} }
} }
@ -859,7 +859,7 @@ termOrder (Term t1, Term t2)
/* compare names */ /* compare names */
int comp; int comp;
comp = strcmp (t1->left.symb->text, t2->left.symb->text); comp = strcmp (TermSymb(t1)->text, TermSymb(t2)->text);
if (comp != 0) if (comp != 0)
{ {
/* names differ */ /* names differ */
@ -868,14 +868,14 @@ termOrder (Term t1, Term t2)
else else
{ {
/* equal names, compare run identifiers */ /* equal names, compare run identifiers */
if (t1->right.runid == t2->right.runid) if (TermRunid(t1) == TermRunid(t2))
{ {
error error
("termOrder: two terms seem to be identical although local precondition says they aren't."); ("termOrder: two terms seem to be identical although local precondition says they aren't.");
} }
else else
{ {
if (t1->right.runid < t2->right.runid) if (TermRunid(t1) < TermRunid(t2))
return -1; return -1;
else else
return 1; return 1;
@ -889,13 +889,13 @@ termOrder (Term t1, Term t2)
if (isTermEncrypt (t1)) if (isTermEncrypt (t1))
{ {
compL = termOrder (t1->left.op, t2->left.op); compL = termOrder (TermOp(t1), TermOp(t2));
compR = termOrder (t1->right.key, t2->right.key); compR = termOrder (TermKey(t1), TermKey(t2));
} }
else else
{ {
compL = termOrder (t1->left.op1, t2->left.op1); compL = termOrder (TermOp1(t1), TermOp1(t2));
compR = termOrder (t1->right.op2, t2->right.op2); compR = termOrder (TermOp2(t1), TermOp2(t2));
} }
if (compL != 0) if (compL != 0)
return compL; return compL;
@ -931,10 +931,10 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
// Left part // Left part
if (realTermTuple (term)) if (realTermTuple (term))
flag = flag flag = flag
&& (term_iterate (term->left.op1, leaf, nodel, nodem, noder)); && (term_iterate (TermOp1(term), leaf, nodel, nodem, noder));
else else
flag = flag flag = flag
&& (term_iterate (term->left.op, leaf, nodel, nodem, noder)); && (term_iterate (TermOp(term), leaf, nodel, nodem, noder));
if (nodem != NULL) if (nodem != NULL)
flag = flag && nodem (term); flag = flag && nodem (term);
@ -942,10 +942,10 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
// Right part // Right part
if (realTermTuple (term)) if (realTermTuple (term))
flag = flag flag = flag
&& (term_iterate (term->right.op2, leaf, nodel, nodem, noder)); && (term_iterate (TermOp2(term), leaf, nodel, nodem, noder));
else else
flag = flag flag = flag
&& (term_iterate (term->right.key, leaf, nodel, nodem, noder)); && (term_iterate (TermKey(term), leaf, nodel, nodem, noder));
if (noder != NULL) if (noder != NULL)
flag = flag && noder (term); flag = flag && noder (term);
@ -990,11 +990,11 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
flag = flag flag = flag
&& &&
(term_iterate_deVar (term_iterate_deVar
(term->left.op1, leaf, nodel, nodem, noder)); (TermOp1(term), leaf, nodel, nodem, noder));
else else
flag = flag flag = flag
&& &&
(term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder)); (term_iterate_deVar (TermOp(term), leaf, nodel, nodem, noder));
if (nodem != NULL) if (nodem != NULL)
flag = flag && nodem (term); flag = flag && nodem (term);
@ -1004,11 +1004,11 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
flag = flag flag = flag
&& &&
(term_iterate_deVar (term_iterate_deVar
(term->right.op2, leaf, nodel, nodem, noder)); (TermOp2(term), leaf, nodel, nodem, noder));
else else
flag = flag flag = flag
&& &&
(term_iterate_deVar (term->right.key, leaf, nodel, nodem, noder)); (term_iterate_deVar (TermKey(term), leaf, nodel, nodem, noder));
if (noder != NULL) if (noder != NULL)
flag = flag && noder (term); flag = flag && noder (term);
@ -1037,11 +1037,11 @@ term_iterate_leaves (const Term term, int (*func) ())
else else
{ {
if (realTermTuple (term)) if (realTermTuple (term))
return (term_iterate_leaves (term->left.op1, func) return (term_iterate_leaves (TermOp1(term), func)
&& term_iterate_leaves (term->right.op2, func)); && term_iterate_leaves (TermOp2(term), func));
else else
return (term_iterate_leaves (term->left.op, func) return (term_iterate_leaves (TermOp(term), func)
&& term_iterate_leaves (term->right.key, func)); && term_iterate_leaves (TermKey(term), func));
} }
} }
return 1; return 1;
@ -1090,8 +1090,8 @@ term_encryption_level (const Term term)
{ {
int l,r; int l,r;
l = iter_maxencrypt (term->left.op1); l = iter_maxencrypt (TermOp1(term));
r = iter_maxencrypt (term->right.op2); r = iter_maxencrypt (TermOp2(term));
if (l>r) if (l>r)
return l; return l;
else else
@ -1100,7 +1100,7 @@ term_encryption_level (const Term term)
else else
{ {
// encrypt // encrypt
return 1+iter_maxencrypt (term->left.op); return 1+iter_maxencrypt (TermOp(term));
} }
} }
} }
@ -1134,13 +1134,13 @@ term_constrain_level (const Term term)
{ {
if (realTermTuple (t)) if (realTermTuple (t))
{ {
tcl_iterate (t->left.op1); tcl_iterate (TermOp1(t));
tcl_iterate (t->right.op2); tcl_iterate (TermOp2(t));
} }
else else
{ {
tcl_iterate (t->left.op); tcl_iterate (TermOp(t));
tcl_iterate (t->right.key); tcl_iterate (TermKey(t));
} }
} }
} }
@ -1184,7 +1184,7 @@ term_set_keylevels (const Term term)
Symbol sym; Symbol sym;
// So, it occurs at 'level' as key. If that is less than known, store. // So, it occurs at 'level' as key. If that is less than known, store.
sym = t->left.symb; sym = TermSymb(t);
if (level < sym->keylevel) if (level < sym->keylevel)
{ {
// New minimum level // New minimum level
@ -1195,13 +1195,13 @@ term_set_keylevels (const Term term)
{ {
if (realTermTuple (t)) if (realTermTuple (t))
{ {
scan_levels (level, t->left.op1); scan_levels (level, TermOp1(t));
scan_levels (level, t->right.op2); scan_levels (level, TermOp2(t));
} }
else else
{ {
scan_levels (level, t->left.op); scan_levels (level, TermOp(t));
scan_levels ((level + 1), t->right.key); scan_levels ((level + 1), TermKey(t));
} }
} }
} }
@ -1257,12 +1257,12 @@ termPrintDiff (Term t1, Term t2)
if (realTermEncrypt (t1)) if (realTermEncrypt (t1))
{ {
// Encryption // Encryption
if (isTermEqual (t1->left.op, t2->left.op) || isTermEqual (t1->right.key, t2->right.key)) if (isTermEqual (TermOp(t1), TermOp(t2)) || isTermEqual (TermKey(t1), TermKey(t2)))
{ {
eprintf ("{"); eprintf ("{");
termPrintDiff (t1->left.op, t2->left.op); termPrintDiff (TermOp(t1), TermOp(t2));
eprintf ("}"); eprintf ("}");
termPrintDiff (t1->right.key, t2->right.key); termPrintDiff (TermKey(t1), TermKey(t2));
} }
else else
{ {
@ -1272,12 +1272,12 @@ termPrintDiff (Term t1, Term t2)
else else
{ {
// Tupling // Tupling
if (isTermEqual (t1->left.op1, t2->left.op1) || isTermEqual (t1->right.op2, t2->right.op2)) if (isTermEqual (TermOp1(t1), TermOp1(t2)) || isTermEqual (TermOp2(t1), TermOp2(t2)))
{ {
eprintf ("("); eprintf ("(");
termPrintDiff (t1->left.op1, t2->left.op1); termPrintDiff (TermOp1(t1), TermOp1(t2));
eprintf (")"); eprintf (")");
termPrintDiff (t1->right.op2, t2->right.op2); termPrintDiff (TermOp2(t1), TermOp2(t2));
} }
else else
{ {

36
src/term.h
View File

@ -53,6 +53,16 @@ struct term
} right; } right;
}; };
//! Component macros (left)
#define TermSymb(t) (t->left.symb)
#define TermOp1(t) (t->left.op1)
#define TermOp(t) (t->left.op)
//! Component macros (right)
#define TermRunid(t) (t->right.runid)
#define TermOp2(t) (t->right.op2)
#define TermKey(t) (t->right.key)
//! Flag for term status //! Flag for term status
extern int rolelocal_variable; extern int rolelocal_variable;
@ -68,7 +78,7 @@ __inline__ Term deVarScan (Term t);
#define realTermLeaf(t) (t != NULL && t->type <= LEAF) #define realTermLeaf(t) (t != NULL && t->type <= LEAF)
#define realTermTuple(t) (t != NULL && t->type == TUPLE) #define realTermTuple(t) (t != NULL && t->type == TUPLE)
#define realTermEncrypt(t) (t != NULL && t->type == ENCRYPT) #define realTermEncrypt(t) (t != NULL && t->type == ENCRYPT)
#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (t->type <= LEAF && rolelocal_variable && t->right.runid == -3))) #define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (t->type <= LEAF && rolelocal_variable && TermRunid(t) == -3)))
#define substVar(t) ((realTermVariable (t) && t->subst != NULL) ? 1 : 0) #define substVar(t) ((realTermVariable (t) && t->subst != NULL) ? 1 : 0)
#define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t) #define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t)
#define isTermLeaf(t) realTermLeaf(deVar(t)) #define isTermLeaf(t) realTermLeaf(deVar(t))
@ -92,10 +102,10 @@ int isTermEqualDebug (Term t1, Term t2);
? isTermEqualFn(t1,t2) \ ? isTermEqualFn(t1,t2) \
: ( \ : ( \
realTermEncrypt(t2) \ realTermEncrypt(t2) \
? (isTermEqualFn(t1->right.key, t2->right.key) && \ ? (isTermEqualFn(TermKey(t1), TermKey(t2)) && \
isTermEqualFn(t1->left.op, t2->left.op)) \ isTermEqualFn(TermOp(t1), TermOp(t2))) \
: (isTermEqualFn(t1->left.op1, t2->left.op1) && \ : (isTermEqualFn(TermOp1(t1), TermOp1(t2)) && \
isTermEqualFn(t1->right.op2, t2->right.op2)) \ isTermEqualFn(TermOp2(t1), TermOp2(t2))) \
) \ ) \
) \ ) \
) \ ) \
@ -115,10 +125,10 @@ int isTermEqualDebug (Term t1, Term t2);
? isTermEqualFn(t1,t2) \ ? isTermEqualFn(t1,t2) \
: ( \ : ( \
realTermEncrypt(t2) \ realTermEncrypt(t2) \
? (isTermEqual1(t1->right.key, t2->right.key) && \ ? (isTermEqual1(TermKey(t1), TermKey(t2)) && \
isTermEqual1(t1->left.op, t2->left.op)) \ isTermEqual1(TermOp(t1), TermOp(t2))) \
: (isTermEqual1(t1->left.op1, t2->left.op1) && \ : (isTermEqual1(TermOp1(t1), TermOp1(t2)) && \
isTermEqual1(t1->right.op2, t2->right.op2)) \ isTermEqual1(TermOp2(t1), TermOp2(t2))) \
) \ ) \
) \ ) \
) \ ) \
@ -138,10 +148,10 @@ int isTermEqualDebug (Term t1, Term t2);
? isTermEqualFn(t1,t2) \ ? isTermEqualFn(t1,t2) \
: ( \ : ( \
realTermEncrypt(t2) \ realTermEncrypt(t2) \
? (isTermEqual2(t1->right.key, t2->right.key) && \ ? (isTermEqual2(TermKey(t1), TermKey(t2)) && \
isTermEqual2(t1->left.op, t2->left.op)) \ isTermEqual2(TermOp(t1), TermOp(t2))) \
: (isTermEqual2(t1->left.op1, t2->left.op1) && \ : (isTermEqual2(TermOp1(t1), TermOp1(t2)) && \
isTermEqual2(t1->right.op2, t2->right.op2)) \ isTermEqual2(TermOp2(t1), TermOp2(t2))) \
) \ ) \
) \ ) \
) \ ) \

42
src/termlist.c
View File

@ -412,12 +412,12 @@ termlistAddVariables (Termlist tl, Term t)
else else
{ {
if (isTermEncrypt (t)) if (isTermEncrypt (t))
return termlistAddVariables (termlistAddVariables (tl, t->left.op), return termlistAddVariables (termlistAddVariables (tl, TermOp(t)),
t->right.key); TermKey(t));
else else
return return
termlistAddVariables (termlistAddVariables (tl, t->left.op1), termlistAddVariables (termlistAddVariables (tl, TermOp1(t)),
t->right.op2); TermOp2(t));
} }
} }
@ -455,12 +455,12 @@ termlistAddRealVariables (Termlist tl, Term t)
else else
{ {
if (realTermEncrypt (t)) if (realTermEncrypt (t))
return termlistAddVariables (termlistAddVariables (tl, t->left.op), return termlistAddVariables (termlistAddVariables (tl, TermOp(t)),
t->right.key); TermKey(t));
else else
return return
termlistAddVariables (termlistAddVariables (tl, t->left.op1), termlistAddVariables (termlistAddVariables (tl, TermOp1(t)),
t->right.op2); TermOp2(t));
} }
} }
@ -479,11 +479,11 @@ termlistAddBasic (Termlist tl, Term t)
if (!isTermLeaf (t)) if (!isTermLeaf (t))
{ {
if (isTermEncrypt (t)) if (isTermEncrypt (t))
return termlistAddBasic (termlistAddBasic (tl, t->left.op), return termlistAddBasic (termlistAddBasic (tl, TermOp(t)),
t->right.key); TermKey(t));
else else
return termlistAddBasic (termlistAddBasic (tl, t->left.op1), return termlistAddBasic (termlistAddBasic (tl, TermOp1(t)),
t->right.op2); TermOp2(t));
} }
else else
{ {
@ -571,8 +571,8 @@ inverseKey (Termlist inverses, Term key)
return termDuplicate (TERM_Hidden); return termDuplicate (TERM_Hidden);
} }
/* check for the special case first: when it is effectively a function application */ /* check for the special case first: when it is effectively a function application */
if (isTermEncrypt (key) && isTermLeaf (key->right.key) if (isTermEncrypt (key) && isTermLeaf (TermKey(key))
&& inTermlist (deVar (key->right.key)->stype, TERM_Function)) && inTermlist (deVar (TermKey(key))->stype, TERM_Function))
{ {
/* we are scanning for functions */ /* we are scanning for functions */
/* scan the list */ /* scan the list */
@ -581,15 +581,15 @@ inverseKey (Termlist inverses, Term key)
{ {
/* in: {op}kk, nk /* in: {op}kk, nk
* out: {op'}nk */ * out: {op'}nk */
return makeTermEncrypt (termDuplicate (orig->left.op), return makeTermEncrypt (termDuplicate (TermOp(orig)),
termDuplicate (newk)); termDuplicate (newk));
} }
while (inverses != NULL && inverses->next != NULL) while (inverses != NULL && inverses->next != NULL)
{ {
if (isTermEqual (key->right.key, inverses->term)) if (isTermEqual (TermKey(key), inverses->term))
return funKey (key, inverses->next->term); return funKey (key, inverses->next->term);
if (isTermEqual (key->right.key, inverses->next->term)) if (isTermEqual (TermKey(key), inverses->next->term))
return funKey (key, inverses->term); return funKey (key, inverses->term);
inverses = inverses->next->next; inverses = inverses->next->next;
} }
@ -645,13 +645,13 @@ termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid)
Term newt = termNodeDuplicate (t); Term newt = termNodeDuplicate (t);
if (realTermTuple (t)) if (realTermTuple (t))
{ {
newt->left.op1 = termLocal (t->left.op1, fromlist, tolist, runid); TermOp1(newt) = termLocal (TermOp1(t), fromlist, tolist, runid);
newt->right.op2 = termLocal (t->right.op2, fromlist, tolist, runid); TermOp2(newt) = termLocal (TermOp2(t), fromlist, tolist, runid);
} }
else else
{ {
newt->left.op = termLocal (t->left.op, fromlist, tolist, runid); TermOp(newt) = termLocal (TermOp(t), fromlist, tolist, runid);
newt->right.key = termLocal (t->right.key, fromlist, tolist, runid); TermKey(newt) = termLocal (TermKey(t), fromlist, tolist, runid);
} }
return newt; return newt;
} }