|
|
|
|
@@ -30,6 +30,7 @@
|
|
|
|
|
#include <limits.h>
|
|
|
|
|
#include <float.h>
|
|
|
|
|
#include <string.h>
|
|
|
|
|
#include <assert.h>
|
|
|
|
|
|
|
|
|
|
#include "mymalloc.h"
|
|
|
|
|
#include "term.h"
|
|
|
|
|
@@ -995,39 +996,36 @@ makeDepend (Term tsmall, struct md_state *state)
|
|
|
|
|
return true;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
//! Try to bind a specific existing run to a goal.
|
|
|
|
|
/**
|
|
|
|
|
* The idea is that we try to bind it this specific run and index. If this
|
|
|
|
|
* requires keys, then we should add such goals as well with the required
|
|
|
|
|
* decryptor things.
|
|
|
|
|
*
|
|
|
|
|
* The 'newdecr' boolean signals the addition of decryptors. If it is false, we should not add any.
|
|
|
|
|
*
|
|
|
|
|
* The key goals are bound to the goal. Iterates on success.
|
|
|
|
|
*/
|
|
|
|
|
void
|
|
|
|
|
bind_existing_to_goal (const Binding b, const int run, const int index,
|
|
|
|
|
int newdecr)
|
|
|
|
|
struct betg_state
|
|
|
|
|
{
|
|
|
|
|
Term bigterm;
|
|
|
|
|
Binding b;
|
|
|
|
|
int run;
|
|
|
|
|
int index;
|
|
|
|
|
int newdecr;
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
int unifiesWithKeys (Termlist substlist, Termlist keylist, void *state)
|
|
|
|
|
{
|
|
|
|
|
int
|
|
|
|
|
unifiesWithKeys (Termlist substlist, Termlist keylist,
|
|
|
|
|
struct betg_state *ptr_betgState)
|
|
|
|
|
{
|
|
|
|
|
int old_length;
|
|
|
|
|
int newgoals;
|
|
|
|
|
|
|
|
|
|
assert (ptr_betgState != NULL);
|
|
|
|
|
|
|
|
|
|
// TODO this is a hack: in this case we really should not use subterm
|
|
|
|
|
// unification but interm instead. However, this effectively does the same
|
|
|
|
|
// by avoiding branches that get immediately pruned anyway.
|
|
|
|
|
if (!newdecr && keylist != NULL)
|
|
|
|
|
if (!ptr_betgState->newdecr && keylist != NULL)
|
|
|
|
|
{
|
|
|
|
|
return true;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// We need some adapting because the height would increase; we therefore
|
|
|
|
|
// have to add recv goals before we know whether it unifies.
|
|
|
|
|
old_length = sys->runs[run].height;
|
|
|
|
|
newgoals = add_recv_goals (run, old_length, index + 1);
|
|
|
|
|
old_length = sys->runs[ptr_betgState->run].height;
|
|
|
|
|
newgoals =
|
|
|
|
|
add_recv_goals (ptr_betgState->run, old_length, ptr_betgState->index + 1);
|
|
|
|
|
|
|
|
|
|
{
|
|
|
|
|
// wrap substitution lists
|
|
|
|
|
@@ -1042,28 +1040,31 @@ bind_existing_to_goal (const Binding b, const int run, const int index,
|
|
|
|
|
|
|
|
|
|
indentPrint ();
|
|
|
|
|
eprintf ("Suppose ");
|
|
|
|
|
termPrint (b->term);
|
|
|
|
|
termPrint ((ptr_betgState->b)->term);
|
|
|
|
|
eprintf (" originates first at run %i, event %i, as part of ",
|
|
|
|
|
run, index);
|
|
|
|
|
rd = roledef_shift (sys->runs[run].start, index);
|
|
|
|
|
ptr_betgState->run, ptr_betgState->index);
|
|
|
|
|
rd =
|
|
|
|
|
roledef_shift (sys->runs[ptr_betgState->run].start,
|
|
|
|
|
ptr_betgState->index);
|
|
|
|
|
termPrint (rd->message);
|
|
|
|
|
eprintf ("\n");
|
|
|
|
|
}
|
|
|
|
|
// new create key goals, bind etc.
|
|
|
|
|
createDecryptionChain (b, run, index, keylist, iterate);
|
|
|
|
|
createDecryptionChain (ptr_betgState->b, ptr_betgState->run,
|
|
|
|
|
ptr_betgState->index, keylist, iterate);
|
|
|
|
|
}
|
|
|
|
|
else
|
|
|
|
|
{
|
|
|
|
|
struct md_state State;
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// TODO CONTEXT for makeDepend in State
|
|
|
|
|
|
|
|
|
|
State.neworders = 0;
|
|
|
|
|
State.sl = sl;
|
|
|
|
|
State.tvar = sl->term;
|
|
|
|
|
State.allgood = true;
|
|
|
|
|
iterateTermOther (run, State.tvar, makeDepend, &State);
|
|
|
|
|
iterateTermOther (ptr_betgState->run, State.tvar, makeDepend,
|
|
|
|
|
&State);
|
|
|
|
|
if (State.allgood)
|
|
|
|
|
{
|
|
|
|
|
wrapSubst (sl->next);
|
|
|
|
|
@@ -1081,12 +1082,34 @@ bind_existing_to_goal (const Binding b, const int run, const int index,
|
|
|
|
|
|
|
|
|
|
// undo
|
|
|
|
|
goal_remove_last (newgoals);
|
|
|
|
|
sys->runs[run].height = old_length;
|
|
|
|
|
sys->runs[ptr_betgState->run].height = old_length;
|
|
|
|
|
return true;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
//! Try to bind a specific existing run to a goal.
|
|
|
|
|
/**
|
|
|
|
|
* The idea is that we try to bind it this specific run and index. If this
|
|
|
|
|
* requires keys, then we should add such goals as well with the required
|
|
|
|
|
* decryptor things.
|
|
|
|
|
*
|
|
|
|
|
* The 'newdecr' boolean signals the addition of decryptors. If it is false, we should not add any.
|
|
|
|
|
*
|
|
|
|
|
* The key goals are bound to the goal. Iterates on success.
|
|
|
|
|
*/
|
|
|
|
|
void
|
|
|
|
|
bind_existing_to_goal (const Binding b, const int run, const int index,
|
|
|
|
|
int newdecr)
|
|
|
|
|
{
|
|
|
|
|
Term bigterm;
|
|
|
|
|
struct betg_state betgState;
|
|
|
|
|
|
|
|
|
|
betgState.b = b;
|
|
|
|
|
betgState.run = run;
|
|
|
|
|
betgState.index = index;
|
|
|
|
|
betgState.newdecr = newdecr;
|
|
|
|
|
|
|
|
|
|
bigterm = roledef_shift (sys->runs[run].start, index)->message;
|
|
|
|
|
subtermUnify (bigterm, b->term, NULL, NULL, unifiesWithKeys, NULL);
|
|
|
|
|
subtermUnify (bigterm, b->term, NULL, NULL, unifiesWithKeys, &betgState);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|