From be44ed047a21a9bee5b3a6f2e3d76c2d5ed701bd Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 20 Aug 2004 09:21:39 +0000 Subject: [PATCH] - Fixed some goal selection issues. - Added note about mirroring model checker semantics. --- src/arachne.c | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index d66b51f..7079166 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -682,7 +682,10 @@ printSemiState () //! Goal selection /** - * Should be ordered to prefer most constrained; for now, it is simply the first one encountered. + * Selects the most constrained goal. + * + * Because the list starts with the newest terms, and we use <= (as opposed to <), we + * ensure that for goals with equal constraint levels, we select the oldest one. */ Binding select_goal () @@ -701,15 +704,16 @@ select_goal () b = (Binding) bl->data; if (!b->done) { - // We don't care about singular agent variables, so... - if (! - (isTermVariable (b->term) - && inTermlist (b->term->stype, TERM_Agent))) + // We don't care about singular variables. + /** + * Note that to mirror the modelchecker semantics, we should check whether the type exists in M_0. + */ + if (!isTermVariable (b->term)) { float cons; cons = term_constrain_level (b->term); - if (cons < min_constrain) + if (cons <= min_constrain) { min_constrain = cons; best = b;