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

Improved goal selection heuristic and trivial goal skipping.

Browse Source 
After the various changes, we were no longer correctly skipping terms like pk(IV#0),
even though it is a trivial goal. This patch fixes the issue.
This commit is contained in:
Cas Cremers 2012-06-12 21:46:51 +02:00
parent 61c451d7f8
commit d44e131f63
1 changed files with 56 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
src/heuristic.c
View File

@ -35,16 +35,47 @@
#include "hidelevel.h" #include "hidelevel.h"
#include "arachne.h" #include "arachne.h"
#include "error.h" #include "error.h"
#include "knowledge.h"
//! Trivial goal detection
/**
* Detect goals that we do not need to solve because they can be trivially solved.
*/
int
isTrivialGoal (const System sys, const Term t)
{
if (isTermVariable (t))
{
return true;
}
else
{
Term f;
f = getTermFunction (t);
if (f != NULL)
{
if (isKnowledgePublicFunction (sys->know, f))
{
return isTrivialGoal (sys, TermOp (t));
}
}
}
return false;
}
//! Check whether a binding (goal) is selectable //! Check whether a binding (goal) is selectable
int int
is_goal_selectable (const Binding b) is_goal_selectable (const System sys, const Binding b)
{ {
if (b != NULL) if (b != NULL)
{ {
if ((!b->blocked) && (!b->done)) if ((!b->blocked) && (!b->done))
{ {
return true; if (!isTrivialGoal (sys, b->term))
{
return true;
}
} }
} }
return false; return false;
@ -64,7 +95,7 @@ count_selectable_goals (const System sys)
Binding b; Binding b;
b = (Binding) bl->data; b = (Binding) bl->data;
if (is_goal_selectable (b)) if (is_goal_selectable (sys, b))
{ {
n++; n++;
} }
@ -78,9 +109,9 @@ count_selectable_goals (const System sys)
* The return list entry is either NULL, or a selectable goal. * The return list entry is either NULL, or a selectable goal.
*/ */
List List
first_selectable_goal (List bl) first_selectable_goal (const System sys, List bl)
{ {
while (bl != NULL && !is_goal_selectable ((Binding) bl->data)) while (bl != NULL && !is_goal_selectable (sys, (Binding) bl->data))
{ {
bl = bl->next; bl = bl->next;
} }
@ -393,31 +424,28 @@ select_goal_masked (const System sys)
b = (Binding) bl->data; b = (Binding) bl->data;
// Only if not done and not blocked // Only if not done and not blocked
if (is_goal_selectable (b)) if (is_goal_selectable (sys, b))
{ {
if (!isTermVariable (b->term)) float w;
w = computeGoalWeight (sys, b);
// Spacing between output
if (switches.output == PROOF && best != NULL)
eprintf (", ");
// Better alternative?
if (w <= best_weight)
{ {
float w; best_weight = w;
best = b;
w = computeGoalWeight (sys, b);
// Spacing between output
if (switches.output == PROOF && best != NULL)
eprintf (", ");
// Better alternative?
if (w <= best_weight)
{
best_weight = w;
best = b;
if (switches.output == PROOF)
eprintf ("*");
}
if (switches.output == PROOF) if (switches.output == PROOF)
{ eprintf ("*");
termPrint (b->term); }
eprintf ("<%.2f>", w); if (switches.output == PROOF)
} {
termPrint (b->term);
eprintf ("<%.2f>", w);
} }
} }
bl = bl->next; bl = bl->next;
@ -453,7 +481,7 @@ select_goal_random (const System sys)
bl = sys->bindings; bl = sys->bindings;
while (choice >= 0) while (choice >= 0)
{ {
bl = first_selectable_goal (bl); bl = first_selectable_goal (sys, bl);
if (bl == NULL) if (bl == NULL)
{ {
error ("Random chooser selected a NULL goal."); error ("Random chooser selected a NULL goal.");