octagonal/picolog
1
1
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Caching was a bad idea

Browse Source
This commit is contained in:
Albin Chaboissier
2026-02-10 21:48:58 +01:00
parent d8180a982e
commit 54724c2f4c
3 changed files with 0 additions and 243 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/prover.rs
View File

@ -4,7 +4,6 @@ pub mod constraints;
pub mod not;
pub mod or;
pub mod predicate;
pub mod proof_cache;
pub mod tracing;
pub mod unification;
@ -19,7 +18,6 @@ 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)]

239
src/prover/proof_cache.rs
View File

@ -1,239 +0,0 @@
use std::cell::RefCell;
use std::num::NonZero;
use std::rc::Rc;
use bimap::BiHashMap;
use lru::LruCache;
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<T: Iterator<Item = Constraints>>
{
proved: Vec<Constraints>,
prover: T,
}
pub struct CachedProver<'a>
{
module: &'a Module,
cache: Rc<RefCell<LruCache<Body, PartialProof<BodyProver<'a>>>>>,
normalized_body: Body,
normalized_counter: usize,
mapping: VariableMap,
constraints: Constraints,
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,
module: &'a Module,
constraints: &Constraints,
body: &Body,
) -> CachedProver<'a>
{
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(),
}
}
}
impl<'a> Iterator for CachedProver<'a>
{
type Item = Constraints;
fn next(&mut self) -> Option<Self::Item>
{
let constraints;
{
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);
}
match constraints
{
Some(c) => Some(c),
None => self.next(),
}
}
}
// Normalization
pub struct VariableMap(BiHashMap<Variable, Variable>);
pub trait Normalizable: Sized
{
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), counter, 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
}
}
}
}
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
}
}

2
src/prover/tracing.rs
View File

@ -5,8 +5,6 @@ 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
{