Module clingox.ast

This module provides highlevel functions to work with clingo's AST.

Theory Parsing Examples

The following examples shows how to construct and use a theory parser:

>>> from clingo.ast import TheoryAtomType, parse_string
>>> from clingox.ast import Arity, Associativity, TheoryParser
>>>
>>> terms = {"term":
...     {("-", Arity.Unary): (3, Associativity.NoAssociativity),
...      ("**", Arity.Binary): (2, Associativity.Right),
...      ("*", Arity.Binary): (1, Associativity.Left),
...      ("+", Arity.Binary): (0, Associativity.Left),
...      ("-", Arity.Binary): (0, Associativity.Left)}}
>>> atoms = {("eval", 0): (TheoryAtomType.Head, "term", None)}
>>> parser = TheoryParser(terms, atoms)
>>>
>>> parse_string('&eval{ -1 * 2 + 3 }.', print)
#program base.
&eval { (- 1 * 2 + 3) }.
>>> parse_string('&eval{ -1 * 2 + 3 }.', lambda x: print(parser(x)))
#program base.
&eval { +(*(-(1),2),3) }.

The same parser can also be constructed from a theory:

>>> from clingo.ast import parse_string, ASTType
>>> from clingox.ast import theory_parser_from_definition
>>>
>>> theory = """\
... #theory test {
...     term {
...         -  : 3, unary;
...         ** : 2, binary, right;
...         *  : 1, binary, left;
...         +  : 0, binary, left;
...         -  : 0, binary, left
...     };
...     &eval/0 : term, head
... }.
... """
>>>
>>> parsers = []
>>> def extract(stm):
...     if stm.ast_type == ASTType.TheoryDefinition:
...         parsers.append(theory_parser_from_definition(stm))
...
>>> parse_string(theory, extract)
>>> parse_string('&eval{ -1 * 2 + 3 }.', print)
#program base.
&eval { (- 1 * 2 + 3) }.
>>> parse_string('&eval{ -1 * 2 + 3 }.', lambda x: print(parsers[0](x)))
#program base.
&eval { +(*(-(1),2),3) }.

Ast To Dict Conversion Example

Another interesting feature is to convert ASTs to YAML:

>>> from json import dumps
>>> from clingo.ast import parse_string
>>> from clingox.ast import ast_to_dict
>>>
>>> prg = []
>>> parse_string('a.', lambda x: prg.append(ast_to_dict(x)))
>>>
>>> print(dumps(prg, indent=2))
[
  {
    "ast_type": "Program",
    "location": "<string>:1:1",
    "name": "base",
    "parameters": []
  },
  {
    "ast_type": "Rule",
    "location": "<string>:1:1-3",
    "head": {
      "ast_type": "Literal",
      "location": "<string>:1:1-2",
      "sign": 0,
      "atom": {
        "ast_type": "SymbolicAtom",
        "symbol": {
          "ast_type": "Function",
          "location": "<string>:1:1-2",
          "name": "a",
          "arguments": [],
          "external": 0
        }
      }
    },
    "body": []
  }
]

Functions

def ast_to_dict(x: AST) ‑> dict

Expand source code

def ast_to_dict(x: AST) -> dict:
    """
    Convert the given ast node into a dictionary representation whose elements
    only involve the data structures: `dict`, `list`, `int`, and `str`.

    The resulting value can be used with other Python modules like the `yaml`
    or `pickle` modules.

    Parameters
    ----------
    x
        The ast to transform.

    Returns
    -------
    The corresponding Python representation.

    See Also
    --------
    dict_to_ast
    """
    ret = {"ast_type": str(x.ast_type).replace("ASTType.", "")}
    for key, val in x.items():
        if key == "location":
            assert isinstance(val, Location)
            enc = location_to_str(val)
        else:
            enc = _encode(val)
        ret[key] = enc
    return ret

Convert the given ast node into a dictionary representation whose elements only involve the data structures: dict, list, int, and str.

The resulting value can be used with other Python modules like the yaml or pickle modules.

Parameters

x

The ast to transform.

Returns

The corresponding Python representation.

See Also

dict_to_ast()

def clingo_literal_parser() ‑> TheoryTermParser

Expand source code

@lru_cache(maxsize=None)
def clingo_literal_parser() -> TheoryTermParser:
    """
    Return a theory term parser that parses theory literals similar to clingo's
    parser for symbolic literals.

    Note that for technical reasons pools and the absolute function are not
    supported.
    """
    clingo_literal_table = _clingo_term_table.copy()
    clingo_literal_table.update(
        {
            ("-", Arity.Unary): (0, Associativity.NoAssociativity),
            ("not", Arity.Unary): (0, Associativity.NoAssociativity),
        }
    )
    return TheoryTermParser(clingo_literal_table)

Return a theory term parser that parses theory literals similar to clingo's parser for symbolic literals.

Note that for technical reasons pools and the absolute function are not supported.

def clingo_term_parser() ‑> TheoryTermParser

