rify/
prove.rs

1use crate::common::forward;
2use crate::common::vertices;
3use crate::common::LowRuleApplication;
4use crate::reasoner::{Quad, Reasoner};
5use crate::rule::{Entity, LowRule, Rule};
6use crate::translator::Translator;
7use alloc::collections::{BTreeMap, BTreeSet};
8use core::fmt::{Debug, Display};
9
10/// Locate a proof of some composite claims given the provided premises and rules.
11///
12/// ```
13/// # fn main() -> Result<(), Box<dyn std::error::Error>> {
14/// use rify::{
15///     prove,
16///     Entity::{Unbound, Bound},
17///     Rule, RuleApplication,
18/// };
19///
20/// // (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
21/// let awesome_score_axiom = Rule::create(
22///     vec![
23///         // if someone is awesome
24///         [Unbound("a"), Bound("is"), Bound("awesome"), Bound("default_graph")],
25///         // and they have some score
26///         [Unbound("a"), Bound("score"), Unbound("s"), Bound("default_graph")],
27///     ],
28///     vec![
29///         // then they must have an awesome score
30///         [Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")]
31///     ],
32/// )?;
33///
34/// assert_eq!(
35///     prove::<&str, &str>(
36///         // list of already known facts (premises)
37///         &[
38///             ["you", "score", "unspecified", "default_graph"],
39///             ["you", "is", "awesome", "default_graph"]
40///         ],
41///         // the thing we want to prove
42///         &[["you", "score", "awesome", "default_graph"]],
43///         // ordered list of logical rules
44///         &[awesome_score_axiom]
45///     )?,
46///     &[
47///         // the desired statement is be proven by instatiating the `awesome_score_axiom`
48///         // (you is awesome) ∧ (you score unspecified) -> (you score awesome)
49///         RuleApplication {
50///             rule_index: 0,
51///             instantiations: vec!["you", "unspecified"]
52///         }
53///     ]
54/// );
55/// # Ok(())
56/// # }
57/// ```
58pub fn prove<'a, Unbound: Ord + Clone, Bound: Ord + Clone>(
59    premises: &'a [[Bound; 4]],
60    to_prove: &'a [[Bound; 4]],
61    rules: &'a [Rule<Unbound, Bound>],
62) -> Result<Vec<RuleApplication<Bound>>, CantProve> {
63    let tran: Translator<Bound> = vertices(premises, rules).cloned().collect();
64    let lpremises: Vec<Quad> = premises
65        .iter()
66        .map(|spog| forward(&tran, spog).unwrap())
67        .collect();
68    let lto_prove: Vec<Quad> = to_prove
69        .iter()
70        .map(|spog| forward(&tran, spog))
71        .collect::<Option<_>>()
72        .ok_or(CantProve::NovelName)?;
73    let lrules: Vec<LowRule> = rules
74        .iter()
75        .cloned()
76        .map(|rule: Rule<Unbound, Bound>| -> LowRule { rule.lower(&tran).map_err(|_| ()).unwrap() })
77        .collect();
78
79    let lproof = low_prove(&lpremises, &lto_prove, &lrules)?;
80
81    // convert to proof
82    Ok(lproof
83        .iter()
84        .map(|rra: &LowRuleApplication| -> RuleApplication<Bound> {
85            rra.raise(&rules[rra.rule_index], &tran)
86        })
87        .collect())
88}
89
90fn low_prove(
91    premises: &[Quad],
92    to_prove: &[Quad],
93    rules: &[LowRule],
94) -> Result<Vec<LowRuleApplication>, CantProve> {
95    let mut rs = Reasoner::default();
96    // statement (Quad) is proved by applying rule (LowRuleApplication)
97    let mut arguments: BTreeMap<Quad, LowRuleApplication> = BTreeMap::new();
98    let mut to_add: BTreeSet<Quad> = premises.iter().cloned().collect();
99
100    for (rule_index, rule) in rules.iter().enumerate() {
101        if rule.if_all.is_empty() {
102            for implied in &rule.then {
103                let new_quad = implied.clone().local_to_global(&rule.inst).unwrap();
104                if to_add.insert(new_quad.clone()) {
105                    arguments.insert(
106                        new_quad,
107                        LowRuleApplication {
108                            rule_index,
109                            instantiations: Default::default(),
110                        },
111                    );
112                }
113            }
114        }
115    }
116    let mut rules2: Vec<(usize, LowRule)> = rules
117        .iter()
118        .cloned()
119        .enumerate()
120        .filter(|(_index, rule)| !rule.if_all.is_empty())
121        .collect();
122
123    // reason
124    while !to_add.is_empty() && !to_prove.iter().all(|tp| rs.contains(tp)) {
125        let mut adding_now = BTreeSet::<Quad>::new();
126        core::mem::swap(&mut adding_now, &mut to_add);
127        for fact in &adding_now {
128            rs.insert(fact.clone());
129            for (
130                rule_index,
131                LowRule {
132                    ref mut if_all,
133                    then,
134                    ref mut inst,
135                },
136            ) in rules2.iter_mut()
137            {
138                rs.apply_related(fact.clone(), if_all, inst, &mut |inst| {
139                    for implied in then.iter().cloned() {
140                        let new_quad = implied.local_to_global(inst).unwrap();
141                        if !rs.contains(&new_quad) && !adding_now.contains(&new_quad) {
142                            arguments.entry(new_quad.clone()).or_insert_with(|| {
143                                LowRuleApplication {
144                                    rule_index: *rule_index,
145                                    instantiations: inst.inner().clone(),
146                                }
147                            });
148                            to_add.insert(new_quad);
149                        }
150                    }
151                });
152            }
153        }
154    }
155
156    if !to_prove.iter().all(|tp| rs.contains(tp)) {
157        return Err(CantProve::ExhaustedSearchSpace);
158    }
159
160    let mut ret: Vec<LowRuleApplication> = Vec::new();
161    for claim in to_prove {
162        recall_proof(claim, &mut arguments, rules, &mut ret);
163    }
164    Ok(ret)
165}
166
167// this function is not tail recursive
168/// As this function populates the output. It removes corresponding arguments from the input.
169/// The reason being that a single argument does not need to be proved twice. Once is is
170/// proved, it can be treated as a premise.
171fn recall_proof(
172    // the globally scoped quad for which to find arguments
173    to_prove: &Quad,
174    arguments: &mut BTreeMap<Quad, LowRuleApplication>,
175    rules: &[LowRule],
176    outp: &mut Vec<LowRuleApplication>,
177) {
178    let to_global_scope = |rra: &LowRuleApplication, locally_scoped: usize| -> usize {
179        let concrete = rules[rra.rule_index].inst.get(locally_scoped);
180        let found = rra
181            .instantiations
182            .get(locally_scoped)
183            .and_then(|o| o.as_ref());
184        if let (Some(c), Some(f)) = (concrete, found) {
185            debug_assert_eq!(c, f);
186        }
187        *concrete.or(found).unwrap()
188    };
189
190    if let Some(application) = arguments.remove(to_prove) {
191        // for every required sub-statement, recurse
192        for quad in &rules[application.rule_index].if_all {
193            let Quad { s, p, o, g } = quad;
194            recall_proof(
195                &[
196                    to_global_scope(&application, s.0),
197                    to_global_scope(&application, p.0),
198                    to_global_scope(&application, o.0),
199                    to_global_scope(&application, g.0),
200                ]
201                .into(),
202                arguments,
203                rules,
204                outp,
205            );
206        }
207        // push the application onto output and return
208        outp.push(application);
209    }
210}
211
212#[derive(Debug, PartialEq, Eq)]
213#[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
214pub enum CantProve {
215    /// Entire search space was exhausted. The requested proof does not exists.
216    ExhaustedSearchSpace,
217    /// One of the entities in to_prove was never mentioned in the provided premises or
218    /// rules. The requested proof does not exists.
219    NovelName,
220}
221
222impl Display for CantProve {
223    fn fmt(&self, fmtr: &mut core::fmt::Formatter<'_>) -> Result<(), core::fmt::Error> {
224        Debug::fmt(self, fmtr)
225    }
226}
227
228#[cfg(feature = "std")]
229impl std::error::Error for CantProve {}
230
231#[derive(Debug, PartialEq, Eq)]
232#[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
233/// An element of a deductive proof. Proofs can be transmitted and later validatated as long as the
234/// validator assumes the same rule list as the prover.
235///
236/// Unbound variables are bound to the values in `instantiations`. They are bound in order of
237/// initial appearance.
238///
239/// Given the rule:
240///
241/// ```customlang
242/// ifall
243///   [?z ex:foo ?x DG]
244/// then
245///   [?x ex:bar ?z DG]
246/// ```
247///
248/// and the RuleApplication:
249///
250/// ```customlang
251/// RuleApplication {
252///   rule_index: 0,
253///   instantiations: vec!["foer", "bary"],
254/// }
255/// ```
256///
257/// The rule application represents the deductive proof:
258///
259/// ```customlang
260/// [foer ex:foo bary DG]
261/// therefore
262/// [bary ex:bar foer DG]
263/// ```
264pub struct RuleApplication<Bound> {
265    /// The index of the rule in the implicitly associated rule list.
266    pub rule_index: usize,
267    /// Bindings for unbound names in the rule in order of appearance.
268    pub instantiations: Vec<Bound>,
269}
270
271impl<Bound: Clone> RuleApplication<Bound> {
272    pub(crate) fn assumptions_when_applied<'a, Unbound: Ord + Clone>(
273        &'a self,
274        rule: &'a Rule<Unbound, Bound>,
275    ) -> Result<impl Iterator<Item = [Bound; 4]> + 'a, BadRuleApplication> {
276        self.bind_claims(rule, rule.if_all())
277    }
278
279    pub(crate) fn implications_when_applied<'a, Unbound: Ord + Clone>(
280        &'a self,
281        rule: &'a Rule<Unbound, Bound>,
282    ) -> Result<impl Iterator<Item = [Bound; 4]> + 'a, BadRuleApplication> {
283        self.bind_claims(rule, rule.then())
284    }
285
286    /// claims must be either if_all or then from rule
287    fn bind_claims<'a, Unbound: Ord + Clone>(
288        &'a self,
289        rule: &'a Rule<Unbound, Bound>,
290        claims: &'a [[Entity<Unbound, Bound>; 4]],
291    ) -> Result<impl Iterator<Item = [Bound; 4]> + 'a, BadRuleApplication> {
292        let cannon: BTreeMap<&Unbound, usize> = rule
293            .cononical_unbound()
294            .enumerate()
295            .map(|(ub, n)| (n, ub))
296            .collect();
297        if cannon.len() != self.instantiations.len() {
298            return Err(BadRuleApplication);
299        }
300        Ok(claims
301            .iter()
302            .cloned()
303            .map(move |claim| bind_claim(claim, &cannon, &self.instantiations)))
304    }
305}
306
307/// Panics
308///
309/// panics if an unbound entity is not registered in map
310/// panics if the canonical index of unbound (according to map) is too large to index instantiations
311fn bind_claim<Unbound: Ord, Bound: Clone>(
312    [s, p, o, g]: [Entity<Unbound, Bound>; 4],
313    map: &BTreeMap<&Unbound, usize>,
314    instantiations: &[Bound],
315) -> [Bound; 4] {
316    [
317        bind_entity(s, map, instantiations),
318        bind_entity(p, map, instantiations),
319        bind_entity(o, map, instantiations),
320        bind_entity(g, map, instantiations),
321    ]
322}
323
324/// Panics
325///
326/// panics if an unbound entity is not registered in map
327/// panics if the canonical index of unbound (according to map) is too large to index instantiations
328fn bind_entity<Unbound: Ord, Bound: Clone>(
329    e: Entity<Unbound, Bound>,
330    map: &BTreeMap<&Unbound, usize>,
331    instantiations: &[Bound],
332) -> Bound {
333    match e {
334        Entity::Unbound(a) => instantiations[map[&a]].clone(),
335        Entity::Bound(e) => e,
336    }
337}
338
339/// The Rule being applied expects a different number of name bindings.
340#[derive(Debug)]
341pub struct BadRuleApplication;
342
343#[cfg(test)]
344mod test {
345    use super::*;
346    use crate::common::decl_rules;
347    use crate::common::inc;
348    use crate::rule::Entity::{Bound as B, Unbound as U};
349    use crate::validate::validate;
350    use crate::validate::Valid;
351
352    #[test]
353    fn novel_name() {
354        assert_eq!(
355            prove::<&str, &str>(&[], &[["andrew", "score", "awesome", "default_graph"]], &[])
356                .unwrap_err(),
357            CantProve::NovelName
358        );
359    }
360
361    #[test]
362    fn search_space_exhausted() {
363        let err = prove::<&str, &str>(
364            &[
365                ["score", "score", "score", "default_graph"],
366                ["andrew", "andrew", "andrew", "default_graph"],
367                ["awesome", "awesome", "awesome", "default_graph"],
368            ],
369            &[["andrew", "score", "awesome", "default_graph"]],
370            &[],
371        )
372        .unwrap_err();
373        assert_eq!(err, CantProve::ExhaustedSearchSpace);
374        let err = prove::<&str, &str>(
375            &[
376                ["score", "score", "score", "default_graph"],
377                ["andrew", "andrew", "andrew", "default_graph"],
378                ["awesome", "awesome", "awesome", "default_graph"],
379                ["backflip", "backflip", "backflip", "default_graph"],
380                ["ability", "ability", "ability", "default_graph"],
381            ],
382            &[["andrew", "score", "awesome", "default_graph"]],
383            &[
384                Rule::create(vec![], vec![]).unwrap(),
385                Rule::create(
386                    vec![[U("a"), B("ability"), B("backflip"), U("g")]],
387                    vec![[U("a"), B("score"), B("awesome"), U("g")]],
388                )
389                .unwrap(),
390            ],
391        )
392        .unwrap_err();
393        assert_eq!(err, CantProve::ExhaustedSearchSpace);
394    }
395
396    #[test]
397    fn prove_already_stated() {
398        assert_eq!(
399            prove::<&str, &str>(
400                &[["doggo", "score", "11", "default_graph"]],
401                &[["doggo", "score", "11", "default_graph"]],
402                &[]
403            )
404            .unwrap(),
405            Vec::new()
406        );
407    }
408
409    #[test]
410    /// generate a single step proof
411    fn prove_single_step() {
412        // (?boi, is, awesome) ∧ (?boi, score, ?s) -> (?boi score, awesome)
413        let awesome_score_axiom = Rule::create(
414            vec![
415                [U("boi"), B("is"), B("awesome"), U("g")], // if someone is awesome
416                [U("boi"), B("score"), U("s"), U("g")],    // and they have some score
417            ],
418            vec![[U("boi"), B("score"), B("awesome"), U("g")]], // then they must have an awesome score
419        )
420        .unwrap();
421        assert_eq!(
422            prove::<&str, &str>(
423                &[
424                    ["you", "score", "unspecified", "default_graph"],
425                    ["you", "is", "awesome", "default_graph"]
426                ],
427                &[["you", "score", "awesome", "default_graph"]],
428                &[awesome_score_axiom]
429            )
430            .unwrap(),
431            vec![
432                // (you is awesome) ∧ (you score unspecified) -> (you score awesome)
433                RuleApplication {
434                    rule_index: 0,
435                    instantiations: vec!["you", "default_graph", "unspecified"]
436                }
437            ]
438        );
439    }
440
441    #[test]
442    /// rules with a single unbound graphname cannot be applied accross graphnames
443    fn graph_separation() {
444        let awesome_score_axiom = Rule::create(
445            vec![
446                [U("boi"), B("is"), B("awesome"), U("g")],
447                [U("boi"), B("score"), U("s"), U("g")],
448            ],
449            vec![[U("boi"), B("score"), B("awesome"), U("g")]],
450        )
451        .unwrap();
452
453        prove::<&str, &str>(
454            &[
455                ["you", "score", "unspecified", "default_graph"],
456                ["you", "is", "awesome", "default_graph"],
457            ],
458            &[["you", "score", "awesome", "default_graph"]],
459            &[awesome_score_axiom.clone()],
460        )
461        .unwrap();
462        assert_eq!(
463            prove(
464                &[
465                    ["you", "score", "unspecified", "default_graph"],
466                    ["you", "is", "awesome", "other_graph"]
467                ],
468                &[["you", "score", "awesome", "default_graph"]],
469                &[awesome_score_axiom.clone()]
470            )
471            .unwrap_err(),
472            CantProve::ExhaustedSearchSpace
473        );
474        assert_eq!(
475            prove(
476                &[
477                    ["you", "score", "unspecified", "default_graph"],
478                    ["you", "is", "awesome", "other_graph"]
479                ],
480                &[["you", "score", "awesome", "other_graph"]],
481                &[awesome_score_axiom.clone()]
482            )
483            .unwrap_err(),
484            CantProve::ExhaustedSearchSpace
485        );
486        assert_eq!(
487            prove(
488                &[
489                    ["you", "score", "unspecified", "default_graph"],
490                    ["you", "is", "awesome", "default_graph"],
491                    // to prevent NovelName error:
492                    ["other_graph", "other_graph", "other_graph", "other_graph"],
493                ],
494                &[["you", "score", "awesome", "other_graph"]],
495                &[awesome_score_axiom.clone()]
496            )
497            .unwrap_err(),
498            CantProve::ExhaustedSearchSpace
499        );
500    }
501
502    #[test]
503    fn prove_multi_step() {
504        // Rules:
505        // (andrew claims ?c) ∧ (?c subject ?s) ∧ (?c property ?p) ∧ (?c object ?o) -> (?s ?p ?o)
506        // (?person_a is awesome) ∧ (?person_a friendswith ?person_b) -> (?person_b is awesome)
507        // (?person_a friendswith ?person_b) -> (?person_b friendswith ?person_a)
508
509        // Facts:
510        // (soyoung friendswith nick)
511        // (nick friendswith elina)
512        // (elina friendswith sam)
513        // (sam friendswith fausto)
514        // (fausto friendswith lovesh)
515        // (andrew claims _:claim1)
516        // (_:claim1 subject lovesh)
517        // (_:claim1 property is)
518        // (_:claim1 object awesome)
519
520        // Composite Claims:
521        // (soyoung is awesome)
522        // (nick is awesome)
523
524        // the following rules operate only on the defualt graph
525        let rules: Vec<Rule<&str, &str>> = {
526            let ru: &[[&[[Entity<&str, &str>; 4]]; 2]] = &[
527                [
528                    &[
529                        [B("andrew"), B("claims"), U("c"), B("default_graph")],
530                        [U("c"), B("subject"), U("s"), B("default_graph")],
531                        [U("c"), B("property"), U("p"), B("default_graph")],
532                        [U("c"), B("object"), U("o"), B("default_graph")],
533                    ],
534                    &[[U("s"), U("p"), U("o"), B("default_graph")]],
535                ],
536                [
537                    &[
538                        [U("person_a"), B("is"), B("awesome"), B("default_graph")],
539                        [
540                            U("person_a"),
541                            B("friendswith"),
542                            U("person_b"),
543                            B("default_graph"),
544                        ],
545                    ],
546                    &[[U("person_b"), B("is"), B("awesome"), B("default_graph")]],
547                ],
548                [
549                    &[[
550                        U("person_a"),
551                        B("friendswith"),
552                        U("person_b"),
553                        B("default_graph"),
554                    ]],
555                    &[[
556                        U("person_b"),
557                        B("friendswith"),
558                        U("person_a"),
559                        B("default_graph"),
560                    ]],
561                ],
562            ];
563            ru.iter()
564                .map(|[ifa, then]| Rule::create(ifa.to_vec(), then.to_vec()).unwrap())
565                .collect()
566        };
567        let facts: &[[&str; 4]] = &[
568            ["soyoung", "friendswith", "nick", "default_graph"],
569            ["nick", "friendswith", "elina", "default_graph"],
570            ["elina", "friendswith", "sam", "default_graph"],
571            ["sam", "friendswith", "fausto", "default_graph"],
572            ["fausto", "friendswith", "lovesh", "default_graph"],
573            ["andrew", "claims", "_:claim1", "default_graph"],
574            ["_:claim1", "subject", "lovesh", "default_graph"],
575            ["_:claim1", "property", "is", "default_graph"],
576            ["_:claim1", "object", "awesome", "default_graph"],
577        ];
578        let composite_claims: &[[&str; 4]] = &[
579            ["soyoung", "is", "awesome", "default_graph"],
580            ["nick", "is", "awesome", "default_graph"],
581        ];
582        let expected_proof: Vec<RuleApplication<&str>> = {
583            let ep: &[(usize, &[&str])] = &[
584                (0, &["_:claim1", "lovesh", "is", "awesome"]),
585                (2, &["fausto", "lovesh"]),
586                (1, &["lovesh", "fausto"]),
587                (2, &["sam", "fausto"]),
588                (1, &["fausto", "sam"]),
589                (2, &["elina", "sam"]),
590                (1, &["sam", "elina"]),
591                (2, &["nick", "elina"]),
592                (1, &["elina", "nick"]),
593                (2, &["soyoung", "nick"]),
594                (1, &["nick", "soyoung"]),
595            ];
596            ep.iter()
597                .map(|(rule_index, inst)| RuleApplication {
598                    rule_index: *rule_index,
599                    instantiations: inst.to_vec(),
600                })
601                .collect()
602        };
603        let proof = prove::<&str, &str>(facts, composite_claims, &rules).unwrap();
604        assert!(
605            proof.len() <= expected_proof.len(),
606            "if this assertion fails, the generated proof length is longer than it was previously"
607        );
608        assert_eq!(
609            proof, expected_proof,
610            "if this assertion fails the proof may still be valid but the order of the proof may \
611             have changed"
612        );
613        let Valid { assumed, implied } = validate(&rules, &proof).unwrap();
614        for claim in composite_claims {
615            assert!(implied.contains(claim));
616            assert!(
617                !facts.contains(claim),
618                "all theorems are expected to be composite for this particular problem"
619            );
620        }
621        for assumption in &assumed {
622            assert!(
623                assumed.contains(assumption),
624                "This problem was expected to use all porvided assumptions."
625            );
626        }
627    }
628
629    #[test]
630    fn ancestry_high_prove_and_verify() {
631        let mut next_uniq = 0u32;
632        let parent = inc(&mut next_uniq);
633        let ancestor = inc(&mut next_uniq);
634        let default_graph = inc(&mut next_uniq);
635        let nodes: Vec<u32> = (0usize..10).map(|_| inc(&mut next_uniq)).collect();
636        let facts: Vec<[u32; 4]> = nodes
637            .iter()
638            .zip(nodes.iter().cycle().skip(1))
639            .map(|(a, b)| [*a, parent, *b, default_graph])
640            .collect();
641        let rules = decl_rules(&[
642            [
643                &[[U("a"), B(parent), U("b"), B(default_graph)]],
644                &[[U("a"), B(ancestor), U("b"), B(default_graph)]],
645            ],
646            [
647                &[
648                    [U("a"), B(ancestor), U("b"), B(default_graph)],
649                    [U("b"), B(ancestor), U("c"), B(default_graph)],
650                ],
651                &[[U("a"), B(ancestor), U("c"), B(default_graph)]],
652            ],
653        ]);
654        let composite_claims = vec![
655            [nodes[0], ancestor, *nodes.last().unwrap(), default_graph],
656            [*nodes.last().unwrap(), ancestor, nodes[0], default_graph],
657            [nodes[0], ancestor, nodes[0], default_graph],
658            // (first node, parent, second node) is a premise
659            [nodes[0], parent, nodes[1], default_graph],
660        ];
661        let proof = prove::<&str, u32>(&facts, &composite_claims, &rules).unwrap();
662        let Valid { assumed, implied } = validate::<&str, u32>(&rules, &proof).unwrap();
663        assert_eq!(
664            &assumed,
665            &facts.iter().cloned().collect(),
666            "all supplied premises are expected to be used for this proof"
667        );
668        assert!(!facts.contains(&composite_claims[0]));
669        assert!(!facts.contains(&composite_claims[1]));
670        assert!(!facts.contains(&composite_claims[2]));
671        assert!(facts.contains(&composite_claims[3]));
672        for claim in composite_claims {
673            assert!(implied.contains(&claim) ^ facts.contains(&claim));
674        }
675        for fact in facts {
676            assert!(!implied.contains(&fact));
677        }
678    }
679
680    #[test]
681    fn no_proof_is_generated_for_facts() {
682        let facts: Vec<[&str; 4]> = vec![
683            ["tacos", "are", "tasty", "default_graph"],
684            ["nachos", "are", "tasty", "default_graph"],
685            ["nachos", "are", "food", "default_graph"],
686        ];
687        let rules = decl_rules::<&str, &str>(&[[
688            &[[B("nachos"), B("are"), B("tasty"), B("default_graph")]],
689            &[[B("nachos"), B("are"), B("food"), B("default_graph")]],
690        ]]);
691        let composite_claims = vec![["nachos", "are", "food", "default_graph"]];
692        let proof = prove::<&str, &str>(&facts, &composite_claims, &rules).unwrap();
693        assert_eq!(&proof, &vec![]);
694    }
695
696    #[test]
697    fn unconditional_rule() {
698        let facts: Vec<[&str; 4]> = vec![];
699        let rules = decl_rules::<&str, &str>(&[[
700            &[],
701            &[[B("nachos"), B("are"), B("food"), B("default_graph")]],
702        ]]);
703        let composite_claims = vec![["nachos", "are", "food", "default_graph"]];
704        let proof = prove::<&str, &str>(&facts, &composite_claims, &rules).unwrap();
705        assert_eq!(
706            &proof,
707            &[RuleApplication {
708                rule_index: 0,
709                instantiations: vec![]
710            }]
711        );
712    }
713}
rify/prove.rs

rify/
prove.rs
