Skip to content

Commit

Permalink
MapStack Optimization
Browse files Browse the repository at this point in the history
impl the optimization described in #9

Results are good.
```
test ancestry::infer_          ... bench:   1,201,454 ns/iter (+/- 20,579)
test ancestry::infer_30        ... bench:   3,758,380 ns/iter (+/- 76,535)
test ancestry::prove_          ... bench:   1,342,813 ns/iter (+/- 31,824)
test ancestry::prove_30        ... bench:   4,210,072 ns/iter (+/- 46,268)
test recursion_minimal::infer_ ... bench:      12,014 ns/iter (+/- 232)
test recursion_minimal::prove_ ... bench:      16,378 ns/iter (+/- 357)
```
  • Loading branch information
bddap committed Apr 23, 2021
1 parent 7bf82a1 commit 65766a9
Show file tree
Hide file tree
Showing 6 changed files with 81 additions and 115 deletions.
10 changes: 5 additions & 5 deletions src/common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,9 @@ where
/// [crate::prove::prove] function does not immediately convert LowRuleApplication's to
/// [RuleApplication]'s. Rather, it converts only the LowRuleApplication's it is going to return
/// to the caller.
pub struct LowRuleApplication {
pub(crate) struct LowRuleApplication {
pub rule_index: usize,
pub instantiations: BTreeMap<usize, usize>,
pub instantiations: Vec<Option<usize>>,
}

impl LowRuleApplication {
Expand Down Expand Up @@ -65,7 +65,7 @@ impl LowRuleApplication {

for unbound_human in original_rule.cononical_unbound() {
let unbound_local: usize = uhul[unbound_human];
let bound_global: usize = self.instantiations[&unbound_local];
let bound_global: usize = self.instantiations.get(unbound_local).unwrap().unwrap();
let bound_human: &Bound = trans.back(bound_global).unwrap();
instantiations.push(bound_human.clone());
}
Expand All @@ -81,7 +81,7 @@ impl LowRuleApplication {
/// This is a helper function. It translates all four element of a quad, calling
/// [Translator::forward] for each element. If any element has no translation
/// this function will return `None`.
pub fn forward<T: Ord>(translator: &Translator<T>, key: &[T; 4]) -> Option<Quad> {
pub(crate) fn forward<T: Ord>(translator: &Translator<T>, key: &[T; 4]) -> Option<Quad> {
let [s, p, o, g] = key;
Some(
[
Expand All @@ -97,7 +97,7 @@ pub fn forward<T: Ord>(translator: &Translator<T>, key: &[T; 4]) -> Option<Quad>
/// Reverse of [forward].
/// [forward] translates each element from `T` to `usize`. This function translates each element
/// from `usize` to `T`. If any element has no translation this function will return `None`.
pub fn back<T: Ord>(translator: &Translator<T>, key: Quad) -> Option<[&T; 4]> {
pub(crate) fn back<T: Ord>(translator: &Translator<T>, key: Quad) -> Option<[&T; 4]> {
let Quad { s, p, o, g } = key;
Some([
translator.back(s.0)?,
Expand Down
11 changes: 2 additions & 9 deletions src/infer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,15 +65,8 @@ fn low_infer(premises: &[Quad], rules: &[LowRule]) -> Vec<Quad> {
} in rules.iter_mut()
{
rs.apply_related(new.clone(), if_all, inst, &mut |inst| {
let ins = inst.as_ref();
for implied in then.iter() {
let new_quad = [
ins[&implied.s.0],
ins[&implied.p.0],
ins[&implied.o.0],
ins[&implied.g.0],
]
.into();
for implied in then.iter().cloned() {
let new_quad = implied.local_to_global(inst).unwrap();
if !rs.contains(&new_quad) && !adding.contains(&new_quad) {
to_add.insert(new_quad);
}
Expand Down
47 changes: 27 additions & 20 deletions src/mapstack.rs
Original file line number Diff line number Diff line change
@@ -1,51 +1,58 @@
use alloc::collections::BTreeMap;
use core::fmt;
use core::fmt::Debug;
use core::iter::FromIterator;

/// A mapping that keeps a history of writes. Writes to the map effect "pushes" to a stack. Those
/// "pushes" can be undone with a "pop".
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct MapStack<K, V> {
current: BTreeMap<K, V>,
history: Vec<(K, Option<V>)>,
///
/// Beware large keys when using this data structure. The memory used byt this structure scales
/// with the size of the largest key!
#[derive(Clone, Debug, PartialEq, Eq, Ord, PartialOrd, Default)]
pub(crate) struct MapStack<V> {
current: Vec<Option<V>>,
history: Vec<(usize, Option<V>)>,
}

impl<K: Ord, V> MapStack<K, V> {
impl<V> MapStack<V> {
pub fn new() -> Self {
Self {
current: BTreeMap::new(),
current: Vec::new(),
history: Vec::new(),
}
}
}

impl<K: Ord + Clone, V> MapStack<K, V> {
impl<V> MapStack<V> {
/// Set a value appending to write history.
pub fn write(&mut self, key: K, val: V) {
let old_val = self.current.insert(key.clone(), val);
self.history.push((key, old_val));
pub fn write(&mut self, key: usize, val: V) {
debug_assert!(key < 30 ^ 2, "Thats a pretty large key. Are you sure?");
if self.current.len() <= key {
self.current.resize_with(key + 1, || None);
}
let mut val = Some(val);
core::mem::swap(&mut self.current[key], &mut val);
self.history.push((key, val));
}

/// Undo most recent write or return error if there is no history to undo.
pub fn undo(&mut self) -> Result<(), NoMoreHistory> {
let (key, old_val) = self.history.pop().ok_or(NoMoreHistory)?;
match old_val {
Some(val) => self.current.insert(key, val),
None => self.current.remove(&key),
};
self.current[key] = old_val;
Ok(())
}
}

impl<K, V> AsRef<BTreeMap<K, V>> for MapStack<K, V> {
fn as_ref(&self) -> &BTreeMap<K, V> {
/// Get the current value at key.
pub fn get(&self, key: usize) -> Option<&V> {
self.current.get(key).and_then(|o| o.as_ref())
}

pub fn inner(&self) -> &Vec<Option<V>> {
&self.current
}
}

impl<K: Ord + Clone, V> FromIterator<(K, V)> for MapStack<K, V> {
fn from_iter<T: IntoIterator<Item = (K, V)>>(kvs: T) -> Self {
impl<V> FromIterator<(usize, V)> for MapStack<V> {
fn from_iter<T: IntoIterator<Item = (usize, V)>>(kvs: T) -> Self {
let mut ret = Self::new();
for (k, v) in kvs.into_iter() {
ret.write(k, v);
Expand Down
40 changes: 18 additions & 22 deletions src/prove.rs
Original file line number Diff line number Diff line change
Expand Up @@ -136,20 +136,13 @@ fn low_prove(
) in rules2.iter_mut()
{
rs.apply_related(fact.clone(), if_all, inst, &mut |inst| {
let ins = inst.as_ref();
for implied in then.iter() {
let new_quad = [
ins[&implied.s.0],
ins[&implied.p.0],
ins[&implied.o.0],
ins[&implied.g.0],
]
.into();
for implied in then.iter().cloned() {
let new_quad = implied.local_to_global(inst).unwrap();
if !rs.contains(&new_quad) && !adding_now.contains(&new_quad) {
arguments.entry(new_quad.clone()).or_insert_with(|| {
LowRuleApplication {
rule_index: *rule_index,
instantiations: ins.clone(),
instantiations: inst.inner().clone(),
}
});
to_add.insert(new_quad);
Expand Down Expand Up @@ -183,8 +176,11 @@ fn recall_proof(
outp: &mut Vec<LowRuleApplication>,
) {
let to_global_scope = |rra: &LowRuleApplication, locally_scoped: usize| -> usize {
let concrete = rules[rra.rule_index].inst.as_ref().get(&locally_scoped);
let found = rra.instantiations.get(&locally_scoped);
let concrete = rules[rra.rule_index].inst.get(locally_scoped);
let found = rra
.instantiations
.get(locally_scoped)
.and_then(|o| o.as_ref());
if let (Some(c), Some(f)) = (concrete, found) {
debug_assert_eq!(c, f);
}
Expand Down Expand Up @@ -237,7 +233,7 @@ impl std::error::Error for CantProve {}
/// An element of a deductive proof. Proofs can be transmitted and later validatated as long as the
/// validator assumes the same rule list as the prover.
///
/// Unbound variables are bound to the values in `instanitations`. They are bound in order of
/// Unbound variables are bound to the values in `instantiations`. They are bound in order of
/// initial appearance.
///
/// Given the rule:
Expand Down Expand Up @@ -311,31 +307,31 @@ impl<Bound: Clone> RuleApplication<Bound> {
/// Panics
///
/// panics if an unbound entity is not registered in map
/// panics if the canonical index of unbound (according to map) is too large to index instanitations
/// panics if the canonical index of unbound (according to map) is too large to index instantiations
fn bind_claim<Unbound: Ord, Bound: Clone>(
[s, p, o, g]: [Entity<Unbound, Bound>; 4],
map: &BTreeMap<&Unbound, usize>,
instanitations: &[Bound],
instantiations: &[Bound],
) -> [Bound; 4] {
[
bind_entity(s, map, instanitations),
bind_entity(p, map, instanitations),
bind_entity(o, map, instanitations),
bind_entity(g, map, instanitations),
bind_entity(s, map, instantiations),
bind_entity(p, map, instantiations),
bind_entity(o, map, instantiations),
bind_entity(g, map, instantiations),
]
}

/// Panics
///
/// panics if an unbound entity is not registered in map
/// panics if the canonical index of unbound (according to map) is too large to index instanitations
/// panics if the canonical index of unbound (according to map) is too large to index instantiations
fn bind_entity<Unbound: Ord, Bound: Clone>(
e: Entity<Unbound, Bound>,
map: &BTreeMap<&Unbound, usize>,
instanitations: &[Bound],
instantiations: &[Bound],
) -> Bound {
match e {
Entity::Unbound(a) => instanitations[map[&a]].clone(),
Entity::Unbound(a) => instantiations[map[&a]].clone(),
Entity::Bound(e) => e,
}
}
Expand Down
69 changes: 27 additions & 42 deletions src/reasoner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use crate::vecset::VecSet;
use core::cmp::Ordering;

#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
pub struct Quad {
pub(crate) struct Quad {
pub s: Subj,
pub p: Prop,
pub o: Obje,
Expand All @@ -22,13 +22,12 @@ impl Quad {

/// Attempt dereference all variable in self.
pub fn local_to_global(self, inst: &Instantiations) -> Option<Quad> {
let inst = inst.as_ref();
Some(
[
*inst.get(&self.s.0)?,
*inst.get(&self.p.0)?,
*inst.get(&self.o.0)?,
*inst.get(&self.g.0)?,
*inst.get(self.s.0)?,
*inst.get(self.p.0)?,
*inst.get(self.o.0)?,
*inst.get(self.g.0)?,
]
.into(),
)
Expand Down Expand Up @@ -82,10 +81,10 @@ type O = (Obje,);
type G = (Grap,);

/// Bindings of slots within the context of a rule.
pub type Instantiations = MapStack<usize, usize>;
pub(crate) type Instantiations = MapStack<usize>;

#[derive(Default)]
pub struct Reasoner {
pub(crate) struct Reasoner {
claims: Vec<Quad>,
spog: VecSet<usize>,
posg: VecSet<usize>,
Expand Down Expand Up @@ -137,7 +136,7 @@ impl Reasoner {
cb: &mut impl FnMut(&Instantiations),
) {
debug_assert!(self.contains(&quad));
debug_assert!(!rule.is_empty(), "potential confusing so disallowed");
debug_assert!(!rule.is_empty(), "potentialy confusing so disallowed");
// for each atom of rule, if the atom can match the quad, bind the unbound variables in the
// atom to the corresponding elements of quad, then call apply.
for i in 0..rule.len() {
Expand Down Expand Up @@ -181,7 +180,7 @@ impl Reasoner {
let to_write = strictest.clone().zip(quad.clone());
for (k, v) in &to_write {
debug_assert!(
if let Some(committed_v) = instantiations.as_ref().get(&k) {
if let Some(committed_v) = instantiations.get(*k) {
committed_v == v
} else {
true
Expand All @@ -200,13 +199,12 @@ impl Reasoner {
/// Return a slice representing all possible matches to the pattern provided.
/// pattern is in a local scope. instantiations is a partial translation of that
/// local scope to the global scope represented by self.claims
fn matches(&self, pattern: &Quad, instantiations: &Instantiations) -> &[usize] {
let inst = instantiations.as_ref();
fn matches(&self, pattern: &Quad, inst: &Instantiations) -> &[usize] {
let pattern: (Option<Subj>, Option<Prop>, Option<Obje>, Option<Grap>) = (
inst.get(&pattern.s.0).cloned().map(Subj),
inst.get(&pattern.p.0).cloned().map(Prop),
inst.get(&pattern.o.0).cloned().map(Obje),
inst.get(&pattern.g.0).cloned().map(Grap),
inst.get(pattern.s.0).cloned().map(Subj),
inst.get(pattern.p.0).cloned().map(Prop),
inst.get(pattern.o.0).cloned().map(Obje),
inst.get(pattern.g.0).cloned().map(Grap),
);
match pattern {
(Some(s), Some(p), Some(o), Some(g)) => (s, p, o, g).search(self),
Expand Down Expand Up @@ -251,7 +249,7 @@ impl Reasoner {
}
}

fn evict<'a, T>(index: usize, unordered_list: &'a mut [T]) -> Option<(&'a T, &'a mut [T])> {
fn evict<T>(index: usize, unordered_list: &mut [T]) -> Option<(&T, &mut [T])> {
if index >= unordered_list.len() {
None
} else {
Expand All @@ -265,12 +263,11 @@ fn evict<'a, T>(index: usize, unordered_list: &'a mut [T]) -> Option<(&'a T, &'a

/// returns whether rule_part could validly be applied to quad assuming the already given
/// instantiations
fn can_match(quad: Quad, rule_part: Quad, instantiations: &Instantiations) -> bool {
let inst = instantiations.as_ref();
fn can_match(quad: Quad, rule_part: Quad, inst: &Instantiations) -> bool {
rule_part
.zip(quad)
.iter()
.all(|(rp, q)| match inst.get(&rp) {
.all(|(rp, q)| match inst.get(*rp) {
Some(a) => a == q,
None => true,
})
Expand Down Expand Up @@ -352,7 +349,7 @@ mod tests {
LowRule, Rule,
};
use crate::translator::Translator;
use alloc::collections::{BTreeMap, BTreeSet};
use alloc::collections::BTreeSet;

#[test]
fn ancestry_raw() {
Expand Down Expand Up @@ -408,15 +405,15 @@ mod tests {

// This test only does one round of reasoning, no forward chaining. We will need a forward
// chaining test eventually.
let mut results = Vec::<BTreeMap<usize, usize>>::new();
let mut results = Vec::<Vec<Option<usize>>>::new();
for rule in rules {
let Rule {
mut if_all,
then: _,
mut inst,
} = rule.clone();
ts.apply(&mut if_all, &mut inst, &mut |inst| {
results.push(inst.as_ref().clone())
results.push(inst.inner().clone())
});
}

Expand All @@ -425,20 +422,15 @@ mod tests {
// The second rule, (?a ancestor ?b ?g) and (?b ancestor ?c ?g) -> (?a ancestor ?c ?g),
// should not activate because results from application of first rule have not been added
// to the rdf store so there are there are are not yet any ancestry relations present.
let mut expected_intantiations: Vec<BTreeMap<usize, usize>> = nodes
let mut expected_intantiations: Vec<Vec<Option<usize>>> = nodes
.iter()
.zip(nodes.iter().cycle().skip(1))
.map(|(a, b)| {
[
(0, *a),
(1, parent.0),
(2, *b),
(3, ancestor.0),
(4, default_graph.0),
]
.iter()
.cloned()
.collect()
[*a, parent.0, *b, ancestor.0, default_graph.0]
.iter()
.cloned()
.map(Some)
.collect()
})
.collect();
results.sort();
Expand Down Expand Up @@ -517,14 +509,7 @@ mod tests {
let then = &rule.then;
ts.apply(&mut if_all, &mut inst, &mut |inst| {
for implied in then {
let inst = inst.as_ref();
let new: Quad = [
inst[&implied.s.0],
inst[&implied.p.0],
inst[&implied.o.0],
inst[&implied.g.0],
]
.into();
let new: Quad = implied.clone().local_to_global(inst).unwrap();
if !ts.contains(&new) {
to_add.insert(new);
}
Expand Down
Loading

0 comments on commit 65766a9

Please sign in to comment.