andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Refactoring.

Browse Source
This commit is contained in:
Cas Cremers 2018-10-19 21:28:22 -04:00
parent 178c20a61c
commit 1c3e32a2da
1 changed files with 33 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
src/arachne.c
View File

@ -1444,6 +1444,38 @@ proof_term_match_none (const Binding b, const int found)
} }
} }
//! Process good candidate
int
process_good_candidate (const Protocol p, const Role r, const Roledef rd,
const int index, const Binding b, const int found)
{
int sflag;
// A good candidate
proof_term_match_first (found, b);
proof_term_match (p, r, rd, index, found);
indentDepth++;
// Bind to existing run
#ifdef DEBUG
debug (5, "Trying to bind to existing run.");
#endif
proof_go_down (TERM_DeEx, b->term);
sflag = bind_existing_run (b, p, r, index);
proof_go_up ();
// bind to new run
#ifdef DEBUG
debug (5, "Trying to bind to new run.");
#endif
proof_go_down (TERM_DeNew, b->term);
sflag = sflag && bind_new_run (b, p, r, index);
proof_go_up ();
indentDepth--;
return sflag;
}
//! Bind a regular goal //! Bind a regular goal
/** /**
* Problem child. Valgrind does not like it. * Problem child. Valgrind does not like it.
@ -1471,32 +1503,9 @@ bind_goal_regular_run (const Binding b)
if (!subtermUnify if (!subtermUnify
(rd->message, b->term, NULL, NULL, test_sub_unification)) (rd->message, b->term, NULL, NULL, test_sub_unification))
{ {
int sflag;
// A good candidate // A good candidate
found++; found++;
proof_term_match_first (found, b); return process_good_candidate (p, r, rd, index, b, found);
proof_term_match (p, r, rd, index, found);
indentDepth++;
// Bind to existing run
#ifdef DEBUG
debug (5, "Trying to bind to existing run.");
#endif
proof_go_down (TERM_DeEx, b->term);
sflag = bind_existing_run (b, p, r, index);
proof_go_up ();
// bind to new run
#ifdef DEBUG
debug (5, "Trying to bind to new run.");
#endif
proof_go_down (TERM_DeNew, b->term);
sflag = sflag && bind_new_run (b, p, r, index);
proof_go_up ();
indentDepth--;
return sflag;
} }
else else
{ {