pumpkin_checking/
inference_checker.rs

1use std::fmt::Debug;
2
3use dyn_clone::DynClone;
4
5use crate::AtomicConstraint;
6use crate::VariableState;
7
8/// An inference checker tests whether the given state is a conflict under the sematics of an
9/// inference rule.
10pub trait InferenceChecker<Atomic: AtomicConstraint>: Debug + DynClone {
11    /// Returns `true` if `state` is a conflict, and `false` if not.
12    ///
13    /// For the conflict check, all the premises are true in the state and the consequent, if
14    /// present, is false.
15    fn check(
16        &self,
17        state: VariableState<Atomic>,
18        premises: &[Atomic],
19        consequent: Option<&Atomic>,
20    ) -> bool;
21}
22
23/// Wrapper around `Box<dyn InferenceChecker<Atomic>>` that implements [`Clone`].
24#[derive(Debug)]
25pub struct BoxedChecker<Atomic: AtomicConstraint>(Box<dyn InferenceChecker<Atomic>>);
26
27impl<Atomic: AtomicConstraint> Clone for BoxedChecker<Atomic> {
28    fn clone(&self) -> Self {
29        BoxedChecker(dyn_clone::clone_box(&*self.0))
30    }
31}
32
33impl<Atomic: AtomicConstraint> From<Box<dyn InferenceChecker<Atomic>>> for BoxedChecker<Atomic> {
34    fn from(value: Box<dyn InferenceChecker<Atomic>>) -> Self {
35        BoxedChecker(value)
36    }
37}
38
39impl<Atomic: AtomicConstraint> BoxedChecker<Atomic> {
40    /// See [`InferenceChecker::check`].
41    pub fn check(
42        &self,
43        variable_state: VariableState<Atomic>,
44        premises: &[Atomic],
45        consequent: Option<&Atomic>,
46    ) -> bool {
47        self.0.check(variable_state, premises, consequent)
48    }
49}
pumpkin_checking/inference_checker.rs

pumpkin_checking/
inference_checker.rs
