oxiz_theories/
theory.rs

1//! Theory trait and common types
2
3use oxiz_core::ast::TermId;
4use oxiz_core::error::Result;
5
6/// Unique identifier for a theory
7#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
8pub enum TheoryId {
9    /// Boolean theory (always present)
10    Bool,
11    /// Equality with Uninterpreted Functions
12    EUF,
13    /// Linear Real Arithmetic
14    LRA,
15    /// Linear Integer Arithmetic
16    LIA,
17    /// BitVectors
18    BV,
19    /// Arrays
20    Arrays,
21    /// Floating-Point (IEEE 754)
22    FP,
23    /// Algebraic Datatypes
24    Datatype,
25    /// Strings and Regular Expressions
26    Strings,
27}
28
29/// Result of a theory check
30#[derive(Debug, Clone)]
31pub enum TheoryResult {
32    /// The theory constraints are satisfiable
33    Sat,
34    /// The theory constraints are unsatisfiable with explanation
35    Unsat(Vec<TermId>),
36    /// Need to propagate these literals
37    Propagate(Vec<(TermId, Vec<TermId>)>),
38    /// Unknown (incomplete theory)
39    Unknown,
40}
41
42/// Trait for theory solvers
43pub trait Theory: Send + Sync {
44    /// Get the theory identifier
45    fn id(&self) -> TheoryId;
46
47    /// Get the name of this theory
48    fn name(&self) -> &str;
49
50    /// Check if this theory can handle a term
51    fn can_handle(&self, term: TermId) -> bool;
52
53    /// Assert a term as true
54    fn assert_true(&mut self, term: TermId) -> Result<TheoryResult>;
55
56    /// Assert a term as false
57    fn assert_false(&mut self, term: TermId) -> Result<TheoryResult>;
58
59    /// Check consistency of current assertions
60    fn check(&mut self) -> Result<TheoryResult>;
61
62    /// Push a context level
63    fn push(&mut self);
64
65    /// Pop a context level
66    fn pop(&mut self);
67
68    /// Reset the theory solver
69    fn reset(&mut self);
70
71    /// Get the current model (if satisfiable)
72    fn get_model(&self) -> Vec<(TermId, TermId)> {
73        Vec::new()
74    }
75}
76
77/// Equality notification for Nelson-Oppen theory combination
78/// When one theory derives that two terms are equal, it notifies other theories
79#[derive(Debug, Clone, Copy, PartialEq, Eq)]
80pub struct EqualityNotification {
81    /// Left-hand side of the equality
82    pub lhs: TermId,
83    /// Right-hand side of the equality
84    pub rhs: TermId,
85    /// The reason/justification for this equality (for proof generation)
86    pub reason: Option<TermId>,
87}
88
89/// Interface for theory combination via Nelson-Oppen
90/// Theories implement this to participate in equality sharing
91pub trait TheoryCombination {
92    /// Notify the theory of a new equality derived by another theory
93    /// Returns true if the equality was accepted and processed
94    fn notify_equality(&mut self, eq: EqualityNotification) -> bool;
95
96    /// Get all equalities derived by this theory that should be shared
97    /// These are equalities between terms that appear in multiple theories
98    fn get_shared_equalities(&self) -> Vec<EqualityNotification>;
99
100    /// Check if a term is relevant to this theory
101    fn is_relevant(&self, term: TermId) -> bool;
102}
oxiz_theories/theory.rs

oxiz_theories/
theory.rs
