From: Markus Triska <triska@metalevel.at>
Date: Tue, 5 Sep 2023 18:47:16 +0000 (+0200)
Subject: ENHANCED: time/1 now shows the number of inferences
X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=e6acfa43adf61e62bd5410574719f137f508d5cc;p=scryer-prolog.git

ENHANCED: time/1 now shows the number of inferences
---

diff --git a/src/lib/time.pl b/src/lib/time.pl
index 003f623b..9758f397 100644
--- a/src/lib/time.pl
+++ b/src/lib/time.pl
@@ -110,62 +110,135 @@ time_next_id(N) :-
 %
 %  Reports the execution time of Goal.
 
+setup_block(Bb, B) :-
+        '$get_current_block'(Bb),
+        '$get_b_value'(B).
+
+remove_call_policy_check(B) :-
+        '$remove_call_policy_check'(B).
+
 time(Goal) :-
         '$cpu_now'(T0),
+        upper_inference(U),
         time_next_id(ID),
         setup_call_cleanup(asserta(time_state(ID, T0)),
-                           (   call_cleanup(catch(Goal, E, (report_time(ID),throw(E))),
+                           (   call_cleanup(catch((setup_block(Bb, B),
+                                                   call_with_inference_limit(Goal, U, _, Bb, B, Inf),
+                                                   remove_call_policy_check(B))
+, E, (report_time(ID, Inf),throw(E))),
                                             Det = true),
-                               time_true(ID),
+                               time_true(ID, Inf),
                                (   Det == true -> !
                                ;   true
                                )
-                           ;   report_time(ID),
+                           ;   report_time(ID, Inf),
                                false
                            ),
                            retract(time_state(ID, _))).
 
-time_true(ID) :-
-        report_time(ID).
-time_true(ID)  :-
+% use a high inference limit so that we can use the limit-based logic
+% for counting inferences which already exists in the engine.
+upper_inference(U) :- U is 2<<222.
+
+time_true(ID, Inf) :-
+        report_time(ID, Inf).
+time_true(ID, _)  :-
         % on backtracking, update the stored CPU time for this ID
         retract(time_state(ID, _)),
         '$cpu_now'(T0),
         asserta(time_state(ID, T0)),
         false.
 
-report_time(ID) :-
+report_time(ID, Inf) :-
         time_state(ID, T0),
         '$cpu_now'(T),
         Time is T - T0,
+        (   var(Inf) ->
+            Infs = ""
+        ;   (   Inf =:= 1 -> Infs = ", 1 inference"
+            ;   phrase(format_(", ~U inferences", [Inf]), Infs)
+            )
+        ),
         (   bb_get('$answer_count', 0) ->
             Pre = "   ", Post = ""
         ;   Pre = "", Post = "   "
         ),
-        format("~s% CPU time: ~3fs~n~s", [Pre,Time,Post]).
+        format("~s% ~3fs CPU~s~n~s", [Pre,Time,Infs,Post]).
+
+
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   The following is from library(iso_ext), slightly adapted so that we
+   can report the number of inferences. A better abstraction may be
+   able to share more inferences-related logic between time/1 and
+   call_with_inference_limit/3.
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+
+:- meta_predicate(call_with_inference_limit(0,?,?,?,?,?)).
+
+:- non_counted_backtracking call_with_inference_limit/6.
+
+call_with_inference_limit(G, L, R, Bb, B, Diff) :-
+    '$install_new_block'(NBb),
+    '$install_inference_counter'(B, L, Count0),
+    '$call_with_inference_counting'(call(G)),
+    '$inference_level'(R, B),
+    '$remove_inference_counter'(B, Count1),
+    Diff is Count1 - Count0,
+    end_block(B, Bb, NBb, Diff).
+call_with_inference_limit(_, _, R, Bb, B, _) :-
+    '$reset_block'(Bb),
+    '$remove_inference_counter'(B, _),
+    (  '$get_ball'(Ball),
+       '$push_ball_stack',
+       '$get_cp'(Cp),
+       '$set_cp_by_default'(Cp)
+    ;  '$remove_call_policy_check'(B),
+       '$fail'
+    ),
+    handle_ile(B, Ball, R).
+
+
+:- non_counted_backtracking end_block/4.
+
+end_block(_, Bb, NBb, _L) :-
+    '$clean_up_block'(NBb),
+    '$reset_block'(Bb).
+end_block(B, _Bb, NBb, L) :-
+    '$install_inference_counter'(B, L, _),
+    '$reset_block'(NBb),
+    '$fail'.
+
+:- non_counted_backtracking handle_ile/3.
+
+handle_ile(B, inference_limit_exceeded(B), _) :-
+    throw(error(representation_error(inference_limit), time/1)).
+handle_ile(B, L, _) :-
+     L \= inference_limit_exceeded(_),
+    '$remove_call_policy_check'(B),
+    '$pop_from_ball_stack',
+    '$unwind_stack'.
+
 
 /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
 ?- time((true;false)).
-%@    % CPU time: 0.006s
+%@    % 0.000s CPU, 2 inferences
 %@    true
-%@ ;  % CPU time: 0.001s
+%@ ;  % 0.000s CPU
 %@    false.
 
 :- time(use_module(library(clpz))).
-%@    % CPU time: 3.711s
+%@    % 0.322s CPU, 406_433 inferences
 %@    true.
 
 :- time(use_module(library(lists))).
-%@    % CPU time: 0.006s
+%@    % 0.000s CPU, 20 inferences
 %@    true.
 
 ?- time(member(X, "abc")).
-%@    % CPU time: 0.005s
+%@    % 0.000s CPU, 2 inferences
 %@    X = a
-%@ ;  % CPU time: 0.000s
+%@ ;  % 0.000s CPU, 4 inferences
 %@    X = b
-%@ ;  % CPU time: 0.000s
-%@    X = c
-%@ ;  % CPU time: 0.000s
-%@    false.
+%@ ;  % 0.000s CPU, 6 inferences
+%@    X = c.
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */