anthem 2.0.0

A command-line application for assisting in the verification of answer set programs
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100

use {
    crate::syntax_tree::asp::mini_gringo::{Head, Predicate, Program},
    indexmap::IndexSet,
    petgraph::{algo::is_cyclic_directed, graph::DiGraph},
    std::collections::HashMap,
};

pub trait PrivateRecursion {
    type Predicates;

    fn has_private_recursion(&self, private_predicates: &Self::Predicates) -> bool;
}

impl PrivateRecursion for Program {
    type Predicates = IndexSet<Predicate>;

    fn has_private_recursion(&self, private_predicates: &Self::Predicates) -> bool {
        for rule in &self.rules {
            match rule.head {
                Head::Choice(ref a) => {
                    if private_predicates.contains(&a.predicate()) {
                        return true;
                    }
                }
                Head::Basic(_) | Head::Falsity => (),
            }
        }

        let mut dependency_graph = DiGraph::<(), ()>::new();
        let mut mapping = HashMap::new();

        for predicate in self.predicates() {
            if private_predicates.contains(&predicate) {
                let node = dependency_graph.add_node(());
                mapping.insert(predicate, node);
            }
        }

        for rule in &self.rules {
            if let Some(head_predicate) = rule.head.predicate() {
                if private_predicates.contains(&head_predicate) {
                    for body_predicate in rule.body.predicates() {
                        if private_predicates.contains(&body_predicate) {
                            dependency_graph.update_edge(
                                mapping[&head_predicate],
                                mapping[&body_predicate],
                                (),
                            );
                        }
                    }
                }
            }
        }

        is_cyclic_directed(&dependency_graph)
    }
}

#[cfg(test)]
mod tests {
    use {
        crate::{
            analyzing::private_recursion::PrivateRecursion,
            syntax_tree::asp::mini_gringo::{Predicate, Program},
        },
        indexmap::IndexSet,
        std::str::FromStr,
    };

    #[test]
    fn test_private_recursion() {
        let private_predicates: IndexSet<Predicate> = IndexSet::from_iter(
            ["a/0", "b/0", "p/1"]
                .into_iter()
                .map(|p| p.parse().unwrap()),
        );

        for program in ["a :- not c. c :- not a.", "a :- p(1). p(X) :- q(X)."] {
            assert!(
                !Program::from_str(program)
                    .unwrap()
                    .has_private_recursion(&private_predicates)
            )
        }

        for program in [
            "{a}.",
            "a :- not a.",
            "a :- not not a.",
            "a :- not b. b :- not a.",
            "{p(X)} :- not not p(X). b :- a.",
        ] {
            assert!(
                Program::from_str(program)
                    .unwrap()
                    .has_private_recursion(&private_predicates)
            )
        }
    }
}