logic_eval/
lib.rs

1#![doc = include_str!("../README.md")]
2
3mod parse;
4mod prove;
5
6// === Re-exports ===
7
8pub use parse::{
9    inner::VAR_PREFIX,
10    inner::{parse_str, Parse},
11    repr::{Clause, ClauseDataset, Expr, Predicate, Term},
12    text::Name,
13};
14pub use prove::{
15    db::{ClauseIter, ClauseRef, Database},
16    prover::ProveCx,
17};
18
19pub mod intern {
20    pub use any_intern::*;
21}
22
23use std::{
24    borrow::Borrow,
25    collections::{HashMap, HashSet},
26    error::Error as StdError,
27    fmt::{self, Debug, Display},
28    hash::{BuildHasherDefault, Hash, Hasher},
29    result::Result as StdResult,
30    sync::{Arc, Mutex},
31};
32
33// === Hash map and set used within this crate ===
34
35pub(crate) type Map<K, V> = HashMap<K, V, fxhash::FxBuildHasher>;
36
37#[derive(Default, Clone, Copy)]
38struct PassThroughHasher {
39    hash: u64,
40}
41
42impl Hasher for PassThroughHasher {
43    fn write(&mut self, _bytes: &[u8]) {
44        panic!("u64 is only allowed");
45    }
46
47    fn write_u64(&mut self, i: u64) {
48        self.hash = i;
49    }
50
51    fn finish(&self) -> u64 {
52        self.hash
53    }
54}
55
56pub(crate) type PassThroughState = BuildHasherDefault<PassThroughHasher>;
57
58// === Result/Error used within this crate ===
59
60pub(crate) type Result<T> = StdResult<T, Error>;
61pub(crate) type Error = Box<dyn StdError + Send + Sync>;
62
63// === Interning dependency ===
64
65pub trait Intern {
66    type InternedStr<'a>: AsRef<str> + Borrow<str> + Clone + Eq + Ord + Hash + Debug + Display
67    where
68        Self: 'a;
69
70    fn intern_formatted_str<T: Display + ?Sized>(
71        &self,
72        value: &T,
73        upper_size: usize,
74    ) -> StdResult<Self::InternedStr<'_>, fmt::Error>;
75
76    fn intern_str(&self, text: &str) -> Self::InternedStr<'_> {
77        self.intern_formatted_str(text, text.len()).unwrap()
78    }
79}
80
81type DefaultInternerInner = HashSet<Arc<str>, fxhash::FxBuildHasher>;
82pub struct DefaultInterner(Mutex<DefaultInternerInner>);
83
84impl Default for DefaultInterner {
85    fn default() -> Self {
86        let set = HashSet::default();
87        Self(Mutex::new(set))
88    }
89}
90
91impl Intern for DefaultInterner {
92    type InternedStr<'a>
93        = Arc<str>
94    where
95        Self: 'a;
96
97    fn intern_formatted_str<T: Display + ?Sized>(
98        &self,
99        value: &T,
100        _: usize,
101    ) -> StdResult<Self::InternedStr<'_>, fmt::Error> {
102        let mut set = self.0.lock().unwrap();
103
104        let value = value.to_string();
105        if let Some(existing_value) = set.get(&*value) {
106            Ok(existing_value.clone())
107        } else {
108            let value: Arc<str> = value.into();
109            set.insert(value.clone());
110            Ok(value)
111        }
112    }
113}
114
115impl Intern for any_intern::DroplessInterner {
116    type InternedStr<'a>
117        = any_intern::Interned<'a, str>
118    where
119        Self: 'a;
120
121    fn intern_formatted_str<T: Display + ?Sized>(
122        &self,
123        value: &T,
124        upper_size: usize,
125    ) -> StdResult<Self::InternedStr<'_>, fmt::Error> {
126        self.intern_formatted_str(value, upper_size)
127    }
128
129    fn intern_str(&self, text: &str) -> Self::InternedStr<'_> {
130        self.intern(text)
131    }
132}
133
134impl Intern for any_intern::Interner {
135    type InternedStr<'a>
136        = any_intern::Interned<'a, str>
137    where
138        Self: 'a;
139
140    fn intern_formatted_str<T: Display + ?Sized>(
141        &self,
142        value: &T,
143        upper_size: usize,
144    ) -> StdResult<Self::InternedStr<'_>, fmt::Error> {
145        self.intern_formatted_str(value, upper_size)
146    }
147
148    fn intern_str(&self, text: &str) -> Self::InternedStr<'_> {
149        self.intern_dropless(text)
150    }
151}
152
153// === Type aliases for complex `Intern` related types ===
154
155pub(crate) use intern_alias::*;
156#[allow(unused)]
157mod intern_alias {
158    use super::{parse, prove, Intern};
159    pub(crate) type NameIn<'int, Int> = parse::text::Name<<Int as Intern>::InternedStr<'int>>;
160    pub(crate) type TermIn<'int, Int> = parse::repr::Term<NameIn<'int, Int>>;
161    pub(crate) type ExprIn<'int, Int> = parse::repr::Expr<NameIn<'int, Int>>;
162    pub(crate) type ClauseIn<'int, Int> = parse::repr::Clause<NameIn<'int, Int>>;
163    pub(crate) type UniqueTermArrayIn<'int, Int> = prove::repr::UniqueTermArray<NameIn<'int, Int>>;
164    pub(crate) type TermStorageIn<'int, Int> = prove::repr::TermStorage<NameIn<'int, Int>>;
165    pub(crate) type ClauseDatasetIn<'int, Int> = parse::repr::ClauseDataset<NameIn<'int, Int>>;
166    pub(crate) type Name2Int<'int, Int> =
167        prove::prover::IdxMap<'int, NameIn<'int, Int>, prove::prover::Integer, Int>;
168    pub(crate) type Int2Name<'int, Int> =
169        prove::prover::IdxMap<'int, prove::prover::Integer, NameIn<'int, Int>, Int>;
170}
logic_eval/lib.rs

logic_eval/
lib.rs
