Reified call_with_time_limit / call_with_inference_limit

Question

I am trying to define a relation callto_status(Goal, Status) that always succeeds and unifies Status according to the result of calling Goal (in other words, I would like to implement a reified version of call_with_inference_limit/3). My implementation uses SWI's call_with_inference_limit/3 which has the same interface as call_with_time_limit/3 (which should make it work in that case as well). The implementation of call_with_..._limit does not backtrack, so I thought it best not to give the impression of reporting an answer substiution for the goal.

I introduced the helper-predicate derivable_st for readability. It handles the success and timeout case but fails otherwise.

% 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
       )
    ).

The main predicate wraps around derivable_st and handles the failure case and possibly thrown exceptions (if any). We might want to single out stack overflows (that happen in case of too high inference limits) but for now we just report any exception.

% 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
    ).

The predicate works for some simple test cases:

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

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

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

My question now is a bit vague: does this predicate do what I claim it does? Do you see any mistakes / points of improvement? I am grateful for any input!

Edit: as suggested by @false, commented out copy_term/2

I wanted to keep the predicate as pure as possible - if I remove copy_term/2, the first query will succeed with `L=[], N=0, Status=true` as the only solution, which is misleading. — lambda.xy.x, Feb 13 '19 at 21:32

score 1 · Answer 1 · answered Jul 27 '19 at 12:57

1

This is a shorter solution:

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

You see how useful the original ! status is to avoid unnecessary choice point:

?- 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.

You could of course also replace Status0 = ! -> !, Status = true by Status0 = ! -> Status = true only. You would then get always a remaining choice point:

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

Its not clear from the question what you exactly want.

answered Jul 27 '19 at 12:57

Thanks, this solution is quite interesting - but wouldn't I also get the `Status = false` in case the solution for the last goal is non-deterministic? For example, `callto(member(1,[1,1,3]), false).` will succeed, but obviously, the query has a result. – lambda.xy.x Jul 27 '19 at 16:58
Perhaps to clarify: `callto_status(G,S)` should unify `S` with `true`, if `G` has solutions, unify with `false`, if it is not derivable and unify with `timeout`, if none of these can be shown within `T` steps. The predicate should also be able to backtrack on solutions of `G`, but keeping `S` intact. – lambda.xy.x Jul 27 '19 at 17:06

Reified call_with_time_limit / call_with_inference_limit

1 Answers1