Expand source code

@lru_cache(maxsize=None)
def clingo_term_parser() -> TheoryTermParser:
    """
    Return a theory term parser that parses theory terms like clingo terms.

    Note that for technical reasons pools and the absolute function are not
    supported.
    """
    return TheoryTermParser(_clingo_term_table)

Return a theory term parser that parses theory terms like clingo terms.

Note that for technical reasons pools and the absolute function are not supported.

def dict_to_ast(x: dict) ‑> AST

Expand source code

def dict_to_ast(x: dict) -> AST:
    """
    Convert the Python dict representation of an AST node into an AST node.

    Parameters
    ----------
    x
        The Python representation of the AST.

    Returns
    -------
    The corresponding AST.

    See Also
    --------
    ast_to_dict
    """
    return getattr(ast, x["ast_type"])(
        **{key: _decode(value, key) for key, value in x.items() if key != "ast_type"}
    )

Convert the Python dict representation of an AST node into an AST node.

Parameters

x

The Python representation of the AST.

Returns

The corresponding AST.

See Also

ast_to_dict()

def filter_body_literals(body: Iterable[AST],
symbolic_atom_predicate: Callable[[AST], bool] | bool = True,
theory_atom_predicate: Callable[[AST], bool] | bool = True,
aggregate_predicate: Callable[[AST], bool] | bool = True,
conditional_literal_predicate: Callable[[AST], bool] | bool = True,
signs: Container[Sign] = (<Sign.NoSign: 0>, <Sign.Negation: 1>, <Sign.DoubleNegation: 2>)) ‑> Iterable[AST]

Expand source code

def filter_body_literals(
    body: Iterable[AST],
    symbolic_atom_predicate: ASTPredicate = True,
    theory_atom_predicate: ASTPredicate = True,
    aggregate_predicate: ASTPredicate = True,
    conditional_literal_predicate: ASTPredicate = True,
    signs: Container[Sign] = (Sign.NoSign, Sign.Negation, Sign.DoubleNegation),
) -> Iterable[AST]:
    """
    Filters the given body literals according to the given predicates.

    Parameters
    ----------
    body
        An iterable of `AST`s for body literals.
    symbolic_atom_predicate
        Predicate to filter symbolic atoms.
    theory_atom_predicate
        Predicate to filter theory atoms.
    aggregate_predicate
        Predicate to filter aggregates.
    conditional_literal_predicate
        Predicate to filter conditional literals.
    signs
        Only include literals with the given signs.

    Returns
    -------
    An iterarable of body literals.

    Notes
    -----
    An `ASTPredicate` is a callable that takes an `AST` and returns a Boolean.
    Booleans `True` and `False` are also accepted, meaning that the predicate
    is always `True` or `False`, respectively.
    """
    pred = partial(
        _body_literal_predicate,
        symbolic_atom_predicate=symbolic_atom_predicate,
        theory_atom_predicate=theory_atom_predicate,
        aggregate_predicate=aggregate_predicate,
        conditional_literal_predicate=conditional_literal_predicate,
        signs=signs,
    )
    return filter(pred, body)

Filters the given body literals according to the given predicates.

Parameters

body

An iterable of ASTs for body literals.

symbolic_atom_predicate

Predicate to filter symbolic atoms.

theory_atom_predicate

Predicate to filter theory atoms.

aggregate_predicate

Predicate to filter aggregates.

conditional_literal_predicate

Predicate to filter conditional literals.

signs

Only include literals with the given signs.

Returns

An iterarable of body literals.

Notes

An ASTPredicate is a callable that takes an AST and returns a Boolean. Booleans True and False are also accepted, meaning that the predicate is always True or False, respectively.

def location_to_str(loc: Location) ‑> str

Expand source code

def location_to_str(loc: Location) -> str:
    """
    This function transfroms a loctation object into a readable string.

    Colons in the location will be quoted ensuring that the resulting is
    parsable using `str_to_location`.

    Parameters
    ----------
    loc
        The location to transform.

    Returns
    -------
    The string representation of the given location.
    """
    begin, end = loc.begin, loc.end
    bf, ef = _quote(begin.filename), _quote(end.filename)
    ret = f"{bf}:{begin.line}:{begin.column}"
    dash, eq = True, bf == ef
    if not eq:
        ret += f"{'-' if dash else ':'}{ef}"
        dash = False
    eq = eq and begin.line == end.line
    if not eq:
        ret += f"{'-' if dash else ':'}{end.line}"
        dash = False
    eq = eq and begin.column == end.column
    if not eq:
        ret += f"{'-' if dash else ':'}{end.column}"
        dash = False
    return ret

This function transfroms a loctation object into a readable string.

Colons in the location will be quoted ensuring that the resulting is parsable using str_to_location().

Parameters

loc

The location to transform.

Returns

The string representation of the given location.

def negate_sign(sign: Sign) ‑> Sign

Expand source code

