- Singular variables need to be bound as well (to ensure ordering is
correct w.r.t. e.g. nonces, if the intruder cannot construct them.)
This commit is contained in:
parent
2ddd1eee13
commit
acb89922f1
@ -898,38 +898,31 @@ select_goal ()
|
|||||||
b = (Binding) bl->data;
|
b = (Binding) bl->data;
|
||||||
if (!b->done)
|
if (!b->done)
|
||||||
{
|
{
|
||||||
// We don't care about singular variables.
|
float cons;
|
||||||
/**
|
|
||||||
* Note that to mirror the modelchecker semantics, we should check whether the type exists in M_0.
|
|
||||||
*/
|
|
||||||
if (!isTermVariable (b->term))
|
|
||||||
{
|
|
||||||
float cons;
|
|
||||||
|
|
||||||
if (sys->output == PROOF && best != NULL)
|
if (sys->output == PROOF && best != NULL)
|
||||||
eprintf (", ");
|
eprintf (", ");
|
||||||
if (b->level >= max_level)
|
if (b->level >= max_level)
|
||||||
|
{
|
||||||
|
if (b->level > max_level)
|
||||||
{
|
{
|
||||||
if (b->level > max_level)
|
max_level = b->level;
|
||||||
{
|
min_constrain = 1; // 1 is the maximum
|
||||||
max_level = b->level;
|
|
||||||
min_constrain = 1; // 1 is the maximum
|
|
||||||
}
|
|
||||||
cons = term_constrain_level (b->term);
|
|
||||||
if (cons <= min_constrain)
|
|
||||||
{
|
|
||||||
min_constrain = cons;
|
|
||||||
best = b;
|
|
||||||
if (sys->output == PROOF)
|
|
||||||
eprintf ("*");
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
if (sys->output == PROOF)
|
cons = term_constrain_level (b->term);
|
||||||
|
if (cons <= min_constrain)
|
||||||
{
|
{
|
||||||
termPrint (b->term);
|
min_constrain = cons;
|
||||||
eprintf ("[%i]", b->level);
|
best = b;
|
||||||
|
if (sys->output == PROOF)
|
||||||
|
eprintf ("*");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
if (sys->output == PROOF)
|
||||||
|
{
|
||||||
|
termPrint (b->term);
|
||||||
|
eprintf ("[%i]", b->level);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
bl = bl->next;
|
bl = bl->next;
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user