Adds not prover
This commit is contained in:
12
1.pl
12
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).
|
||||
|
||||
|
||||
|
||||
454
src/prover.rs
454
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<dyn Iterator<Item = Constraints> + '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<BodyProver<'a>>,
|
||||
}
|
||||
|
||||
pub struct AndProver<'a, T: Tracer>
|
||||
{
|
||||
module: &'a Module,
|
||||
bodies: Vec<Body>,
|
||||
tracer: T,
|
||||
|
||||
global_counter: GlobalCounter,
|
||||
sub_proofs: Vec<(Counter, BodyProver<'a>)>,
|
||||
}
|
||||
|
||||
pub struct OrProver<'a, T: Tracer>
|
||||
{
|
||||
module: &'a Module,
|
||||
bodies: Vec<Body>,
|
||||
constraints: Constraints,
|
||||
tracer: T,
|
||||
|
||||
current_proving: usize,
|
||||
global_counter: GlobalCounter,
|
||||
counter_snapshot: Counter,
|
||||
sub_proof: Option<BodyProver<'a>>,
|
||||
}
|
||||
|
||||
impl<'a> BodyProver<'a>
|
||||
{
|
||||
pub fn new<T: Tracer + 'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
body: Body,
|
||||
constraints: Constraints,
|
||||
tracer: &mut T,
|
||||
) -> BodyProver<'a>
|
||||
{
|
||||
let prover: Box<dyn Iterator<Item = Constraints>> = 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::<Green>(),
|
||||
predicate
|
||||
));
|
||||
PredicateProver {
|
||||
module,
|
||||
tracer: predicate_prover,
|
||||
predicate,
|
||||
constraints,
|
||||
current_clause: 0,
|
||||
sub_proof: None,
|
||||
counter_snapshot: global_counter.snapshot(),
|
||||
global_counter,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<T: Tracer> AndProver<'_, T>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
bodies: Vec<Body>,
|
||||
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::<Green>(),));
|
||||
tracer.print_step(format!("{} : {}", "Proving".fg::<Yellow>(), bodies[0]));
|
||||
tracer.print_step(format!("{} : {}", "Next".fg::<Red>(), 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<T: Tracer> OrProver<'_, T>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
bodies: Vec<Body>,
|
||||
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<Self::Item>
|
||||
{
|
||||
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::<Green>(),
|
||||
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<Constraints>
|
||||
{
|
||||
self.prover.next()
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
|
||||
{
|
||||
type Item = Constraints;
|
||||
|
||||
fn next(&mut self) -> Option<Self::Item>
|
||||
{
|
||||
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::<Green>(), proved));
|
||||
self.tracer
|
||||
.print_step(format!("{} : {}", "Proving".fg::<Yellow>(), proving));
|
||||
self.tracer
|
||||
.print_step(format!("{} : {}", "Next".fg::<Red>(), 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<Self::Item>
|
||||
{
|
||||
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>
|
||||
|
||||
71
src/prover/not.rs
Normal file
71
src/prover/not.rs
Normal file
@ -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<BodyProver<'a>>,
|
||||
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<Constraints>
|
||||
{
|
||||
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
|
||||
}
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user