具体化的call_with_time_limit / call_with_inference_limit

Question

具体化的call_with_time_limit / call_with_inference_limit

6

我试图定义一个关系callto_status(Goal, Status)，它总是成功的，并根据调用Goal的结果（换句话说，我想实现call_with_inference_limit/3的重新实现版本）统一Status。我的实现使用了SWI的call_with_inference_limit/3，它与call_with_time_limit/3具有相同的接口（这样也可以在该情况下运行）。call_with_..._limit的实现不回溯，因此我认为最好不要给出目标的答案替代的印象。

我引入了助手谓词derivable_st以提高可读性。它处理了成功和超时的情况，但其他情况则失败。

% if Goal succeeds, succeed with Status = true,
% if Goal times out, succeed with Status = timeout
% if Goal fails, fail
derivable_st(Goal, Status) :-
    T = 10000,                               % set inference limit
%    copy_term(Goal, G),                    % work on a copy of Goal, we don't want to report an answer substitution
    call_with_inference_limit(G, T, R),     % actual call to set inference limit
    (  R == !
    -> Status = true                        % succeed deterministically, status = true
    ;  R == true
    -> Status = true                        % succeed non-deterministically, status = true
    ;  (  R == inference_limit_exceeded     % timeout
       -> (
              !,                            % make sure we do not backtrack after timeout
              Status = timeout              % status = timeout
          )
       ;  throw(unhandled_case)             % this should never happen
       )
    ).

主要谓词包裹了“derivable_st”，处理失败情况和可能抛出的异常（如果有）。我们可能想单独处理堆栈溢出（在推理限制过高的情况下发生），但现在我们只报告任何异常。

% if Goal succeeds, succeed with Status = true,
% if Goal times out, succeed with Status = timeout
% if Goal fails, succeed with Status = false
% if Goal throws an error, succeed with Status = exception(The_Exception)
% Goal must be sufficiently instantiated for call(Goal) but will stay unchanged
callto_status(Goal, Status) :-
    catch((  derivable_st(Goal, S)            % try to derive Goal
          -> Status = S                       % in case of success / timeout, pass status on
          ;  Status = false                   % in case of failure, pass failure status on, but succeed
          ),
          Exception,
          Status = exception(Exception)       % wrap the exception into a status term
    ).

谓词可适用于一些简单的测试案例：

?- callto_reif( length(N,X), Status).
Status = true.

?- callto_reif( false, Status).
Status = false.

?- callto_reif( (length(N,X), false), Status).
Status = timeout.

我的问题有点模糊：这个谓词是否确实执行我所声称的功能？您看到任何错误/改进点吗？感谢任何意见！

编辑：根据@false的建议，将copy_term/2注释掉

- lambda.xy.x

1

为什么要使用copy_term/2？约束问题在前面。 - false

1

我希望保持谓词尽可能纯净 - 如果我删除copy_term/2，第一个查询将成功，并且L = []，N = 0，Status = true是唯一的解决方案，这是误导性的。 - lambda.xy.x

FYI - false

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- user502187 · Accepted Answer

这是一个更短的解决方案：

callto_status(Goal, Status) :-
    call_with_inference_limit(Goal, 10000, Status0),
    (Status0 = ! -> !, Status = true; Status = Status0).
callto_status(_, false).

你可以看到原始的 ! 状态是多么有用，它可以避免不必要的选择点：

?- callto_status(member(X,[1,2,3]), Y).
X = 1,
Y = true 
X = 2,
Y = true 
X = 3,
Y = true.

?- callto_status(fail, Y).
Y = false.

当然，您也可以仅将Status0 = ! -> !, Status = true替换为Status0 = ! -> Status = true。这样，您将始终获得一个剩余的选择点：

?- callto_status(member(X,[1,2,3]), Y).
X = 1,
Y = true 
X = 2,
Y = true 
X = 3,
Y = true 
Y = false.

从问题中并不清楚您确切想要什么。