mrs-tptp 0.2.2

A robust TPTP parser for Rust using winnow
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

//! CNF (Clause Normal Form) AST types.
//!
//! CNF formulas are disjunctions of literals, where literals are atomic formulas
//! or their negations. Variables are implicitly universally quantified.

use super::common::*;
use super::fof::FOFTerm;

/// A CNF statement (the formula part of a cnf() annotated formula)
#[derive(Debug, Clone, PartialEq)]
pub enum CNFStatement<'a> {
    /// A logical formula (disjunction of literals)
    Logical(CNFFormula<'a>),
}

/// A CNF formula: a disjunction of literals or parenthesized formula
#[derive(Debug, Clone, PartialEq)]
pub enum CNFFormula<'a> {
    /// Disjunction of literals
    Disjunction(Vec<CNFLiteral<'a>>),
    /// Parenthesized formula
    Parens(Box<CNFFormula<'a>>),
}

impl<'a> CNFFormula<'a> {
    /// Create a disjunction from literals
    pub fn disjunction(literals: Vec<CNFLiteral<'a>>) -> Self {
        CNFFormula::Disjunction(literals)
    }

    /// Get all literals in this formula
    pub fn literals(&self) -> Vec<&CNFLiteral<'a>> {
        match self {
            CNFFormula::Disjunction(lits) => lits.iter().collect(),
            CNFFormula::Parens(inner) => inner.literals(),
        }
    }
}

/// A CNF literal: an atomic formula or its negation
#[derive(Debug, Clone, PartialEq)]
pub enum CNFLiteral<'a> {
    /// Positive literal
    Positive(CNFAtomicFormula<'a>),
    /// Negative literal (negated atomic formula)
    Negative(CNFAtomicFormula<'a>),
    /// Infix equality: term = term
    Equality(FOFTerm<'a>, FOFTerm<'a>),
    /// Infix inequality: term != term
    Inequality(FOFTerm<'a>, FOFTerm<'a>),
}

impl<'a> CNFLiteral<'a> {
    /// Check if this literal is positive
    pub fn is_positive(&self) -> bool {
        matches!(self, CNFLiteral::Positive(_) | CNFLiteral::Equality(_, _))
    }

    /// Check if this literal is negative
    pub fn is_negative(&self) -> bool {
        !self.is_positive()
    }
}

/// A CNF atomic formula: predicate application or defined/system predicate
#[derive(Debug, Clone, PartialEq)]
pub enum CNFAtomicFormula<'a> {
    /// Plain atomic formula: predicate(args) or proposition
    Plain(AtomicWord<'a>, Vec<FOFTerm<'a>>),
    /// Defined atomic formula: $predicate(args)
    Defined(DefinedWord<'a>, Vec<FOFTerm<'a>>),
    /// System atomic formula: $$predicate(args)
    System(SystemWord<'a>, Vec<FOFTerm<'a>>),
    /// $true
    True,
    /// $false
    False,
}

impl<'a> CNFAtomicFormula<'a> {
    /// Create a plain atomic formula
    pub fn plain(predicate: AtomicWord<'a>, args: Vec<FOFTerm<'a>>) -> Self {
        CNFAtomicFormula::Plain(predicate, args)
    }

    /// Create a proposition (0-ary predicate)
    pub fn proposition(name: AtomicWord<'a>) -> Self {
        CNFAtomicFormula::Plain(name, Vec::new())
    }
}