introduce and use the notion of unlimited inference counting in time/1 (#1039, #2009)

diff --git a/build/instructions_template.rs b/build/instructions_template.rs
index 69cf2d12e986837c7c8e566fc61f36f77c384179..0dff8d77f27b89b62639906a0f6531e5219aca57 100644 (file)
--- a/build/instructions_template.rs
+++ b/build/instructions_template.rs
@@ -329,6 +329,11 @@ enum SystemClauseType {
     InstallSCCCleaner,
     #[strum_discriminants(strum(props(Arity = "3", Name = "$install_inference_counter")))]
     InstallInferenceCounter,
+    #[strum_discriminants(strum(props(
+        Arity = "1",
+        Name = "$install_unlimited_inference_counter"
+    )))]
+    InstallUnlimitedInferenceCounter,
     #[strum_discriminants(strum(props(Arity = "1", Name = "$lh_length")))]
     LiftedHeapLength,
     #[strum_discriminants(strum(props(Arity = "3", Name = "$load_library_as_stream")))]
@@ -1720,6 +1725,7 @@ fn generate_instruction_preface() -> TokenStream {
                     &Instruction::CallHeadIsDynamic |
                     &Instruction::CallInstallSCCCleaner |
                     &Instruction::CallInstallInferenceCounter |
+                    &Instruction::CallInstallUnlimitedInferenceCounter |
                     &Instruction::CallLiftedHeapLength |
                     &Instruction::CallLoadLibraryAsStream |
                     &Instruction::CallModuleExists |
@@ -1954,6 +1960,7 @@ fn generate_instruction_preface() -> TokenStream {
                     &Instruction::ExecuteHeadIsDynamic |
                     &Instruction::ExecuteInstallSCCCleaner |
                     &Instruction::ExecuteInstallInferenceCounter |
+                    &Instruction::ExecuteInstallUnlimitedInferenceCounter |
                     &Instruction::ExecuteLiftedHeapLength |
                     &Instruction::ExecuteLoadLibraryAsStream |
                     &Instruction::ExecuteModuleExists |

diff --git a/src/forms.rs b/src/forms.rs
index 3a2b743f2e043b62fcb2514310500c43d7741f73..d18d41f1539a171e8885c1b8fc7fefd8ed15ff40 100644 (file)
--- a/src/forms.rs
+++ b/src/forms.rs
@@ -744,11 +744,11 @@ impl Number {
             Number::Float(f) => Number::Float(OrderedFloat(f.signum())),
             _ => {
                 if self.is_positive() {
-                   if self.is_zero() {
-                       Number::Fixnum(Fixnum::build_with(0))
-                   } else {
-                       Number::Fixnum(Fixnum::build_with(1))
-                   }
+                    if self.is_zero() {
+                        Number::Fixnum(Fixnum::build_with(0))
+                    } else {
+                        Number::Fixnum(Fixnum::build_with(1))
+                    }
                 } else if self.is_negative() {
                     Number::Fixnum(Fixnum::build_with(-1))
                 } else {

diff --git a/src/lib/time.pl b/src/lib/time.pl
index 9758f39733586503c550d0e37a0d07070532444b..c009a6d15d2b9d8b89deaab02ff24fa6e14eb902 100644 (file)
--- a/src/lib/time.pl
+++ b/src/lib/time.pl
@@ -110,22 +110,13 @@ 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((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))),
+                           (   call_cleanup(catch(call_with_unlimited_inference_limit(Goal, Inf, Result),
+                                                  E,
+                                                  (report_time(ID, Inf),throw(E))),
                                             Det = true),
                                time_true(ID, Inf),
                                (   Det == true -> !
@@ -134,11 +125,9 @@ time(Goal) :-
                            ;   report_time(ID, Inf),
                                false
                            ),
-                           retract(time_state(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.
+                           retract(time_state(ID, _))
+                          ),
+        call(Result).
 
 time_true(ID, Inf) :-
         report_time(ID, Inf).
@@ -171,52 +160,48 @@ report_time(ID, Inf) :-
    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.
+
+   call_with_unlimited_inference_limit/3 is introduced with new system
+   predicates '$install_unlimited_inference_counter'/1 and '$inference_count'/1.
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
-:- meta_predicate(call_with_inference_limit(0,?,?,?,?,?)).
+:- meta_predicate(call_with_unlimited_inference_limit(0,?,?)).
+
+:- non_counted_backtracking call_with_unlimited_inference_limit/3.
 
-:- non_counted_backtracking call_with_inference_limit/6.
+call_with_unlimited_inference_limit(G, Inf, Result) :-
+    '$install_unlimited_inference_counter'(Count),
+    '$get_current_block'(Bb),
+    '$get_b_value'(B),
+    call_with_unlimited_inference_limit(G, Bb, B, Count, Inf, Result),
+    '$remove_call_policy_check'(B).
 
-call_with_inference_limit(G, L, R, Bb, B, Diff) :-
+:- non_counted_backtracking call_with_unlimited_inference_limit/6.
+
+call_with_unlimited_inference_limit(G, Bb, _B, Count0, Inf, true) :-
     '$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, _) :-
+    '$remove_inference_counter'(NBb, Count1),
+    Inf is Count1 - Count0,
+    (  '$clean_up_block'(NBb),
+       '$reset_block'(Bb)
+    ;  '$install_unlimited_inference_counter'(_),
+       '$reset_block'(NBb),
+       '$fail'
+    ).
+call_with_unlimited_inference_limit(_, Bb, B, Count0, Inf, false) :-
+    '$get_current_block'(NBb),
+    '$remove_inference_counter'(NBb, Count1),
     '$reset_block'(Bb),
-    '$remove_inference_counter'(B, _),
-    (  '$get_ball'(Ball),
+    '$remove_call_policy_check'(B),
+    (  '$get_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'.
+       '$set_cp_by_default'(Cp),
+       '$pop_from_ball_stack',
+       '$unwind_stack'
+    ;  Inf is Count1 - Count0
+    ).
 
 
 /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

diff --git a/src/machine/dispatch.rs b/src/machine/dispatch.rs
index 6afce9263334c809e96b842211a29c42d3e151f2..9bbc62f186f966d7d002c7df115bdeaec2ceb1b4 100644 (file)
--- a/src/machine/dispatch.rs
+++ b/src/machine/dispatch.rs
@@ -3675,6 +3675,14 @@ impl Machine {
                         try_or_throw!(self.machine_st, self.install_inference_counter());
                         step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
                     }
+                    &Instruction::CallInstallUnlimitedInferenceCounter => {
+                        try_or_throw!(self.machine_st, self.install_unlimited_inference_counter());
+                        step_or_fail!(self, self.machine_st.p += 1);
+                    }
+                    &Instruction::ExecuteInstallUnlimitedInferenceCounter => {
+                        try_or_throw!(self.machine_st, self.install_unlimited_inference_counter());
+                        step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
+                    }
                     &Instruction::CallLiftedHeapLength => {
                         self.lifted_heap_length();
                         step_or_fail!(self, self.machine_st.p += 1);

diff --git a/src/machine/machine_state.rs b/src/machine/machine_state.rs
index 7f682e0a74f6702fd63549cbd100ed283a4d687f..10ed3da02f52649ae8849b740ee69a94e879dac9 100644 (file)
--- a/src/machine/machine_state.rs
+++ b/src/machine/machine_state.rs
@@ -967,7 +967,7 @@ impl MachineState {
 #[allow(clippy::upper_case_acronyms)]
 #[derive(Debug)]
 pub(crate) struct CWIL {
-    count: Integer,
+    pub(crate) count: Integer,
     limits: Vec<(Integer, usize)>,
     pub(crate) inference_limit_exceeded: bool,
 }
@@ -981,16 +981,13 @@ impl CWIL {
         }
     }
 
-    pub(crate) fn add_limit(&mut self, limit: usize, block: usize) -> &Integer {
-        let mut limit = Integer::from(limit);
+    pub(crate) fn add_limit(&mut self, mut limit: Integer, block: usize) {
         limit += &self.count;
 
         match self.limits.last() {
             Some((ref inner_limit, _)) if *inner_limit <= limit => {}
             _ => self.limits.push((limit, block)),
         };
-
-        &self.count
     }
 
     #[inline(always)]

diff --git a/src/machine/system_calls.rs b/src/machine/system_calls.rs
index aa78f1a1079b459d9c85025412e632a06450ed7c..dd27a1eaed3e051bc14ec5f3a3ef286a427abd26 100644 (file)
--- a/src/machine/system_calls.rs
+++ b/src/machine/system_calls.rs
@@ -5516,11 +5516,8 @@ impl Machine {
         let a2 = self.deref_register(2);
 
         let n = match Number::try_from(a2) {
-            Ok(Number::Fixnum(bp)) => bp.get_num() as usize,
-            Ok(Number::Integer(n)) => {
-                let value: usize = (&*n).try_into().unwrap();
-                value
-            }
+            Ok(Number::Fixnum(bp)) => Integer::from(bp.get_num() as usize),
+            Ok(Number::Integer(n)) => (*n).clone(),
             _ => {
                 let stub = functor_stub(atom!("call_with_inference_limit"), 3);
 
@@ -5531,21 +5528,38 @@ impl Machine {
 
         let bp = cell_as_fixnum!(a1).get_num() as usize;
         let a3 = self.deref_register(3);
-        let count = self.machine_st.cwil.add_limit(n, bp);
 
-        let result = count.try_into();
-        if let Ok(value) = result {
-            self.machine_st.unify_fixnum(Fixnum::build_with(value), a3);
-        } else {
-            let count = arena_alloc!(count.clone(), &mut self.machine_st.arena);
-            self.machine_st.unify_big_int(count, a3);
-        }
+        self.machine_st.cwil.add_limit(n, bp);
+        self.inference_count(a3);
+        self.machine_st.increment_call_count_fn = MachineState::increment_call_count;
+
+        Ok(())
+    }
+
+    #[inline(always)]
+    pub(crate) fn install_unlimited_inference_counter(&mut self) -> CallResult {
+        let count_var = self.machine_st.registers[1];
 
+        self.machine_st.cwil.add_limit(Integer::from(-1), 0);
+        self.inference_count(count_var);
         self.machine_st.increment_call_count_fn = MachineState::increment_call_count;
 
         Ok(())
     }
 
+    #[inline(always)]
+    pub(crate) fn inference_count(&mut self, count_var: HeapCellValue) {
+        let count = &self.machine_st.cwil.count;
+
+        if let Ok(value) = count.try_into() {
+            self.machine_st
+                .unify_fixnum(Fixnum::build_with(value), count_var);
+        } else {
+            let count = arena_alloc!(count.clone(), &mut self.machine_st.arena);
+            self.machine_st.unify_big_int(count, count_var);
+        }
+    }
+
     #[inline(always)]
     pub(crate) fn module_exists(&mut self) {
         let module = self.deref_register(1);