asdi/idb/eval/
strata.rs

1/*!
2One-line description.
3
4![module UML](https://raw.githubusercontent.com/johnstonskj/rust-asdi/main/book/src/model/idb_eval_strata.svg)
5
6More detailed description, with
7
8# Example
9
10*/
11
12use crate::edb::{Predicate, RelationSet};
13use crate::error::{program_not_stratifiable, Result};
14use crate::features::{FeatureSet, FEATURE_DISJUNCTION};
15use crate::idb::{Literal, Rule, RuleSet};
16use crate::{Collection, Labeled, MaybePositive, Program, ProgramCore};
17use std::collections::HashSet;
18use std::fmt::{Display, Formatter};
19use std::time::Instant;
20use tracing::trace;
21
22// ------------------------------------------------------------------------------------------------
23// Public Types & Constants
24// ------------------------------------------------------------------------------------------------
25
26///
27/// The result of stratification, this representation of an IDB [RuleSet](../struct.RuleSet.html) is an optimization in
28/// evaluation.
29///
30/// # Details
31///
32/// A stratification of a $\small\text{Datalog}^{\lnot}$, strictly termed $\small\text{Datalog}^{\lnot{s}}$,
33/// program $P$ is a partition of $P$ into Datalog sub-programs $P_1, \ldots, P_m$ such that:
34///
35/// * All the rules defining the same IDB relation, $r$, are in the same partition.
36/// * If an IDB $r$ appears positive in the body of a rule with head $r^{\prime}$, $r$ should be
37///   defined in a partition before or where $r^{\prime}$ is defined.
38/// * If an IDB $r$ appears negated in the body of a rule with head $r^{\prime}$, $r$ should be
39///   defined in partition strictly before where $r^{\prime}$ is defined.
40///
41/// ```datalog
42/// [P1]   v(X) :- r(X, Y).
43/// [P1]   v(Y) :- r(X, Y).
44/// [P2]   t(X, Y) :- r(X, Y).
45/// [P2]   t(X, Y) :- t(X, Z), r(Z, Y).
46/// [P3]   tc(X, Y):- v(X), v(Y), not t(X, Y).
47/// ```
48///
49/// Notice that (P2) defines the IDB $t$, and (P3) defines $tc$; $tc$ has a negated IDB in the body of
50/// a rule that defines it, but this IDB appears in the previous stratum (P2).
51///
52#[derive(Debug)]
53pub struct StratifiedProgram<'a> {
54    strata: Vec<SubProgram<'a>>,
55}
56
57#[derive(Debug, PartialEq)]
58#[allow(single_use_lifetimes)]
59pub struct SubProgram<'a> {
60    program: &'a Program,
61    strata: RuleSet,
62}
63
64///
65///
66/// # Example
67///
68/// ```datalog
69/// .feature(negation).
70/// .assert r(string, string).
71///
72/// v(X) :- r(X, Y).
73/// v(Y) :- r(X, Y).
74/// t(X, Y) :- r(X, Y).
75/// t(X, Y) :- t(X, Z), r(Z, Y).
76/// tc(X, Y):- v(X), v(Y), not t(X, Y).
77/// ```
78///
79/// ```text
80/// digraph G {
81///   t -> r;
82///   t -> t;
83///   tc -> t [arrowhead=empty];
84///   tc -> v;
85///   v -> r;
86///
87///   r [style=filled; color=lightgrey];
88/// }
89/// ```
90///
91#[derive(Debug, Default)]
92#[allow(single_use_lifetimes)]
93pub struct PrecedenceGraph<'a>(HashSet<PrecedenceNode<'a>>);
94
95#[derive(Debug, PartialEq, Eq, Hash)]
96#[allow(single_use_lifetimes)]
97pub struct PrecedenceNode<'a> {
98    negative: bool,
99    extensional: bool,
100    source: &'a Predicate,
101    target: &'a Predicate,
102}
103
104// ------------------------------------------------------------------------------------------------
105// Private Types & Constants
106// ------------------------------------------------------------------------------------------------
107
108// ------------------------------------------------------------------------------------------------
109// Private Macros
110// ------------------------------------------------------------------------------------------------
111
112// ------------------------------------------------------------------------------------------------
113// Public Functions
114// ------------------------------------------------------------------------------------------------
115
116// ------------------------------------------------------------------------------------------------
117// Implementations
118// ------------------------------------------------------------------------------------------------
119
120impl Display for StratifiedProgram<'_> {
121    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
122        for (i, strata) in self.strata.iter().enumerate() {
123            writeln!(f, "[{}", i)?;
124            for (j, rule) in strata.rules().iter().enumerate() {
125                writeln!(f, "  [{}] {:?}", j, rule)?;
126            }
127            writeln!(f, "]")?;
128        }
129        Ok(())
130    }
131}
132
133impl<'a> Collection<SubProgram<'a>> for StratifiedProgram<'a> {
134    fn is_empty(&self) -> bool {
135        self.strata.is_empty()
136    }
137
138    fn len(&self) -> usize {
139        self.strata.len()
140    }
141
142    fn iter(&self) -> Box<dyn Iterator<Item = &'_ SubProgram<'a>> + '_> {
143        Box::new(self.strata.iter())
144    }
145
146    fn contains(&self, value: &SubProgram<'_>) -> bool {
147        self.strata.contains(value)
148    }
149}
150
151impl<'a> StratifiedProgram<'a> {
152    pub fn from(program: &'a Program) -> Result<Self> {
153        // TODO: (ISSUE/rust-asdi/7) Design for disjunction
154        assert!(!program.features().supports(&FEATURE_DISJUNCTION));
155
156        let start = Instant::now();
157
158        let rules = program.rules();
159        let graph = PrecedenceGraph::from(program);
160        let mut strata: Vec<SubProgram<'_>> = Vec::with_capacity(graph.sources().len());
161
162        if graph.is_stratifiable() {
163            for rule in rules.iter() {
164                if strata.is_empty() {
165                    strata.push(SubProgram::from_with_rule(program, rule));
166                } else {
167                    let mut leveled: bool = false;
168                    let head_label = rule.head().map(|atom| atom.label()).next().unwrap();
169
170                    // 1. All the rules defining the same IDB relation are in the same partition.
171                    for stratum in strata.iter_mut() {
172                        if stratum
173                            .rules()
174                            .iter()
175                            .next()
176                            .unwrap()
177                            .head()
178                            .map(|atom| atom.label())
179                            .next()
180                            .unwrap()
181                            == head_label
182                        {
183                            stratum.add_rule(rule);
184                            leveled = true;
185                            break;
186                        }
187                    }
188
189                    // 2. If an IDB R appears positive in the body of a rule with head R0, R should
190                    //    be defined in a partition before or where R0 is defined.
191                    //
192                    // r0(X) :- r(X). => [[r...][r0...]] | [[r..., r0...]]
193                    //
194                    // 3. If an IDB R appears negated in the body of a rule with head R0, R should
195                    //    be defined in partition strictly before where R0 is defined.
196                    //
197                    // r0(X) :- r(X). => [[r...][r0...]]
198                    //
199                    if !leveled {
200                        for (i, stratum) in strata.iter().enumerate() {
201                            if stratum.rules().iter().any(|r2| {
202                                r2.literals()
203                                    .filter_map(Literal::as_relational)
204                                    .any(|atom| atom.label() == head_label)
205                            }) {
206                                strata.insert(i, SubProgram::from_with_rule(program, rule));
207                                leveled = true;
208                                break;
209                            }
210                        }
211                    }
212
213                    if !leveled {
214                        strata.push(SubProgram::from_with_rule(program, rule));
215                    }
216                }
217            }
218            let delta = start.elapsed();
219            trace!(
220                "Stratified {} rules into {} strata, in {}s",
221                program.rules().len(),
222                strata.len(),
223                delta.as_secs_f64()
224            );
225            Ok(Self { strata })
226        } else {
227            Err(program_not_stratifiable())
228        }
229    }
230}
231
232// ------------------------------------------------------------------------------------------------
233
234impl ProgramCore for SubProgram<'_> {
235    fn features(&self) -> &FeatureSet {
236        self.program.features()
237    }
238
239    fn extensional(&self) -> &RelationSet {
240        self.program.extensional()
241    }
242
243    fn intensional(&self) -> &RelationSet {
244        self.program.intensional()
245    }
246
247    fn rules(&self) -> &RuleSet {
248        &self.strata
249    }
250}
251
252impl<'a> SubProgram<'a> {
253    fn from_with_rule(program: &'a Program, rule: &Rule) -> Self {
254        let mut new = Self {
255            program,
256            strata: Default::default(),
257        };
258        new.add_rule(rule);
259        new
260    }
261
262    fn add_rule(&mut self, rule: &Rule) {
263        self.strata.add(rule.clone());
264    }
265}
266
267// ------------------------------------------------------------------------------------------------
268
269impl<'a> PrecedenceGraph<'a> {
270    pub fn from(program: &'a Program) -> Self {
271        let mut graph = PrecedenceGraph::default();
272        for rule in program.rules().iter() {
273            for from_label in head_predicates(rule) {
274                for (negative, to_label) in body_predicates(rule) {
275                    graph.0.insert(PrecedenceNode {
276                        negative,
277                        extensional: program.extensional().contains(to_label),
278                        source: from_label,
279                        target: to_label,
280                    });
281                }
282            }
283        }
284        graph
285    }
286
287    pub fn edges(&self) -> impl Iterator<Item = &'_ PrecedenceNode<'_>> {
288        self.0.iter()
289    }
290
291    pub fn sources(&self) -> HashSet<&'_ Predicate> {
292        self.edges().map(|e| e.source()).collect()
293    }
294
295    pub fn targets(&self) -> HashSet<&'_ Predicate> {
296        self.edges().map(|e| e.target()).collect()
297    }
298
299    pub fn is_level_zero(&self, source: &Predicate) -> bool {
300        self.directly_reachable_nodes_from(source)
301            .into_iter()
302            .all(|node| node.is_extensional_target())
303    }
304
305    pub fn is_recursive(&self) -> bool {
306        self.sources()
307            .into_iter()
308            .any(|source| self.reachable_from(source).contains(source))
309    }
310
311    pub fn is_positive(&self) -> bool {
312        self.edges().all(|edge| !edge.is_negative_target())
313    }
314
315    pub fn is_semi_positive(&self) -> bool {
316        let all_sources = self.sources();
317        all_sources.iter().all(|source| {
318            self.directly_reachable_nodes_from(source)
319                .into_iter()
320                .filter(|node| node.is_negative_target())
321                .all(|node| node.is_extensional_target())
322        })
323    }
324
325    pub fn is_stratifiable(&self) -> bool {
326        let all_sources = self.sources();
327        all_sources.iter().all(|source| {
328            self.directly_reachable_nodes_from(source)
329                .into_iter()
330                .filter(|node| node.is_negative_target())
331                .all(|node| !self.reachable_from(node.target()).contains(source))
332        })
333    }
334
335    pub fn directly_reachable_from(&self, source: &Predicate) -> HashSet<&'_ Predicate> {
336        self.edges()
337            .filter(|e| e.source() == source)
338            .map(PrecedenceNode::target)
339            .collect()
340    }
341
342    pub fn reachable_from(&self, source: &Predicate) -> HashSet<&'_ Predicate> {
343        let mut initial: HashSet<&Predicate> = self.directly_reachable_from(source);
344        if initial.contains(source) {
345            initial
346        } else {
347            let next: HashSet<&Predicate> = initial
348                .iter()
349                .map(|s| self.directly_reachable_from(s))
350                .flatten()
351                .collect();
352            initial.extend(next);
353            initial
354        }
355    }
356
357    fn directly_reachable_nodes_from(&self, source: &Predicate) -> HashSet<&'_ PrecedenceNode<'_>> {
358        self.edges().filter(|e| e.source() == source).collect()
359    }
360
361    pub fn to_graphviz_string(&self) -> Result<String> {
362        let mut edges: Vec<String> = self
363            .edges()
364            .map(|edge| {
365                format!(
366                    "  {} -> {}{};\n",
367                    edge.source(),
368                    edge.target(),
369                    if edge.is_negative_target() {
370                        " [arrowhead=empty]"
371                    } else {
372                        ""
373                    },
374                )
375            })
376            .collect();
377        edges.sort();
378
379        let mut edb: Vec<String> = self
380            .edges()
381            .filter_map(|r| {
382                if r.is_extensional_target() {
383                    Some(format!(
384                        "  {} [style=filled; color=lightgrey];\n",
385                        r.target()
386                    ))
387                } else {
388                    None
389                }
390            })
391            .collect();
392        edb.sort();
393        edb.dedup();
394
395        Ok(format!(
396            "digraph G {{\n{}\n{}}}",
397            edges.join(""),
398            edb.join("")
399        ))
400    }
401}
402
403// ------------------------------------------------------------------------------------------------
404
405impl<'a> PrecedenceNode<'a> {
406    #[inline]
407    pub fn is_negative_target(&self) -> bool {
408        self.negative
409    }
410
411    #[inline]
412    pub fn is_extensional_target(&self) -> bool {
413        self.extensional
414    }
415
416    #[inline]
417    pub fn source(&self) -> &'a Predicate {
418        self.source
419    }
420
421    #[inline]
422    pub fn target(&self) -> &'a Predicate {
423        self.target
424    }
425}
426
427// ------------------------------------------------------------------------------------------------
428// Private Functions
429// ------------------------------------------------------------------------------------------------
430
431#[inline]
432fn head_predicates(rule: &Rule) -> HashSet<&Predicate> {
433    rule.head().map(|a| a.label()).collect()
434}
435
436#[inline]
437fn body_predicates(rule: &Rule) -> HashSet<(bool, &Predicate)> {
438    rule.literals()
439        .filter_map(|l| l.as_relational().map(|a| (l.is_negative(), a.label())))
440        .collect()
441}
442
443// ------------------------------------------------------------------------------------------------
444// Modules
445// ------------------------------------------------------------------------------------------------
446
447// ------------------------------------------------------------------------------------------------
448// Unit Tests
449// ------------------------------------------------------------------------------------------------
450
451#[cfg(test)]
452mod tests {
453    use crate::idb::eval::strata::{PrecedenceGraph, StratifiedProgram};
454    use crate::parse::parse_str;
455    use crate::Predicate;
456    use std::str::FromStr;
457
458    #[test]
459    fn test_stratification() {
460        let program = parse_str(
461            r#".feature(negation).
462.assert r(string, string).
463
464v(X) :- r(X, Y).
465v(Y) :- r(X, Y).
466t(X, Y) :- r(X, Y).
467t(X, Y) :- t(X, Z), r(Z, Y).
468tc(X, Y):- v(X), v(Y), NOT t(X, Y).
469"#,
470        )
471        .unwrap()
472        .into_parsed();
473
474        let stratified = StratifiedProgram::from(&program);
475        assert!(stratified.is_ok());
476        println!("{}", stratified.unwrap());
477    }
478
479    #[test]
480    fn test_precedence_graph() {
481        let program = parse_str(
482            r#".feature(negation).
483.assert r(string, string).
484
485v(X) :- r(X, Y).
486v(Y) :- r(X, Y).
487t(X, Y) :- r(X, Y).
488t(X, Y) :- t(X, Z), r(Z, Y).
489tc(X, Y):- v(X), v(Y), NOT t(X, Y).
490"#,
491        )
492        .unwrap()
493        .into_parsed();
494
495        assert!(program.is_recursive());
496
497        let graph = PrecedenceGraph::from(&program);
498        println!("{}", graph.to_graphviz_string().unwrap());
499
500        assert!(graph.is_recursive());
501        assert!(!graph.is_semi_positive());
502        assert!(graph.is_stratifiable());
503
504        let pred_t = Predicate::from_str("t").unwrap();
505        let pred_v = Predicate::from_str("v").unwrap();
506        let pred_tc = Predicate::from_str("tc").unwrap();
507
508        assert!(graph.is_level_zero(&pred_v));
509        assert!(!graph.is_level_zero(&pred_t));
510        assert!(!graph.is_level_zero(&pred_tc));
511
512        println!(
513            "t -> {:?}",
514            graph.reachable_from(&Predicate::from_str("t").unwrap())
515        );
516        println!(
517            "tc -> {:?}",
518            graph.reachable_from(&Predicate::from_str("tc").unwrap())
519        );
520    }
521
522    #[test]
523    fn test_precedence_graph_rdfs() {
524        let program = parse_str(
525            r#".feature(comparisons).
526.assert triple(string, string, string).
527
528% Section 2.2: Class
529class(C) :- triple(_, rdf:type, C).
530
531% Section 2.4: Datatype
532subClass(R, rdfs:Literal) :- instanceOf(R, rdfs:Datatype).
533
534% Section 2.8: Property
535property(P) :- triple(_, P, _).
536property(P) :- triple(P, rdf:type, rdfs:Property).
537
538% Section 3.1: range
539range(P, C) :- triple(P, rdfs:range, C).
540instanceOf(R, C) :- triple(_, P, R), range(P, C).
541range(P2, R) :- range(P, R), subProperty(P2, P).
542
543% Section 3.2: domain
544domain(P, C) :- triple(P, rdfs:domain, C).
545instanceOf(R, C) :- triple(R, P, _), domain(P, C).
546domain(P2, R) :- domain(P, R), subProperty(P2, P).
547
548% Section 3.3: rdf:type
549instanceOf(R, C) :- triple(R, rdf:type, C).
550instanceOf(R, C) :- triple(R, P, _), triple(P, rdfs:domain, C).
551instanceOf(R, C) :- triple(_, P, R), triple(P, rdfs:range, C).
552
553% Section 3.4: subClassOf
554subClass(C, P) :- triple(C, rdfs:subClassOf, P).
555class(C) :- subClass(C, _).
556class(C) :- subClass(_, C).
557instanceOf(C, C2) :- instanceOf(C, C1), subClass(C1, C2).
558subClass(C, rdfs:Class) :- class(C) AND C /= rdfs:Class.
559
560% Section 3.5: subPropertyOf
561subProperty(C, P) :- triple(C, rdfs:subPropertyOf, P).
562property(P) :- subProperty(P, _).
563property(P) :- subProperty(_, P).
564instanceOf(P, P2) :- instanceOf(P, P1), subProperty(P1, P2).
565subProperty(P, rdfs:Property) :- property(P) AND P /= rdfs:Property.
566
567% Section 5.1.5: ContainerMembershipProperty
568subProperty(P, rdfs:member) :- instanceOf(P, rdfs:ContainerMembershipProperty).
569"#,
570        )
571        .unwrap()
572        .into_parsed();
573
574        let graph = PrecedenceGraph::from(&program);
575        println!("{}", graph.to_graphviz_string().unwrap());
576
577        assert!(graph.is_recursive());
578        assert!(graph.is_semi_positive());
579        assert!(graph.is_stratifiable());
580
581        println!(
582            "property -> {:?}",
583            graph.reachable_from(&Predicate::from_str("property").unwrap())
584        );
585
586        println!(
587            "instanceOf -> {:?}",
588            graph.reachable_from(&Predicate::from_str("instanceOf").unwrap())
589        );
590    }
591
592    #[test]
593    fn test_is_semi_positive() {
594        let program = parse_str(
595            r#".feature(negation).
596.assert link(string, string).
597
598reachable(X, Y) :- link(X, Y).
599reachable(X, Y) :- link(X, Z), reachable(Z, Y).
600indirect(X, Y) :- reachable(X, Y), NOT link(X, Y).
601"#,
602        )
603        .unwrap()
604        .into_parsed();
605
606        let graph = PrecedenceGraph::from(&program);
607        println!("{}", graph.to_graphviz_string().unwrap());
608
609        assert!(graph.is_recursive());
610        assert!(graph.is_semi_positive());
611        assert!(graph.is_stratifiable());
612    }
613
614    #[test]
615    fn test_is_stratifiable() {
616        let program = parse_str(
617            r#".feature(negation).
618.assert link(string, string).
619
620reachable(X, Y) :- link(X, Y).
621reachable(X, Y) :- link(X, Z), reachable(Z, Y).
622anode(X) :- link(X, _).
623anode(Y) :- link(_, Y).
624unreachable(X, Y) :- reachable(X, Y), anode(X), anode(Y), NOT reachable(X, Y).
625"#,
626        )
627        .unwrap()
628        .into_parsed();
629
630        let graph = PrecedenceGraph::from(&program);
631        println!("{}", graph.to_graphviz_string().unwrap());
632
633        assert!(graph.is_recursive());
634        assert!(!graph.is_semi_positive());
635        assert!(graph.is_stratifiable());
636    }
637
638    #[test]
639    fn test_is_not_stratifiable() {
640        let program = parse_str(
641            r#".feature(negation).
642.assert link(string, string).
643
644reachable(X, Y) :- link(X, Y).
645reachable(X, Y) :- link(X, Z), reachable(Z, Y).
646absurdity(X, Y) :- unreachable(X, Y).
647unreachable(X, Y) :- reachable(X, Y), NOT absurdity(X, Y).
648"#,
649        )
650        .unwrap()
651        .into_parsed();
652
653        let graph = PrecedenceGraph::from(&program);
654        println!("{}", graph.to_graphviz_string().unwrap());
655
656        assert!(graph.is_recursive());
657        assert!(!graph.is_semi_positive());
658        assert!(!graph.is_stratifiable());
659
660        let stratified = StratifiedProgram::from(&program);
661        assert!(stratified.is_err());
662    }
663}
asdi/idb/eval/strata.rs

asdi/idb/eval/
strata.rs
