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

use crate::syntax_tree::fol::sigma_0::{
    AtomicFormula, BinaryConnective, Formula, Quantification, UnaryConnective,
};

pub enum UnboxedFormula {
    AtomicFormula(AtomicFormula),
    UnaryFormula {
        connective: UnaryConnective,
        formula: Formula,
    },
    BinaryFormula {
        connective: BinaryConnective,
        lhs: Formula,
        rhs: Formula,
    },
    QuantifiedFormula {
        quantification: Quantification,
        formula: Formula,
    },
}

impl UnboxedFormula {
    pub fn rebox(self) -> Formula {
        match self {
            Self::AtomicFormula(f) => Formula::AtomicFormula(f),
            Self::UnaryFormula {
                connective,
                formula,
            } => Formula::UnaryFormula {
                connective,
                formula: Box::new(formula),
            },
            Self::BinaryFormula {
                connective,
                lhs,
                rhs,
            } => Formula::BinaryFormula {
                connective,
                lhs: Box::new(lhs),
                rhs: Box::new(rhs),
            },
            Self::QuantifiedFormula {
                quantification,
                formula,
            } => Formula::QuantifiedFormula {
                quantification,
                formula: Box::new(formula),
            },
        }
    }
}