From: Mark Date: Mon, 20 Nov 2023 17:53:00 +0000 (-0700) Subject: introduce and use the notion of unlimited inference counting in time/1 (#1039, #2009) X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=a234934e50718cc7f8b5b2222a71956fa0926e21;p=scryer-prolog.git 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 69cf2d12..0dff8d77 100644 --- 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 3a2b743f..d18d41f1 100644 --- 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 9758f397..c009a6d1 100644 --- 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 6afce926..9bbc62f1 100644 --- 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 7f682e0a..10ed3da0 100644 --- 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 aa78f1a1..dd27a1ea 100644 --- 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);