def negate_sign(sign: ast.Sign) -> ast.Sign:
    """
    Negate the given sign.
    """
    if sign == ast.Sign.Negation:
        return ast.Sign.DoubleNegation
    return ast.Sign.Negation

Negate the given sign.

def normalize_symbolic_terms(x: AST)

Expand source code

def normalize_symbolic_terms(x: AST):
    """
    Replaces all occurrences of objects of the class clingo.Function in an AST
    by the corresponding object of the class ast.Function.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    return _NormalizeSymbolicTermTransformer().visit(x)

Replaces all occurrences of objects of the class clingo.Function in an AST by the corresponding object of the class ast.Function.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

def parse_theory(s: str) ‑> TheoryParser

Expand source code

def parse_theory(s: str) -> TheoryParser:
    """
    Turn the given theory into a parser.
    """
    parser = None

    def extract(stm):
        nonlocal parser
        if stm.ast_type == ASTType.TheoryDefinition:
            if parser is not None:
                raise ValueError("multiple theory definitions")
            parser = theory_parser_from_definition(stm)
        else:
            assert (
                stm.ast_type == ASTType.Program
                and stm.name == "base"
                and not stm.parameters
            )

    parse_string(f"{s}.", extract)
    if parser is None:
        raise ValueError("no theory definition found")
    return cast(TheoryParser, parser)

Turn the given theory into a parser.

def partition_body_literals(body: Iterable[AST],
symbolic_atom_predicate: Callable[[AST], bool] | bool = True,
theory_atom_predicate: Callable[[AST], bool] | bool = True,
aggregate_predicate: Callable[[AST], bool] | bool = True,
conditional_literal_predicate: Callable[[AST], bool] | bool = True,
signs: Container[Sign] = (<Sign.NoSign: 0>, <Sign.Negation: 1>, <Sign.DoubleNegation: 2>)) ‑> Tuple[List[AST], List[AST]]

Expand source code

def partition_body_literals(
    body: Iterable[AST],
    symbolic_atom_predicate: ASTPredicate = True,
    theory_atom_predicate: ASTPredicate = True,
    aggregate_predicate: ASTPredicate = True,
    conditional_literal_predicate: ASTPredicate = True,
    signs: Container[Sign] = (Sign.NoSign, Sign.Negation, Sign.DoubleNegation),
) -> Tuple[List[AST], List[AST]]:
    """
    Partition the given body literals according to the given predicates.

    Parameters
    ----------
    body
        An iterable of `AST` that represents a body.
    symbolic_atom_predicate
        Predicate to partition symbolic atoms.
    theory_atom_predicate
        Predicate to partition theory atoms.
    aggregate_predicate
        Predicate to partition aggregates.
    conditional_literal_predicate
        Predicate to partition conditional literals.
    signs
        Only include literals with the given signs in the first list.

    Returns
    -------
    A pair of lists of body literals. The first iterable yields the literals
    that satisfy the predicate while the second one yields the ones that do
    not.

    Notes
    -----
    An `ASTPredicate` is a callable that takes an `AST` and returns a Boolean.
    Booleans `True` and `False` are also accepted, meaning that the predicate
    is always `True` or `False`, respectively.
    """
    pred = partial(
        _body_literal_predicate,
        symbolic_atom_predicate=symbolic_atom_predicate,
        theory_atom_predicate=theory_atom_predicate,
        aggregate_predicate=aggregate_predicate,
        conditional_literal_predicate=conditional_literal_predicate,
        signs=signs,
    )
    part_a: List[AST] = []
    part_b: List[AST] = []
    for lit in body:
        if pred(lit):
            part_a.append(lit)
        else:
            part_b.append(lit)
    return part_a, part_b

Partition the given body literals according to the given predicates.

Parameters

body

An iterable of AST that represents a body.

symbolic_atom_predicate

Predicate to partition symbolic atoms.

theory_atom_predicate

Predicate to partition theory atoms.

aggregate_predicate

Predicate to partition aggregates.

conditional_literal_predicate

Predicate to partition conditional literals.

signs

Only include literals with the given signs in the first list.

Returns

A pair of lists of body literals. The first iterable yields the literals

 

that satisfy the predicate while the second one yields the ones that do

 

not.

Notes

An ASTPredicate is a callable that takes an AST and returns a Boolean. Booleans True and False are also accepted, meaning that the predicate is always True or False, respectively.

def prefix_symbolic_atoms(x: AST,
prefix: str) ‑> AST

Expand source code

def prefix_symbolic_atoms(x: AST, prefix: str) -> AST:
    """
    Prefix all symbolic atoms in the given AST with the given string.

    Parameters
    ----------
    x
        The ast in which to prefix symbolic atom names.
    prefix
        The prefix to add.

    Returns
    -------
    The rewritten AST.

    See Also
    --------
    rename_symbolic_atoms
    """
    return rename_symbolic_atoms(x, lambda s: prefix + s)

Prefix all symbolic atoms in the given AST with the given string.

Parameters

x

The ast in which to prefix symbolic atom names.

prefix

The prefix to add.

Returns

The rewritten AST.

See Also

rename_symbolic_atoms()

def reify_symbolic_atoms(x: AST,
name: str,
argument_extender: Callable[[AST], Sequence[AST]] | None = None,
reify_strong_negation: bool = False) ‑> AST

Expand source code

def reify_symbolic_atoms(
    x: AST,
    name: str,
    argument_extender: Optional[Callable[[AST], Sequence[AST]]] = None,
    reify_strong_negation: bool = False,
) -> AST:
    """
    Reify all symbolic atoms in the given AST node with the given name and
    function.

    Parameters
    ----------
    x
        The ast in which to rename symbolic atoms.
    name
        A string to serve as name of the new symbolic atom.
    argument_extender
        A function to provide extra arguments. If not provided, no extra
        arguments are added. The term passed as argument should be placed in
        the correct position.
    reify_strong_negation
        Boolean indicating how to encode strong negation. If false, `-p(X)` is
        reified as `-name(p(X))`. If true, then `-p(X)` is reified as
        `name(-p(X))`. In the latter case, this means that stable models
        containing both `name(p(a))` and `name(-p(a))` are possible. Clingo
        style consistency can be restored by adding the constraint
        `:- name(X), name(-X), X<-X.`

    Returns
    -------
    The rewritten AST.
    """

    def reifier(term: AST):
        if term.ast_type == ASTType.UnaryOperation and not reify_strong_negation:
            return UnaryOperation(
                term.location, term.operator_type, reifier(term.argument)
            )
        arguments = argument_extender(term) if argument_extender else [term]
        return Function(term.location, name, arguments, False)

    return rewrite_symbolic_atoms(x, reifier)

Reify all symbolic atoms in the given AST node with the given name and function.

Parameters

x

The ast in which to rename symbolic atoms.

name

A string to serve as name of the new symbolic atom.

argument_extender

A function to provide extra arguments. If not provided, no extra arguments are added. The term passed as argument should be placed in the correct position.

reify_strong_negation

Boolean indicating how to encode strong negation. If false, -p(X) is reified as -name(p(X)). If true, then -p(X) is reified as name(-p(X)). In the latter case, this means that stable models containing both name(p(a)) and name(-p(a)) are possible. Clingo style consistency can be restored by adding the constraint :- name(X), name(-X), X<-X.

Returns

The rewritten AST.

def rename_symbolic_atoms(x: AST,
rename_function: Callable[[str], str]) ‑> AST

Expand source code

def rename_symbolic_atoms(x: AST, rename_function: Callable[[str], str]) -> AST:
    """
    Rename all symbolic atoms in the given AST node with the given function.

    Parameters
    ----------
    x
        The ast in which to rename symbolic atoms.
    rename_function
        A function for renaming symbols.

    Returns
    -------
    The rewritten AST.
    """

    def renamer(term: AST):
        if term.ast_type == ASTType.UnaryOperation:
            return UnaryOperation(
                term.location, term.operator_type, renamer(term.argument)
            )
        if term.ast_type == ASTType.SymbolicTerm:
            sym = term.symbol
            new_name = rename_function(sym.name)
            return SymbolicTerm(
                term.location, clingo.Function(new_name, sym.arguments, sym.positive)
            )
        if term.ast_type == ASTType.Function:
            return Function(
                term.location, rename_function(term.name), term.arguments, term.external
            )
        return term

    return rewrite_symbolic_atoms(x, renamer)

Rename all symbolic atoms in the given AST node with the given function.

Parameters

x

The ast in which to rename symbolic atoms.

rename_function

A function for renaming symbols.

Returns

The rewritten AST.

def str_to_location(loc: str) ‑> Location

Expand source code

def str_to_location(loc: str) -> Location:
    """
    This function parses a location from its string representation.

    Parameters
    ----------
    loc
        The string to parse.

    Returns
    -------
    The parsed location.

    See Also
    --------
    location_to_str
    """
    m = fullmatch(
        r"(?P<bf>([^\\:]|\\\\|\\:)*):(?P<bl>[0-9]*):(?P<bc>[0-9]+)"
        r"(-(((?P<ef>([^\\:]|\\\\|\\:)*):)?(?P<el>[0-9]*):)?(?P<ec>[0-9]+))?",
        loc,
    )
    if not m:
        raise RuntimeError("could not parse location")
    begin = Position(_unquote(m["bf"]), int(m["bl"]), int(m["bc"]))
    end = Position(
        _unquote(_s(m, "bf", "ef")), int(_s(m, "bl", "el")), int(_s(m, "bc", "ec"))
    )
    return Location(begin, end)

This function parses a location from its string representation.

Parameters

loc

The string to parse.

Returns

The parsed location.

See Also

location_to_str()

def theory_parser_from_definition(x: AST) ‑> TheoryParser

Expand source code

def theory_parser_from_definition(x: AST) -> TheoryParser:
    """
    Turn an AST node of type TheoryDefinition into a TheoryParser.

    Parameters
    ----------
    x
        An AST representing a theory definition.

    Returns
    -------
    The corresponding `TheoryParser`.
    """
    assert x.ast_type == ASTType.TheoryDefinition

    terms = {}
    atoms = {}

    for term_def in x.terms:
        term_table = {}

        for op_def in term_def.operators:
            op_assoc: Associativity
            if op_def.operator_type == TheoryOperatorType.BinaryLeft:
                op_type = Arity.Binary
                op_assoc = Associativity.Left
            elif op_def.operator_type == TheoryOperatorType.BinaryRight:
                op_type = Arity.Binary
                op_assoc = Associativity.Right
            else:
                op_type = Arity.Unary
                op_assoc = Associativity.NoAssociativity

            term_table[(op_def.name, op_type)] = (op_def.priority, op_assoc)

        terms[term_def.name] = term_table

    for atom_def in x.atoms:
        guard = None
        if atom_def.guard is not None:
            guard = (atom_def.guard.operators, atom_def.guard.term)

        atoms[(atom_def.name, atom_def.arity)] = (
            atom_def.atom_type,
            atom_def.term,
            guard,
        )

    return TheoryParser(terms, atoms)

Turn an AST node of type TheoryDefinition into a TheoryParser.

Parameters

x

An AST representing a theory definition.

Returns

The corresponding TheoryParser.

def theory_term_to_literal(x: AST,
parse: bool = True) ‑> AST

Expand source code

def theory_term_to_literal(x: AST, parse: bool = True) -> AST:
    """
    Convert the given theory term into a symbolic clingo literal.

    If argument `parse` is set to true, occurences of unparsed theory terms are
    parsed using `clingo_literal_parser()`.

    Literals can use an arbitrary number of classical and default negation
    signs. They are normalized using the following equivalences:

    - `- - lit = lit`
    - `- not lit = not not lit`
    - `not not not lit = not lit`
    """
    if parse:
        x = clingo_literal_parser()(x)
    return _theory_term_to_literal(x, True, ast.Sign.NoSign)

Convert the given theory term into a symbolic clingo literal.

If argument parse is set to true, occurences of unparsed theory terms are parsed using clingo_literal_parser().

Literals can use an arbitrary number of classical and default negation signs. They are normalized using the following equivalences:

• - - lit = lit
• - not lit = not not lit
• not not not lit = not lit

def theory_term_to_term(x: AST,
parse: bool = True) ‑> AST

Expand source code

def theory_term_to_term(x: AST, parse: bool = True) -> AST:
    """
    Convert the given theory term into a plain clingo term.

    If argument `parse` is set to true, occurences of unparsed theory terms are
    parsed using `clingo_term_parser()`.
    """
    if parse:
        x = clingo_term_parser()(x)
    return _theory_term_to_term(x)

Convert the given theory term into a plain clingo term.

If argument parse is set to true, occurences of unparsed theory terms are parsed using clingo_term_parser().

Classes

class Arity (*args, **kwds)

Expand source code

class Arity(Enum):
    """
    Enumeration of operator arities.
    """

    # pylint:disable=invalid-name
    Unary = 1
    Binary = 2

Enumeration of operator arities.

Ancestors

• enum.Enum

Class variables

var Binary

var Unary

class Associativity (*args, **kwds)

Expand source code

class Associativity(Enum):
    """
    Enumeration of operator associativities.
    """

    # pylint: disable=invalid-name
    Left = auto()
    Right = auto()
    NoAssociativity = auto()

Enumeration of operator associativities.

Ancestors

• enum.Enum

Class variables

var Left

var NoAssociativity

var Right

class TheoryParser (terms: Mapping[str, Mapping[Tuple[str, Arity], Tuple[int, Associativity]] | TheoryTermParser],
atoms: Mapping[Tuple[str, int], Tuple[TheoryAtomType, str, Tuple[List[str], str] | None]])

Expand source code

class TheoryParser(Transformer):
    """
    This class parses theory atoms in the same way as clingo's internal parser.

    Parameters
    ----------
    terms
        Mapping from term identifiers to `TheoryTermParser`s. If an operator
        table is given, the `TheoryTermParser` is constructed from this table.

    atoms
        Mapping from atom name/arity pairs to tuples defining the acceptable
        structure of the theory atom.
    """

    # pylint: disable=invalid-name
    _table: Mapping[
        Tuple[str, int],
        Tuple[
            TheoryAtomType,
            TheoryTermParser,
            Optional[Tuple[Set[str], TheoryTermParser]],
        ],
    ]
    _in_body: bool
    _in_head: bool
    _is_directive: bool

    def __init__(
        self,
        terms: Mapping[str, Union[OperatorTable, TheoryTermParser]],
        atoms: AtomTable,
    ):
        self._reset()

        term_parsers = {}
        for term_key, parser in terms.items():
            if isinstance(parser, TheoryTermParser):
                term_parsers[term_key] = parser
            else:
                term_parsers[term_key] = TheoryTermParser(parser)

        self._table = {}
        for atom_key, (atom_type, term_key, guard) in atoms.items():
            guard_table = None
            if guard is not None:
                guard_table = (set(guard[0]), term_parsers[guard[1]])
            self._table[atom_key] = (atom_type, term_parsers[term_key], guard_table)

    def _reset(self, in_head=True, in_body=True, is_directive=True):
        """
        Set state information about active scope.
        """
        self._in_head = in_head
        self._in_body = in_body
        self._is_directive = is_directive

    def _visit_body(self, x: AST) -> AST:
        try:
            self._reset(False, True, False)
            old = x.body
            new = self.visit_sequence(old)
            return x if new is old else x.update(body=new)
        finally:
            self._reset()

    def visit_Rule(self, x: AST) -> AST:
        """
        Parse theory atoms in body and head.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        ret = self._visit_body(x)
        try:
            self._reset(True, False, not x.body)
            head = self(x.head)
            if head is not x.head:
                if ret is x:
                    ret = copy(ret)
                ret.head = head
        finally:
            self._reset()

        return ret

    def visit_ShowTerm(self, x: AST) -> AST:
        """
        Parse theory atoms in body.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        return self._visit_body(x)

    def visit_Minimize(self, x: AST) -> AST:
        """
        Parse theory atoms in body.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        return self._visit_body(x)

    def visit_Edge(self, x: AST) -> AST:
        """
        Parse theory atoms in body.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        return self._visit_body(x)

    def visit_Heuristic(self, x: AST) -> AST:
        """
        Parse theory atoms in body.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        return self._visit_body(x)

    def visit_ProjectAtom(self, x: AST) -> AST:
        """
        Parse theory atoms in body.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        return self._visit_body(x)

    def visit_TheoryAtom(self, x: AST) -> AST:
        """
        Parse the given theory atom.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        name = x.term.name
        arity = len(x.term.arguments)
        if (name, arity) not in self._table:
            raise RuntimeError(
                f"theory atom definiton not found: {location_to_str(x.location)}"
            )

        type_, element_parser, guard_table = self._table[(name, arity)]
        if type_ == TheoryAtomType.Head and not self._in_head:
            raise RuntimeError(
                f"theory atom only accepted in head: {location_to_str(x.location)}"
            )
        if type_ == TheoryAtomType.Body and not self._in_body:
            raise RuntimeError(
                f"theory atom only accepted in body: {location_to_str(x.location)}"
            )
        if type_ == TheoryAtomType.Directive and not (
            self._in_head and self._is_directive
        ):
            raise RuntimeError(
                f"theory atom must be a directive: {location_to_str(x.location)}"
            )

        x = copy(x)
        x.term = element_parser(x.term)
        x.elements = element_parser.visit_sequence(x.elements)

        if x.guard is not None:
            if guard_table is None:
                raise RuntimeError(
                    f"unexpected guard in theory atom: {location_to_str(x.location)}"
                )

            guards, guard_parser = guard_table
            if x.guard.operator_name not in guards:
                raise RuntimeError(
                    f"unexpected guard in theory atom: {location_to_str(x.location)}"
                )

            x.guard = copy(x.guard)
            x.guard.term = guard_parser(x.guard.term)

        return x

