oxiz_proof/
metadata.rs

1//! Proof node metadata and annotations.
2//!
3//! This module provides a flexible metadata system for annotating proof nodes
4//! with additional information useful for proof search, analysis, and debugging.
5
6use rustc_hash::FxHashMap;
7use std::fmt;
8
9#[cfg(feature = "serde")]
10use serde::{Deserialize, Serialize};
11
12/// Priority level for proof nodes (for proof search guidance).
13#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
14#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
15pub enum Priority {
16    /// Lowest priority
17    VeryLow,
18    /// Low priority
19    Low,
20    /// Normal priority (default)
21    #[default]
22    Normal,
23    /// High priority
24    High,
25    /// Highest priority
26    VeryHigh,
27}
28
29impl fmt::Display for Priority {
30    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
31        match self {
32            Priority::VeryLow => write!(f, "very-low"),
33            Priority::Low => write!(f, "low"),
34            Priority::Normal => write!(f, "normal"),
35            Priority::High => write!(f, "high"),
36            Priority::VeryHigh => write!(f, "very-high"),
37        }
38    }
39}
40
41/// Difficulty estimate for proof steps.
42#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
43#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
44pub enum Difficulty {
45    /// Trivial step (e.g., axiom, reflexivity)
46    Trivial,
47    /// Easy step (e.g., simple resolution)
48    Easy,
49    /// Medium difficulty
50    #[default]
51    Medium,
52    /// Hard step (e.g., complex theory reasoning)
53    Hard,
54    /// Very hard step (e.g., quantifier instantiation)
55    VeryHard,
56}
57
58impl fmt::Display for Difficulty {
59    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
60        match self {
61            Difficulty::Trivial => write!(f, "trivial"),
62            Difficulty::Easy => write!(f, "easy"),
63            Difficulty::Medium => write!(f, "medium"),
64            Difficulty::Hard => write!(f, "hard"),
65            Difficulty::VeryHard => write!(f, "very-hard"),
66        }
67    }
68}
69
70/// Strategy hint for proof search.
71#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
72#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
73pub enum Strategy {
74    /// Case splitting
75    CaseSplit,
76    /// Induction
77    Induction,
78    /// Contradiction
79    Contradiction,
80    /// Resolution-based
81    Resolution,
82    /// Theory reasoning
83    Theory,
84    /// Quantifier instantiation
85    Quantifier,
86    /// Rewriting
87    Rewrite,
88    /// Simplification
89    Simplify,
90}
91
92impl fmt::Display for Strategy {
93    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
94        match self {
95            Strategy::CaseSplit => write!(f, "case-split"),
96            Strategy::Induction => write!(f, "induction"),
97            Strategy::Contradiction => write!(f, "contradiction"),
98            Strategy::Resolution => write!(f, "resolution"),
99            Strategy::Theory => write!(f, "theory"),
100            Strategy::Quantifier => write!(f, "quantifier"),
101            Strategy::Rewrite => write!(f, "rewrite"),
102            Strategy::Simplify => write!(f, "simplify"),
103        }
104    }
105}
106
107/// Metadata attached to a proof node.
108#[derive(Debug, Clone, Default)]
109#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
110pub struct ProofMetadata {
111    /// Priority level
112    priority: Priority,
113    /// Difficulty estimate
114    difficulty: Difficulty,
115    /// Strategy hints
116    strategies: Vec<Strategy>,
117    /// User-defined tags
118    tags: Vec<String>,
119    /// Custom key-value attributes
120    attributes: FxHashMap<String, String>,
121    /// Optional description
122    description: Option<String>,
123}
124
125impl ProofMetadata {
126    /// Create new empty metadata.
127    #[must_use]
128    pub fn new() -> Self {
129        Self::default()
130    }
131
132    /// Set priority level.
133    pub fn with_priority(mut self, priority: Priority) -> Self {
134        self.priority = priority;
135        self
136    }
137
138    /// Set difficulty estimate.
139    pub fn with_difficulty(mut self, difficulty: Difficulty) -> Self {
140        self.difficulty = difficulty;
141        self
142    }
143
144    /// Add a strategy hint.
145    pub fn with_strategy(mut self, strategy: Strategy) -> Self {
146        self.strategies.push(strategy);
147        self
148    }
149
150    /// Add a tag.
151    pub fn with_tag(mut self, tag: impl Into<String>) -> Self {
152        self.tags.push(tag.into());
153        self
154    }
155
156    /// Set description.
157    pub fn with_description(mut self, description: impl Into<String>) -> Self {
158        self.description = Some(description.into());
159        self
160    }
161
162    /// Add a custom attribute.
163    pub fn with_attribute(mut self, key: impl Into<String>, value: impl Into<String>) -> Self {
164        self.attributes.insert(key.into(), value.into());
165        self
166    }
167
168    /// Get priority level.
169    #[must_use]
170    pub fn priority(&self) -> Priority {
171        self.priority
172    }
173
174    /// Get difficulty estimate.
175    #[must_use]
176    pub fn difficulty(&self) -> Difficulty {
177        self.difficulty
178    }
179
180    /// Get strategy hints.
181    #[must_use]
182    pub fn strategies(&self) -> &[Strategy] {
183        &self.strategies
184    }
185
186    /// Get tags.
187    #[must_use]
188    pub fn tags(&self) -> &[String] {
189        &self.tags
190    }
191
192    /// Get description.
193    #[must_use]
194    pub fn description(&self) -> Option<&str> {
195        self.description.as_deref()
196    }
197
198    /// Get custom attribute.
199    #[must_use]
200    pub fn get_attribute(&self, key: &str) -> Option<&str> {
201        self.attributes.get(key).map(|s| s.as_str())
202    }
203
204    /// Get all custom attributes.
205    #[must_use]
206    pub fn attributes(&self) -> &FxHashMap<String, String> {
207        &self.attributes
208    }
209
210    /// Check if has tag.
211    #[must_use]
212    pub fn has_tag(&self, tag: &str) -> bool {
213        self.tags.iter().any(|t| t == tag)
214    }
215
216    /// Check if has strategy.
217    #[must_use]
218    pub fn has_strategy(&self, strategy: Strategy) -> bool {
219        self.strategies.contains(&strategy)
220    }
221
222    /// Set priority (mutable).
223    pub fn set_priority(&mut self, priority: Priority) {
224        self.priority = priority;
225    }
226
227    /// Set difficulty (mutable).
228    pub fn set_difficulty(&mut self, difficulty: Difficulty) {
229        self.difficulty = difficulty;
230    }
231
232    /// Add strategy (mutable).
233    pub fn add_strategy(&mut self, strategy: Strategy) {
234        if !self.strategies.contains(&strategy) {
235            self.strategies.push(strategy);
236        }
237    }
238
239    /// Add tag (mutable).
240    pub fn add_tag(&mut self, tag: impl Into<String>) {
241        let tag = tag.into();
242        if !self.tags.contains(&tag) {
243            self.tags.push(tag);
244        }
245    }
246
247    /// Set attribute (mutable).
248    pub fn set_attribute(&mut self, key: impl Into<String>, value: impl Into<String>) {
249        self.attributes.insert(key.into(), value.into());
250    }
251
252    /// Remove tag.
253    pub fn remove_tag(&mut self, tag: &str) -> bool {
254        if let Some(pos) = self.tags.iter().position(|t| t == tag) {
255            self.tags.remove(pos);
256            true
257        } else {
258            false
259        }
260    }
261
262    /// Clear all metadata.
263    pub fn clear(&mut self) {
264        self.priority = Priority::default();
265        self.difficulty = Difficulty::default();
266        self.strategies.clear();
267        self.tags.clear();
268        self.attributes.clear();
269        self.description = None;
270    }
271}
272
273#[cfg(test)]
274mod tests {
275    use super::*;
276
277    #[test]
278    fn test_metadata_creation() {
279        let meta = ProofMetadata::new()
280            .with_priority(Priority::High)
281            .with_difficulty(Difficulty::Hard)
282            .with_strategy(Strategy::Resolution)
283            .with_tag("important")
284            .with_description("Critical proof step");
285
286        assert_eq!(meta.priority(), Priority::High);
287        assert_eq!(meta.difficulty(), Difficulty::Hard);
288        assert!(meta.has_strategy(Strategy::Resolution));
289        assert!(meta.has_tag("important"));
290        assert_eq!(meta.description(), Some("Critical proof step"));
291    }
292
293    #[test]
294    fn test_metadata_attributes() {
295        let meta = ProofMetadata::new()
296            .with_attribute("author", "Alice")
297            .with_attribute("timestamp", "2024-01-01");
298
299        assert_eq!(meta.get_attribute("author"), Some("Alice"));
300        assert_eq!(meta.get_attribute("timestamp"), Some("2024-01-01"));
301        assert_eq!(meta.get_attribute("nonexistent"), None);
302    }
303
304    #[test]
305    fn test_metadata_mutation() {
306        let mut meta = ProofMetadata::new();
307        meta.set_priority(Priority::VeryHigh);
308        meta.set_difficulty(Difficulty::Trivial);
309        meta.add_strategy(Strategy::Simplify);
310        meta.add_tag("automated");
311
312        assert_eq!(meta.priority(), Priority::VeryHigh);
313        assert_eq!(meta.difficulty(), Difficulty::Trivial);
314        assert!(meta.has_strategy(Strategy::Simplify));
315        assert!(meta.has_tag("automated"));
316    }
317
318    #[test]
319    fn test_metadata_removal() {
320        let mut meta = ProofMetadata::new().with_tag("temp").with_tag("keep");
321
322        assert!(meta.remove_tag("temp"));
323        assert!(!meta.has_tag("temp"));
324        assert!(meta.has_tag("keep"));
325        assert!(!meta.remove_tag("nonexistent"));
326    }
327
328    #[test]
329    fn test_priority_ordering() {
330        assert!(Priority::VeryHigh > Priority::High);
331        assert!(Priority::High > Priority::Normal);
332        assert!(Priority::Normal > Priority::Low);
333        assert!(Priority::Low > Priority::VeryLow);
334    }
335
336    #[test]
337    fn test_difficulty_ordering() {
338        assert!(Difficulty::VeryHard > Difficulty::Hard);
339        assert!(Difficulty::Hard > Difficulty::Medium);
340        assert!(Difficulty::Medium > Difficulty::Easy);
341        assert!(Difficulty::Easy > Difficulty::Trivial);
342    }
343
344    #[test]
345    fn test_metadata_clear() {
346        let mut meta = ProofMetadata::new()
347            .with_priority(Priority::High)
348            .with_tag("test");
349
350        meta.clear();
351        assert_eq!(meta.priority(), Priority::Normal);
352        assert!(!meta.has_tag("test"));
353    }
354
355    #[test]
356    fn test_strategy_display() {
357        assert_eq!(Strategy::CaseSplit.to_string(), "case-split");
358        assert_eq!(Strategy::Resolution.to_string(), "resolution");
359        assert_eq!(Strategy::Quantifier.to_string(), "quantifier");
360    }
361
362    #[test]
363    fn test_multiple_strategies() {
364        let meta = ProofMetadata::new()
365            .with_strategy(Strategy::Resolution)
366            .with_strategy(Strategy::Theory);
367
368        assert_eq!(meta.strategies().len(), 2);
369        assert!(meta.has_strategy(Strategy::Resolution));
370        assert!(meta.has_strategy(Strategy::Theory));
371        assert!(!meta.has_strategy(Strategy::Induction));
372    }
373
374    #[test]
375    fn test_duplicate_tag_prevention() {
376        let mut meta = ProofMetadata::new();
377        meta.add_tag("unique");
378        meta.add_tag("unique");
379
380        assert_eq!(meta.tags().len(), 1);
381    }
382}
oxiz_proof/metadata.rs

oxiz_proof/
metadata.rs
