oxilean_std/bool/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, InductiveEnv, Level, Name};
7
8/// A simple Kleene three-valued logic evaluator.
9#[allow(dead_code)]
10#[derive(Debug, Clone, Copy, PartialEq, Eq)]
11pub enum Kleene3Val {
12    /// Definitely false.
13    False,
14    /// Unknown/undecided.
15    Unknown,
16    /// Definitely true.
17    True,
18}
19impl Kleene3Val {
20    /// Kleene NOT operation.
21    #[allow(dead_code)]
22    pub fn not(self) -> Self {
23        match self {
24            Kleene3Val::True => Kleene3Val::False,
25            Kleene3Val::False => Kleene3Val::True,
26            Kleene3Val::Unknown => Kleene3Val::Unknown,
27        }
28    }
29    /// Kleene AND operation: min of values.
30    #[allow(dead_code)]
31    pub fn and(self, other: Self) -> Self {
32        match (self, other) {
33            (Kleene3Val::False, _) | (_, Kleene3Val::False) => Kleene3Val::False,
34            (Kleene3Val::True, Kleene3Val::True) => Kleene3Val::True,
35            _ => Kleene3Val::Unknown,
36        }
37    }
38    /// Kleene OR operation: max of values.
39    #[allow(dead_code)]
40    pub fn or(self, other: Self) -> Self {
41        match (self, other) {
42            (Kleene3Val::True, _) | (_, Kleene3Val::True) => Kleene3Val::True,
43            (Kleene3Val::False, Kleene3Val::False) => Kleene3Val::False,
44            _ => Kleene3Val::Unknown,
45        }
46    }
47    /// Convert from Bool to Kleene3.
48    #[allow(dead_code)]
49    pub fn from_bool(b: bool) -> Self {
50        if b {
51            Kleene3Val::True
52        } else {
53            Kleene3Val::False
54        }
55    }
56}
57/// A complete truth table for a 2-input boolean function.
58#[allow(dead_code)]
59#[derive(Debug, Clone)]
60pub struct TruthTable {
61    /// All four entries (FF, FT, TF, TT).
62    pub entries: [TruthTableEntry; 4],
63    /// Name of the operation.
64    pub name: &'static str,
65}
66impl TruthTable {
67    /// Compute the truth table for a given 2-input function.
68    #[allow(dead_code)]
69    pub fn compute(name: &'static str, f: fn(bool, bool) -> bool) -> Self {
70        Self {
71            name,
72            entries: [
73                TruthTableEntry {
74                    a: false,
75                    b: false,
76                    output: f(false, false),
77                },
78                TruthTableEntry {
79                    a: false,
80                    b: true,
81                    output: f(false, true),
82                },
83                TruthTableEntry {
84                    a: true,
85                    b: false,
86                    output: f(true, false),
87                },
88                TruthTableEntry {
89                    a: true,
90                    b: true,
91                    output: f(true, true),
92                },
93            ],
94        }
95    }
96    /// Look up the output for given inputs.
97    #[allow(dead_code)]
98    pub fn lookup(&self, a: bool, b: bool) -> bool {
99        self.entries
100            .iter()
101            .find(|e| e.a == a && e.b == b)
102            .map(|e| e.output)
103            .expect("Truth table must have all 4 entries")
104    }
105    /// Check if the function is commutative: f(a,b) == f(b,a) for all inputs.
106    #[allow(dead_code)]
107    pub fn is_commutative(&self) -> bool {
108        self.lookup(true, false) == self.lookup(false, true)
109    }
110    /// Check if the function always returns true (tautology).
111    #[allow(dead_code)]
112    pub fn is_tautology(&self) -> bool {
113        self.entries.iter().all(|e| e.output)
114    }
115    /// Check if the function always returns false (contradiction).
116    #[allow(dead_code)]
117    pub fn is_contradiction(&self) -> bool {
118        self.entries.iter().all(|e| !e.output)
119    }
120    /// Count the number of true outputs.
121    #[allow(dead_code)]
122    pub fn true_count(&self) -> usize {
123        self.entries.iter().filter(|e| e.output).count()
124    }
125}
126/// Decidable predicate: a predicate P: T -> Bool computable at runtime.
127#[allow(dead_code)]
128pub struct DecidablePred<T> {
129    /// The underlying decision procedure.
130    pub decide: Box<dyn Fn(&T) -> bool>,
131    /// Name of this predicate for display.
132    pub name: String,
133}
134/// SAT instance: a propositional formula in conjunctive normal form.
135#[allow(dead_code)]
136pub struct SATInstance {
137    /// Number of variables.
138    pub num_vars: usize,
139    /// Clauses as disjunctions of literals (positive = var index, negative = -(var index+1)).
140    pub clauses: Vec<Vec<i32>>,
141}
142impl SATInstance {
143    /// Create a new empty SAT instance with given number of variables.
144    #[allow(dead_code)]
145    pub fn new(num_vars: usize) -> Self {
146        SATInstance {
147            num_vars,
148            clauses: Vec::new(),
149        }
150    }
151    /// Add a clause to the SAT instance.
152    #[allow(dead_code)]
153    pub fn add_clause(&mut self, clause: Vec<i32>) {
154        self.clauses.push(clause);
155    }
156    /// Naive SAT solver by exhaustive enumeration.
157    #[allow(dead_code)]
158    pub fn solve(&self) -> Option<Vec<bool>> {
159        let n = self.num_vars;
160        for mask in 0..(1u64 << n) {
161            let assignment: Vec<bool> = (0..n).map(|i| (mask >> i) & 1 == 1).collect();
162            if self.evaluate(&assignment) {
163                return Some(assignment);
164            }
165        }
166        None
167    }
168    /// Evaluate all clauses under a given assignment.
169    #[allow(dead_code)]
170    pub fn evaluate(&self, assignment: &[bool]) -> bool {
171        self.clauses.iter().all(|clause| {
172            clause.iter().any(|&lit| {
173                if lit > 0 {
174                    assignment.get((lit - 1) as usize).copied().unwrap_or(false)
175                } else {
176                    !assignment.get((-lit - 1) as usize).copied().unwrap_or(true)
177                }
178            })
179        })
180    }
181}
182/// A boolean expression tree used to represent propositional formulas.
183#[allow(dead_code)]
184#[derive(Debug, Clone, PartialEq)]
185pub enum BoolExpr {
186    /// A constant boolean value.
187    Const(bool),
188    /// A named variable.
189    Var(String),
190    /// Logical NOT.
191    Not(Box<BoolExpr>),
192    /// Logical AND.
193    And(Box<BoolExpr>, Box<BoolExpr>),
194    /// Logical OR.
195    Or(Box<BoolExpr>, Box<BoolExpr>),
196    /// Logical XOR.
197    Xor(Box<BoolExpr>, Box<BoolExpr>),
198    /// Logical implication (a → b = ¬a ∨ b).
199    Implies(Box<BoolExpr>, Box<BoolExpr>),
200    /// Logical IFF (biconditional).
201    Iff(Box<BoolExpr>, Box<BoolExpr>),
202}
203impl BoolExpr {
204    /// Evaluate the expression under a variable assignment.
205    ///
206    /// Returns `None` if any variable is unassigned.
207    #[allow(dead_code)]
208    pub fn eval(&self, env: &std::collections::HashMap<&str, bool>) -> Option<bool> {
209        match self {
210            BoolExpr::Const(b) => Some(*b),
211            BoolExpr::Var(name) => env.get(name.as_str()).copied(),
212            BoolExpr::Not(e) => e.eval(env).map(|b| !b),
213            BoolExpr::And(l, r) => Some(l.eval(env)? && r.eval(env)?),
214            BoolExpr::Or(l, r) => Some(l.eval(env)? || r.eval(env)?),
215            BoolExpr::Xor(l, r) => Some(l.eval(env)? ^ r.eval(env)?),
216            BoolExpr::Implies(l, r) => Some(!l.eval(env)? || r.eval(env)?),
217            BoolExpr::Iff(l, r) => Some(l.eval(env)? == r.eval(env)?),
218        }
219    }
220    /// Collect all variable names in this expression.
221    #[allow(dead_code)]
222    pub fn variables(&self) -> Vec<String> {
223        let mut vars = Vec::new();
224        self.collect_vars(&mut vars);
225        vars
226    }
227    fn collect_vars(&self, vars: &mut Vec<String>) {
228        match self {
229            BoolExpr::Var(name) => {
230                if !vars.contains(name) {
231                    vars.push(name.clone());
232                }
233            }
234            BoolExpr::Not(e) => e.collect_vars(vars),
235            BoolExpr::And(l, r)
236            | BoolExpr::Or(l, r)
237            | BoolExpr::Xor(l, r)
238            | BoolExpr::Implies(l, r)
239            | BoolExpr::Iff(l, r) => {
240                l.collect_vars(vars);
241                r.collect_vars(vars);
242            }
243            BoolExpr::Const(_) => {}
244        }
245    }
246    /// Check if the expression is a tautology by enumerating all assignments.
247    #[allow(dead_code)]
248    pub fn is_tautology(&self) -> bool {
249        let vars = self.variables();
250        let n = vars.len();
251        for mask in 0..(1u64 << n) {
252            let mut env = std::collections::HashMap::new();
253            for (i, var) in vars.iter().enumerate() {
254                env.insert(var.as_str(), (mask >> i) & 1 == 1);
255            }
256            if self.eval(&env) != Some(true) {
257                return false;
258            }
259        }
260        true
261    }
262}
263/// XOR monoid structure: (Bool, XOR, false) is a commutative group.
264#[allow(dead_code)]
265pub struct XorMonoid {
266    /// Identity element is false.
267    pub identity: bool,
268    /// XOR is associative and commutative.
269    pub associative: bool,
270    /// Every element is its own inverse: a XOR a = false.
271    pub self_inverse: bool,
272}
273/// Boolean algebra structure witnessing the laws of a Boolean algebra.
274#[allow(dead_code)]
275pub struct BoolAlgebra {
276    /// The carrier set size (2 for the standard Boolean algebra B2).
277    pub carrier_size: usize,
278    /// Whether complementation is involutive: ¬¬a = a.
279    pub involutive: bool,
280    /// Whether the structure satisfies De Morgan laws.
281    pub de_morgan: bool,
282}
283/// Boolean lattice structure: (Bool, OR=join, AND=meet, false=bot, true=top).
284#[allow(dead_code)]
285pub struct BoolLattice {
286    /// Bottom element (false).
287    pub bottom: bool,
288    /// Top element (true).
289    pub top: bool,
290    /// Is this a distributive lattice?
291    pub distributive: bool,
292    /// Is this a complemented lattice?
293    pub complemented: bool,
294}
295/// A truth table entry for a 2-input boolean function.
296#[allow(dead_code)]
297#[derive(Debug, Clone, Copy, PartialEq, Eq)]
298pub struct TruthTableEntry {
299    /// Input a.
300    pub a: bool,
301    /// Input b.
302    pub b: bool,
303    /// Output value.
304    pub output: bool,
305}
oxilean_std/bool/types.rs

oxilean_std/bool/
types.rs
