Starts proof cache infra

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>,
+    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, ", ")?;

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<T: Iterator<Item = Constraints>>
+{
+    proved: Vec<Constraints>,
+    prover: T,
+}
+
+pub struct CachedProver<'a>
+{
+    cache: Rc<RefCell<LruCache<Body, PartialProof<BodyProver<'a>>>>>,
+    body: Body,
+    mapping: VariableMap,
+    proof_counter: usize,
+}
+
+pub struct ProofCache<'a>
+{
+    cache: Rc<RefCell<LruCache<Body, PartialProof<BodyProver<'a>>>>>,
+}
+
+impl<'a> ProofCache<'a>
+{
+    pub fn new(size: NonZero<usize>) -> 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<Variable, Variable>);
+
+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<Variable, Variable>)
+    -> Self;
+}
+
+impl<T: Normalizable> Normalizable for Vec<T>
+{
+    fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap<Variable, Variable>)
+    -> 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<Variable, Variable>)
+    -> 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<Variable, Variable>,
+    ) -> 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, Variable>,
+    ) -> 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
+            }
+        }
+    }
+}

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::<Gray>();
-    format!("{}{}", var, unique)
-}