- Fixed the term union issue for portability.
This commit is contained in:
ccremers
parent
2cae2d2a08
commit
4d90395d7e
@ -192,7 +192,7 @@ levelFind (Symbol s, int level)
|
||||
{
|
||||
if (isTermLeaf (tl->term))
|
||||
{
|
||||
if (tl->term->symb == s)
|
||||
if (tl->term->left.symb == s)
|
||||
{
|
||||
return tl->term;
|
||||
}
|
||||
@ -395,7 +395,7 @@ commEvent (int event, Tac tc)
|
||||
else
|
||||
{
|
||||
/* n parameters */
|
||||
msg = deVar (claimbig)->op2;
|
||||
msg = deVar (claimbig)->right.op2;
|
||||
if (tupleCount (msg) != n)
|
||||
{
|
||||
printf
|
||||
@ -533,7 +533,7 @@ runInstanceCreate (Tac tc)
|
||||
/* first, locate the protocol */
|
||||
psym = tc->t1.tac->t1.sym;
|
||||
p = sys->protocols;
|
||||
while (p != NULL && p->nameterm->symb != psym)
|
||||
while (p != NULL && p->nameterm->left.symb != psym)
|
||||
p = p->next;
|
||||
if (p == NULL)
|
||||
{
|
||||
@ -546,7 +546,7 @@ runInstanceCreate (Tac tc)
|
||||
/* locate the role */
|
||||
rsym = tc->t1.tac->t2.sym;
|
||||
r = p->roles;
|
||||
while (r != NULL && r->nameterm->symb != rsym)
|
||||
while (r != NULL && r->nameterm->left.symb != rsym)
|
||||
r = r->next;
|
||||
if (r == NULL)
|
||||
{
|
||||
|
||||
@ -156,8 +156,8 @@ knowledgeAddTerm (Knowledge know, Term term)
|
||||
|
||||
if (isTermTuple (term))
|
||||
{
|
||||
knowledgeAddTerm (know, term->op1);
|
||||
knowledgeAddTerm (know, term->op2);
|
||||
knowledgeAddTerm (know, term->left.op1);
|
||||
knowledgeAddTerm (know, term->right.op2);
|
||||
}
|
||||
|
||||
/* adding variables? */
|
||||
@ -170,12 +170,12 @@ knowledgeAddTerm (Knowledge know, Term term)
|
||||
}
|
||||
if (term->type == ENCRYPT)
|
||||
{
|
||||
Term invkey = inverseKey (know->inverses, term->key);
|
||||
Term invkey = inverseKey (know->inverses, term->right.key);
|
||||
if (inKnowledge (know, invkey))
|
||||
{
|
||||
/* we can decrypt it */
|
||||
knowledgeAddTerm (know, term->op);
|
||||
if (!inKnowledge (know, term->key))
|
||||
knowledgeAddTerm (know, term->left.op);
|
||||
if (!inKnowledge (know, term->right.key))
|
||||
{
|
||||
/* we know the op now, but not the key, so add it anyway */
|
||||
know->encrypt = termlistAdd (know->encrypt, term);
|
||||
@ -207,9 +207,9 @@ knowledgeSimplify (Knowledge know, Term key)
|
||||
|
||||
while (scan != NULL)
|
||||
{
|
||||
if (isTermEqual ((scan->term)->key, invkey))
|
||||
if (isTermEqual ((scan->term)->right.key, invkey))
|
||||
{
|
||||
tldecrypts = termlistAdd (tldecrypts, (scan->term)->op);
|
||||
tldecrypts = termlistAdd (tldecrypts, (scan->term)->left.op);
|
||||
know->encrypt = termlistDelTerm (scan);
|
||||
scan = know->encrypt;
|
||||
}
|
||||
@ -284,13 +284,13 @@ inKnowledge (const Knowledge know, Term term)
|
||||
if (term->type == ENCRYPT)
|
||||
{
|
||||
return inTermlist (know->encrypt, term) ||
|
||||
(inKnowledge (know, term->key) && inKnowledge (know, term->op));
|
||||
(inKnowledge (know, term->right.key) && inKnowledge (know, term->left.op));
|
||||
}
|
||||
if (term->type == TUPLE)
|
||||
{
|
||||
return (inTermlist (know->encrypt, term) ||
|
||||
(inKnowledge (know, term->op1) &&
|
||||
inKnowledge (know, term->op2)));
|
||||
(inKnowledge (know, term->left.op1) &&
|
||||
inKnowledge (know, term->right.op2)));
|
||||
}
|
||||
return 0; /* unrecognized term type, weird */
|
||||
}
|
||||
|
||||
24
src/latex.c
24
src/latex.c
@ -117,12 +117,12 @@ latexTermPrint (Term term, Termlist highlight)
|
||||
{
|
||||
if (inTermlist (highlight, term))
|
||||
printf ("\\mathbf{");
|
||||
symbolPrint (term->symb);
|
||||
symbolPrint (term->left.symb);
|
||||
if (realTermVariable (term))
|
||||
printf ("V");
|
||||
if (term->runid >= 0)
|
||||
if (term->right.runid >= 0)
|
||||
{
|
||||
printf ("\\sharp%i", term->runid);
|
||||
printf ("\\sharp%i", term->right.runid);
|
||||
}
|
||||
if (term->subst != NULL)
|
||||
{
|
||||
@ -141,22 +141,22 @@ latexTermPrint (Term term, Termlist highlight)
|
||||
}
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
if (isTermLeaf (term->key)
|
||||
&& inTermlist (term->key->stype, TERM_Function))
|
||||
if (isTermLeaf (term->right.key)
|
||||
&& inTermlist (term->right.key->stype, TERM_Function))
|
||||
{
|
||||
/* function application */
|
||||
latexTermPrint (term->key, highlight);
|
||||
latexTermPrint (term->right.key, highlight);
|
||||
printf ("(");
|
||||
latexTermTuplePrint (term->op, highlight);
|
||||
latexTermTuplePrint (term->left.op, highlight);
|
||||
printf (")");
|
||||
}
|
||||
else
|
||||
{
|
||||
/* normal encryption */
|
||||
printf ("\\{");
|
||||
latexTermTuplePrint (term->op, highlight);
|
||||
latexTermTuplePrint (term->left.op, highlight);
|
||||
printf ("\\}_{");
|
||||
latexTermPrint (term->key, highlight);
|
||||
latexTermPrint (term->right.key, highlight);
|
||||
printf ("}");
|
||||
}
|
||||
}
|
||||
@ -180,9 +180,9 @@ latexTermTuplePrint (Term term, Termlist hl)
|
||||
while (realTermTuple (term))
|
||||
{
|
||||
// To remove any brackets, change this into latexTermTuplePrint.
|
||||
latexTermPrint (term->op1, hl);
|
||||
latexTermPrint (term->left.op1, hl);
|
||||
printf (",");
|
||||
term = deVar(term->op2);
|
||||
term = deVar(term->right.op2);
|
||||
}
|
||||
latexTermPrint(term, hl);
|
||||
return;
|
||||
@ -963,7 +963,7 @@ attackDisplayLatex (System sys)
|
||||
{
|
||||
/* detect whether it's really local to this run */
|
||||
Term t = deVar (tl->term);
|
||||
if (isTermLeaf (t) && t->runid == i)
|
||||
if (isTermLeaf (t) && t->right.runid == i)
|
||||
{
|
||||
if (first)
|
||||
{
|
||||
|
||||
@ -51,11 +51,11 @@ solve (const struct solvepass sp, Constraintlist solvecons)
|
||||
cl = constraintlistDuplicate (solvecons);
|
||||
cl =
|
||||
constraintlistAdd (cl,
|
||||
makeConstraint (deVar (activeco->term)->op1,
|
||||
makeConstraint (deVar (activeco->term)->left.op1,
|
||||
activeco->know));
|
||||
cl =
|
||||
constraintlistAdd (cl,
|
||||
makeConstraint (deVar (activeco->term)->op2,
|
||||
makeConstraint (deVar (activeco->term)->right.op2,
|
||||
activeco->know));
|
||||
solvecons = cl;
|
||||
flag = solve (sp, solvecons) || flag;
|
||||
@ -181,11 +181,11 @@ solve (const struct solvepass sp, Constraintlist solvecons)
|
||||
cl = constraintlistDuplicate (oldcl);
|
||||
cl =
|
||||
constraintlistAdd (cl,
|
||||
makeConstraint (activeco->term->op,
|
||||
makeConstraint (activeco->term->left.op,
|
||||
activeco->know));
|
||||
cl =
|
||||
constraintlistAdd (cl,
|
||||
makeConstraint (activeco->term->key,
|
||||
makeConstraint (activeco->term->right.key,
|
||||
activeco->know));
|
||||
solvecons = cl;
|
||||
flag = solve (sp, solvecons) || flag;
|
||||
@ -352,8 +352,8 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
|
||||
{
|
||||
/* tuple */
|
||||
tl2 = termlistShallow (tl->next);
|
||||
tl2 = termlistAdd (tl2, t->op1);
|
||||
tl2 = termlistAdd (tl2, t->op2);
|
||||
tl2 = termlistAdd (tl2, t->left.op1);
|
||||
tl2 = termlistAdd (tl2, t->right.op2);
|
||||
sendAdd_clp (sys, run, tl2);
|
||||
termlistDelete (tl2);
|
||||
}
|
||||
@ -362,14 +362,14 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
|
||||
/* encrypt */
|
||||
Term invkey;
|
||||
|
||||
invkey = inverseKey (sys->know->inverses, t->key);
|
||||
invkey = inverseKey (sys->know->inverses, t->right.key);
|
||||
if (!hasTermVariable (invkey))
|
||||
{
|
||||
/* simple case: no variable inside */
|
||||
knowledgeAddTerm (sys->know, t);
|
||||
tl2 = termlistShallow (tl->next);
|
||||
if (inKnowledge (sys->know, invkey) && hasTermVariable (t->op))
|
||||
tl2 = termlistAdd (tl2, t->op);
|
||||
if (inKnowledge (sys->know, invkey) && hasTermVariable (t->left.op))
|
||||
tl2 = termlistAdd (tl2, t->left.op);
|
||||
sendAdd_clp (sys, run, tl2);
|
||||
termlistDelete (tl2);
|
||||
}
|
||||
@ -398,7 +398,7 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
|
||||
sys->constraints = constraintlistAdd (clbuf, co);
|
||||
/* we _could_ explore first if this is solveable */
|
||||
knowledgeAddTerm (sys->know, t);
|
||||
tl2 = termlistAdd (tl2, t->op);
|
||||
tl2 = termlistAdd (tl2, t->left.op);
|
||||
sendAdd_clp (sys, run, tl2);
|
||||
|
||||
termlistDelete (tl2);
|
||||
|
||||
@ -110,14 +110,14 @@ termMguTerm (Term t1, Term t2)
|
||||
{
|
||||
Termlist tl1, tl2;
|
||||
|
||||
tl1 = termMguTerm (t1->key, t2->key);
|
||||
tl1 = termMguTerm (t1->right.key, t2->right.key);
|
||||
if (tl1 == MGUFAIL)
|
||||
{
|
||||
return MGUFAIL;
|
||||
}
|
||||
else
|
||||
{
|
||||
tl2 = termMguTerm (t1->op, t2->op);
|
||||
tl2 = termMguTerm (t1->left.op, t2->left.op);
|
||||
if (tl2 == MGUFAIL)
|
||||
{
|
||||
termlistSubstReset (tl1);
|
||||
@ -137,14 +137,14 @@ termMguTerm (Term t1, Term t2)
|
||||
{
|
||||
Termlist tl1, tl2;
|
||||
|
||||
tl1 = termMguTerm (t1->op1, t2->op1);
|
||||
tl1 = termMguTerm (t1->left.op1, t2->left.op1);
|
||||
if (tl1 == MGUFAIL)
|
||||
{
|
||||
return MGUFAIL;
|
||||
}
|
||||
else
|
||||
{
|
||||
tl2 = termMguTerm (t1->op2, t2->op2);
|
||||
tl2 = termMguTerm (t1->right.op2, t2->right.op2);
|
||||
if (tl2 == MGUFAIL)
|
||||
{
|
||||
termlistSubstReset (tl1);
|
||||
|
||||
@ -937,7 +937,7 @@ claimSecrecy (const System sys, const Term t)
|
||||
{
|
||||
t = deVar (t);
|
||||
if (isTermTuple (t))
|
||||
return csScan (t->op1) && csScan (t->op2);
|
||||
return csScan (t->left.op1) && csScan (t->right.op2);
|
||||
else
|
||||
return isTermSecret (sys, t);
|
||||
}
|
||||
@ -961,8 +961,8 @@ secrecyUnfolding (Term t, const Knowledge know)
|
||||
{
|
||||
t = deVar (t);
|
||||
if (isTermTuple (t))
|
||||
return termlistConcat (secrecyUnfolding(t->op1,know),
|
||||
secrecyUnfolding(t->op2,know)
|
||||
return termlistConcat (secrecyUnfolding(t->left.op1,know),
|
||||
secrecyUnfolding(t->right.op2,know)
|
||||
);
|
||||
else
|
||||
{
|
||||
|
||||
@ -493,7 +493,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
|
||||
{
|
||||
/* There is a TYPE constant in the parameter list.
|
||||
* Generate a new local variable for this run, with this type */
|
||||
Term newvar = makeTermType (VARIABLE, scanfrom->term->symb, rid);
|
||||
Term newvar = makeTermType (VARIABLE, scanfrom->term->left.symb, rid);
|
||||
sys->variables = termlistAdd (sys->variables, newvar);
|
||||
newvar->stype = termlistAdd (NULL, scanto->term);
|
||||
tolist = termlistAdd (tolist, newvar);
|
||||
@ -547,7 +547,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
|
||||
{
|
||||
if (realTermLeaf (t))
|
||||
{
|
||||
Term newt = makeTermType (t->type, t->symb, rid);
|
||||
Term newt = makeTermType (t->type, t->left.symb, rid);
|
||||
if (realTermVariable (newt))
|
||||
{
|
||||
sys->variables = termlistAdd (sys->variables, newt);
|
||||
|
||||
@ -64,14 +64,14 @@ termSubstitute (Term term, Substitution subs)
|
||||
{
|
||||
if (isTermEncrypt (term))
|
||||
{
|
||||
return makeTermEncrypt (termSubstitute (term->op, subs),
|
||||
termSubstitute (term->key, subs));
|
||||
return makeTermEncrypt (termSubstitute (term->left.op, subs),
|
||||
termSubstitute (term->right.key, subs));
|
||||
}
|
||||
else
|
||||
{
|
||||
return
|
||||
makeTermTuple (termSubstitute (term->op1, subs),
|
||||
termSubstitute (term->op2, subs));
|
||||
makeTermTuple (termSubstitute (term->left.op1, subs),
|
||||
termSubstitute (term->right.op2, subs));
|
||||
}
|
||||
}
|
||||
else
|
||||
|
||||
@ -372,11 +372,11 @@ termlistAddVariables (Termlist tl, Term t)
|
||||
else
|
||||
{
|
||||
if (isTermEncrypt (t))
|
||||
return termlistAddVariables (termlistAddVariables (tl, t->op),
|
||||
t->key);
|
||||
return termlistAddVariables (termlistAddVariables (tl, t->left.op),
|
||||
t->right.key);
|
||||
else
|
||||
return
|
||||
termlistAddVariables (termlistAddVariables (tl, t->op1), t->op2);
|
||||
termlistAddVariables (termlistAddVariables (tl, t->left.op1), t->right.op2);
|
||||
}
|
||||
}
|
||||
|
||||
@ -414,11 +414,11 @@ termlistAddRealVariables (Termlist tl, Term t)
|
||||
else
|
||||
{
|
||||
if (realTermEncrypt (t))
|
||||
return termlistAddVariables (termlistAddVariables (tl, t->op),
|
||||
t->key);
|
||||
return termlistAddVariables (termlistAddVariables (tl, t->left.op),
|
||||
t->right.key);
|
||||
else
|
||||
return
|
||||
termlistAddVariables (termlistAddVariables (tl, t->op1), t->op2);
|
||||
termlistAddVariables (termlistAddVariables (tl, t->left.op1), t->right.op2);
|
||||
}
|
||||
}
|
||||
|
||||
@ -437,9 +437,9 @@ termlistAddBasic (Termlist tl, Term t)
|
||||
if (!isTermLeaf (t))
|
||||
{
|
||||
if (isTermEncrypt (t))
|
||||
return termlistAddBasic (termlistAddBasic (tl, t->op), t->key);
|
||||
return termlistAddBasic (termlistAddBasic (tl, t->left.op), t->right.key);
|
||||
else
|
||||
return termlistAddBasic (termlistAddBasic (tl, t->op1), t->op2);
|
||||
return termlistAddBasic (termlistAddBasic (tl, t->left.op1), t->right.op2);
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -528,8 +528,8 @@ inverseKey (Termlist inverses, Term key)
|
||||
return termDuplicate (TERM_Hidden);
|
||||
}
|
||||
/* check for the special case first: when it is effectively a function application */
|
||||
if (isTermEncrypt (key) && isTermLeaf (key->key)
|
||||
&& inTermlist (deVar (key->key)->stype, TERM_Function))
|
||||
if (isTermEncrypt (key) && isTermLeaf (key->right.key)
|
||||
&& inTermlist (deVar (key->right.key)->stype, TERM_Function))
|
||||
{
|
||||
/* we are scanning for functions */
|
||||
/* scan the list */
|
||||
@ -538,15 +538,15 @@ inverseKey (Termlist inverses, Term key)
|
||||
{
|
||||
/* in: {op}kk, nk
|
||||
* out: {op'}nk */
|
||||
return makeTermEncrypt (termDuplicate (orig->op),
|
||||
return makeTermEncrypt (termDuplicate (orig->left.op),
|
||||
termDuplicate (newk));
|
||||
}
|
||||
while (inverses != NULL && inverses->next != NULL)
|
||||
{
|
||||
|
||||
if (isTermEqual (key->key, inverses->term))
|
||||
if (isTermEqual (key->right.key, inverses->term))
|
||||
return funKey (key, inverses->next->term);
|
||||
if (isTermEqual (key->key, inverses->next->term))
|
||||
if (isTermEqual (key->right.key, inverses->next->term))
|
||||
return funKey (key, inverses->term);
|
||||
inverses = inverses->next->next;
|
||||
}
|
||||
@ -604,13 +604,13 @@ termLocal (const Term t, Termlist fromlist, Termlist tolist,
|
||||
Term newt = termDuplicate (t);
|
||||
if (realTermTuple (t))
|
||||
{
|
||||
newt->op1 = termLocal (t->op1, fromlist, tolist, locals, runid);
|
||||
newt->op2 = termLocal (t->op2, fromlist, tolist, locals, runid);
|
||||
newt->left.op1 = termLocal (t->left.op1, fromlist, tolist, locals, runid);
|
||||
newt->right.op2 = termLocal (t->right.op2, fromlist, tolist, locals, runid);
|
||||
}
|
||||
else
|
||||
{
|
||||
newt->op = termLocal (t->op, fromlist, tolist, locals, runid);
|
||||
newt->key = termLocal (t->key, fromlist, tolist, locals, runid);
|
||||
newt->left.op = termLocal (t->left.op, fromlist, tolist, locals, runid);
|
||||
newt->right.key = termLocal (t->right.key, fromlist, tolist, locals, runid);
|
||||
}
|
||||
return newt;
|
||||
}
|
||||
|
||||
150
src/terms.c
150
src/terms.c
@ -66,8 +66,8 @@ makeTermEncrypt (Term t1, Term t2)
|
||||
Term term = makeTerm ();
|
||||
term->type = ENCRYPT;
|
||||
term->stype = NULL;
|
||||
term->op = t1;
|
||||
term->key = t2;
|
||||
term->left.op = t1;
|
||||
term->right.key = t2;
|
||||
return term;
|
||||
}
|
||||
|
||||
@ -98,8 +98,8 @@ makeTermTuple (Term t1, Term t2)
|
||||
Term tt = makeTerm ();
|
||||
tt->type = TUPLE;
|
||||
tt->stype = NULL;
|
||||
tt->op1 = t1;
|
||||
tt->op2 = t2;
|
||||
tt->left.op1 = t1;
|
||||
tt->right.op2 = t2;
|
||||
return tt;
|
||||
}
|
||||
|
||||
@ -115,8 +115,8 @@ makeTermType (const int type, const Symbol symb, const int runid)
|
||||
term->type = type;
|
||||
term->stype = NULL;
|
||||
term->subst = NULL;
|
||||
term->symb = symb;
|
||||
term->runid = runid;
|
||||
term->left.symb = symb;
|
||||
term->right.runid = runid;
|
||||
return term;
|
||||
}
|
||||
|
||||
@ -150,9 +150,9 @@ hasTermVariable (Term term)
|
||||
else
|
||||
{
|
||||
if (realTermTuple (term))
|
||||
return (hasTermVariable (term->op1) || hasTermVariable (term->op2));
|
||||
return (hasTermVariable (term->left.op1) || hasTermVariable (term->right.op2));
|
||||
else
|
||||
return (hasTermVariable (term->op) || hasTermVariable (term->key));
|
||||
return (hasTermVariable (term->left.op) || hasTermVariable (term->right.key));
|
||||
}
|
||||
}
|
||||
|
||||
@ -184,7 +184,7 @@ isTermEqualFn (Term term1, Term term2)
|
||||
}
|
||||
if (realTermLeaf (term1))
|
||||
{
|
||||
return (term1->symb == term2->symb && term1->runid == term2->runid);
|
||||
return (term1->left.symb == term2->left.symb && term1->right.runid == term2->right.runid);
|
||||
}
|
||||
else
|
||||
{
|
||||
@ -195,15 +195,15 @@ isTermEqualFn (Term term1, Term term2)
|
||||
/* for optimization of encryption equality, we compare
|
||||
operator 2 first (we expect it to be a smaller term)
|
||||
*/
|
||||
return (isTermEqualFn (term1->key, term2->key) &&
|
||||
isTermEqualFn (term1->op, term2->op));
|
||||
return (isTermEqualFn (term1->right.key, term2->right.key) &&
|
||||
isTermEqualFn (term1->left.op, term2->left.op));
|
||||
}
|
||||
else
|
||||
{
|
||||
/* tuple */
|
||||
|
||||
return (isTermEqualFn (term1->op1, term2->op1) &&
|
||||
isTermEqualFn (term1->op2, term2->op2));
|
||||
return (isTermEqualFn (term1->left.op1, term2->left.op1) &&
|
||||
isTermEqualFn (term1->right.op2, term2->right.op2));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -225,9 +225,9 @@ termOccurs (Term t, Term tsub)
|
||||
if (realTermLeaf (t))
|
||||
return 0;
|
||||
if (realTermTuple (t))
|
||||
return (termOccurs (t->op1, tsub) || termOccurs (t->op2, tsub));
|
||||
return (termOccurs (t->left.op1, tsub) || termOccurs (t->right.op2, tsub));
|
||||
else
|
||||
return (termOccurs (t->op, tsub) || termOccurs (t->key, tsub));
|
||||
return (termOccurs (t->left.op, tsub) || termOccurs (t->right.key, tsub));
|
||||
}
|
||||
|
||||
//! Print a term to stdout.
|
||||
@ -255,15 +255,15 @@ termPrint (Term term)
|
||||
#endif
|
||||
if (realTermLeaf (term))
|
||||
{
|
||||
symbolPrint (term->symb);
|
||||
symbolPrint (term->left.symb);
|
||||
if (realTermVariable (term))
|
||||
printf ("V");
|
||||
if (term->runid >= 0)
|
||||
if (term->right.runid >= 0)
|
||||
{
|
||||
if (globalLatex)
|
||||
printf ("\\sharp%i", term->runid);
|
||||
printf ("\\sharp%i", term->right.runid);
|
||||
else
|
||||
printf ("#%i", term->runid);
|
||||
printf ("#%i", term->right.runid);
|
||||
}
|
||||
if (term->subst != NULL)
|
||||
{
|
||||
@ -283,13 +283,13 @@ termPrint (Term term)
|
||||
}
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
if (isTermLeaf (term->key)
|
||||
&& inTermlist (term->key->stype, TERM_Function))
|
||||
if (isTermLeaf (term->right.key)
|
||||
&& inTermlist (term->right.key->stype, TERM_Function))
|
||||
{
|
||||
/* function application */
|
||||
termPrint (term->key);
|
||||
termPrint (term->right.key);
|
||||
printf ("(");
|
||||
termTuplePrint (term->op);
|
||||
termTuplePrint (term->left.op);
|
||||
printf (")");
|
||||
}
|
||||
else
|
||||
@ -298,17 +298,17 @@ termPrint (Term term)
|
||||
if (globalLatex)
|
||||
{
|
||||
printf ("\\{");
|
||||
termTuplePrint (term->op);
|
||||
termTuplePrint (term->left.op);
|
||||
printf ("\\}_{");
|
||||
termPrint (term->key);
|
||||
termPrint (term->right.key);
|
||||
printf ("}");
|
||||
}
|
||||
else
|
||||
{
|
||||
printf ("{");
|
||||
termTuplePrint (term->op);
|
||||
termTuplePrint (term->left.op);
|
||||
printf ("}");
|
||||
termPrint (term->key);
|
||||
termPrint (term->right.key);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -332,9 +332,9 @@ termTuplePrint (Term term)
|
||||
while (realTermTuple (term))
|
||||
{
|
||||
// To remove any brackets, change this into termTuplePrint.
|
||||
termPrint (term->op1);
|
||||
termPrint (term->left.op1);
|
||||
printf (",");
|
||||
term = deVar(term->op2);
|
||||
term = deVar(term->right.op2);
|
||||
}
|
||||
termPrint(term);
|
||||
return;
|
||||
@ -361,13 +361,13 @@ termDuplicate (const Term term)
|
||||
newterm->type = term->type;
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
newterm->op = termDuplicate (term->op);
|
||||
newterm->key = termDuplicate (term->key);
|
||||
newterm->left.op = termDuplicate (term->left.op);
|
||||
newterm->right.key = termDuplicate (term->right.key);
|
||||
}
|
||||
else
|
||||
{
|
||||
newterm->op1 = termDuplicate (term->op1);
|
||||
newterm->op2 = termDuplicate (term->op2);
|
||||
newterm->left.op1 = termDuplicate (term->left.op1);
|
||||
newterm->right.op2 = termDuplicate (term->right.op2);
|
||||
}
|
||||
return newterm;
|
||||
}
|
||||
@ -398,13 +398,13 @@ termDuplicateDeep (const Term term)
|
||||
newterm->type = term->type;
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
newterm->op = termDuplicateDeep (term->op);
|
||||
newterm->key = termDuplicateDeep (term->key);
|
||||
newterm->left.op = termDuplicateDeep (term->left.op);
|
||||
newterm->right.key = termDuplicateDeep (term->right.key);
|
||||
}
|
||||
else
|
||||
{
|
||||
newterm->op1 = termDuplicateDeep (term->op1);
|
||||
newterm->op2 = termDuplicateDeep (term->op2);
|
||||
newterm->left.op1 = termDuplicateDeep (term->left.op1);
|
||||
newterm->right.op2 = termDuplicateDeep (term->right.op2);
|
||||
}
|
||||
}
|
||||
return newterm;
|
||||
@ -431,13 +431,13 @@ termDuplicateUV (Term term)
|
||||
newterm->type = term->type;
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
newterm->op = termDuplicateUV (term->op);
|
||||
newterm->key = termDuplicateUV (term->key);
|
||||
newterm->left.op = termDuplicateUV (term->left.op);
|
||||
newterm->right.key = termDuplicateUV (term->right.key);
|
||||
}
|
||||
else
|
||||
{
|
||||
newterm->op1 = termDuplicateUV (term->op1);
|
||||
newterm->op2 = termDuplicateUV (term->op2);
|
||||
newterm->left.op1 = termDuplicateUV (term->left.op1);
|
||||
newterm->right.op2 = termDuplicateUV (term->right.op2);
|
||||
}
|
||||
return newterm;
|
||||
}
|
||||
@ -468,13 +468,13 @@ realTermDuplicate (const Term term)
|
||||
newterm->type = term->type;
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
newterm->op = realTermDuplicate (term->op);
|
||||
newterm->key = realTermDuplicate (term->key);
|
||||
newterm->left.op = realTermDuplicate (term->left.op);
|
||||
newterm->right.key = realTermDuplicate (term->right.key);
|
||||
}
|
||||
else
|
||||
{
|
||||
newterm->op1 = realTermDuplicate (term->op1);
|
||||
newterm->op2 = realTermDuplicate (term->op2);
|
||||
newterm->left.op1 = realTermDuplicate (term->left.op1);
|
||||
newterm->right.op2 = realTermDuplicate (term->right.op2);
|
||||
}
|
||||
}
|
||||
return newterm;
|
||||
@ -494,13 +494,13 @@ termDelete (const Term term)
|
||||
{
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
termDelete (term->op);
|
||||
termDelete (term->key);
|
||||
termDelete (term->left.op);
|
||||
termDelete (term->right.key);
|
||||
}
|
||||
else
|
||||
{
|
||||
termDelete (term->op1);
|
||||
termDelete (term->op2);
|
||||
termDelete (term->left.op1);
|
||||
termDelete (term->right.op2);
|
||||
}
|
||||
memFree (term, sizeof (struct term));
|
||||
}
|
||||
@ -523,29 +523,29 @@ termNormalize (Term term)
|
||||
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
termNormalize (term->op);
|
||||
termNormalize (term->key);
|
||||
termNormalize (term->left.op);
|
||||
termNormalize (term->right.key);
|
||||
}
|
||||
else
|
||||
{
|
||||
/* normalize left hand first,both for tupling and for
|
||||
encryption */
|
||||
termNormalize (term->op1);
|
||||
termNormalize (term->left.op1);
|
||||
/* check for ((x,y),z) construct */
|
||||
if (realTermTuple (term->op1))
|
||||
if (realTermTuple (term->left.op1))
|
||||
{
|
||||
/* temporarily store the old terms */
|
||||
Term tx = (term->op1)->op1;
|
||||
Term ty = (term->op1)->op2;
|
||||
Term tz = term->op2;
|
||||
Term tx = (term->left.op1)->left.op1;
|
||||
Term ty = (term->left.op1)->right.op2;
|
||||
Term tz = term->right.op2;
|
||||
/* move node */
|
||||
term->op2 = term->op1;
|
||||
term->right.op2 = term->left.op1;
|
||||
/* construct (x,(y,z)) version */
|
||||
term->op1 = tx;
|
||||
(term->op2)->op1 = ty;
|
||||
(term->op2)->op2 = tz;
|
||||
term->left.op1 = tx;
|
||||
(term->right.op2)->left.op1 = ty;
|
||||
(term->right.op2)->right.op2 = tz;
|
||||
}
|
||||
termNormalize (term->op2);
|
||||
termNormalize (term->right.op2);
|
||||
}
|
||||
}
|
||||
|
||||
@ -563,12 +563,12 @@ termRunid (Term term, int runid)
|
||||
if (realTermLeaf (term))
|
||||
{
|
||||
/* leaf */
|
||||
if (term->runid == runid)
|
||||
if (term->right.runid == runid)
|
||||
return term;
|
||||
else
|
||||
{
|
||||
Term newt = termDuplicate (term);
|
||||
newt->runid = runid;
|
||||
newt->right.runid = runid;
|
||||
return newt;
|
||||
}
|
||||
}
|
||||
@ -577,13 +577,13 @@ termRunid (Term term, int runid)
|
||||
/* anything else, recurse */
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
return makeTermEncrypt (termRunid (term->op, runid),
|
||||
termRunid (term->key, runid));
|
||||
return makeTermEncrypt (termRunid (term->left.op, runid),
|
||||
termRunid (term->right.key, runid));
|
||||
}
|
||||
else
|
||||
{
|
||||
return makeTermTuple (termRunid (term->op1, runid),
|
||||
termRunid (term->op2, runid));
|
||||
return makeTermTuple (termRunid (term->left.op1, runid),
|
||||
termRunid (term->right.op2, runid));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -608,7 +608,7 @@ tupleCount (Term tt)
|
||||
}
|
||||
else
|
||||
{
|
||||
return (tupleCount (tt->op1) + tupleCount (tt->op2));
|
||||
return (tupleCount (tt->left.op1) + tupleCount (tt->right.op2));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -644,16 +644,16 @@ tupleProject (Term tt, int n)
|
||||
else
|
||||
{
|
||||
/* there is a tuple to traverse */
|
||||
int left = tupleCount (tt->op1);
|
||||
int left = tupleCount (tt->left.op1);
|
||||
if (n >= left)
|
||||
{
|
||||
/* it's in the right hand side */
|
||||
return tupleProject (tt->op2, n - left);
|
||||
return tupleProject (tt->right.op2, n - left);
|
||||
}
|
||||
else
|
||||
{
|
||||
/* left hand side */
|
||||
return tupleProject (tt->op1, n);
|
||||
return tupleProject (tt->left.op1, n);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -683,11 +683,11 @@ termSize(Term t)
|
||||
{
|
||||
if (realTermEncrypt(t))
|
||||
{
|
||||
return 1 + termSize(t->op) + termSize(t->key);
|
||||
return 1 + termSize(t->left.op) + termSize(t->right.key);
|
||||
}
|
||||
else
|
||||
{
|
||||
return termSize(t->op1) + termSize(t->op2);
|
||||
return termSize(t->left.op1) + termSize(t->right.op2);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -742,11 +742,11 @@ termDistance(Term t1, Term t2)
|
||||
if (isTermEncrypt(t1))
|
||||
{
|
||||
/* encryption */
|
||||
return (termDistance(t1->op, t2->op) + termDistance(t1->key, t2->key)) / 2;
|
||||
return (termDistance(t1->left.op, t2->left.op) + termDistance(t1->right.key, t2->right.key)) / 2;
|
||||
}
|
||||
else
|
||||
{
|
||||
return (termDistance(t1->op1, t2->op1) + termDistance(t1->op2, t2->op2)) / 2;
|
||||
return (termDistance(t1->left.op1, t2->left.op1) + termDistance(t1->right.op2, t2->right.op2)) / 2;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
16
src/terms.h
16
src/terms.h
@ -36,7 +36,7 @@ struct term
|
||||
*/
|
||||
struct term *subst; // only for variable/leaf, substitution term
|
||||
|
||||
union
|
||||
union
|
||||
{
|
||||
Symbol symb;
|
||||
//! Encrypted subterm.
|
||||
@ -44,7 +44,7 @@ struct term
|
||||
//! Left-hand side of tuple pair.
|
||||
struct term *op1;
|
||||
struct term *next; // for alternative memory management
|
||||
};
|
||||
} left;
|
||||
union
|
||||
{
|
||||
int runid;
|
||||
@ -52,7 +52,7 @@ struct term
|
||||
struct term *key;
|
||||
//! Right-hand side of tuple pair.
|
||||
struct term *op2;
|
||||
};
|
||||
} right;
|
||||
};
|
||||
|
||||
//! Pointer shorthand.
|
||||
@ -84,13 +84,13 @@ Term deVarScan (Term t);
|
||||
? 0 \
|
||||
: ( \
|
||||
realTermLeaf(t1) \
|
||||
? (t1->symb == t2->symb && t1->runid == t2->runid) \
|
||||
? (t1->left.symb == t2->left.symb && t1->right.runid == t2->right.runid) \
|
||||
: ( \
|
||||
realTermEncrypt(t2) \
|
||||
? (isTermEqualFn(t1->key, t2->key) && \
|
||||
isTermEqualFn(t1->op, t2->op)) \
|
||||
: (isTermEqualFn(t1->op1, t2->op1) && \
|
||||
isTermEqualFn(t1->op2, t2->op2)) \
|
||||
? (isTermEqualFn(t1->right.key, t2->right.key) && \
|
||||
isTermEqualFn(t1->left.op, t2->left.op)) \
|
||||
: (isTermEqualFn(t1->left.op1, t2->left.op1) && \
|
||||
isTermEqualFn(t1->right.op2, t2->right.op2)) \
|
||||
) \
|
||||
) \
|
||||
) \
|
||||
|
||||
Loading…
Reference in New Issue
Block a user