argumentation/aspic/
language.rs

1//! Propositional language for ASPIC+.
2//!
3//! A `Literal` is either a positive atom (`Atom("bird")`) or its negation
4//! (`Neg("bird")`). Contrariness is symmetric literal negation.
5
6use std::fmt;
7
8/// A propositional literal: an atom or its negation.
9#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
10pub enum Literal {
11    /// Positive atom.
12    Atom(String),
13    /// Negated atom.
14    Neg(String),
15}
16
17impl Literal {
18    /// Construct a positive literal.
19    ///
20    /// # Panics (debug builds)
21    ///
22    /// Panics if `name` starts with the reserved prefix `__applicable_`,
23    /// which is used internally by [`crate::aspic::StructuredSystem::add_undercut_rule`]
24    /// to encode undercut attacks. Use `add_undercut_rule` to target a
25    /// defeasible rule rather than constructing the literal directly.
26    pub fn atom(name: impl Into<String>) -> Self {
27        let name = name.into();
28        debug_assert!(
29            !name.starts_with("__applicable_"),
30            "`__applicable_` prefix is reserved for ASPIC+ undercut encoding; use StructuredSystem::add_undercut_rule"
31        );
32        Literal::Atom(name)
33    }
34
35    /// Construct a negated literal.
36    ///
37    /// # Panics (debug builds)
38    ///
39    /// Panics if `name` starts with the reserved prefix `__applicable_`.
40    /// See [`Self::atom`] for context.
41    pub fn neg(name: impl Into<String>) -> Self {
42        let name = name.into();
43        debug_assert!(
44            !name.starts_with("__applicable_"),
45            "`__applicable_` prefix is reserved for ASPIC+ undercut encoding; use StructuredSystem::add_undercut_rule"
46        );
47        Literal::Neg(name)
48    }
49
50    /// Construct the reserved undercut-marker literal for a given rule id.
51    ///
52    /// This is the single sanctioned constructor for the `__applicable_<id>`
53    /// reserved namespace and is used internally by
54    /// [`crate::aspic::StructuredSystem::add_undercut_rule`] and
55    /// [`crate::aspic::compute_attacks`]. Consumers should never call this
56    /// directly — use `add_undercut_rule` instead.
57    pub(crate) fn undercut_marker(rule_id: usize) -> Literal {
58        Literal::Neg(format!("__applicable_{}", rule_id))
59    }
60
61    /// Return the contrary of this literal (negation).
62    pub fn contrary(&self) -> Literal {
63        match self {
64            Literal::Atom(n) => Literal::Neg(n.clone()),
65            Literal::Neg(n) => Literal::Atom(n.clone()),
66        }
67    }
68
69    /// Check whether two literals are contraries of each other.
70    pub fn is_contrary_of(&self, other: &Literal) -> bool {
71        &self.contrary() == other
72    }
73}
74
75impl fmt::Display for Literal {
76    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
77        match self {
78            Literal::Atom(n) => write!(f, "{}", n),
79            Literal::Neg(n) => write!(f, "¬{}", n),
80        }
81    }
82}
83
84#[cfg(test)]
85mod tests {
86    use super::*;
87
88    #[test]
89    fn contrary_of_atom_is_neg() {
90        let p = Literal::atom("p");
91        assert_eq!(p.contrary(), Literal::neg("p"));
92    }
93
94    #[test]
95    fn contrary_is_symmetric() {
96        let p = Literal::atom("p");
97        let np = Literal::neg("p");
98        assert!(p.is_contrary_of(&np));
99        assert!(np.is_contrary_of(&p));
100    }
101
102    #[test]
103    fn different_atoms_are_not_contraries() {
104        let p = Literal::atom("p");
105        let q = Literal::atom("q");
106        assert!(!p.is_contrary_of(&q));
107    }
108
109    #[test]
110    #[should_panic(expected = "__applicable_")]
111    fn atom_rejects_reserved_prefix_in_debug() {
112        let _ = Literal::atom("__applicable_42");
113    }
114
115    #[test]
116    #[should_panic(expected = "__applicable_")]
117    fn neg_rejects_reserved_prefix_in_debug() {
118        let _ = Literal::neg("__applicable_42");
119    }
120
121    #[test]
122    fn undercut_marker_bypasses_the_check() {
123        // The sanctioned constructor is allowed to use the reserved prefix.
124        let m = Literal::undercut_marker(42);
125        assert_eq!(m, Literal::Neg("__applicable_42".to_string()));
126    }
127}
argumentation/aspic/language.rs

argumentation/aspic/
language.rs
