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

Proof output improved for occurrences of the Athena problem.

Browse Source
This commit is contained in:
Cas Cremers 2007-09-18 15:36:11 +02:00
parent 59bcb18fec
commit 2107d76532
3 changed files with 18 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/arachne.c
View File

@ -2703,7 +2703,17 @@ isTriviallyKnownAfterArachne (const System sys, const Term t, const int run,
* Currently used in mgusubterm in mgu.c * Currently used in mgusubterm in mgu.c
*/ */
void void
markNoFullProof () markNoFullProof (const Term tbig, const Term tsmall)
{ {
// Comment in proof
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Note: the pattern set will be incomplete, because ");
termPrint (tbig);
eprintf (" allows for infinitely many ways to subtermUnify ");
termPrint (tsmall);
eprintf (".\n");
}
sys->current_claim->complete = false; sys->current_claim->complete = false;
} }

2
src/arachne.h
View File

@ -35,6 +35,6 @@ void arachneOutputAttack ();
void printSemiState (); void printSemiState ();
int countIntruderActions (); int countIntruderActions ();
void role_name_print (const int run); void role_name_print (const int run);
void markNoFullProof (); void markNoFullProof (const Term tbig, const Term tsmall);
#endif #endif

12
src/mgu.c
View File

@ -328,12 +328,12 @@ subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist,
if (isOpenVariable (tbig)) if (isOpenVariable (tbig))
{ {
// This one needs to be pursued by further constraint adding // This one needs to be pursued by further constraint adding
/** /**
* Currently, this is not implemented yet. TODO. * Currently, this is not implemented yet. TODO.
* This is actually the main Athena problem that we haven't solved yet. * This is actually the main Athena problem that we haven't solved yet.
*/ */
// Mark that we don't have a full proof. // Mark that we don't have a full proof, and possibly remark in proof output.
markNoFullProof (); markNoFullProof (tbig, tsmall);
} }
} }