Optimizations

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "rify"
-version = "0.7.0"
+version = "0.7.1"
 authors = [
   "Andrew Dirksen <[email protected]>",
   "Sam Hellawell <[email protected]>"

benches/.gitignore

@@ -0,0 +1,5 @@
+/target
+/pkg
+/wasm-pack.log
+/tmp
+/Cargo.lock

benches/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "benches"
+version = "0.1.0"
+authors = ["Andrew Dirksen <[email protected]>"]
+edition = "2018"
+
+[dependencies]
+rify = { path = ".." }

benches/rust-toolchain

@@ -0,0 +1 @@
+nightly

benches/src/lib.rs

@@ -0,0 +1,137 @@
+#![cfg(test)]
+#![feature(test)]
+
+extern crate test;
+
+use core::fmt::Debug;
+use rify::Entity::{Bound as B, Unbound as U};
+use rify::*;
+use test::Bencher;
+
+const DG: &str = "default_graph";
+
+mod ancestry {
+    use super::*;
+    const PARENT: &str = "parent";
+    const ANCESTOR: &str = "ancestor";
+
+    fn rules() -> Vec<rify::Rule<&'static str, &'static str>> {
+        decl_rules(&[
+            [
+                &[[U("a"), B(PARENT), U("b"), B(DG)]],
+                &[[U("a"), B(ANCESTOR), U("b"), B(DG)]],
+            ],
+            [
+                &[
+                    [U("a"), B(ANCESTOR), U("b"), B(DG)],
+                    [U("b"), B(ANCESTOR), U("c"), B(DG)],
+                ],
+                &[[U("a"), B(ANCESTOR), U("c"), B(DG)]],
+            ],
+        ])
+    }
+
+    // Contains intentional leak; don't use outside of tests.
+    fn facts(numnodes: usize) -> Vec<[&'static str; 4]> {
+        let nodes: Vec<&str> = (0..numnodes)
+            .map(|n| Box::leak(format!("node_{}", n).into_boxed_str()) as &str)
+            .collect();
+        let facts: Vec<[&str; 4]> = nodes
+            .iter()
+            .zip(nodes.iter().cycle().skip(1))
+            .map(|(a, b)| [a, PARENT, b, DG])
+            .collect();
+        facts
+    }
+
+    #[bench]
+    fn infer_(b: &mut Bencher) {
+        let facts = facts(20);
+        let rules = rules();
+        b.iter(|| infer(&facts, &rules));
+    }
+
+    #[bench]
+    fn prove_(b: &mut Bencher) {
+        let facts = facts(20);
+        let rules = rules();
+        b.iter(|| prove(&facts, &[[PARENT, PARENT, PARENT, PARENT]], &rules).unwrap_err());
+    }
+
+    #[bench]
+    fn infer_30(b: &mut Bencher) {
+        let facts = facts(30);
+        let rules = rules();
+        b.iter(|| infer(&facts, &rules));
+    }
+
+    #[bench]
+    fn prove_30(b: &mut Bencher) {
+        let facts = facts(30);
+        let rules = rules();
+        b.iter(|| prove(&facts, &[[PARENT, PARENT, PARENT, PARENT]], &rules).unwrap_err());
+    }
+}
+
+mod recursion_minimal {
+    use super::*;
+
+    const RULES: &[[&[[rify::Entity<&str, &str>; 4]]; 2]] = &[
+        [
+            &[
+                [B("andrew"), B("claims"), U("c"), B(DG)],
+                [U("c"), B("subject"), U("s"), B(DG)],
+                [U("c"), B("property"), U("p"), B(DG)],
+                [U("c"), B("object"), U("o"), B(DG)],
+            ],
+            &[[U("s"), U("p"), U("o"), B(DG)]],
+        ],
+        [
+            &[
+                [U("person_a"), B("is"), B("awesome"), B(DG)],
+                [U("person_a"), B("friendswith"), U("person_b"), B(DG)],
+            ],
+            &[[U("person_b"), B("is"), B("awesome"), B(DG)]],
+        ],
+        [
+            &[[U("person_a"), B("friendswith"), U("person_b"), B(DG)]],
+            &[[U("person_b"), B("friendswith"), U("person_a"), B(DG)]],
+        ],
+    ];
+
+    const FACTS: &[[&str; 4]] = &[
+        ["soyoung", "friendswith", "nick", DG],
+        ["nick", "friendswith", "elina", DG],
+        ["elina", "friendswith", "sam", DG],
+        ["sam", "friendswith", "fausto", DG],
+        ["fausto", "friendswith", "lovesh", DG],
+        ["andrew", "claims", "_:claim1", DG],
+        ["_:claim1", "subject", "lovesh", DG],
+        ["_:claim1", "property", "is", DG],
+        ["_:claim1", "object", "awesome", DG],
+    ];
+
+    #[bench]
+    fn infer_(b: &mut Bencher) {
+        let rules = decl_rules(RULES);
+        b.iter(|| infer(FACTS, &rules));
+    }
+
+    #[bench]
+    fn prove_(b: &mut Bencher) {
+        let rules = decl_rules(RULES);
+        let composite_claims: &[[&str; 4]] = &[
+            ["soyoung", "is", "awesome", "default_graph"],
+            ["nick", "is", "awesome", "default_graph"],
+        ];
+        b.iter(|| prove(FACTS, composite_claims, &rules));
+    }
+}
+
+pub fn decl_rules<Unbound: Ord + Debug + Clone, Bound: Ord + Clone>(
+    rs: &[[&[[rify::Entity<Unbound, Bound>; 4]]; 2]],
+) -> Vec<rify::Rule<Unbound, Bound>> {
+    rs.iter()
+        .map(|[ifa, then]| rify::Rule::create(ifa.to_vec(), then.to_vec()).unwrap())
+        .collect()
+}

bindings/js_wasm/package.json

@@ -5,7 +5,7 @@
     "Sam Hellawell <[email protected]>"
   ],
   "description": "RDF reasoner that operates on RIF-like conjunctive rules. Outputs a machine\nreadable proof of some claim which can be cheaply verified.\n",