This class parses theory atoms in the same way as clingo's internal parser.

Parameters

terms

Mapping from term identifiers to TheoryTermParsers. If an operator table is given, the TheoryTermParser is constructed from this table.

atoms

Mapping from atom name/arity pairs to tuples defining the acceptable structure of the theory atom.

Ancestors

• Transformer

Methods

def visit_Edge(self,
x: AST) ‑> AST

Expand source code

def visit_Edge(self, x: AST) -> AST:
    """
    Parse theory atoms in body.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    return self._visit_body(x)

Parse theory atoms in body.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

def visit_Heuristic(self,
x: AST) ‑> AST

Expand source code

def visit_Heuristic(self, x: AST) -> AST:
    """
    Parse theory atoms in body.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    return self._visit_body(x)

Parse theory atoms in body.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

def visit_Minimize(self,
x: AST) ‑> AST

Expand source code

def visit_Minimize(self, x: AST) -> AST:
    """
    Parse theory atoms in body.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    return self._visit_body(x)

Parse theory atoms in body.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

def visit_ProjectAtom(self,
x: AST) ‑> AST

Expand source code

def visit_ProjectAtom(self, x: AST) -> AST:
    """
    Parse theory atoms in body.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    return self._visit_body(x)

Parse theory atoms in body.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

