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

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

precomputed_term = { infimum | integer | symbol | supremum }
precomputed_term_eoi = _{ precomputed_term ~ EOI }
    infimum = @{ "#infimum" | "#inf" }
    integer = @{ "0" | "-"? ~ ASCII_NONZERO_DIGIT ~ ASCII_DIGIT* }
    symbol = @{ !negation ~ "_"? ~ ASCII_ALPHA_LOWER ~ (ASCII_ALPHANUMERIC | "_")* }
    supremum = @{ "#supremum" | "#sup" }

variable = @{ ASCII_ALPHA_UPPER ~ ASCII_ALPHANUMERIC* }
variable_eoi = _{ variable ~ EOI }

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

binary_operator = _{ add | subtract | multiply | divide | modulo | interval }
binary_operator_eoi = _{ binary_operator ~ EOI }
    add = { "+" }
    subtract = { "-" }
    multiply = { "*" }
    divide = { "/" }
    modulo = { "\\" }
    interval = { ".." }

term = { unary_operator* ~ primary_term ~ (binary_operator ~ unary_operator* ~ primary_term)* }
term_eoi = _{ term ~ EOI }
    primary_term = _{ precomputed_term | variable | "(" ~ term ~ ")"}

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

atom = { symbol ~ term_tuple? }
atom_eoi = _{ atom ~ EOI }
    term_tuple = _{ "(" ~ (term ~ ("," ~ term)*)? ~ ")" }

sign = { negation{0, 2} }
sign_eoi = _{ sign ~ EOI }
    negation = @{ "not" ~ &(WHITESPACE | EOI)}

literal = { sign ~ atom }
literal_eoi = _{ literal ~ EOI }

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

comparison = { term ~ relation ~ term }
comparison_eoi = _{ comparison ~ EOI }

atomic_formula = { comparison | literal }
atomic_formula_eoi = _{ atomic_formula ~ EOI }

head = { basic_head | choice_head | falsity }
head_eoi = _{ head ~ EOI }
    basic_head = { atom }
    choice_head = { "{" ~ atom ~ "}" }
    falsity = { "#false"? }

body = { (atomic_formula ~ (("," | ";") ~ atomic_formula)*)? }
body_eoi = _{ body ~ EOI }

rule = { (!"." ~ head ~ (":-" ~ body)?) ~ "." }
rule_eoi = _{ rule ~ EOI }

program = { rule* }
program_eoi = _{ program ~ EOI }