From d8180a982e1a82ebe8df53d22c01f1be3b66cec2 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Tue, 10 Feb 2026 18:11:50 +0100 Subject: [PATCH] Finishes cache --- src/main.rs | 2 +- src/prover.rs | 9 ++- src/prover/constraints.rs | 2 +- src/prover/proof_cache.rs | 135 +++++++++++++++++++++++++++++++------- src/prover/tracing.rs | 26 ++++++-- 5 files changed, 142 insertions(+), 32 deletions(-) diff --git a/src/main.rs b/src/main.rs index ef05226..8de4cf3 100644 --- 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) diff --git a/src/prover.rs b/src/prover.rs index dccd472..7903f2c 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -19,6 +19,7 @@ use crate::ast::Predicate; use crate::ast::Variable; use crate::prover::body::BodyProver; use crate::prover::constraints::Constraints; +use crate::prover::tracing::EmptyTracer; use crate::prover::tracing::IndentedTracer; #[derive(Clone, Copy, Debug, Default)] @@ -31,7 +32,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 @@ -61,6 +67,7 @@ impl Module GlobalCounter::new(), body.clone(), Constraints::none(), + //&mut EmptyTracer, &mut IndentedTracer::new(), //&SimpleTracer::new(ProofType::Body), ) diff --git a/src/prover/constraints.rs b/src/prover/constraints.rs index 020182d..bf17625 100644 --- a/src/prover/constraints.rs +++ b/src/prover/constraints.rs @@ -8,7 +8,7 @@ use crate::ast::Variable; #[derive(Clone, Debug)] pub struct Constraints { - set: HashMap, + pub(crate) set: HashMap, } impl Constraints diff --git a/src/prover/proof_cache.rs b/src/prover/proof_cache.rs index f8c8cd4..ef8f354 100644 --- a/src/prover/proof_cache.rs +++ b/src/prover/proof_cache.rs @@ -1,15 +1,20 @@ -use std::{cell::RefCell, num::NonZero, rc::Rc}; +use std::cell::RefCell; +use std::num::NonZero; +use std::rc::Rc; use bimap::BiHashMap; use lru::LruCache; -use crate::{ - ast::{Body, Predicate, Variable}, - prover::{ - body::{self, BodyProver}, - constraints::Constraints, - }, -}; +use crate::ast::Body; +use crate::ast::Module; +use crate::ast::Predicate; +use crate::ast::Variable; +use crate::prover::GlobalCounter; +use crate::prover::body::BodyProver; +use crate::prover::body::{self}; +use crate::prover::constraints; +use crate::prover::constraints::Constraints; +use crate::prover::tracing::EmptyTracer; pub struct PartialProof> { @@ -19,9 +24,13 @@ pub struct PartialProof> pub struct CachedProver<'a> { + module: &'a Module, cache: Rc>>>>, - body: Body, + normalized_body: Body, + normalized_counter: usize, mapping: VariableMap, + constraints: Constraints, + proof_counter: usize, } @@ -39,22 +48,68 @@ impl<'a> ProofCache<'a> } } - pub fn prove(&mut self, body: &Body) -> CachedProver<'a> + pub fn prove( + &mut self, + module: &'a Module, + constraints: &Constraints, + body: &Body, + ) -> CachedProver<'a> { - let (varmap, normalized) = body.normalized(); + let (varmap, counter, normalized) = body.normalized(); + CachedProver { + module, + cache: self.cache.clone(), + normalized_body: normalized, + normalized_counter: counter, + mapping: varmap, + proof_counter: 0, + constraints: constraints.clone(), + } + } +} - // Check if in cache ? - match self.cache.borrow().get(&normalized) +impl<'a> Iterator for CachedProver<'a> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + let constraints; { - Some() => todo!(), - None => todo!(), + let mut cache_borrow = self.cache.borrow_mut(); + let partial_proof = + cache_borrow.get_or_insert_mut(self.normalized_body.clone(), || PartialProof { + proved: vec![], + prover: BodyProver::new( + self.module, + GlobalCounter::with(self.normalized_counter), + self.normalized_body.clone(), + Constraints::none(), + &mut EmptyTracer, + ), + }); + + while partial_proof.proved.len() <= self.proof_counter + { + let constraints = partial_proof.prover.next(); + match constraints + { + Some(constraints) => partial_proof.proved.push(constraints), + None => return None, + } + } + self.proof_counter += 1; + let normalized_proof = partial_proof.proved[self.proof_counter] + .clone() + .contextualized(&self.mapping); + // Check if we can get a match + constraints = self.constraints.and(&normalized_proof); } - CachedProver { - cache: self.cache.clone(), - body: normalized, - mapping: todo!(), - proof_counter: todo!(), + match constraints + { + Some(c) => Some(c), + None => self.next(), } } } @@ -65,13 +120,13 @@ pub struct VariableMap(BiHashMap); pub trait Normalizable: Sized { - fn normalized(&self) -> (VariableMap, Self) + fn normalized(&self) -> (VariableMap, usize, Self) { let mut bimap = BiHashMap::new(); let mut counter = 0; let normalized = self.normalized_with(&mut counter, &mut bimap); - (VariableMap(bimap), normalized) + (VariableMap(bimap), counter, normalized) } fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap) @@ -133,7 +188,7 @@ impl Normalizable for Variable map: &mut BiHashMap, ) -> Variable { - match map.get_by_left(&self) + match map.get_by_left(self) { Some(normalized) => normalized.clone(), None => @@ -148,3 +203,37 @@ impl Normalizable for Variable } } } + +impl Predicate +{ + fn contextualized(&self, map: &VariableMap) -> Predicate + { + match self + { + Predicate::Variable(variable) => + { + Predicate::Variable(map.0.get_by_right(variable).unwrap().clone()) + } + Predicate::Fixed(name, predicates) => Predicate::Fixed( + name.clone(), + predicates.iter().map(|p| p.contextualized(map)).collect(), + ), + } + } +} + +impl Constraints +{ + pub fn contextualized(&self, map: &VariableMap) -> Constraints + { + let mut new = Constraints::none(); + for (var, pred) in self.set.iter() + { + let ctx_var = map.0.get_by_right(var).unwrap(); + let ctx_pred = pred.contextualized(map); + new.set.insert(ctx_var.clone(), ctx_pred); + } + + new + } +} diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 0687c66..2c4fde1 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -1,8 +1,8 @@ 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; @@ -110,8 +110,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) @@ -132,3 +132,17 @@ impl Default for IndentedTracer Self::new() } } + +pub struct EmptyTracer; + +impl Tracer for EmptyTracer +{ + fn begin_proof(&mut self, _proof_type: ProofType) -> Self + { + EmptyTracer + } + + fn print_step(&mut self, _show: T) {} + + fn end_proof(self) {} +}