diff --git a/src/heuristic.c b/src/heuristic.c index 2923092..c9016c6 100644 --- a/src/heuristic.c +++ b/src/heuristic.c @@ -12,6 +12,7 @@ #include "system.h" #include "specialterm.h" #include "switches.h" +#include "hidelevel.h" //! Check whether a binding (goal) is selectable int @@ -205,6 +206,35 @@ term_noncevariables_level (const Term t) } } +//! Determine weight based on hidelevel +float +weighHidelevel (const System sys, const Term t) +{ + unsigned int hl; + + switch (hidelevelFlag (sys, t)) + { + case HLFLAG_NONE: + return 0; + case HLFLAG_KNOW: + return 0.3; + case HLFLAG_PROT: + return 0.6; + } + return 1; +} + +//! newkeylevel (weighted) +int +newkeylevel (const int level) +{ + // keylevel is from { -1,0,1 } where -1 means delay + if (level == 1) + return 0; + else + return 1; +} + //! Goal selection /** * Selects the most constrained goal. @@ -223,6 +253,7 @@ term_noncevariables_level (const Term t) * 4: consequences determination * 8: select also single variables (that are not role variables) * 16: single variables are better + * 32: incorporate keylevel information * * special tactics for --select-goal * -1: random goal selection @@ -320,13 +351,20 @@ select_goal_masked (const System sys) erode (1, 0.5 * (1 - b->level)); // Bit 2: 4 consequence level erode (1, termBindConsequences (sys, b->term)); - // Bit 3: 8 single variables first + // Bit 3: 8 single variables first (crappy performance, counter-intuitive anyway) erode (1, 1 - isTermVariable (b->term)); // Bit 4: 16 nonce variables level (Cf. what I think is in Athena) erode (1, term_noncevariables_level (b->term)); + // Bit 5: 32 use hidelevel information + erode (1, weighHidelevel (sys, b->term)); + // Bit 5: 64 use hidelevel information + erode (1, 2 * weighHidelevel (sys, b->term)); + // Bit 6: 128 use key level + erode (1, newkeylevel (b->level)); + // Define legal range if (smode > 0) - error ("--goal-select mode %i is illegal", mode); + error ("--heuristic mode %i is illegal", mode); // Weigh result if (buf_weight == 0 || buf_constrain <= min_constrain) diff --git a/src/hidelevel.c b/src/hidelevel.c index d27c4e2..fd7950b 100644 --- a/src/hidelevel.c +++ b/src/hidelevel.c @@ -221,7 +221,7 @@ hidelevelImpossible (const System sys, const Term goalterm) } //! Return flag on the basis of the Hidelevel lemma -int +unsigned int hidelevelFlag (const System sys, const Term goalterm) { unsigned int flag; diff --git a/src/hidelevel.h b/src/hidelevel.h index b24d0a7..a16472c 100644 --- a/src/hidelevel.h +++ b/src/hidelevel.h @@ -22,5 +22,6 @@ void hidelevelCompute (const System sys); int hidelevelInteresting (const System sys, const Term goalterm); int hidelevelImpossible (const System sys, const Term goalterm); +unsigned int hidelevelFlag (const System sys, const Term goalterm); #endif diff --git a/src/switches.c b/src/switches.c index b410161..9d51bfe 100644 --- a/src/switches.c +++ b/src/switches.c @@ -618,7 +618,7 @@ switcher (const int process, int index, int commandline) if (!process) { helptext ("-r, --max-runs=", - "maximum number of runs in the system [defaults to 5]"); + "maximum number of runs in the system [5]"); } else { @@ -824,14 +824,14 @@ switcher (const int process, int index, int commandline) } */ - if (detect (' ', "goal-select", 1)) + if (detect (' ', "heuristic", 1)) { if (!process) { - /* discourage: hide - helptext (" --goal-select=", - "use goal selection method [3]"); - */ + if (switches.expert) + { + helptext (" --heuristic=", "use heuristic [3]"); + } } else {