From a151b772aa4c070f299c69461bef03ff5ef55768 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Mon, 9 Feb 2026 16:40:51 +0100 Subject: [PATCH 01/10] Starts a good tracing interface --- Cargo.lock | 7 +++++++ Cargo.toml | 1 + src/ast.rs | 6 +++++- src/main.rs | 4 ++-- src/prover.rs | 21 +++++++++++++++++++-- src/prover/constraints.rs | 3 ++- src/prover/tracing.rs | 18 ++++++++++++++++++ 7 files changed, 54 insertions(+), 6 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 3d771a3..c7c015a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -144,6 +144,12 @@ version = "1.70.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" +[[package]] +name = "owo-colors" +version = "4.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c6901729fa79e91a0913333229e9ca5dc725089d1c363b2f4b4760709dc4a52" + [[package]] name = "picolog" version = "0.1.0" @@ -151,6 +157,7 @@ dependencies = [ "env_logger", "litemap", "log", + "owo-colors", "winnow", ] diff --git a/Cargo.toml b/Cargo.toml index 6952248..7d57d83 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,4 +7,5 @@ edition = "2024" env_logger = "0.11.8" litemap = "0.8.1" log = "0.4.29" +owo-colors = "4.2.3" winnow = "0.7.14" diff --git a/src/ast.rs b/src/ast.rs index f56d75d..f07abbc 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,5 +1,9 @@ use std::fmt::Display; +use owo_colors::{OwoColorize, colors::css::Gray}; + +use crate::prover::tracing::colored_var; + pub type Variable = String; #[derive(Clone, Debug)] @@ -60,7 +64,7 @@ impl Display for Predicate { match self { - Predicate::Variable(variable) => write!(f, "{}", variable), + Predicate::Variable(variable) => write!(f, "{}", colored_var(variable)), Predicate::Fixed(name, predicates) => { write!(f, "{}", name)?; diff --git a/src/main.rs b/src/main.rs index d120503..9b537fa 100644 --- a/src/main.rs +++ b/src/main.rs @@ -20,8 +20,8 @@ fn main() " .into(); - //let prop: Body = "integer(s(X))".into(); - let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into(); + let prop: Body = "integer(s(X))".into(); + //let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into(); for c in module.prove(&prop) { println!("true:"); diff --git a/src/prover.rs b/src/prover.rs index d081f10..9208a3d 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -7,6 +7,10 @@ use std::rc::Rc; use litemap::LiteMap; use log::info; +use owo_colors::OwoColorize; +use owo_colors::colors::Green; +use owo_colors::colors::Red; +use owo_colors::colors::css::Gray; use crate::ast::Body; use crate::ast::Clause; @@ -143,9 +147,15 @@ impl<'a, T: Tracer + 'a> PredicateProver<'a, T> ) -> PredicateProver<'a, T> { //info!(target: "PredicateProver", "Proving {}", predicate); + let predicate_prover = tracer.begin_proof(ProofType::Predicate); + predicate_prover.print_step(format!( + "{} '{}'", + "Proving predicate".fg::(), + predicate + )); PredicateProver { module, - tracer: tracer.begin_proof(ProofType::Predicate), + tracer: predicate_prover, predicate, constraints, current_clause: 0, @@ -209,16 +219,23 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> let clause = &self.module.clauses[self.current_clause] .make_unique(self.global_counter.clone()); //info!(target: "PredicateProver", "Unifying '{}' against '{}'", self.predicate, clause); + self.tracer.print_step(format!( + "🭆 Unifying '{}' aginst '{}'", + self.predicate, clause + )); let uni = self.predicate.matches(&clause.head); let full_constraints = uni.and_then(|x| x.and(&self.constraints)); if let Some(c) = &full_constraints { //info!(target: "PredicateProver", " => {}", c); + self.tracer + .print_step(format!("🭧 ↳ {}: {}", "Matches".fg::(), c)); } else { - //info!(target: "PredicateProver", " => (Can't unify)"); + self.tracer + .print_step(format!("🭧 ↳ {}", "Contradictory".fg::())); } match full_constraints { diff --git a/src/prover/constraints.rs b/src/prover/constraints.rs index a13eab2..4bad744 100644 --- a/src/prover/constraints.rs +++ b/src/prover/constraints.rs @@ -5,6 +5,7 @@ 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 @@ -187,7 +188,7 @@ impl Display for Constraints let len = self.set.len(); for (i, (var, pred)) in self.set.iter().enumerate() { - write!(f, "{} = {}", var, pred)?; + write!(f, "{} = {}", colored_var(var), pred)?; if i != len - 1 { write!(f, ", ")?; diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 94ef708..47ccfbf 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -1,6 +1,9 @@ use std::{default, fmt::Display}; use log::info; +use owo_colors::{OwoColorize, colors::css::Gray}; + +use crate::ast::Variable; #[derive(Clone, Copy)] pub enum ProofType @@ -61,3 +64,18 @@ impl Tracer for SimpleTracer todo!() } } + +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) +} From 1ab7d7bf95f9a93e7dbe0431c60cc77d9fd8c076 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Mon, 9 Feb 2026 18:08:13 +0100 Subject: [PATCH 02/10] Ugly and print, and simplified body prover depth --- src/main.rs | 4 ++-- src/prover.rs | 46 ++++++++++++++++++++++++++++++++++++++++++++-- src/tracing.rs | 0 3 files changed, 46 insertions(+), 4 deletions(-) create mode 100644 src/tracing.rs diff --git a/src/main.rs b/src/main.rs index 9b537fa..d120503 100644 --- a/src/main.rs +++ b/src/main.rs @@ -20,8 +20,8 @@ fn main() " .into(); - let prop: Body = "integer(s(X))".into(); - //let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into(); + //let prop: Body = "integer(s(X))".into(); + let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into(); for c in module.prove(&prop) { println!("true:"); diff --git a/src/prover.rs b/src/prover.rs index 9208a3d..fd52146 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -3,14 +3,15 @@ pub mod tracing; pub mod unification; use std::cell::Cell; +use std::fmt::Write; use std::rc::Rc; use litemap::LiteMap; -use log::info; use owo_colors::OwoColorize; +use owo_colors::Style; use owo_colors::colors::Green; use owo_colors::colors::Red; -use owo_colors::colors::css::Gray; +use owo_colors::colors::Yellow; use crate::ast::Body; use crate::ast::Clause; @@ -79,6 +80,7 @@ pub struct AndProver<'a, T: Tracer> bodies: Vec, constraints: Constraints, tracer: T, + current_tracer: Option, global_counter: GlobalCounter, sub_proofs: Vec<(Counter, BodyProver<'a, T>)>, @@ -111,6 +113,16 @@ impl<'a, T: Tracer + 'a> BodyProver<'a, T> constraints.clone(), tracer, )), + + // Shortcut And & Or prover if it contains only one element to simplify proofs + Body::And(items) | Body::Or(items) if items.len() == 1 => Box::new(BodyProver::new( + module, + global_counter, + items[0].clone(), + constraints.clone(), + tracer, + )), + Body::And(items) => Box::new(AndProver::new( module, global_counter, @@ -182,6 +194,7 @@ impl AndProver<'_, T> AndProver { tracer: tracer.begin_proof(ProofType::And), + current_tracer: None, module, sub_proofs: vec![( global_counter.snapshot(), @@ -316,6 +329,35 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> } else { + // Pretty logging + self.current_tracer = Some(self.tracer.begin_proof(ProofType::And)); + self.current_tracer.as_ref().unwrap().print_step(format!( + "And. {} {} {} :", + "Proved".fg::(), + "Proving".fg::(), + "Left".fg::() + )); + let mut output = String::new(); + for (i, x) in self.bodies.iter().enumerate() + { + let mut color = Style::new(); + if i == self.sub_proofs.len() - 1 + { + color = color.fg::(); + } + else if i < self.sub_proofs.len() - 1 + { + color = color.fg::(); + } + else + { + color = color.fg::(); + } + let _ = output.write_str(&format!("{}, ", x.style(color))); + } + self.current_tracer.as_ref().unwrap().print_step(output); + + // End pretty logging self.sub_proofs.push((current_proof_snap, current_proof)); self.sub_proofs.push(( self.global_counter.snapshot(), diff --git a/src/tracing.rs b/src/tracing.rs new file mode 100644 index 0000000..e69de29 From 5b9df71704e5035611c9bec5f884a82f283651d3 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Mon, 9 Feb 2026 22:32:01 +0100 Subject: [PATCH 03/10] Somewhat indented trace + Or prover --- src/main.rs | 3 +- src/prover.rs | 232 ++++++++++++++++++++++++++++++++++-------- src/prover/tracing.rs | 86 ++++++++++++++-- src/tracing.rs | 0 4 files changed, 273 insertions(+), 48 deletions(-) delete mode 100644 src/tracing.rs diff --git a/src/main.rs b/src/main.rs index d120503..d80f084 100644 --- a/src/main.rs +++ b/src/main.rs @@ -21,7 +21,8 @@ fn main() .into(); //let prop: Body = "integer(s(X))".into(); - let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into(); + //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); + let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); for c in module.prove(&prop) { println!("true:"); diff --git a/src/prover.rs b/src/prover.rs index fd52146..0f3187e 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -18,6 +18,7 @@ use crate::ast::Clause; use crate::ast::Module; use crate::ast::Predicate; use crate::prover::constraints::Constraints; +use crate::prover::tracing::IndentedTracer; use crate::prover::tracing::ProofType; use crate::prover::tracing::SimpleTracer; use crate::prover::tracing::Tracer; @@ -80,12 +81,26 @@ pub struct AndProver<'a, T: Tracer> bodies: Vec, constraints: Constraints, tracer: T, - current_tracer: Option, + current_tracer: T, global_counter: GlobalCounter, sub_proofs: Vec<(Counter, BodyProver<'a, T>)>, } +pub struct OrProver<'a, T: Tracer> +{ + module: &'a Module, + bodies: Vec, + constraints: Constraints, + tracer: T, + current_tracer: T, + + current_proving: usize, + global_counter: GlobalCounter, + counter_snapshot: Counter, + sub_proof: Option>, +} + impl<'a, T: Tracer + 'a> BodyProver<'a, T> { pub fn new( @@ -93,7 +108,7 @@ impl<'a, T: Tracer + 'a> BodyProver<'a, T> global_counter: GlobalCounter, body: Body, constraints: Constraints, - tracer: &T, + tracer: &mut T, ) -> BodyProver<'a, T> { let body_tracer = if let Body::And(_) = body @@ -155,11 +170,11 @@ impl<'a, T: Tracer + 'a> PredicateProver<'a, T> global_counter: GlobalCounter, predicate: Predicate, constraints: Constraints, - tracer: &T, + tracer: &mut T, ) -> PredicateProver<'a, T> { //info!(target: "PredicateProver", "Proving {}", predicate); - let predicate_prover = tracer.begin_proof(ProofType::Predicate); + let mut predicate_prover = tracer.begin_proof(ProofType::Predicate); predicate_prover.print_step(format!( "{} '{}'", "Proving predicate".fg::(), @@ -185,16 +200,42 @@ impl AndProver<'_, T> global_counter: GlobalCounter, bodies: Vec, constraints: Constraints, - tracer: &T, + tracer: &mut T, ) -> AndProver<'a, T> where T: 'a, { assert!(!bodies.is_empty()); + // Pretty logging + let mut whole_trace = tracer.begin_proof(ProofType::And); + let mut current_tracer = whole_trace.begin_proof(ProofType::And); + let mut next = String::new(); + for x in bodies.iter().skip(1) + { + let _ = next.write_str(&format!("{}, ", x)); + } + + let mut conjuction = String::new(); + let len = bodies.len(); + for (i, x) in bodies.iter().enumerate() + { + let _ = conjuction.write_str(&format!("{}", x)); + if i != len - 1 + { + let _ = conjuction.write_str(" ∧ "); + } + } + + current_tracer.print_step(format!("Proving conjuction {}", conjuction)); + current_tracer.print_step(format!("{} :", "Proved".fg::(),)); + current_tracer.print_step(format!("{} : {}", "Proving".fg::(), bodies[0])); + current_tracer.print_step(format!("{} : {}", "Next".fg::(), next)); + current_tracer.print_step(format!("With constraints : {}", constraints.simplified())); + // End pretty logging + AndProver { - tracer: tracer.begin_proof(ProofType::And), - current_tracer: None, + tracer: whole_trace, module, sub_proofs: vec![( global_counter.snapshot(), @@ -203,9 +244,67 @@ impl AndProver<'_, T> global_counter.clone(), bodies[0].clone(), constraints.clone(), - tracer, + &mut current_tracer, ), )], + current_tracer, + bodies, + constraints, + global_counter, + } + } +} + +impl OrProver<'_, T> +{ + pub fn new<'a>( + module: &'a Module, + global_counter: GlobalCounter, + bodies: Vec, + constraints: Constraints, + tracer: &mut T, + ) -> OrProver<'a, T> + where + T: 'a, + { + assert!(!bodies.is_empty()); + + // Pretty logging + let mut whole_trace = tracer.begin_proof(ProofType::And); + let mut current_tracer = whole_trace.begin_proof(ProofType::And); + + let mut next = String::new(); + for x in bodies.iter().skip(1) + { + let _ = next.write_str(&format!("{}, ", x)); + } + + let mut disjunction = String::new(); + let len = bodies.len(); + for (i, x) in bodies.iter().enumerate() + { + let _ = disjunction.write_str(&format!("{}", x)); + if i != len - 1 + { + let _ = disjunction.write_str(" ∨ "); + } + } + + // End pretty logging + + OrProver { + tracer: whole_trace, + module, + sub_proof: Some(BodyProver::new( + module, + global_counter.clone(), + bodies[0].clone(), + constraints.clone(), + &mut current_tracer, + )), + current_proving: 0, + counter_snapshot: global_counter.snapshot(), + current_tracer, bodies, constraints, global_counter, @@ -232,24 +331,22 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> let clause = &self.module.clauses[self.current_clause] .make_unique(self.global_counter.clone()); //info!(target: "PredicateProver", "Unifying '{}' against '{}'", self.predicate, clause); - self.tracer.print_step(format!( - "🭆 Unifying '{}' aginst '{}'", - self.predicate, clause - )); let uni = self.predicate.matches(&clause.head); let full_constraints = uni.and_then(|x| x.and(&self.constraints)); if let Some(c) = &full_constraints { - //info!(target: "PredicateProver", " => {}", c); - self.tracer - .print_step(format!("🭧 ↳ {}: {}", "Matches".fg::(), c)); - } - else - { - self.tracer - .print_step(format!("🭧 ↳ {}", "Contradictory".fg::())); + self.tracer.print_step(format!( + "Unifying '{}' aginst '{}'", + self.predicate, clause + )); + self.tracer.print_step(format!( + "↳ {}: {}", + "Matches".fg::(), + c.simplified() + )); } + match full_constraints { Some(constraints) if clause.body.is_none() => @@ -266,12 +363,13 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> self.global_counter.clone(), clause.body.clone().unwrap(), constraints, - &self.tracer, + &mut self.tracer, )); self.next() } None => { + self.global_counter.restore(self.counter_snapshot); self.current_clause += 1; self.next() } @@ -330,34 +428,41 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> else { // Pretty logging - self.current_tracer = Some(self.tracer.begin_proof(ProofType::And)); - self.current_tracer.as_ref().unwrap().print_step(format!( - "And. {} {} {} :", - "Proved".fg::(), - "Proving".fg::(), - "Left".fg::() - )); - let mut output = String::new(); + self.current_tracer = self.tracer.begin_proof(ProofType::And); + let mut proved = String::new(); + let mut proving = String::new(); + let mut next = String::new(); for (i, x) in self.bodies.iter().enumerate() { - let mut color = Style::new(); - if i == self.sub_proofs.len() - 1 + let dest; + if i == self.sub_proofs.len() + 1 { - color = color.fg::(); + dest = &mut proving; } - else if i < self.sub_proofs.len() - 1 + else if i < self.sub_proofs.len() + 1 { - color = color.fg::(); + dest = &mut proved; } else { - color = color.fg::(); + dest = &mut next; } - let _ = output.write_str(&format!("{}, ", x.style(color))); + let _ = dest.write_str(&format!("{}, ", x)); } - self.current_tracer.as_ref().unwrap().print_step(output); - + self.current_tracer.print_step(format!( + "{} : {}", + "Proved".fg::(), + proved + )); + self.current_tracer.print_step(format!( + "{} : {}", + "Proving".fg::(), + proving + )); + self.current_tracer + .print_step(format!("{} : {}", "Next".fg::(), next)); // End pretty logging + self.sub_proofs.push((current_proof_snap, current_proof)); self.sub_proofs.push(( self.global_counter.snapshot(), @@ -366,7 +471,7 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> self.global_counter.clone(), self.bodies[self.sub_proofs.len()].clone(), constraints, - &self.tracer, + &mut self.current_tracer, ), )); self.next() @@ -381,16 +486,61 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> } } +impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + let proof = match &mut self.sub_proof + { + Some(sub_proof) => sub_proof.next(), + None => + { + return None; + } + }; + + match proof + { + Some(x) => Some(x), + None => + { + // Advance to next possibility + if self.current_proving == self.bodies.len() - 1 + { + self.sub_proof = None; + None + } + else + { + self.current_proving += 1; + self.global_counter.restore(self.counter_snapshot); + self.sub_proof = Some(BodyProver::new( + self.module, + self.global_counter.clone(), + self.bodies[self.current_proving].clone(), + self.constraints.clone(), + &mut self.current_tracer, + )); + self.next() + } + } + } + } +} + impl Module { - pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, SimpleTracer> + pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, impl Tracer> { BodyProver::new( self, GlobalCounter::new(), body.clone(), Constraints::none(), - &SimpleTracer::new(ProofType::Body), + &mut IndentedTracer::new(), + //&SimpleTracer::new(ProofType::Body), ) } } diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 47ccfbf..6e7c6d0 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -1,7 +1,10 @@ -use std::{default, fmt::Display}; +use std::{cell::RefCell, default, fmt::Display, rc::Rc}; use log::info; -use owo_colors::{OwoColorize, colors::css::Gray}; +use owo_colors::{ + OwoColorize, Style, + colors::css::{DarkGray, Gray}, +}; use crate::ast::Variable; @@ -28,8 +31,8 @@ impl Display for ProofType pub trait Tracer { - fn begin_proof(&self, proof_type: ProofType) -> Self; - fn print_step(&self, show: T); + fn begin_proof(&mut self, proof_type: ProofType) -> Self; + fn print_step(&mut self, show: T); fn end_proof(self); } @@ -48,12 +51,12 @@ impl SimpleTracer impl Tracer for SimpleTracer { - fn begin_proof(&self, proof_type: ProofType) -> Self + fn begin_proof(&mut self, proof_type: ProofType) -> Self { SimpleTracer { proof_type } } - fn print_step(&self, show: T) + fn print_step(&mut self, show: T) { let str = format!("{}", self.proof_type); info!(target: &str, "{}", show); @@ -65,6 +68,77 @@ impl Tracer for SimpleTracer } } +pub struct IndentedTracer +{ + first: bool, + depth: usize, +} + +impl IndentedTracer +{ + pub fn new() -> IndentedTracer + { + IndentedTracer { + first: true, + depth: 0, + } + } +} + +impl Tracer for IndentedTracer +{ + fn begin_proof(&mut self, _proof_type: ProofType) -> Self + { + IndentedTracer { + first: true, + depth: self.depth + 1, + } + } + + fn print_step(&mut self, show: T) + { + for i in 0..self.depth + { + let style = if i % 2 == 0 + { + Style::new().fg::() + } + else + { + Style::new().fg::() + }; + if i == self.depth - 1 && self.first + { + print!("{}", "🭋".style(style)); + } + else + { + print!("{}", "▐".style(style)); + } + } + self.first = false; + println!("{}", show); + } + + fn end_proof(self) + { + drop(self); + } +} + +impl Drop for IndentedTracer +{ + fn drop(&mut self) {} +} + +impl Default for IndentedTracer +{ + fn default() -> Self + { + Self::new() + } +} + pub fn colored_var(var: &Variable) -> String { let mut idx = None; diff --git a/src/tracing.rs b/src/tracing.rs deleted file mode 100644 index e69de29..0000000 From c920ef8d9998b57de962cdb66837486de5689dc4 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Mon, 9 Feb 2026 22:38:23 +0100 Subject: [PATCH 04/10] Removes all warnings --- src/ast.rs | 5 +---- src/prover.rs | 45 +++++++++++---------------------------- src/prover/tracing.rs | 3 +-- src/prover/unification.rs | 2 -- 4 files changed, 15 insertions(+), 40 deletions(-) diff --git a/src/ast.rs b/src/ast.rs index f07abbc..19f413a 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,8 +1,5 @@ -use std::fmt::Display; - -use owo_colors::{OwoColorize, colors::css::Gray}; - use crate::prover::tracing::colored_var; +use std::fmt::Display; pub type Variable = String; diff --git a/src/prover.rs b/src/prover.rs index 0f3187e..8c95c4f 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -8,7 +8,6 @@ use std::rc::Rc; use litemap::LiteMap; use owo_colors::OwoColorize; -use owo_colors::Style; use owo_colors::colors::Green; use owo_colors::colors::Red; use owo_colors::colors::Yellow; @@ -20,7 +19,6 @@ use crate::ast::Predicate; use crate::prover::constraints::Constraints; use crate::prover::tracing::IndentedTracer; use crate::prover::tracing::ProofType; -use crate::prover::tracing::SimpleTracer; use crate::prover::tracing::Tracer; #[derive(Clone, Copy, Debug, Default)] @@ -54,11 +52,8 @@ impl GlobalCounter } } -pub struct BodyProver<'a, T: Tracer + 'a> +pub struct BodyProver<'a> { - module: &'a Module, - constraints: Constraints, - tracer: Option, prover: Box + 'a>, } @@ -72,19 +67,18 @@ pub struct PredicateProver<'a, T: Tracer> global_counter: GlobalCounter, current_clause: usize, - sub_proof: Option>, + sub_proof: Option>, } pub struct AndProver<'a, T: Tracer> { module: &'a Module, bodies: Vec, - constraints: Constraints, tracer: T, current_tracer: T, global_counter: GlobalCounter, - sub_proofs: Vec<(Counter, BodyProver<'a, T>)>, + sub_proofs: Vec<(Counter, BodyProver<'a>)>, } pub struct OrProver<'a, T: Tracer> @@ -98,27 +92,19 @@ pub struct OrProver<'a, T: Tracer> current_proving: usize, global_counter: GlobalCounter, counter_snapshot: Counter, - sub_proof: Option>, + sub_proof: Option>, } -impl<'a, T: Tracer + 'a> BodyProver<'a, T> +impl<'a> BodyProver<'a> { - pub fn new( + pub fn new( module: &'a Module, global_counter: GlobalCounter, body: Body, constraints: Constraints, tracer: &mut T, - ) -> BodyProver<'a, T> + ) -> BodyProver<'a> { - let body_tracer = if let Body::And(_) = body - { - Some(tracer.begin_proof(ProofType::Body)) - } - else - { - None - }; let prover: Box> = match &body { Body::Term(predicate) => Box::new(PredicateProver::new( @@ -153,13 +139,8 @@ impl<'a, T: Tracer + 'a> BodyProver<'a, T> tracer, )), }; - //info!(target: "BodyProver", "Proving {}", body); - BodyProver { - tracer: body_tracer, - module, - constraints, - prover, - } + + BodyProver { prover } } } @@ -249,7 +230,6 @@ impl AndProver<'_, T> )], current_tracer, bodies, - constraints, global_counter, } } @@ -330,7 +310,6 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> { let clause = &self.module.clauses[self.current_clause] .make_unique(self.global_counter.clone()); - //info!(target: "PredicateProver", "Unifying '{}' against '{}'", self.predicate, clause); let uni = self.predicate.matches(&clause.head); let full_constraints = uni.and_then(|x| x.and(&self.constraints)); @@ -394,7 +373,7 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> } } -impl<'a, T: Tracer + 'a> Iterator for BodyProver<'a, T> +impl<'a> Iterator for BodyProver<'a> { type Item = Constraints; fn next(&mut self) -> Option @@ -516,6 +495,8 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> { self.current_proving += 1; self.global_counter.restore(self.counter_snapshot); + self.tracer + .print_step(format!("Tring with {}", self.bodies[self.current_proving])); self.sub_proof = Some(BodyProver::new( self.module, self.global_counter.clone(), @@ -532,7 +513,7 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> impl Module { - pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, impl Tracer> + pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a> { BodyProver::new( self, diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 6e7c6d0..60ea6f5 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -1,10 +1,9 @@ -use std::{cell::RefCell, default, fmt::Display, rc::Rc}; - use log::info; use owo_colors::{ OwoColorize, Style, colors::css::{DarkGray, Gray}, }; +use std::fmt::Display; use crate::ast::Variable; diff --git a/src/prover/unification.rs b/src/prover/unification.rs index 747d458..d6d5042 100644 --- a/src/prover/unification.rs +++ b/src/prover/unification.rs @@ -1,5 +1,3 @@ -use log::debug; - use crate::ast::Predicate; use crate::prover::constraints::Constraints; From 3fd8414ba2edbc66e72050953643ebf128120ec6 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Mon, 9 Feb 2026 22:49:26 +0100 Subject: [PATCH 05/10] Better looking indentation --- src/main.rs | 2 +- src/prover.rs | 49 ++++++++++++++++--------------------------- src/prover/tracing.rs | 9 +------- 3 files changed, 20 insertions(+), 40 deletions(-) diff --git a/src/main.rs b/src/main.rs index d80f084..0034206 100644 --- a/src/main.rs +++ b/src/main.rs @@ -21,8 +21,8 @@ fn main() .into(); //let prop: Body = "integer(s(X))".into(); - //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); + //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); for c in module.prove(&prop) { println!("true:"); diff --git a/src/prover.rs b/src/prover.rs index 8c95c4f..5aff903 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -75,7 +75,6 @@ pub struct AndProver<'a, T: Tracer> module: &'a Module, bodies: Vec, tracer: T, - current_tracer: T, global_counter: GlobalCounter, sub_proofs: Vec<(Counter, BodyProver<'a>)>, @@ -87,7 +86,6 @@ pub struct OrProver<'a, T: Tracer> bodies: Vec, constraints: Constraints, tracer: T, - current_tracer: T, current_proving: usize, global_counter: GlobalCounter, @@ -189,8 +187,7 @@ impl AndProver<'_, T> assert!(!bodies.is_empty()); // Pretty logging - let mut whole_trace = tracer.begin_proof(ProofType::And); - let mut current_tracer = whole_trace.begin_proof(ProofType::And); + let mut tracer = tracer.begin_proof(ProofType::And); let mut next = String::new(); for x in bodies.iter().skip(1) { @@ -208,15 +205,14 @@ impl AndProver<'_, T> } } - current_tracer.print_step(format!("Proving conjuction {}", conjuction)); - current_tracer.print_step(format!("{} :", "Proved".fg::(),)); - current_tracer.print_step(format!("{} : {}", "Proving".fg::(), bodies[0])); - current_tracer.print_step(format!("{} : {}", "Next".fg::(), next)); - current_tracer.print_step(format!("With constraints : {}", constraints.simplified())); + tracer.print_step(format!("Proving conjuction {}", conjuction)); + tracer.print_step(format!("{} :", "Proved".fg::(),)); + tracer.print_step(format!("{} : {}", "Proving".fg::(), bodies[0])); + tracer.print_step(format!("{} : {}", "Next".fg::(), next)); + tracer.print_step(format!("With constraints : {}", constraints.simplified())); // End pretty logging AndProver { - tracer: whole_trace, module, sub_proofs: vec![( global_counter.snapshot(), @@ -225,10 +221,10 @@ impl AndProver<'_, T> global_counter.clone(), bodies[0].clone(), constraints.clone(), - &mut current_tracer, + &mut tracer, ), )], - current_tracer, + tracer, bodies, global_counter, } @@ -250,8 +246,7 @@ impl OrProver<'_, T> assert!(!bodies.is_empty()); // Pretty logging - let mut whole_trace = tracer.begin_proof(ProofType::And); - let mut current_tracer = whole_trace.begin_proof(ProofType::And); + let mut tracer = tracer.begin_proof(ProofType::And); let mut next = String::new(); for x in bodies.iter().skip(1) @@ -273,18 +268,17 @@ impl OrProver<'_, T> // End pretty logging OrProver { - tracer: whole_trace, module, sub_proof: Some(BodyProver::new( module, global_counter.clone(), bodies[0].clone(), constraints.clone(), - &mut current_tracer, + &mut tracer, )), + tracer, current_proving: 0, counter_snapshot: global_counter.snapshot(), - current_tracer, bodies, constraints, global_counter, @@ -407,7 +401,6 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> else { // Pretty logging - self.current_tracer = self.tracer.begin_proof(ProofType::And); let mut proved = String::new(); let mut proving = String::new(); let mut next = String::new(); @@ -428,17 +421,11 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> } let _ = dest.write_str(&format!("{}, ", x)); } - self.current_tracer.print_step(format!( - "{} : {}", - "Proved".fg::(), - proved - )); - self.current_tracer.print_step(format!( - "{} : {}", - "Proving".fg::(), - proving - )); - self.current_tracer + self.tracer + .print_step(format!("{} : {}", "Proved".fg::(), proved)); + self.tracer + .print_step(format!("{} : {}", "Proving".fg::(), proving)); + self.tracer .print_step(format!("{} : {}", "Next".fg::(), next)); // End pretty logging @@ -450,7 +437,7 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> self.global_counter.clone(), self.bodies[self.sub_proofs.len()].clone(), constraints, - &mut self.current_tracer, + &mut self.tracer, ), )); self.next() @@ -502,7 +489,7 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> self.global_counter.clone(), self.bodies[self.current_proving].clone(), self.constraints.clone(), - &mut self.current_tracer, + &mut self.tracer, )); self.next() } diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 60ea6f5..51d90ca 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -106,14 +106,7 @@ impl Tracer for IndentedTracer { Style::new().fg::() }; - if i == self.depth - 1 && self.first - { - print!("{}", "🭋".style(style)); - } - else - { - print!("{}", "▐".style(style)); - } + print!("{}", "│".style(style)); } self.first = false; println!("{}", show); From 70afc2a20199a856cf263562c024acfdafaf1222 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Mon, 9 Feb 2026 23:26:29 +0100 Subject: [PATCH 06/10] Putting provers in separate files --- 1.pl | 1 + src/main.rs | 3 +- src/prover.rs | 4 + src/prover/and.rs | 172 ++++++++++++++++++++++++++++++++++++++++ src/prover/body.rs | 70 ++++++++++++++++ src/prover/or.rs | 124 +++++++++++++++++++++++++++++ src/prover/predicate.rs | 132 ++++++++++++++++++++++++++++++ src/prover/tracing.rs | 2 + 8 files changed, 507 insertions(+), 1 deletion(-) create mode 100644 src/prover/and.rs create mode 100644 src/prover/body.rs create mode 100644 src/prover/or.rs create mode 100644 src/prover/predicate.rs diff --git a/1.pl b/1.pl index 4363d7e..4c0d8bc 100644 --- a/1.pl +++ b/1.pl @@ -7,3 +7,4 @@ add(X, s(Y), Z) :- add(s(X), Y, Z). mult(zero, X, zero). mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z). + diff --git a/src/main.rs b/src/main.rs index 0034206..ef05226 100644 --- a/src/main.rs +++ b/src/main.rs @@ -21,7 +21,8 @@ fn main() .into(); //let prop: Body = "integer(s(X))".into(); - let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); + let prop: Body = "mult(X, s(zero), 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 5aff903..4a4928e 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -1,4 +1,8 @@ +pub mod and; +pub mod body; pub mod constraints; +pub mod or; +pub mod predicate; pub mod tracing; pub mod unification; diff --git a/src/prover/and.rs b/src/prover/and.rs new file mode 100644 index 0000000..a7c9125 --- /dev/null +++ b/src/prover/and.rs @@ -0,0 +1,172 @@ +use std::fmt::Write; + +use owo_colors::OwoColorize; + +use crate::ast::Body; +use crate::ast::Module; +use crate::prover::Counter; +use crate::prover::GlobalCounter; +use crate::prover::body::BodyProver; +use crate::prover::constraints::Constraints; +use crate::prover::tracing::ProofType; +use crate::prover::tracing::Tracer; + +pub struct AndProver<'a, T: Tracer> +{ + module: &'a Module, + bodies: Vec, + tracer: T, + + global_counter: GlobalCounter, + sub_proofs: Vec<(Counter, BodyProver<'a>)>, +} +impl AndProver<'_, T> +{ + pub fn new<'a>( + module: &'a Module, + global_counter: GlobalCounter, + bodies: Vec, + constraints: Constraints, + tracer: &mut T, + ) -> AndProver<'a, T> + where + T: 'a, + { + assert!(!bodies.is_empty()); + + // Pretty logging + let mut tracer = tracer.begin_proof(ProofType::And); + let mut next = String::new(); + for x in bodies.iter().skip(1) + { + let _ = next.write_str(&format!("{}, ", x)); + } + + let mut conjuction = String::new(); + let len = bodies.len(); + for (i, x) in bodies.iter().enumerate() + { + let _ = conjuction.write_str(&format!("{}", x)); + if i != len - 1 + { + let _ = conjuction.write_str(" ∧ "); + } + } + + tracer.print_step(format!("Proving conjuction {}", conjuction)); + tracer.print_step(format!("{} :", "Proved".fg::(),)); + tracer.print_step(format!( + "{} : {}", + "Proving".fg::(), + bodies[0] + )); + tracer.print_step(format!( + "{} : {}", + "Next".fg::(), + next + )); + tracer.print_step(format!("With constraints : {}", constraints.simplified())); + // End pretty logging + + AndProver { + module, + sub_proofs: vec![( + global_counter.snapshot(), + BodyProver::new( + module, + global_counter.clone(), + bodies[0].clone(), + constraints.clone(), + &mut tracer, + ), + )], + tracer, + bodies, + global_counter, + } + } +} +impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + if self.sub_proofs.is_empty() + { + return None; + } + + let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap(); + + match current_proof.next() + { + Some(constraints) => + { + if self.sub_proofs.len() == self.bodies.len() - 1 + { + self.sub_proofs.push((current_proof_snap, current_proof)); + Some(constraints) + } + else + { + // Pretty logging + let mut proved = String::new(); + let mut proving = String::new(); + let mut next = String::new(); + for (i, x) in self.bodies.iter().enumerate() + { + let dest; + if i == self.sub_proofs.len() + 1 + { + dest = &mut proving; + } + else if i < self.sub_proofs.len() + 1 + { + dest = &mut proved; + } + else + { + dest = &mut next; + } + let _ = dest.write_str(&format!("{}, ", x)); + } + self.tracer.print_step(format!( + "{} : {}", + "Proved".fg::(), + proved + )); + self.tracer.print_step(format!( + "{} : {}", + "Proving".fg::(), + proving + )); + self.tracer.print_step(format!( + "{} : {}", + "Next".fg::(), + next + )); + // End pretty logging + + self.sub_proofs.push((current_proof_snap, current_proof)); + self.sub_proofs.push(( + self.global_counter.snapshot(), + BodyProver::new( + self.module, + self.global_counter.clone(), + self.bodies[self.sub_proofs.len()].clone(), + constraints, + &mut self.tracer, + ), + )); + self.next() + } + } + None => + { + self.global_counter.restore(current_proof_snap); + self.next() + } + } + } +} diff --git a/src/prover/body.rs b/src/prover/body.rs new file mode 100644 index 0000000..3388d19 --- /dev/null +++ b/src/prover/body.rs @@ -0,0 +1,70 @@ +use crate::ast::Body; +use crate::ast::Module; +use crate::prover::GlobalCounter; +use crate::prover::and::AndProver; +use crate::prover::constraints::Constraints; +use crate::prover::predicate::PredicateProver; +use crate::prover::tracing::Tracer; + +pub struct BodyProver<'a> +{ + prover: Box + 'a>, +} + +impl<'a> BodyProver<'a> +{ + pub fn new( + module: &'a Module, + global_counter: GlobalCounter, + body: Body, + constraints: Constraints, + tracer: &mut T, + ) -> BodyProver<'a> + { + let prover: Box> = match &body + { + Body::Term(predicate) => Box::new(PredicateProver::new( + module, + global_counter, + predicate.clone(), + constraints.clone(), + tracer, + )), + + // Shortcut And & Or prover if it contains only one element to simplify proofs + Body::And(items) | Body::Or(items) if items.len() == 1 => Box::new(BodyProver::new( + module, + global_counter, + items[0].clone(), + constraints.clone(), + tracer, + )), + + Body::And(items) => Box::new(AndProver::new( + module, + global_counter, + items.clone(), + constraints.clone(), + tracer, + )), + Body::Or(items) => Box::new(BodyProver::new( + module, + global_counter, + items[0].clone(), + constraints.clone(), + tracer, + )), + }; + + BodyProver { prover } + } +} + +impl<'a> Iterator for BodyProver<'a> +{ + type Item = Constraints; + fn next(&mut self) -> Option + { + self.prover.next() + } +} diff --git a/src/prover/or.rs b/src/prover/or.rs new file mode 100644 index 0000000..e12f35b --- /dev/null +++ b/src/prover/or.rs @@ -0,0 +1,124 @@ +use std::fmt::Write; + +use crate::ast::Body; +use crate::ast::Module; +use crate::prover::Counter; +use crate::prover::GlobalCounter; +use crate::prover::body::BodyProver; +use crate::prover::constraints::Constraints; +use crate::prover::tracing::ProofType; +use crate::prover::tracing::Tracer; + +pub struct OrProver<'a, T: Tracer> +{ + module: &'a Module, + bodies: Vec, + constraints: Constraints, + tracer: T, + + current_proving: usize, + global_counter: GlobalCounter, + counter_snapshot: Counter, + sub_proof: Option>, +} + +impl OrProver<'_, T> +{ + pub fn new<'a>( + module: &'a Module, + global_counter: GlobalCounter, + bodies: Vec, + constraints: Constraints, + tracer: &mut T, + ) -> OrProver<'a, T> + where + T: 'a, + { + assert!(!bodies.is_empty()); + + // Pretty logging + let mut tracer = tracer.begin_proof(ProofType::And); + + let mut next = String::new(); + for x in bodies.iter().skip(1) + { + let _ = next.write_str(&format!("{}, ", x)); + } + + let mut disjunction = String::new(); + let len = bodies.len(); + for (i, x) in bodies.iter().enumerate() + { + let _ = disjunction.write_str(&format!("{}", x)); + if i != len - 1 + { + let _ = disjunction.write_str(" ∨ "); + } + } + + // End pretty logging + + OrProver { + module, + sub_proof: Some(BodyProver::new( + module, + global_counter.clone(), + bodies[0].clone(), + constraints.clone(), + &mut tracer, + )), + tracer, + current_proving: 0, + counter_snapshot: global_counter.snapshot(), + bodies, + constraints, + global_counter, + } + } +} + +impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + let proof = match &mut self.sub_proof + { + Some(sub_proof) => sub_proof.next(), + None => + { + return None; + } + }; + + match proof + { + Some(x) => Some(x), + None => + { + // Advance to next possibility + if self.current_proving == self.bodies.len() - 1 + { + self.sub_proof = None; + None + } + else + { + self.current_proving += 1; + self.global_counter.restore(self.counter_snapshot); + self.tracer + .print_step(format!("Tring with {}", self.bodies[self.current_proving])); + self.sub_proof = Some(BodyProver::new( + self.module, + self.global_counter.clone(), + self.bodies[self.current_proving].clone(), + self.constraints.clone(), + &mut self.tracer, + )); + self.next() + } + } + } + } +} diff --git a/src/prover/predicate.rs b/src/prover/predicate.rs new file mode 100644 index 0000000..5ae7edb --- /dev/null +++ b/src/prover/predicate.rs @@ -0,0 +1,132 @@ +use owo_colors::OwoColorize; +use owo_colors::colors::Green; + +use crate::ast::{Module, Predicate}; +use crate::prover::body::BodyProver; +use crate::prover::constraints::Constraints; +use crate::prover::tracing::{ProofType, Tracer}; +use crate::prover::{Counter, GlobalCounter}; + +pub struct PredicateProver<'a, T: Tracer> +{ + module: &'a Module, + predicate: Predicate, + constraints: Constraints, + counter_snapshot: Counter, + tracer: T, + + global_counter: GlobalCounter, + current_clause: usize, + sub_proof: Option>, +} + +impl<'a, T: Tracer + 'a> PredicateProver<'a, T> +{ + pub fn new( + module: &'a Module, + global_counter: GlobalCounter, + predicate: Predicate, + constraints: Constraints, + tracer: &mut T, + ) -> PredicateProver<'a, T> + { + //info!(target: "PredicateProver", "Proving {}", predicate); + let mut predicate_prover = tracer.begin_proof(ProofType::Predicate); + predicate_prover.print_step(format!( + "{} '{}'", + "Proving predicate".fg::(), + predicate + )); + PredicateProver { + module, + tracer: predicate_prover, + predicate, + constraints, + current_clause: 0, + sub_proof: None, + counter_snapshot: global_counter.snapshot(), + global_counter, + } + } +} + +impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + match self.sub_proof.as_mut() + { + None => + { + if self.current_clause == self.module.clauses.len() + { + None + } + else + { + let clause = &self.module.clauses[self.current_clause] + .make_unique(self.global_counter.clone()); + let uni = self.predicate.matches(&clause.head); + let full_constraints = uni.and_then(|x| x.and(&self.constraints)); + + if let Some(c) = &full_constraints + { + self.tracer.print_step(format!( + "Unifying '{}' aginst '{}'", + self.predicate, clause + )); + self.tracer.print_step(format!( + "↳ {}: {}", + "Matches".fg::(), + c.simplified() + )); + } + + match full_constraints + { + Some(constraints) if clause.body.is_none() => + { + self.current_clause += 1; + Some(constraints) + } + Some(constraints) => + { + self.current_clause += 1; + self.counter_snapshot = self.global_counter.snapshot(); + self.sub_proof = Some(BodyProver::new( + self.module, + self.global_counter.clone(), + clause.body.clone().unwrap(), + constraints, + &mut self.tracer, + )); + self.next() + } + None => + { + self.global_counter.restore(self.counter_snapshot); + self.current_clause += 1; + self.next() + } + } + } + } + Some(prover) => + { + let next = prover.next(); + match next + { + Some(constraints) => Some(constraints), + None => + { + self.global_counter.restore(self.counter_snapshot); + self.sub_proof = None; + self.next() + } + } + } + } + } +} diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 51d90ca..f97400e 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -110,6 +110,8 @@ impl Tracer for IndentedTracer } self.first = false; println!("{}", show); + let _ = std::io::stdin().read_line(&mut String::new()); + println!("\x1b[2A"); } fn end_proof(self) From 298d17994385319d47dcf25442bf80a87bcdf184 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Tue, 10 Feb 2026 00:07:06 +0100 Subject: [PATCH 07/10] Adds not prover --- 1.pl | 12 ++ src/prover.rs | 454 +--------------------------------------------- src/prover/not.rs | 71 ++++++++ 3 files changed, 84 insertions(+), 453 deletions(-) create mode 100644 src/prover/not.rs diff --git a/1.pl b/1.pl index 4c0d8bc..29e751f 100644 --- a/1.pl +++ b/1.pl @@ -1,10 +1,22 @@ +:- use_module(library(clpfd)). + entier(zero). entier(s(X)) :- entier(X). add(X, zero, X). add(X, s(Y), Z) :- add(s(X), Y, Z). +inf(zero, X) :- entier(X). +inf(s(X), s(Y)) :- inf(X, Y). + mult(zero, X, zero). mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z). +div(A, B) :- inf(A, B), inf(X, B), mult(X, A, B). +div_w(X, Y) :- inf(s(X), Y), inf(s(s(zero)), X), div(X, Y). +prime(X) :- entier(X), \+ div_w(_, X). + +peano(X, zero) :- X #= 0. +peano(X, s(P)) :- X #> 0, X #= Y + 1, peano(Y, P). + diff --git a/src/prover.rs b/src/prover.rs index 4a4928e..70022f2 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -1,20 +1,16 @@ pub mod and; pub mod body; pub mod constraints; +pub mod not; pub mod or; pub mod predicate; pub mod tracing; pub mod unification; use std::cell::Cell; -use std::fmt::Write; use std::rc::Rc; use litemap::LiteMap; -use owo_colors::OwoColorize; -use owo_colors::colors::Green; -use owo_colors::colors::Red; -use owo_colors::colors::Yellow; use crate::ast::Body; use crate::ast::Clause; @@ -22,8 +18,6 @@ use crate::ast::Module; use crate::ast::Predicate; use crate::prover::constraints::Constraints; use crate::prover::tracing::IndentedTracer; -use crate::prover::tracing::ProofType; -use crate::prover::tracing::Tracer; #[derive(Clone, Copy, Debug, Default)] pub struct Counter(usize); @@ -56,452 +50,6 @@ impl GlobalCounter } } -pub struct BodyProver<'a> -{ - prover: Box + 'a>, -} - -pub struct PredicateProver<'a, T: Tracer> -{ - module: &'a Module, - predicate: Predicate, - constraints: Constraints, - counter_snapshot: Counter, - tracer: T, - - global_counter: GlobalCounter, - current_clause: usize, - sub_proof: Option>, -} - -pub struct AndProver<'a, T: Tracer> -{ - module: &'a Module, - bodies: Vec, - tracer: T, - - global_counter: GlobalCounter, - sub_proofs: Vec<(Counter, BodyProver<'a>)>, -} - -pub struct OrProver<'a, T: Tracer> -{ - module: &'a Module, - bodies: Vec, - constraints: Constraints, - tracer: T, - - current_proving: usize, - global_counter: GlobalCounter, - counter_snapshot: Counter, - sub_proof: Option>, -} - -impl<'a> BodyProver<'a> -{ - pub fn new( - module: &'a Module, - global_counter: GlobalCounter, - body: Body, - constraints: Constraints, - tracer: &mut T, - ) -> BodyProver<'a> - { - let prover: Box> = match &body - { - Body::Term(predicate) => Box::new(PredicateProver::new( - module, - global_counter, - predicate.clone(), - constraints.clone(), - tracer, - )), - - // Shortcut And & Or prover if it contains only one element to simplify proofs - Body::And(items) | Body::Or(items) if items.len() == 1 => Box::new(BodyProver::new( - module, - global_counter, - items[0].clone(), - constraints.clone(), - tracer, - )), - - Body::And(items) => Box::new(AndProver::new( - module, - global_counter, - items.clone(), - constraints.clone(), - tracer, - )), - Body::Or(items) => Box::new(BodyProver::new( - module, - global_counter, - items[0].clone(), - constraints.clone(), - tracer, - )), - }; - - BodyProver { prover } - } -} - -impl<'a, T: Tracer + 'a> PredicateProver<'a, T> -{ - pub fn new( - module: &'a Module, - global_counter: GlobalCounter, - predicate: Predicate, - constraints: Constraints, - tracer: &mut T, - ) -> PredicateProver<'a, T> - { - //info!(target: "PredicateProver", "Proving {}", predicate); - let mut predicate_prover = tracer.begin_proof(ProofType::Predicate); - predicate_prover.print_step(format!( - "{} '{}'", - "Proving predicate".fg::(), - predicate - )); - PredicateProver { - module, - tracer: predicate_prover, - predicate, - constraints, - current_clause: 0, - sub_proof: None, - counter_snapshot: global_counter.snapshot(), - global_counter, - } - } -} - -impl AndProver<'_, T> -{ - pub fn new<'a>( - module: &'a Module, - global_counter: GlobalCounter, - bodies: Vec, - constraints: Constraints, - tracer: &mut T, - ) -> AndProver<'a, T> - where - T: 'a, - { - assert!(!bodies.is_empty()); - - // Pretty logging - let mut tracer = tracer.begin_proof(ProofType::And); - let mut next = String::new(); - for x in bodies.iter().skip(1) - { - let _ = next.write_str(&format!("{}, ", x)); - } - - let mut conjuction = String::new(); - let len = bodies.len(); - for (i, x) in bodies.iter().enumerate() - { - let _ = conjuction.write_str(&format!("{}", x)); - if i != len - 1 - { - let _ = conjuction.write_str(" ∧ "); - } - } - - tracer.print_step(format!("Proving conjuction {}", conjuction)); - tracer.print_step(format!("{} :", "Proved".fg::(),)); - tracer.print_step(format!("{} : {}", "Proving".fg::(), bodies[0])); - tracer.print_step(format!("{} : {}", "Next".fg::(), next)); - tracer.print_step(format!("With constraints : {}", constraints.simplified())); - // End pretty logging - - AndProver { - module, - sub_proofs: vec![( - global_counter.snapshot(), - BodyProver::new( - module, - global_counter.clone(), - bodies[0].clone(), - constraints.clone(), - &mut tracer, - ), - )], - tracer, - bodies, - global_counter, - } - } -} - -impl OrProver<'_, T> -{ - pub fn new<'a>( - module: &'a Module, - global_counter: GlobalCounter, - bodies: Vec, - constraints: Constraints, - tracer: &mut T, - ) -> OrProver<'a, T> - where - T: 'a, - { - assert!(!bodies.is_empty()); - - // Pretty logging - let mut tracer = tracer.begin_proof(ProofType::And); - - let mut next = String::new(); - for x in bodies.iter().skip(1) - { - let _ = next.write_str(&format!("{}, ", x)); - } - - let mut disjunction = String::new(); - let len = bodies.len(); - for (i, x) in bodies.iter().enumerate() - { - let _ = disjunction.write_str(&format!("{}", x)); - if i != len - 1 - { - let _ = disjunction.write_str(" ∨ "); - } - } - - // End pretty logging - - OrProver { - module, - sub_proof: Some(BodyProver::new( - module, - global_counter.clone(), - bodies[0].clone(), - constraints.clone(), - &mut tracer, - )), - tracer, - current_proving: 0, - counter_snapshot: global_counter.snapshot(), - bodies, - constraints, - global_counter, - } - } -} - -impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> -{ - type Item = Constraints; - - fn next(&mut self) -> Option - { - match self.sub_proof.as_mut() - { - None => - { - if self.current_clause == self.module.clauses.len() - { - None - } - else - { - let clause = &self.module.clauses[self.current_clause] - .make_unique(self.global_counter.clone()); - let uni = self.predicate.matches(&clause.head); - let full_constraints = uni.and_then(|x| x.and(&self.constraints)); - - if let Some(c) = &full_constraints - { - self.tracer.print_step(format!( - "Unifying '{}' aginst '{}'", - self.predicate, clause - )); - self.tracer.print_step(format!( - "↳ {}: {}", - "Matches".fg::(), - c.simplified() - )); - } - - match full_constraints - { - Some(constraints) if clause.body.is_none() => - { - self.current_clause += 1; - Some(constraints) - } - Some(constraints) => - { - self.current_clause += 1; - self.counter_snapshot = self.global_counter.snapshot(); - self.sub_proof = Some(BodyProver::new( - self.module, - self.global_counter.clone(), - clause.body.clone().unwrap(), - constraints, - &mut self.tracer, - )); - self.next() - } - None => - { - self.global_counter.restore(self.counter_snapshot); - self.current_clause += 1; - self.next() - } - } - } - } - Some(prover) => - { - let next = prover.next(); - match next - { - Some(constraints) => Some(constraints), - None => - { - self.global_counter.restore(self.counter_snapshot); - self.sub_proof = None; - self.next() - } - } - } - } - } -} - -impl<'a> Iterator for BodyProver<'a> -{ - type Item = Constraints; - fn next(&mut self) -> Option - { - self.prover.next() - } -} - -impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> -{ - type Item = Constraints; - - fn next(&mut self) -> Option - { - if self.sub_proofs.is_empty() - { - return None; - } - - let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap(); - - match current_proof.next() - { - Some(constraints) => - { - if self.sub_proofs.len() == self.bodies.len() - 1 - { - self.sub_proofs.push((current_proof_snap, current_proof)); - Some(constraints) - } - else - { - // Pretty logging - let mut proved = String::new(); - let mut proving = String::new(); - let mut next = String::new(); - for (i, x) in self.bodies.iter().enumerate() - { - let dest; - if i == self.sub_proofs.len() + 1 - { - dest = &mut proving; - } - else if i < self.sub_proofs.len() + 1 - { - dest = &mut proved; - } - else - { - dest = &mut next; - } - let _ = dest.write_str(&format!("{}, ", x)); - } - self.tracer - .print_step(format!("{} : {}", "Proved".fg::(), proved)); - self.tracer - .print_step(format!("{} : {}", "Proving".fg::(), proving)); - self.tracer - .print_step(format!("{} : {}", "Next".fg::(), next)); - // End pretty logging - - self.sub_proofs.push((current_proof_snap, current_proof)); - self.sub_proofs.push(( - self.global_counter.snapshot(), - BodyProver::new( - self.module, - self.global_counter.clone(), - self.bodies[self.sub_proofs.len()].clone(), - constraints, - &mut self.tracer, - ), - )); - self.next() - } - } - None => - { - self.global_counter.restore(current_proof_snap); - self.next() - } - } - } -} - -impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> -{ - type Item = Constraints; - - fn next(&mut self) -> Option - { - let proof = match &mut self.sub_proof - { - Some(sub_proof) => sub_proof.next(), - None => - { - return None; - } - }; - - match proof - { - Some(x) => Some(x), - None => - { - // Advance to next possibility - if self.current_proving == self.bodies.len() - 1 - { - self.sub_proof = None; - None - } - else - { - self.current_proving += 1; - self.global_counter.restore(self.counter_snapshot); - self.tracer - .print_step(format!("Tring with {}", self.bodies[self.current_proving])); - self.sub_proof = Some(BodyProver::new( - self.module, - self.global_counter.clone(), - self.bodies[self.current_proving].clone(), - self.constraints.clone(), - &mut self.tracer, - )); - self.next() - } - } - } - } -} - impl Module { pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a> diff --git a/src/prover/not.rs b/src/prover/not.rs new file mode 100644 index 0000000..8fa41ed --- /dev/null +++ b/src/prover/not.rs @@ -0,0 +1,71 @@ +use crate::ast::Body; +use crate::ast::Module; +use crate::prover::GlobalCounter; +use crate::prover::body::BodyProver; +use crate::prover::constraints::Constraints; +use crate::prover::tracing::ProofType; +use crate::prover::tracing::Tracer; + +pub struct NotProver<'a, T: Tracer + 'a> +{ + prover: Option>, + constraints: Constraints, + tracer: T, +} + +impl<'a, T: Tracer + 'a> NotProver<'a, T> +{ + pub fn new( + module: &'a Module, + global_counter: GlobalCounter, + body: Body, + constraints: Constraints, + tracer: &mut T, + ) -> NotProver<'a, T> + { + let mut not_tracer = tracer.begin_proof(ProofType::Body); + NotProver { + prover: Some(BodyProver::new( + module, + global_counter, + body, + constraints.clone(), + &mut not_tracer, + )), + tracer: not_tracer, + constraints: constraints.clone(), + } + } +} + +impl<'a, T: Tracer + 'a> Iterator for NotProver<'a, T> +{ + type Item = Constraints; + fn next(&mut self) -> Option + { + if let Some(x) = self.prover.as_mut() + { + match &mut x.next() + { + Some(_) => + { + // The prover showed that the proof is true. + // Thus the negation is never true + self.prover = None; + None + } + None => + { + // The prover did not find any proof + // Thus the negation is true + self.prover = None; + Some(self.constraints.clone()) + } + } + } + else + { + None + } + } +} From 1c17aa20c2226bd597a0837113e5f81a13022c10 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Tue, 10 Feb 2026 17:21:06 +0100 Subject: [PATCH 08/10] Starts proof cache infra --- Cargo.lock | 53 ++++++++++++-- Cargo.toml | 3 +- src/ast.rs | 25 +++++-- src/parsing.rs | 3 +- src/prover.rs | 42 ++++++++--- src/prover/constraints.rs | 14 ++-- src/prover/proof_cache.rs | 150 ++++++++++++++++++++++++++++++++++++++ src/prover/tracing.rs | 15 ---- 8 files changed, 256 insertions(+), 49 deletions(-) create mode 100644 src/prover/proof_cache.rs 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) -} From d8180a982e1a82ebe8df53d22c01f1be3b66cec2 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Tue, 10 Feb 2026 18:11:50 +0100 Subject: [PATCH 09/10] 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) {} +} From 54724c2f4c3343aba112d2743f9a5102c0e8761d Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Tue, 10 Feb 2026 21:48:58 +0100 Subject: [PATCH 10/10] Caching was a bad idea --- src/prover.rs | 2 - src/prover/proof_cache.rs | 239 -------------------------------------- src/prover/tracing.rs | 2 - 3 files changed, 243 deletions(-) delete mode 100644 src/prover/proof_cache.rs diff --git a/src/prover.rs b/src/prover.rs index 7903f2c..00177c3 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -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)] diff --git a/src/prover/proof_cache.rs b/src/prover/proof_cache.rs deleted file mode 100644 index ef8f354..0000000 --- a/src/prover/proof_cache.rs +++ /dev/null @@ -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> -{ - proved: Vec, - prover: T, -} - -pub struct CachedProver<'a> -{ - module: &'a Module, - cache: Rc>>>>, - normalized_body: Body, - normalized_counter: usize, - mapping: VariableMap, - constraints: Constraints, - - 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, - 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 - { - 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); - -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) - -> 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 - } - } - } -} - -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 2c4fde1..f427793 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -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 {