def visit_Rule(self,
x: AST) ‑> AST

Expand source code

def visit_Rule(self, x: AST) -> AST:
    """
    Parse theory atoms in body and head.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    ret = self._visit_body(x)
    try:
        self._reset(True, False, not x.body)
        head = self(x.head)
        if head is not x.head:
            if ret is x:
                ret = copy(ret)
            ret.head = head
    finally:
        self._reset()

    return ret

Parse theory atoms in body and head.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

def visit_ShowTerm(self,
x: AST) ‑> AST

Expand source code

def visit_ShowTerm(self, x: AST) -> AST:
    """
    Parse theory atoms in body.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    return self._visit_body(x)

Parse theory atoms in body.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

def visit_TheoryAtom(self,
x: AST) ‑> AST

Expand source code

def visit_TheoryAtom(self, x: AST) -> AST:
    """
    Parse the given theory atom.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    name = x.term.name
    arity = len(x.term.arguments)
    if (name, arity) not in self._table:
        raise RuntimeError(
            f"theory atom definiton not found: {location_to_str(x.location)}"
        )

    type_, element_parser, guard_table = self._table[(name, arity)]
    if type_ == TheoryAtomType.Head and not self._in_head:
        raise RuntimeError(
            f"theory atom only accepted in head: {location_to_str(x.location)}"
        )
    if type_ == TheoryAtomType.Body and not self._in_body:
        raise RuntimeError(
            f"theory atom only accepted in body: {location_to_str(x.location)}"
        )
    if type_ == TheoryAtomType.Directive and not (
        self._in_head and self._is_directive
    ):
        raise RuntimeError(
            f"theory atom must be a directive: {location_to_str(x.location)}"
        )

    x = copy(x)
    x.term = element_parser(x.term)
    x.elements = element_parser.visit_sequence(x.elements)

    if x.guard is not None:
        if guard_table is None:
            raise RuntimeError(
                f"unexpected guard in theory atom: {location_to_str(x.location)}"
            )

        guards, guard_parser = guard_table
        if x.guard.operator_name not in guards:
            raise RuntimeError(
                f"unexpected guard in theory atom: {location_to_str(x.location)}"
            )

        x.guard = copy(x.guard)
        x.guard.term = guard_parser(x.guard.term)

    return x

Parse the given theory atom.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

Inherited members

• Transformer:
  • visit
  • visit_children
  • visit_sequence

class TheoryTermParser (table: Mapping[Tuple[str, Arity], Tuple[int, Associativity]] | TheoryUnparsedTermParser)

Expand source code

class TheoryTermParser(Transformer):
    """
    Parser for theory terms in clingo's AST that works like the inbuilt one.

    This is implemented as a transformer that traverses the AST replacing all
    terms found.

    Parameters
    ----------
    table
        This must either be a table of operators or a `TheoryUnparsedTermParser`.

    See Also
    --------
    TheoryUnparsedTermParser
    """

    # pylint: disable=invalid-name

    def __init__(self, table: Union[OperatorTable, TheoryUnparsedTermParser]):
        self._parser = (
            table
            if isinstance(table, TheoryUnparsedTermParser)
            else TheoryUnparsedTermParser(table)
        )

    def visit_TheoryFunction(self, x) -> AST:
        """
        Parse the theory function and check if it agrees with the grammar.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        arity = None
        if len(x.arguments) == 1:
            arity = Arity.Unary
        if len(x.arguments) == 2:
            arity = Arity.Binary
        if arity is not None and is_operator(x.name):
            self._parser.check_operator(x.name, arity, x.location)

        return x.update(**self.visit_children(x))

    def visit_TheoryUnparsedTerm(self, x: AST) -> AST:
        """
        Parse the given unparsed term.

        Parameters
        ----------
        x
            The AST to rewrite.

        Returns
        -------
        The rewritten AST.
        """
        return cast(AST, self(self._parser.parse(x)))

