- Bugfixed --extravert.
This commit is contained in:
parent
dff7fcaee3
commit
b224344b59
@ -212,36 +212,29 @@ prune_theorems (const System sys)
|
|||||||
{
|
{
|
||||||
int run;
|
int run;
|
||||||
|
|
||||||
run = 0;
|
for (run = 0; run < sys->maxruns; run++)
|
||||||
while (run < sys->maxruns)
|
|
||||||
{
|
{
|
||||||
// Check this run only if it is an initiator role
|
// Check this run only if it is an initiator role
|
||||||
if (sys->runs[run].role->initiator)
|
if (sys->runs[run].role->initiator)
|
||||||
{
|
{
|
||||||
// Check this initiator run
|
// Check this initiator run
|
||||||
Termlist tl;
|
Termlist tl;
|
||||||
|
Termlist found;
|
||||||
|
|
||||||
tl = sys->runs[run].rho;
|
found = NULL;
|
||||||
while (tl != NULL)
|
for (tl = sys->runs[run].rho; tl != NULL; tl = tl->next)
|
||||||
{
|
{
|
||||||
Termlist tlscan;
|
if (inTermlist (found, tl->term))
|
||||||
|
|
||||||
tlscan = tl->next;
|
|
||||||
while (tlscan != NULL)
|
|
||||||
{
|
{
|
||||||
if (isTermEqual (tl->term, tlscan->term))
|
// XXX TODO
|
||||||
{
|
// Still need to fix proof output for this
|
||||||
// XXX TODO
|
//
|
||||||
// Still need to fix proof output for this
|
// Pruning because some agents are equal for this role.
|
||||||
//
|
return true;
|
||||||
// Pruning because some agents are equal for this role.
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
tlscan = tlscan->next;
|
|
||||||
}
|
}
|
||||||
tl = tl->next;
|
found = termlistAdd (found, tl->term);
|
||||||
}
|
}
|
||||||
run++;
|
termlistDelete (found);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user