Working
This commit is contained in:
382
src/prover.rs
Normal file
382
src/prover.rs
Normal file
@ -0,0 +1,382 @@
|
||||
pub mod constraints;
|
||||
pub mod trace;
|
||||
pub mod unification;
|
||||
|
||||
use std::cell::Cell;
|
||||
use std::collections::VecDeque;
|
||||
use std::rc::Rc;
|
||||
|
||||
use litemap::LiteMap;
|
||||
use log::info;
|
||||
|
||||
use crate::ast::Body;
|
||||
use crate::ast::Clause;
|
||||
use crate::ast::Module;
|
||||
use crate::ast::Predicate;
|
||||
use crate::prover::constraints::Constraints;
|
||||
|
||||
#[derive(Clone, Copy, Debug, Default)]
|
||||
pub struct Counter(usize);
|
||||
|
||||
#[derive(Clone, Debug, Default)]
|
||||
pub struct GlobalCounter(Rc<Cell<usize>>);
|
||||
|
||||
impl GlobalCounter
|
||||
{
|
||||
pub fn new() -> GlobalCounter
|
||||
{
|
||||
GlobalCounter(Rc::new(Cell::new(0)))
|
||||
}
|
||||
|
||||
pub fn get(&self) -> usize
|
||||
{
|
||||
let val = self.0.get();
|
||||
self.0.set(val + 1);
|
||||
val
|
||||
}
|
||||
|
||||
pub fn snapshot(&self) -> Counter
|
||||
{
|
||||
Counter(self.0.get())
|
||||
}
|
||||
|
||||
pub fn restore(&mut self, snapshot: Counter)
|
||||
{
|
||||
self.0.set(snapshot.0);
|
||||
}
|
||||
}
|
||||
|
||||
pub struct BodyProver<'a>
|
||||
{
|
||||
module: &'a Module,
|
||||
constraints: Constraints,
|
||||
|
||||
prover: Box<dyn Iterator<Item = Constraints> + 'a>,
|
||||
}
|
||||
|
||||
pub struct PredicateProver<'a>
|
||||
{
|
||||
module: &'a Module,
|
||||
predicate: Predicate,
|
||||
constraints: Constraints,
|
||||
counter_snapshot: Counter,
|
||||
|
||||
global_counter: GlobalCounter,
|
||||
current_clause: usize,
|
||||
sub_proof: Option<BodyProver<'a>>,
|
||||
}
|
||||
|
||||
pub struct AndProver<'a>
|
||||
{
|
||||
module: &'a Module,
|
||||
bodies: Vec<Body>,
|
||||
constraints: Constraints,
|
||||
|
||||
global_counter: GlobalCounter,
|
||||
sub_proofs: VecDeque<(Counter, BodyProver<'a>)>,
|
||||
}
|
||||
|
||||
impl BodyProver<'_>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
body: Body,
|
||||
constraints: Constraints,
|
||||
) -> 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(),
|
||||
)),
|
||||
Body::And(items) => Box::new(AndProver::new(
|
||||
module,
|
||||
global_counter,
|
||||
items.clone(),
|
||||
constraints.clone(),
|
||||
)),
|
||||
Body::Or(items) => Box::new(BodyProver::new(
|
||||
module,
|
||||
global_counter,
|
||||
items[0].clone(),
|
||||
constraints.clone(),
|
||||
)),
|
||||
};
|
||||
info!(target: "BodyProver", "Proving {}", body);
|
||||
BodyProver {
|
||||
module,
|
||||
constraints,
|
||||
prover,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl PredicateProver<'_>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
predicate: Predicate,
|
||||
constraints: Constraints,
|
||||
) -> PredicateProver<'a>
|
||||
{
|
||||
info!(target: "PredicateProver", "Proving {}", predicate);
|
||||
PredicateProver {
|
||||
module,
|
||||
predicate,
|
||||
constraints,
|
||||
current_clause: 0,
|
||||
sub_proof: None,
|
||||
counter_snapshot: global_counter.snapshot(),
|
||||
global_counter,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl AndProver<'_>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
bodies: Vec<Body>,
|
||||
constraints: Constraints,
|
||||
) -> AndProver<'a>
|
||||
{
|
||||
assert!(!bodies.is_empty());
|
||||
|
||||
AndProver {
|
||||
module,
|
||||
sub_proofs: VecDeque::from(vec![(
|
||||
global_counter.snapshot(),
|
||||
BodyProver::new(
|
||||
module,
|
||||
global_counter.clone(),
|
||||
bodies[0].clone(),
|
||||
constraints.clone(),
|
||||
),
|
||||
)]),
|
||||
bodies,
|
||||
constraints,
|
||||
global_counter,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Iterator for PredicateProver<'_>
|
||||
{
|
||||
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());
|
||||
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));
|
||||
|
||||
if let Some(c) = &full_constraints
|
||||
{
|
||||
info!(target: "PredicateProver", " => {}", c);
|
||||
}
|
||||
else
|
||||
{
|
||||
info!(target: "PredicateProver", " => (Can't unify)");
|
||||
}
|
||||
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,
|
||||
));
|
||||
self.next()
|
||||
}
|
||||
None =>
|
||||
{
|
||||
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 Iterator for BodyProver<'_>
|
||||
{
|
||||
type Item = Constraints;
|
||||
fn next(&mut self) -> Option<Constraints>
|
||||
{
|
||||
self.prover.next()
|
||||
}
|
||||
}
|
||||
|
||||
impl Iterator for AndProver<'_>
|
||||
{
|
||||
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_back().unwrap();
|
||||
|
||||
match current_proof.next()
|
||||
{
|
||||
Some(constraints) =>
|
||||
{
|
||||
if self.sub_proofs.len() == self.bodies.len() - 1
|
||||
{
|
||||
self.sub_proofs
|
||||
.push_back((current_proof_snap, current_proof));
|
||||
Some(constraints)
|
||||
}
|
||||
else
|
||||
{
|
||||
self.sub_proofs
|
||||
.push_back((current_proof_snap, current_proof));
|
||||
self.sub_proofs.push_back((
|
||||
self.global_counter.snapshot(),
|
||||
BodyProver::new(
|
||||
self.module,
|
||||
self.global_counter.clone(),
|
||||
self.bodies[self.sub_proofs.len()].clone(),
|
||||
constraints,
|
||||
),
|
||||
));
|
||||
self.next()
|
||||
}
|
||||
}
|
||||
None =>
|
||||
{
|
||||
self.global_counter.restore(current_proof_snap);
|
||||
self.next()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Module
|
||||
{
|
||||
pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a>
|
||||
{
|
||||
BodyProver::new(
|
||||
self,
|
||||
GlobalCounter::new(),
|
||||
body.clone(),
|
||||
Constraints::none(),
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
impl Clause
|
||||
{
|
||||
pub fn make_unique(&self, counter: GlobalCounter) -> Clause
|
||||
{
|
||||
let mut unique_map = LiteMap::new();
|
||||
Clause {
|
||||
head: self.head.make_unique(counter.clone(), &mut unique_map),
|
||||
body: self
|
||||
.body
|
||||
.as_ref()
|
||||
.map(|body| body.make_unique(counter.clone(), &mut unique_map)),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Body
|
||||
{
|
||||
pub fn make_unique(
|
||||
&self,
|
||||
counter: GlobalCounter,
|
||||
unique_map: &mut LiteMap<String, usize>,
|
||||
) -> Body
|
||||
{
|
||||
match self
|
||||
{
|
||||
Body::Term(predicate) => Body::Term(predicate.make_unique(counter.clone(), unique_map)),
|
||||
Body::And(items) => Body::And(
|
||||
items
|
||||
.iter()
|
||||
.map(|x| x.make_unique(counter.clone(), unique_map))
|
||||
.collect(),
|
||||
),
|
||||
Body::Or(items) => Body::Or(
|
||||
items
|
||||
.iter()
|
||||
.map(|x| x.make_unique(counter.clone(), unique_map))
|
||||
.collect(),
|
||||
),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Predicate
|
||||
{
|
||||
pub fn make_unique(
|
||||
&self,
|
||||
counter: GlobalCounter,
|
||||
unique_map: &mut LiteMap<String, usize>,
|
||||
) -> Self
|
||||
{
|
||||
match self
|
||||
{
|
||||
Predicate::Variable(name) => Predicate::Variable(format!(
|
||||
"_{}[{}]",
|
||||
name,
|
||||
unique_map
|
||||
.entry(name.clone())
|
||||
.or_insert_with(|| counter.get())
|
||||
)),
|
||||
Predicate::Fixed(name, predicates) => Predicate::Fixed(
|
||||
name.clone(),
|
||||
predicates
|
||||
.iter()
|
||||
.map(|x| x.make_unique(counter.clone(), unique_map))
|
||||
.collect(),
|
||||
),
|
||||
}
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user