diff --git a/Cargo.lock b/Cargo.lock index c7c015a..0474669 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -11,6 +11,12 @@ dependencies = [ "memchr", ] +[[package]] +name = "allocator-api2" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" + [[package]] name = "anstream" version = "0.6.21" @@ -61,6 +67,12 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "bimap" +version = "0.6.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "230c5f1ca6a325a32553f8640d31ac9b49f2411e901e427570154868b46da4f7" + [[package]] name = "colorchoice" version = "1.0.4" @@ -90,6 +102,29 @@ dependencies = [ "log", ] +[[package]] +name = "equivalent" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" + +[[package]] +name = "foldhash" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77ce24cb58228fbb8aa041425bb1050850ac19177686ea6e0f41a70416f56fdb" + +[[package]] +name = "hashbrown" +version = "0.16.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100" +dependencies = [ + "allocator-api2", + "equivalent", + "foldhash", +] + [[package]] name = "is_terminal_polyfill" version = "1.70.2" @@ -120,18 +155,21 @@ dependencies = [ "syn", ] -[[package]] -name = "litemap" -version = "0.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77" - [[package]] name = "log" version = "0.4.29" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" +[[package]] +name = "lru" +version = "0.16.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1dc47f592c06f33f8e3aea9591776ec7c9f9e4124778ff8a3c3b87159f7e593" +dependencies = [ + "hashbrown", +] + [[package]] name = "memchr" version = "2.8.0" @@ -154,9 +192,10 @@ checksum = "9c6901729fa79e91a0913333229e9ca5dc725089d1c363b2f4b4760709dc4a52" name = "picolog" version = "0.1.0" dependencies = [ + "bimap", "env_logger", - "litemap", "log", + "lru", "owo-colors", "winnow", ] diff --git a/Cargo.toml b/Cargo.toml index 7d57d83..b7817fa 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,8 +4,9 @@ version = "0.1.0" edition = "2024" [dependencies] +bimap = "0.6.3" env_logger = "0.11.8" -litemap = "0.8.1" log = "0.4.29" +lru = "0.16.3" owo-colors = "4.2.3" winnow = "0.7.14" diff --git a/src/ast.rs b/src/ast.rs index 19f413a..1eb315b 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,7 +1,9 @@ -use crate::prover::tracing::colored_var; +use owo_colors::{OwoColorize, colors::css::Gray}; + use std::fmt::Display; -pub type Variable = String; +#[derive(Clone, PartialEq, Eq, Debug, Hash)] +pub struct Variable(pub String, pub Option); #[derive(Clone, Debug)] pub struct Module @@ -16,7 +18,7 @@ pub struct Clause pub body: Option, } -#[derive(Clone, Debug)] +#[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum Body { Term(Predicate), @@ -24,7 +26,7 @@ pub enum Body Or(Vec), } -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, Eq, PartialEq, Hash)] pub enum Predicate { Variable(Variable), // Upercase variable like X @@ -55,13 +57,26 @@ impl Display for Body } } +impl Display for Variable +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result + { + write!(f, "{}", self.0)?; + if let Some(num) = self.1 + { + write!(f, "{}", format!("[{}]", num).fg::())?; + } + Ok(()) + } +} + impl Display for Predicate { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { - Predicate::Variable(variable) => write!(f, "{}", colored_var(variable)), + Predicate::Variable(variable) => write!(f, "{}", variable), Predicate::Fixed(name, predicates) => { write!(f, "{}", name)?; diff --git a/src/parsing.rs b/src/parsing.rs index 44d5dfc..b328d16 100644 --- a/src/parsing.rs +++ b/src/parsing.rs @@ -15,6 +15,7 @@ use crate::ast::Body; use crate::ast::Clause; use crate::ast::Module; use crate::ast::Predicate; +use crate::ast::Variable; pub fn predicate_parse(input: &mut &str) -> Result { @@ -23,7 +24,7 @@ pub fn predicate_parse(input: &mut &str) -> Result // Check if output is a variable if ident.chars().next().is_some_and(|char| char.is_uppercase()) { - Ok(Predicate::Variable(String::from(ident))) + Ok(Predicate::Variable(Variable(String::from(ident), None))) } else { diff --git a/src/prover.rs b/src/prover.rs index 70022f2..dccd472 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -4,18 +4,20 @@ pub mod constraints; pub mod not; pub mod or; pub mod predicate; +pub mod proof_cache; pub mod tracing; pub mod unification; use std::cell::Cell; +use std::collections::HashMap; use std::rc::Rc; -use litemap::LiteMap; - use crate::ast::Body; use crate::ast::Clause; use crate::ast::Module; use crate::ast::Predicate; +use crate::ast::Variable; +use crate::prover::body::BodyProver; use crate::prover::constraints::Constraints; use crate::prover::tracing::IndentedTracer; @@ -69,7 +71,7 @@ impl Clause { pub fn make_unique(&self, counter: GlobalCounter) -> Clause { - let mut unique_map = LiteMap::new(); + let mut unique_map = HashMap::new(); Clause { head: self.head.make_unique(counter.clone(), &mut unique_map), body: self @@ -85,7 +87,7 @@ impl Body pub fn make_unique( &self, counter: GlobalCounter, - unique_map: &mut LiteMap, + unique_map: &mut HashMap, ) -> Body { match self @@ -112,18 +114,15 @@ impl Predicate pub fn make_unique( &self, counter: GlobalCounter, - unique_map: &mut LiteMap, + unique_map: &mut HashMap, ) -> Self { match self { - Predicate::Variable(name) => Predicate::Variable(format!( - "_{}[{}]", - name, - unique_map - .entry(name.clone()) - .or_insert_with(|| counter.get()) - )), + Predicate::Variable(var) => + { + Predicate::Variable(var.make_unique(counter.clone(), unique_map)) + } Predicate::Fixed(name, predicates) => Predicate::Fixed( name.clone(), predicates @@ -134,3 +133,22 @@ impl Predicate } } } + +impl Variable +{ + pub fn make_unique( + &self, + counter: GlobalCounter, + unique_map: &mut HashMap, + ) -> Self + { + Variable( + self.0.clone(), + Some( + *unique_map + .entry(self.clone()) + .or_insert_with(|| counter.get()), + ), + ) + } +} diff --git a/src/prover/constraints.rs b/src/prover/constraints.rs index 4bad744..020182d 100644 --- a/src/prover/constraints.rs +++ b/src/prover/constraints.rs @@ -1,16 +1,14 @@ +use std::collections::HashMap; use std::fmt::Display; -use litemap::LiteMap; - use crate::ast::Body; use crate::ast::Predicate; use crate::ast::Variable; -use crate::prover::tracing::colored_var; #[derive(Clone, Debug)] pub struct Constraints { - set: LiteMap, + set: HashMap, } impl Constraints @@ -18,7 +16,7 @@ impl Constraints pub fn none() -> Self { Constraints { - set: LiteMap::new(), + set: HashMap::new(), } } @@ -103,7 +101,7 @@ impl Constraints let mut stripped = max_sub.clone(); 'outer: for (var, _) in max_sub.set.iter() { - if var.chars().next().is_some_and(|x| x == '_') + if var.0.chars().next().is_some_and(|x| x == '_') || var.1.is_some() { for (_, other_pred) in max_sub.set.iter() { @@ -147,7 +145,7 @@ impl Predicate } } - pub fn contains_variable(&self, name: &String) -> bool + pub fn contains_variable(&self, name: &Variable) -> bool { match self { @@ -188,7 +186,7 @@ impl Display for Constraints let len = self.set.len(); for (i, (var, pred)) in self.set.iter().enumerate() { - write!(f, "{} = {}", colored_var(var), pred)?; + write!(f, "{} = {}", var, pred)?; if i != len - 1 { write!(f, ", ")?; diff --git a/src/prover/proof_cache.rs b/src/prover/proof_cache.rs new file mode 100644 index 0000000..f8c8cd4 --- /dev/null +++ b/src/prover/proof_cache.rs @@ -0,0 +1,150 @@ +use std::{cell::RefCell, num::NonZero, rc::Rc}; + +use bimap::BiHashMap; +use lru::LruCache; + +use crate::{ + ast::{Body, Predicate, Variable}, + prover::{ + body::{self, BodyProver}, + constraints::Constraints, + }, +}; + +pub struct PartialProof> +{ + proved: Vec, + prover: T, +} + +pub struct CachedProver<'a> +{ + cache: Rc>>>>, + body: Body, + mapping: VariableMap, + proof_counter: usize, +} + +pub struct ProofCache<'a> +{ + cache: Rc>>>>, +} + +impl<'a> ProofCache<'a> +{ + pub fn new(size: NonZero) -> Self + { + ProofCache { + cache: Rc::new(RefCell::new(LruCache::new(size))), + } + } + + pub fn prove(&mut self, body: &Body) -> CachedProver<'a> + { + let (varmap, normalized) = body.normalized(); + + // Check if in cache ? + match self.cache.borrow().get(&normalized) + { + Some() => todo!(), + None => todo!(), + } + + CachedProver { + cache: self.cache.clone(), + body: normalized, + mapping: todo!(), + proof_counter: todo!(), + } + } +} + +// Normalization + +pub struct VariableMap(BiHashMap); + +pub trait Normalizable: Sized +{ + fn normalized(&self) -> (VariableMap, Self) + { + let mut bimap = BiHashMap::new(); + let mut counter = 0; + let normalized = self.normalized_with(&mut counter, &mut bimap); + + (VariableMap(bimap), normalized) + } + + fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap) + -> Self; +} + +impl Normalizable for Vec +{ + fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap) + -> Self + { + self.iter() + .map(|x| x.normalized_with(counter, map)) + .collect() + } +} + +impl Normalizable for Body +{ + fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap) + -> Body + { + match self + { + Body::Term(predicate) => Body::Term(predicate.normalized_with(counter, map)), + Body::And(items) => Body::And(items.normalized_with(counter, map)), + Body::Or(items) => Body::Or(items.normalized_with(counter, map)), + } + } +} + +impl Normalizable for Predicate +{ + fn normalized_with( + &self, + counter: &mut usize, + map: &mut BiHashMap, + ) -> Predicate + { + match self + { + Predicate::Variable(variable) => + { + Predicate::Variable(variable.normalized_with(counter, map)) + } + Predicate::Fixed(name, predicates) => + { + Predicate::Fixed(name.clone(), predicates.normalized_with(counter, map)) + } + } + } +} + +impl Normalizable for Variable +{ + fn normalized_with( + &self, + counter: &mut usize, + map: &mut BiHashMap, + ) -> Variable + { + match map.get_by_left(&self) + { + Some(normalized) => normalized.clone(), + None => + { + let val = *counter; + *counter += 1; + + let var = Variable(self.0.clone(), Some(val)); + map.insert(self.clone(), var.clone()); + var + } + } + } +} diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index f97400e..0687c66 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -132,18 +132,3 @@ impl Default for IndentedTracer Self::new() } } - -pub fn colored_var(var: &Variable) -> String -{ - let mut idx = None; - for (i, char) in var.chars().enumerate() - { - if char == '[' - { - idx = Some(i); - } - } - let (var, unique) = var.split_at(idx.unwrap_or(var.len())); - let unique = unique.fg::(); - format!("{}{}", var, unique) -}