diff --git a/src/arachne.c b/src/arachne.c index cecf2a6..383153d 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -1291,6 +1291,7 @@ termBindConsequences (Term t) * 1: constrain level of term * 2: key or not * 4: consequences determination + * 8: select also single variables (that are not role variables) */ Binding select_goal () @@ -1319,47 +1320,74 @@ select_goal () b = (Binding) bl->data; // Ignore singular variables - if (!b->done && !realTermVariable (deVar (b->term))) - //if (!b->done) + if (!b->done) { - float buf_constrain; - int buf_weight; + int allow; + Term gterm; - void adapt (int w, float fl) + allow = 0; + gterm = deVar (b->term); + if (mode & 8) { - buf_constrain = buf_constrain + w * fl; - buf_weight = buf_weight + w; - } - - // buf_constrain is the addition of the factors before division by weight - buf_constrain = 0; - buf_weight = 0; - - if (sys->output == PROOF && best != NULL) - eprintf (", "); - - // Determine buf_constrain levels - // Bit 0: 1 constrain level - if (mode & 1) adapt (1, term_constrain_level (b->term)); - // Bit 1: 2 key level (inverted) - if (mode & 2) adapt (1, 0.5 * (1 - b->level)); - // Bit 2: 4 consequence level - if (mode & 4) adapt (1, termBindConsequences (b->term)); - - // Weigh result - if (buf_weight == 0 || buf_constrain <= min_constrain) - { - min_constrain = buf_constrain; - best = b; - if (sys->output == PROOF) - eprintf ("*"); - } - if (sys->output == PROOF) - { - termPrint (b->term); - if (mode & 2) + // check for singular variable + if (realTermVariable (gterm)) { - eprintf ("[%i]", b->level); + // singular variable only if it is not a role name variable + allow = !gterm->roleVar; + } + else + { + // not a singular variable, allow + allow = 1; + } + } + else + { + // Normally (mode & 8 == 0) we ignore any singular variables + allow = !realTermVariable (gterm); + } + + if (allow) + { + float buf_constrain; + int buf_weight; + + void adapt (int w, float fl) + { + buf_constrain = buf_constrain + w * fl; + buf_weight = buf_weight + w; + } + + // buf_constrain is the addition of the factors before division by weight + buf_constrain = 0; + buf_weight = 0; + + if (sys->output == PROOF && best != NULL) + eprintf (", "); + + // Determine buf_constrain levels + // Bit 0: 1 constrain level + if (mode & 1) adapt (1, term_constrain_level (b->term)); + // Bit 1: 2 key level (inverted) + if (mode & 2) adapt (1, 0.5 * (1 - b->level)); + // Bit 2: 4 consequence level + if (mode & 4) adapt (1, termBindConsequences (b->term)); + + // Weigh result + if (buf_weight == 0 || buf_constrain <= min_constrain) + { + min_constrain = buf_constrain; + best = b; + if (sys->output == PROOF) + eprintf ("*"); + } + if (sys->output == PROOF) + { + termPrint (b->term); + if (mode & 2) + { + eprintf ("[%i]", b->level); + } } } } diff --git a/src/system.c b/src/system.c index 0bd9688..a81a4c8 100644 --- a/src/system.c +++ b/src/system.c @@ -704,7 +704,12 @@ roleInstanceArachne (const System sys, const Protocol protocol, if (isTermVariable (newt)) { - // It is a protocol role name, maybe add choose? + // It is a protocol role name + + // Flag this + newt->roleVar = 1; + + // maybe add choose? // Note that for anything but full type flaws, this is not an issue. // In the POR reduction, force choose was the default. Here it is not. if (not_read_first (rd, oldt) && sys->match == 2) diff --git a/src/term.c b/src/term.c index 342595f..4949539 100644 --- a/src/term.c +++ b/src/term.c @@ -111,6 +111,7 @@ makeTermTuple (Term t1, Term t2) tt = makeTerm (); tt->type = TUPLE; tt->stype = NULL; + tt->roleVar = 0; TermOp1 (tt) = t1; TermOp2 (tt) = t2; return tt; @@ -127,6 +128,7 @@ makeTermType (const int type, const Symbol symb, const int runid) Term term = makeTerm (); term->type = type; term->stype = NULL; + term->roleVar = 0; term->subst = NULL; TermSymb (term) = symb; TermRunid (term) = runid; diff --git a/src/term.h b/src/term.h index bb7d5da..13de6b8 100644 --- a/src/term.h +++ b/src/term.h @@ -27,6 +27,8 @@ struct term //! Data Type termlist (e.g. agent or nonce) /** Only for leaves. */ void *stype; + int roleVar; // only for leaf, arachne engine: role variable flag + //! Substitution term. /** * If this is non-NULL, this leaf term is apparently substituted by