sim_lib_logic/
model.rs

1//! Tuning values for the logic organ: search strategy, occurs-check policy,
2//! resource limits, and the aggregate [`LogicConfig`].
3//!
4//! See the [`README`](https://docs.rs/sim-runtime) for how the logic organ
5//! layers concrete resolution over the kernel `Shape` contracts.
6
7use sim_kernel::Symbol;
8
9/// Order in which the resolver explores pending goal states.
10#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
11pub enum SearchStrategy {
12    /// Depth-first search: explore the most recent state first (the default).
13    #[default]
14    Dfs,
15    /// Breadth-first search: explore the oldest pending state first.
16    Bfs,
17    /// Fair search: round-robin over pending states to avoid starvation.
18    Fair,
19}
20
21impl SearchStrategy {
22    /// Parses a strategy from its surface symbol (`dfs`, `bfs`, or `fair`).
23    ///
24    /// Returns `None` for any other symbol name.
25    pub fn from_symbol(symbol: &Symbol) -> Option<Self> {
26        match symbol.name.as_ref() {
27            "dfs" => Some(Self::Dfs),
28            "bfs" => Some(Self::Bfs),
29            "fair" => Some(Self::Fair),
30            _ => None,
31        }
32    }
33
34    /// Returns the surface symbol for this strategy (the inverse of
35    /// [`SearchStrategy::from_symbol`]).
36    pub fn as_symbol(self) -> Symbol {
37        Symbol::new(match self {
38            Self::Dfs => "dfs",
39            Self::Bfs => "bfs",
40            Self::Fair => "fair",
41        })
42    }
43}
44
45/// Whether the unifier runs the occurs check when binding a variable.
46#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
47pub enum OccursCheck {
48    /// Always run the occurs check, rejecting bindings that build cyclic terms
49    /// (the safe default).
50    #[default]
51    Always,
52    /// Skip the occurs check, trusting that terms stay acyclic.
53    TrustedAcyclic,
54}
55
56/// Resource ceilings that bound a single logic query.
57///
58/// Each limit aborts the query with an error rather than looping forever.
59#[derive(Clone, Copy, Debug, PartialEq, Eq)]
60pub struct LogicLimits {
61    /// Maximum resolution depth before the query is aborted.
62    pub max_depth: usize,
63    /// Maximum number of answers to collect, or `None` for unbounded.
64    pub max_answers: Option<usize>,
65    /// Maximum number of pending goals allowed in a single state.
66    pub max_goals: usize,
67    /// Maximum number of candidate clauses scanned across the whole query.
68    pub max_clause_scan: usize,
69}
70
71impl Default for LogicLimits {
72    fn default() -> Self {
73        Self {
74            max_depth: 128,
75            max_answers: Some(256),
76            max_goals: 1024,
77            max_clause_scan: 8192,
78        }
79    }
80}
81
82/// Aggregate tuning for the logic organ, threaded through every query.
83///
84/// Combines [`LogicLimits`], the [`SearchStrategy`], the [`OccursCheck`]
85/// policy, and the indexing/tabling switches.
86#[derive(Clone, Debug, PartialEq, Eq)]
87pub struct LogicConfig {
88    /// Resource ceilings applied to each query.
89    pub limits: LogicLimits,
90    /// Channel buffer size for streamed answers.
91    pub stream_buffer: usize,
92    /// Goal-exploration order.
93    pub strategy: SearchStrategy,
94    /// Occurs-check policy used by the unifier.
95    pub occurs_check: OccursCheck,
96    /// Whether first-argument clause indexing is enabled.
97    pub enable_indexing: bool,
98    /// Whether goal tabling (loop detection) is enabled.
99    pub enable_tabling: bool,
100}
101
102impl Default for LogicConfig {
103    fn default() -> Self {
104        Self {
105            limits: LogicLimits::default(),
106            stream_buffer: 64,
107            strategy: SearchStrategy::Dfs,
108            occurs_check: OccursCheck::Always,
109            enable_indexing: true,
110            enable_tabling: true,
111        }
112    }
113}
sim_lib_logic/model.rs

sim_lib_logic/
model.rs
