Caching was a bad idea

Finishes cache
Starts proof cache infra
2026-02-10 21:48:58 +01:00 · 2026-02-10 18:11:50 +01:00 · 2026-02-10 17:21:06 +01:00
8 changed files with 128 additions and 54 deletions
--- 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",
 ]
--- 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"
--- 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<usize>);

 #[derive(Clone, Debug)]
 pub struct Module
@ -16,7 +18,7 @@ pub struct Clause
    pub body: Option<Body>,
 }

-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub enum Body
 {
    Term(Predicate),
@ -24,7 +26,7 @@ pub enum Body
    Or(Vec<Body>),
 }

-#[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::<Gray>())?;
+        }
+        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)?;
--- a/src/main.rs
+++ b/src/main.rs
@ -21,7 +21,7 @@ fn main()
    .into();

    //let prop: Body = "integer(s(X))".into();
-    let prop: Body = "mult(X, s(zero), s(zero))".into();
+    let prop: Body = "mult(X, s(s(zero)), s(s(s(s(zero)))))".into();
    //let prop: Body = "mult(X, Y, Z)".into();
    //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into();
    for c in module.prove(&prop)
--- 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<Predicate>
 {
@ -23,7 +24,7 @@ pub fn predicate_parse(input: &mut &str) -> Result<Predicate>
    // 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
    {
--- a/src/prover.rs
+++ b/src/prover.rs
@ -8,14 +8,15 @@ 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;

@ -29,7 +30,12 @@ impl GlobalCounter
 {
    pub fn new() -> GlobalCounter
    {
-        GlobalCounter(Rc::new(Cell::new(0)))
+        Self::with(0)
+    }
+
+    pub fn with(n: usize) -> GlobalCounter
+    {
+        GlobalCounter(Rc::new(Cell::new(n)))
    }

    pub fn get(&self) -> usize
@ -59,6 +65,7 @@ impl Module
            GlobalCounter::new(),
            body.clone(),
            Constraints::none(),
+            //&mut EmptyTracer,
            &mut IndentedTracer::new(),
            //&SimpleTracer::new(ProofType::Body),
        )
@ -69,7 +76,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 +92,7 @@ impl Body
    pub fn make_unique(
        &self,
        counter: GlobalCounter,
-        unique_map: &mut LiteMap<String, usize>,
+        unique_map: &mut HashMap<Variable, usize>,
    ) -> Body
    {
        match self
@ -112,18 +119,15 @@ impl Predicate
    pub fn make_unique(
        &self,
        counter: GlobalCounter,
-        unique_map: &mut LiteMap<String, usize>,
+        unique_map: &mut HashMap<Variable, usize>,
    ) -> 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 +138,22 @@ impl Predicate
        }
    }
 }
+
+impl Variable
+{
+    pub fn make_unique(
+        &self,
+        counter: GlobalCounter,
+        unique_map: &mut HashMap<Variable, usize>,
+    ) -> Self
+    {
+        Variable(
+            self.0.clone(),
+            Some(
+                *unique_map
+                    .entry(self.clone())
+                    .or_insert_with(|| counter.get()),
+            ),
+        )
+    }
+}
--- 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<Variable, Predicate>,
+    pub(crate) set: HashMap<Variable, Predicate>,
 }

 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, ", ")?;
--- a/src/prover/tracing.rs
+++ b/src/prover/tracing.rs
@ -1,12 +1,10 @@
 use log::info;
-use owo_colors::{
-    OwoColorize, Style,
-    colors::css::{DarkGray, Gray},
-};
+use owo_colors::OwoColorize;
+use owo_colors::Style;
+use owo_colors::colors::css::DarkGray;
+use owo_colors::colors::css::Gray;
 use std::fmt::Display;

-use crate::ast::Variable;
-
 #[derive(Clone, Copy)]
 pub enum ProofType
 {
@ -110,8 +108,8 @@ impl Tracer for IndentedTracer
        }
        self.first = false;
        println!("{}", show);
-        let _ = std::io::stdin().read_line(&mut String::new());
-        println!("\x1b[2A");
+        // let _ = std::io::stdin().read_line(&mut String::new());
+        // println!("\x1b[2A");
    }

    fn end_proof(self)
@ -133,17 +131,16 @@ impl Default for IndentedTracer
    }
 }

-pub fn colored_var(var: &Variable) -> String
+pub struct EmptyTracer;
+
+impl Tracer for EmptyTracer
 {
-    let mut idx = None;
-    for (i, char) in var.chars().enumerate()
+    fn begin_proof(&mut self, _proof_type: ProofType) -> Self
    {
-        if char == '['
-        {
-            idx = Some(i);
-        }
+        EmptyTracer
    }
-    let (var, unique) = var.split_at(idx.unwrap_or(var.len()));
-    let unique = unique.fg::<Gray>();
-    format!("{}{}", var, unique)
+
+    fn print_step<T: Display>(&mut self, _show: T) {}
+
+    fn end_proof(self) {}
 }
Author	SHA1	Message	Date
Albin Chaboissier	54724c2f4c	Caching was a bad idea	2026-02-10 21:48:58 +01:00
Albin Chaboissier	d8180a982e	Finishes cache	2026-02-10 18:11:50 +01:00
Albin Chaboissier	1c17aa20c2	Starts proof cache infra	2026-02-10 17:21:06 +01:00