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

use crate::{
    convenience::unbox::{Unbox, fol::sigma_0::UnboxedFormula},
    syntax_tree::fol::sigma_0::{
        AnnotatedFormula, BinaryConnective, Formula, Quantification, Quantifier, Specification,
        Theory,
    },
};

pub fn break_equivalences_annotated_formula(annotated_formula: AnnotatedFormula) -> Specification {
    Specification {
        formulas: break_equivalences_formula(annotated_formula.formula)
            .formulas
            .into_iter()
            .enumerate()
            .map(|(i, formula)| AnnotatedFormula {
                role: annotated_formula.role,
                direction: annotated_formula.direction,
                name: format!("{}_{}", annotated_formula.name, i),
                formula,
            })
            .collect(),
    }
}

pub fn break_equivalences_theory(theory: Theory) -> Theory {
    theory
        .into_iter()
        .flat_map(break_equivalences_formula)
        .collect()
}

pub fn break_equivalences_formula(formula: Formula) -> Theory {
    match formula.unbox() {
        UnboxedFormula::BinaryFormula {
            connective: BinaryConnective::Equivalence,
            lhs,
            rhs,
        } => Theory {
            formulas: vec![
                Formula::BinaryFormula {
                    connective: BinaryConnective::Implication,
                    lhs: Box::new(lhs.clone()),
                    rhs: Box::new(rhs.clone()),
                },
                Formula::BinaryFormula {
                    connective: BinaryConnective::ReverseImplication,
                    lhs: Box::new(lhs),
                    rhs: Box::new(rhs),
                },
            ],
        },
        UnboxedFormula::QuantifiedFormula {
            quantification:
                Quantification {
                    quantifier: Quantifier::Forall,
                    variables,
                },
            formula,
        } => Theory {
            formulas: break_equivalences_formula(formula)
                .formulas
                .into_iter()
                .map(|f| f.quantify(Quantifier::Forall, variables.clone()))
                .collect(),
        },
        x => Theory {
            formulas: vec![x.rebox()],
        },
    }
}

#[cfg(test)]
mod tests {
    use {
        super::break_equivalences_formula,
        crate::syntax_tree::fol::sigma_0::{Formula, Theory},
    };

    #[test]
    fn test_break_equivalences_formula() {
        for (src, target) in [
            ("p <-> q", "p -> q. p <- q."),
            ("p(X) <-> q(X)", "p(X) -> q(X). p(X) <- q(X)."),
            (
                "forall X (p(X) <-> q(X))",
                "forall X (p(X) -> q(X)). forall X (p(X) <- q(X)).",
            ),
            (
                "forall X (forall Y (p(X, Y) <-> q(X, Y)))",
                "forall X (forall Y (p(X, Y) -> q(X, Y))). forall X (forall Y (p(X, Y) <- q(X, Y))).",
            ),
        ] {
            let src: Formula = src.parse().unwrap();
            let target: Theory = target.parse().unwrap();
            assert_eq!(break_equivalences_formula(src), target)
        }
    }
}