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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137

WHITESPACE = _{ " " | NEWLINE }
COMMENT = _{ "%" ~ (!NEWLINE ~ ANY)* ~ (NEWLINE | EOI) }

keyword = _{ (primitive | binary_connective | unary_connective | quantifier) ~ !ANY }
    primitive = _{ infimum | supremum }
        infimum  = { "#inf" }
        supremum = { "#sup" }

sort = { general_sort | integer_sort | symbolic_sort }
sort_eoi = _{ sort ~ EOI }
    general_sort = @{ "g" ~ "eneral"? }
    integer_sort = @{ "i" ~ "nteger"? }
    symbolic_sort = @{ "s" ~ "ymbol"? }

basic_integer_term = _{ numeral | integer_function_constant | integer_variable }
    numeral           = @{ ("0") | ("-"? ~ ASCII_NONZERO_DIGIT ~ ASCII_DIGIT*) }
    integer_function_constant = ${ symbolic_constant ~ "$" ~ integer_sort }
    unsorted_variable = @{ "_"? ~ ASCII_ALPHA_UPPER ~ (ASCII_ALPHANUMERIC | "_")* }
    integer_variable  = ${ (unsorted_variable ~ "$" ~ integer_sort) | !(unsorted_variable ~ "$" ~ sort) ~ (unsorted_variable ~ "$") }

unary_operator = _{ negative }
unary_operator_eoi = _{ unary_operator ~ EOI }
    negative = { !numeral ~ "-" }

binary_operator = _{ add | subtract | multiply }
binary_operator_eoi = _{ binary_operator ~ EOI }
    add      = { "+" }
    subtract = { "-" }
    multiply = { "*" }

integer_term = { unary_operator* ~ n_primary ~ (binary_operator ~ unary_operator* ~ n_primary)* }
integer_term_eoi = _{ integer_term ~ EOI }
    n_primary = _{ basic_integer_term | "(" ~ integer_term ~ ")" }

symbolic_term = { symbolic_function_constant | symbolic_constant | symbolic_variable }
symbolic_term_eoi = _{ symbolic_term ~ EOI }
    symbolic_constant = @{ !keyword ~ "_"? ~ ASCII_ALPHA_LOWER ~ (ASCII_ALPHANUMERIC | "_")* }
    symbolic_function_constant = ${ symbolic_constant ~ "$" ~ symbolic_sort }
    symbolic_variable  = ${ (unsorted_variable ~ "$" ~ symbolic_sort) }

general_term = { general_function_constant | integer_term | symbolic_term | general_variable | infimum | supremum }
general_term_eoi = _{ general_term ~ EOI }
    general_variable  = ${ unsorted_variable ~ ("$" ~ general_sort)? }
    general_function_constant = ${ symbolic_constant ~ "$" ~ general_sort }

function_constant = { integer_function_constant | symbolic_function_constant | general_function_constant }
function_constant_eoi = _{ function_constant ~ EOI }

variable = { integer_variable | symbolic_variable | general_variable }
variable_eoi = _{ variable ~ EOI }

predicate = { predicate_symbol ~ "/" ~ arity }
predicate_eoi = _{ predicate ~ EOI }
    predicate_symbol  = _{ symbolic_constant }
    arity =  @{ ("0") | (ASCII_NONZERO_DIGIT ~ ASCII_DIGIT*) }

atom = { predicate_symbol ~ term_tuple? }
atom_eoi = _{ atom ~ EOI }
    term_tuple = _{ "(" ~ (general_term ~ ("," ~ general_term)*)? ~ ")" }

relation = { greater_equal | less_equal | greater | less | not_equal | equal }
relation_eoi = _{ relation ~ EOI }
    greater_equal = { ">=" }
    less_equal    = { "<=" }
    greater       = { ">"  }
    less          = { "<"  }
    not_equal     = { "!=" }
    equal         = { "="  }

guard = { relation ~ general_term }
guard_eoi = _{ guard ~ EOI }

comparison = { general_term ~ guard+ }
comparison_eoi = _{ comparison ~ EOI }

atomic_formula = { truth | falsity | comparison | atom }
atomic_formula_eoi = _{ atomic_formula ~ EOI }
    truth      = { "#true" }
    falsity    = { "#false" }

quantifier = _{ forall | exists }
quantifier_eoi = _{ quantifier ~ EOI }
    forall = { "forall" }
    exists = { "exists" }

quantification = { quantifier ~ variable+ }
quantification_eoi = _{ quantification ~ EOI }

unary_connective = _{ negation }
unary_connective_eoi = _{ unary_connective ~ EOI }
    negation = { "not" }

binary_connective = _{ equivalence | implication | reverse_implication | conjunction | disjunction }
binary_connective_eoi = _{ binary_connective ~ EOI }
    equivalence         = { "<->" }
    implication         = { "->"  }
    reverse_implication = { "<-"  }
    conjunction         = { "and" }
    disjunction         = { "or"  }

formula = { prefix* ~ primary ~ (infix ~ prefix* ~ primary)* }
formula_eoi = _{ formula ~ EOI }
    prefix  = _{ quantification | unary_connective }
    infix   = _{ binary_connective }
    primary = _{ "(" ~ formula ~ ")" | atomic_formula }

theory = { &ANY? ~ (formula ~ ".")* }
theory_eoi = _{ theory ~ EOI }

role = { assumption | spec | lemma | definition | inductive_lemma }
role_eoi = _{ role ~ EOI }
    assumption  = { "assumption" }
    spec        = { "spec" }
    lemma       = { "lemma" }
    definition  = { "definition" }
    inductive_lemma  = { "inductive-lemma" }

direction = { universal | forward | backward }
direction_eoi = _{ direction ~ EOI }
    universal = { "universal" }
    forward   = { "forward" }
    backward  = { "backward" }

annotated_formula = { role ~ ("(" ~ direction ~ ")")? ~ ("[" ~ symbolic_constant ~ "]")? ~ ":" ~ formula }
annotated_formula_eoi = _{ annotated_formula ~ EOI }

specification = { &ANY? ~ (annotated_formula ~ ".")* }
specification_eoi = _{ specification ~ EOI }

user_guide_entry = { input_predicate | output_predicate | placeholder_declaration | annotated_formula }
user_guide_entry_eoi = _{ user_guide_entry ~ EOI }
    input_predicate         = { "input" ~ ":" ~ predicate}
    output_predicate        = { "output" ~ ":" ~ predicate}
    placeholder_declaration = { "input" ~ ":" ~ symbolic_constant ~ ("->" ~ sort)? }

user_guide = { &ANY? ~ (user_guide_entry ~ ".")* }
user_guide_eoi = _{ user_guide ~ EOI }