Parser for theory terms in clingo's AST that works like the inbuilt one.

This is implemented as a transformer that traverses the AST replacing all terms found.

Parameters

table

This must either be a table of operators or a TheoryUnparsedTermParser.

See Also

TheoryUnparsedTermParser

Ancestors

• Transformer

Methods

def visit_TheoryFunction(self, x) ‑> AST

Expand source code

def visit_TheoryFunction(self, x) -> AST:
    """
    Parse the theory function and check if it agrees with the grammar.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    arity = None
    if len(x.arguments) == 1:
        arity = Arity.Unary
    if len(x.arguments) == 2:
        arity = Arity.Binary
    if arity is not None and is_operator(x.name):
        self._parser.check_operator(x.name, arity, x.location)

    return x.update(**self.visit_children(x))

Parse the theory function and check if it agrees with the grammar.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

def visit_TheoryUnparsedTerm(self,
x: AST) ‑> AST

Expand source code

def visit_TheoryUnparsedTerm(self, x: AST) -> AST:
    """
    Parse the given unparsed term.

    Parameters
    ----------
    x
        The AST to rewrite.

    Returns
    -------
    The rewritten AST.
    """
    return cast(AST, self(self._parser.parse(x)))

Parse the given unparsed term.

Parameters

x

The AST to rewrite.

Returns

The rewritten AST.

Inherited members

• Transformer:
  • visit
  • visit_children
  • visit_sequence

class TheoryUnparsedTermParser (table: Mapping[Tuple[str, Arity], Tuple[int, Associativity]])

Expand source code

class TheoryUnparsedTermParser:
    """
    Parser for unparsed theory terms in clingo's AST that works like the
    inbuilt one.

    Note that associativity for unary operators is ignored and binary
    operators must use either `Associativity.Left` or `Associativity.Right`.

    Parameters
    ----------
    table
        Mapping of operator/arity pairs to priority/associativity pairs.
    """

    _stack: List[Tuple[str, Arity]]
    _terms: List[AST]
    _table: OperatorTable

    def __init__(self, table: OperatorTable):
        self._stack = []
        self._terms = []
        self._table = table

    def _priority_and_associativity(self, operator: str) -> Tuple[int, Associativity]:
        """
        Get priority and associativity of the given binary operator.
        """
        return self._table[(operator, Arity.Binary)]

    def _priority(self, operator: str, arity: Arity) -> int:
        """
        Get priority of the given unary or binary operator.
        """
        return self._table[(operator, arity)][0]

    def _check(self, operator: str) -> bool:
        """
        Returns true if the stack has to be reduced because of the precedence
        of the given binary operator is lower than the preceeding operator on
        the stack.
        """
        if not self._stack:
            return False
        priority, associativity = self._priority_and_associativity(operator)
        previous_priority = self._priority(*self._stack[-1])
        return previous_priority > priority or (
            previous_priority == priority and associativity == Associativity.Left
        )

    def _reduce(self) -> None:
        """
        Combines the last unary or binary term on the stack.
        """
        b = self._terms.pop()
        operator, arity = self._stack.pop()
        if arity == Arity.Unary:
            self._terms.append(TheoryFunction(b.location, operator, [b]))
        else:
            a = self._terms.pop()
            loc = Location(a.location.begin, b.location.end)
            self._terms.append(TheoryFunction(loc, operator, [a, b]))

    def check_operator(self, operator: str, arity: Arity, location: Location) -> None:
        """
        Check if the given operator is in the parse table raising a runtime
        error if absent.

        Parameters
        ----------
        operator
            The operator name.
        arity
            The arity of the operator.
        location
            Location of the operator for error reporting.
        """
        if (operator, arity) not in self._table:
            raise RuntimeError(
                f"cannot parse operator `{operator}`: {location_to_str(location)}"
            )

    def parse(self, x: AST) -> AST:
        """
        Parses the given unparsed term, replacing it by nested theory
        functions.

        Parameters
        ----------
        x
            The AST to parse.

        Returns
        -------
        The rewritten AST.
        """
        del self._stack[:]
        del self._terms[:]

        arity = Arity.Unary

        for element in x.elements:
            for operator in element.operators:
                self.check_operator(operator, arity, x.location)

                while arity == Arity.Binary and self._check(operator):
                    self._reduce()

                self._stack.append((operator, arity))
                arity = Arity.Unary

            self._terms.append(element.term)
            arity = Arity.Binary

        while self._stack:
            self._reduce()

        return self._terms[0]

Parser for unparsed theory terms in clingo's AST that works like the inbuilt one.

Note that associativity for unary operators is ignored and binary operators must use either Associativity.Left or Associativity.Right.

Parameters

table

Mapping of operator/arity pairs to priority/associativity pairs.

Methods

def check_operator(self,
operator: str,
arity: Arity,
location: Location) ‑> None

Expand source code

def check_operator(self, operator: str, arity: Arity, location: Location) -> None:
    """
    Check if the given operator is in the parse table raising a runtime
    error if absent.

    Parameters
    ----------
    operator
        The operator name.
    arity
        The arity of the operator.
    location
        Location of the operator for error reporting.
    """
    if (operator, arity) not in self._table:
        raise RuntimeError(
            f"cannot parse operator `{operator}`: {location_to_str(location)}"
        )

Check if the given operator is in the parse table raising a runtime error if absent.

Parameters

operator

The operator name.

arity

The arity of the operator.

location

Location of the operator for error reporting.

def parse(self,
x: AST) ‑> AST

Expand source code

def parse(self, x: AST) -> AST:
    """
    Parses the given unparsed term, replacing it by nested theory
    functions.

    Parameters
    ----------
    x
        The AST to parse.

    Returns
    -------
    The rewritten AST.
    """
    del self._stack[:]
    del self._terms[:]

    arity = Arity.Unary

    for element in x.elements:
        for operator in element.operators:
            self.check_operator(operator, arity, x.location)

            while arity == Arity.Binary and self._check(operator):
                self._reduce()

            self._stack.append((operator, arity))
            arity = Arity.Unary

        self._terms.append(element.term)
        arity = Arity.Binary

    while self._stack:
        self._reduce()

    return self._terms[0]

Parses the given unparsed term, replacing it by nested theory functions.

Parameters

x

The AST to parse.

Returns

The rewritten AST.