-  "version": "0.7.0",
+  "version": "0.7.1",
   "license": "MIT OR Apache-2.0",
   "repository": {
     "type": "git",

justfile

@@ -30,10 +30,36 @@ js-test:
 # remove dist and node_modules from js bindings tests
 clean:
   cargo clean
-  rm -r bindings/js_wasm/pkg || true
+  cd benches; cargo clean
+  rm -rf bindings/js_wasm/pkg
   just clean-js
 
 # remove artifacts from js bindings tests
 clean-js:
-  rm -r bindings/js_wasm/binding_tests/dist || true
-  rm -r bindings/js_wasm/binding_tests/node_modules || true
+  rm -rf bindings/js_wasm/binding_tests/dist
+  rm -rf bindings/js_wasm/binding_tests/node_modules
+
+bench:
+  #!/usr/bin/env bash
+  cd benches
+  cargo bench
+
+checkall-buildall:
+  just clean
+  cargo test
+  cargo clippy -- -D warnings
+  just bench
+  just js-test
+
+assert-clean-workdir:
+  ! test -n "$(git status --porcelain)" # please commit before publish
+
+publish-js:
+  just checkall-buildall
+  just assert-clean-workdir
+  cd bindings/js_wasm/pkg && npm publish
+
+publish-rs:
+  just checkall-buildall
+  just assert-clean-workdir
+  cargo publish

src/common.rs

@@ -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 {
@@ -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());
         }
@@ -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(
         [
@@ -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)?,

src/infer.rs

@@ -28,36 +28,51 @@ pub fn infer<Unbound: Ord + Clone, Bound: Ord + Clone>(
 /// A version of infer that operates on lowered input an returns output in lowered form.
 fn low_infer(premises: &[Quad], rules: &[LowRule]) -> Vec<Quad> {
     let mut rs = Reasoner::default();
-    for prem in premises {
-        rs.insert(prem.clone());
+
+    let mut to_add: BTreeSet<Quad> = premises.iter().cloned().collect();
+    let initial_len = to_add.len(); // number of premises after dedup
+    assert!(initial_len <= premises.len());
+
+    // apply_related is sufficient except for in the case of unconditional rules.
+    // in order to avoid calling apply() directly, rules with empty "if" clauses
+    // lists will get special treatment.
+    for rule in rules {
+        if rule.if_all.is_empty() {
+            for rule_part in &rule.then {
+                to_add.insert(rule_part.clone().local_to_global(&rule.inst).unwrap());
+            }
+        }
     }
-    let initial_len = rs.claims_ref().len(); // number of premises after dedup
-    debug_assert!(initial_len <= premises.len());
+    let mut rules: Vec<LowRule> = rules
+        .iter()
+        .filter(|r| !r.if_all.is_empty())
+        .cloned()
+        .collect();
 
+    // subsequent reasoning is done in a loop using apply_related
     loop {
-        let mut to_add = BTreeSet::<Quad>::new();
-        for rr in rules.iter() {
-            rs.apply(&mut rr.if_all.clone(), &mut rr.inst.clone(), &mut |inst| {
-                let ins = inst.as_ref();
-                for implied in &rr.then {
-                    let new_quad = [
-                        ins[&implied.s.0],
-                        ins[&implied.p.0],
-                        ins[&implied.o.0],
-                        ins[&implied.g.0],
-                    ]
-                    .into();
-                    if !rs.contains(&new_quad) {
-                        to_add.insert(new_quad);
-                    }
-                }
-            });
-        }
         if to_add.is_empty() {
             break;
         }
-        for new in to_add.into_iter() {
-            rs.insert(new);
+        let mut adding = BTreeSet::default();
+        core::mem::swap(&mut to_add, &mut adding);
+        for new in adding.iter().cloned() {
+            rs.insert(new.clone());
+            for LowRule {
+                ref mut if_all,
+                then,
+                ref mut inst,
+            } in rules.iter_mut()
+            {
+                rs.apply_related(new.clone(), if_all, inst, &mut |inst| {
+                    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);
+                        }
+                    }
+                });
+            }
         }
     }