- Fixed bug in new tuple expansion code (again, caused by the intricate
"realX" versus "isX" distinction.) - Added structures for rho, sigma, constants, but did not activate them yet.
This commit is contained in:
parent
2b9246bb64
commit
25244c5b23
113
src/arachne.c
113
src/arachne.c
@ -400,7 +400,7 @@ add_read_goals (const int run, const int old, const int new)
|
||||
|
||||
sys->runs[run].height = new;
|
||||
i = old;
|
||||
rd = roledef_shift (sys->runs[run].start, i);
|
||||
rd = eventRoledef (sys, run, i);
|
||||
count = 0;
|
||||
while (i < new && rd != NULL)
|
||||
{
|
||||
@ -432,54 +432,6 @@ add_read_goals (const int run, const int old, const int new)
|
||||
}
|
||||
}
|
||||
|
||||
//! Determine the run that follows from a substitution.
|
||||
/**
|
||||
* After an Arachne unification, stuff might go wrong w.r.t. nonce instantiation.
|
||||
* This function determines the run that is implied by a substitution list.
|
||||
* @returns >= 0: a run, -1 for invalid, -2 for any run.
|
||||
*/
|
||||
int
|
||||
determine_unification_run (Termlist tl)
|
||||
{
|
||||
int run;
|
||||
|
||||
run = -2;
|
||||
while (tl != NULL)
|
||||
{
|
||||
//! Again, hardcoded reference to compiler.c. Level -3 means a local constant for a role.
|
||||
if (tl->term->type != VARIABLE && TermRunid (tl->term) == -3)
|
||||
{
|
||||
Term t;
|
||||
|
||||
t = tl->term->subst;
|
||||
|
||||
// It is required that it is actually a leaf, because we construct it.
|
||||
if (!realTermLeaf (t))
|
||||
{
|
||||
return -1;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (run == -2)
|
||||
{
|
||||
// Any run
|
||||
run = TermRunid (t);
|
||||
}
|
||||
else
|
||||
{
|
||||
// Specific run: compare
|
||||
if (run != TermRunid (t))
|
||||
{
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
tl = tl->next;
|
||||
}
|
||||
return run;
|
||||
}
|
||||
|
||||
//! Determine trace length
|
||||
int
|
||||
get_semitrace_length ()
|
||||
@ -1915,9 +1867,11 @@ makeTraceClass (const System sys, Termlist varlist)
|
||||
Term var;
|
||||
|
||||
var = tl->term;
|
||||
deleteNewTerm (var->subst);
|
||||
var->subst = NULL;
|
||||
|
||||
if (realTermVariable (var))
|
||||
{
|
||||
deleteNewTerm (var->subst);
|
||||
var->subst = NULL;
|
||||
}
|
||||
tl = tl->next;
|
||||
}
|
||||
termlistDelete (varlist);
|
||||
@ -2067,34 +2021,39 @@ iterate ()
|
||||
{
|
||||
/* Substitution or something resulted in a tuple goal: we immediately split them into compounds.
|
||||
*/
|
||||
int count;
|
||||
Term tupletermbuffer;
|
||||
Term tuple;
|
||||
|
||||
tupletermbuffer = btup->term;
|
||||
|
||||
/*
|
||||
* We solve this by replacing the tuple goal by the left term, and adding a goal for the right term.
|
||||
*/
|
||||
btup->term = TermOp1 (tupletermbuffer);
|
||||
count =
|
||||
goal_add (TermOp2 (tupletermbuffer), btup->run_to,
|
||||
btup->ev_to, btup->level);
|
||||
|
||||
// Show this in output
|
||||
if (switches.output == PROOF)
|
||||
tuple = deVar (btup->term);
|
||||
if (realTermTuple (tuple))
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Expanding tuple goal ");
|
||||
termPrint (tupletermbuffer);
|
||||
eprintf (" into %i subgoals.\n", count);
|
||||
int count;
|
||||
Term tupletermbuffer;
|
||||
|
||||
tupletermbuffer = btup->term;
|
||||
/*
|
||||
* We solve this by replacing the tuple goal by the left term, and adding a goal for the right term.
|
||||
*/
|
||||
btup->term = TermOp1 (tuple);
|
||||
count =
|
||||
goal_add (TermOp2 (tuple), btup->run_to,
|
||||
btup->ev_to, btup->level);
|
||||
|
||||
// Show this in output
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Expanding tuple goal ");
|
||||
termPrint (tupletermbuffer);
|
||||
eprintf (" into %i subgoals.\n", count);
|
||||
}
|
||||
|
||||
// iterate
|
||||
flag = iterate ();
|
||||
|
||||
// undo
|
||||
goal_remove_last (count);
|
||||
btup->term = tupletermbuffer;
|
||||
}
|
||||
|
||||
// iterate
|
||||
flag = iterate ();
|
||||
|
||||
// undo
|
||||
goal_remove_last (count);
|
||||
btup->term = tupletermbuffer;
|
||||
}
|
||||
else
|
||||
{
|
||||
|
@ -220,7 +220,14 @@ goal_add (Term term, const int run, const int ev, const int level)
|
||||
term = deVar (term);
|
||||
#ifdef DEBUG
|
||||
if (term == NULL)
|
||||
error ("Trying to add an emtpy goal term");
|
||||
{
|
||||
globalError++;
|
||||
roledefPrint (eventRoledef (sys, run, ev));
|
||||
eprintf ("\n");
|
||||
globalError--;
|
||||
error ("Trying to add an emtpy goal term to r%ii%i, with level %i.",
|
||||
run, ev, level);
|
||||
}
|
||||
if (run >= sys->maxruns)
|
||||
error ("Trying to add a goal for a run that does not exist.");
|
||||
if (ev >= sys->runs[run].step)
|
||||
|
@ -234,6 +234,9 @@ ensureValidRun (const System sys, int run)
|
||||
myrun.index = NULL;
|
||||
myrun.start = NULL;
|
||||
|
||||
myrun.rho = NULL;
|
||||
myrun.sigma = NULL;
|
||||
myrun.constants = NULL;
|
||||
myrun.locals = NULL;
|
||||
myrun.artefacts = NULL;
|
||||
myrun.substitutions = NULL;
|
||||
@ -589,6 +592,9 @@ roleInstanceArachne (const System sys, const Protocol protocol,
|
||||
Termlist fromlist = NULL; // deleted at the end
|
||||
Termlist tolist = NULL; // -> .locals
|
||||
Termlist artefacts = NULL; // -> .artefacts
|
||||
Termlist rho = NULL; // -> .rho
|
||||
Termlist sigma = NULL; // -> .sigma
|
||||
Termlist constants = NULL; // -> .constants
|
||||
Term extterm = NULL; // construction thing (will go to artefacts)
|
||||
|
||||
/* claim runid, allocate space */
|
||||
|
@ -47,7 +47,10 @@ struct run
|
||||
Roledef index; //!< Current execution point in the run (roledef pointer)
|
||||
Roledef start; //!< Head of the run definition.
|
||||
Knowledge know; //!< Current knowledge of the run.
|
||||
Termlist locals; //!< Locals of the run.
|
||||
Termlist rho; //!< As in semantics (copies in artefacts)
|
||||
Termlist sigma; //!< As in semantics (copies in artefacts)
|
||||
Termlist constants; //!< As in semantics (copies in artefacts)
|
||||
Termlist locals; //!< Locals of the run (will be deprecated eventually)
|
||||
Termlist artefacts; //!< Stuff created especially for this run.
|
||||
Termlist substitutions; //!< The substitutions as they came from the roledef unifier
|
||||
int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter.
|
||||
|
Loading…
Reference in New Issue
Block a user