anthem 2.0.0-rc.1

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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119

use crate::{
    convenience::apply::Apply as _,
    syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Theory, UnaryConnective},
};

pub fn gamma(theory: Theory) -> Theory {
    let mut formulas = Vec::new();
    for formula in theory.formulas {
        formulas.push(gamma_formula(formula));
    }

    Theory { formulas }
}

pub fn gamma_formula(formula: Formula) -> Formula {
    match formula {
        x @ Formula::AtomicFormula(_) => here(x),

        Formula::UnaryFormula {
            connective: connective @ UnaryConnective::Negation,
            formula,
        } => Formula::UnaryFormula {
            connective,
            formula: there(*formula).into(),
        },

        Formula::BinaryFormula {
            connective:
                connective @ BinaryConnective::Conjunction | connective @ BinaryConnective::Disjunction,
            lhs,
            rhs,
        } => Formula::BinaryFormula {
            connective,
            lhs: gamma_formula(*lhs).into(),
            rhs: gamma_formula(*rhs).into(),
        },

        Formula::BinaryFormula {
            connective:
                connective @ BinaryConnective::Implication
                | connective @ BinaryConnective::ReverseImplication
                | connective @ BinaryConnective::Equivalence,
            lhs,
            rhs,
        } => Formula::BinaryFormula {
            connective: BinaryConnective::Conjunction,
            lhs: Formula::BinaryFormula {
                connective: connective.clone(),
                lhs: gamma_formula(*lhs.clone()).into(),
                rhs: gamma_formula(*rhs.clone()).into(),
            }
            .into(),
            rhs: Formula::BinaryFormula {
                connective,
                lhs: there(*lhs).into(),
                rhs: there(*rhs).into(),
            }
            .into(),
        },

        Formula::QuantifiedFormula {
            quantification,
            formula,
        } => Formula::QuantifiedFormula {
            quantification,
            formula: gamma_formula(*formula).into(),
        },
    }
}

pub fn here(formula: Formula) -> Formula {
    prepend_predicate(formula, "h")
}

pub fn there(formula: Formula) -> Formula {
    prepend_predicate(formula, "t")
}

fn prepend_predicate(formula: Formula, prefix: &'static str) -> Formula {
    formula.apply(&mut |formula| match formula {
        Formula::AtomicFormula(AtomicFormula::Atom(mut a)) => {
            a.predicate_symbol.insert_str(0, prefix);
            Formula::AtomicFormula(AtomicFormula::Atom(a))
        }
        x => x,
    })
}

#[cfg(test)]
mod tests {
    use super::gamma_formula;

    #[test]
    fn test_gamma() {
        for (src, target) in [
            ("#true", "#true"),
            ("a", "ha"),
            ("a(a)", "ha(a)"),
            ("X > 1", "X > 1"),
            ("not a", "not ta"),
            ("not X > 1", "not X > 1"),
            ("a and not b", "ha and not tb"),
            ("a or not b", "ha or not tb"),
            ("a -> b", "(ha -> hb) and (ta -> tb)"),
            ("a <- b", "(ha <- hb) and (ta <- tb)"),
            ("a <-> b", "(ha <-> hb) and (ta <-> tb)"),
            ("forall X p(X)", "forall X hp(X)"),
            ("exists X p(X)", "exists X hp(X)"),
        ] {
            let left = gamma_formula(src.parse().unwrap());
            let right = target.parse().unwrap();

            assert!(
                left == right,
                "assertion `left == right` failed:\n left:\n{left}\n right:\n{right}"
            );
        }
    }
}