`clingo` module

The clingo-5.4.0 module.

This module provides functions and classes to control the grounding and solving process.

If the clingo application is build with Python support, clingo will also be able to execute Python code embedded in logic programs. Functions defined in a Python script block are callable during the instantiation process using @-syntax. The default grounding/solving process can be customized if a main function is provided.

Note that gringo's precomputed terms (terms without variables and interpreted functions), called symbols in the following, are wrapped in the Symbol class. Furthermore, strings, numbers, and tuples can be passed wherever a symbol is expected - they are automatically converted into a Symbol object. Functions called during the grounding process from the logic program must either return a symbol or a sequence of symbols. If a sequence is returned, the corresponding @-term is successively substituted by the values in the sequence.

Examples

The first example shows how to use the clingo module from Python.

>>> import clingo
>>> class Context:
...     def id(self, x):
...         return x
...     def seq(self, x, y):
...         return [x, y]
...
>>> def on_model(m):
...     print (m)
...
>>> ctl = clingo.Control()
>>> ctl.add("base", [], """\
... p(@id(10)).
... q(@seq(1,2)).
... """)
>>> ctl.ground([("base", [])], context=Context())
>>> ctl.solve(on_model=on_model)
p(10) q(1) q(2)
SAT

The second example shows how to use Python code from clingo.

#script (python)

import clingo

class Context:
    def id(x):
        return x

    def seq(x, y):
        return [x, y]

def main(prg):
    prg.ground([("base", [])], context=Context())
    prg.solve()

#end.

p(@id(10)).
q(@seq(1,2)).

Overview

Sub-modules

clingo.ast: The clingo.ast-5.4.0 module …

Global variables

var Infimum : Symbol: Represents a symbol of type SymbolType.Infimum.
var Supremum : Symbol: Represents a symbol of type SymbolType.Supremum.
var __version__ : str: Version of the clingo module ('5.4.0').

Functions

def Function(name:str, arguments:List[Symbol]=[], positive:bool=True) -> Symbol

Construct a function symbol.

This includes constants and tuples. Constants have an empty argument list and tuples have an empty name. Functions can represent classically negated atoms. Argument positive has to be set to false to represent such atoms.

Parameters

name : str: The name of the function (empty for tuples).
arguments : List[Symbol] = []: The arguments in form of a list of symbols.
positive : bool = True: The sign of the function (tuples must not have signs).

Returns

Symbol

def Number(number:int) -> Symbol

Construct a numeric symbol given a number.

Parameters

number : int: The given number.

Returns

Symbol

def String(string:str) -> Symbol

Construct a string symbol given a string.

Parameters

string : str: The given string.

Returns

Symbol

def Tuple(arguments:List[Symbol]) -> Symbol

A shortcut for Function("", arguments).

Parameters

arguments : List[Symbol]: The arguments in form of a list of symbols.

Returns

Symbol

Parameters

application : Application: The Application object (see notes).
files : List[str]: The files to pass to the main function of the application.

Returns

int: The exit code of the application.

Notes

The application object must implement a main function and additionally can override the other functions.

class Application(object):
    """
    Interface that has to be implemented to customize clingo.

    Attributes
    ----------
    program_name: str = 'clingo'
        Optional program name to be used in the help output.

    message_limit: int = 20
        Maximum number of messages passed to the logger.
    """

    def main(self, control: Control, files: List[str]) -> None:
        """
        Function to replace clingo's default main function.

        Parameters
        ----------
        control : Control
            The main control object.
        files : List[str]
            The files passed to clingo_main.

        Returns
        -------
        None
        """

    def register_options(self, options: ApplicationOptions) -> None:
        """
        Function to register custom options.

        Parameters
        ----------
        options : ApplicationOptions
            Object to register additional options

        Returns
        -------
        None
        """

    def validate_options(self) -> bool:
        """
        Function to validate custom options.

        This function should return false or throw an exception if option
        validation fails.

        Returns
        -------
        bool
        """

    def logger(self, code: MessageCode, message: str) -> None:
        """
        Function to intercept messages normally printed to standard error.

        By default, messages are printed to stdandard error.

        Parameters
        ----------
        code : MessageCode
            The message code.
        message : str
            The message string.

        Returns
        -------
        None

        Notes
        -----
        This function should not raise exceptions.
        """

Examples

The following example reproduces the default clingo application:

import sys
import clingo

class Application:
    def __init__(self, name):
        self.program_name = name

    def main(self, ctl, files):
        if len(files) > 0:
            for f in files:
                ctl.load(f)
        else:
            ctl.load("-")
        ctl.ground([("base", [])])
        ctl.solve()

clingo.clingo_main(Application(sys.argv[0]), sys.argv[1:])

def parse_program(program:str, callback:Callable[[AST],None]) -> None

Parse the given program and return an abstract syntax tree for each statement via a callback.

Parameters

program : str: String representation of the program.
callback : Callable[[AST], None]: Callback taking an ast as argument.

Returns

None

Parameters

string : str: The string to be parsed.
logger : Callback[[MessageCode,str],None] = None: Function to intercept messages normally printed to standard error.
message_limit : int = 20: Maximum number of messages passed to the logger.

Returns

Symbol

Examples

>>> import clingo
>>> clingo.parse_term('p(1+2)')
p(3)

Classes

class ApplicationOptions

Object to add custom options to a clingo based application.

Methods

def add_flag(self, group:str, option:str, description:str, parser:Callback[[str],bool], multi:bool=False, argument:str=None) -> None

Add an option that is processed with a custom parser.

Parameters

group : str: Options are grouped into sections as given by this string.
option : str: Parameter option specifies the name(s) of the option. For example, "ping,p" adds the short option -p and its long form --ping. It is also possible to associate an option with a help level by adding "@l" to the option specification. Options with a level greater than zero are only shown if the argument to help is greater or equal to l.
description : str: The description of the option shown in the help output.
parser : Callback[[str], bool]: An option parser is a function that takes a string as input and returns true or false depending on whether the option was parsed successively.
multi : bool=False: Whether the option can appear multiple times on the command-line.
argument : str=None: Otional string to change the value name in the generated help.

Returns

None

Raises

RuntimeError: An error is raised if an option with the same name already exists.

Notes

The parser also has to take care of storing the semantic value of the option somewhere.

def add_flag(self, group:str, option:str, description:str, target:Flag) -> None

Add an option that is a simple flag.

This function is similar to ApplicationOptions.add() but simpler because it only supports flags, which do not have values. Note that the target parameter must be of type Flag, which is set to true if the flag is passed on the command line.

Parameters

group : str: Options are grouped into sections as given by this string.
option : str: Same as for ApplicationOptions.add().
description : str: The description of the option shown in the help output.
target : Flag: The object that receives the value.

Returns

None

class Assignment

Object to inspect the (parital) assignment of an associated solver.

Assigns truth values to solver literals. Each solver literal is either true, false, or undefined, represented by the Python constants True, False, or None, respectively.

Instance variables

var decision_level : int: The current decision level.
var has_conflict : bool: True if the assignment is conflicting.
var is_total : bool: Whether the assignment is total.
var max_size : int: The maximum size of the assignment (if all literals are assigned).
var root_level : int: The current root level.
var size : int: The number of assigned literals.

Methods

def decision(self, level:int) -> int

Return the decision literal of the given level.

Parameters

literal : int: The solver literal.

Returns

int

def has_literal(self, literal:int) -> bool

Determine if the given literal is valid in this solver.

Parameters

literal : int: The solver literal.

Returns

bool

def is_false(self, literal:int) -> bool

Determine if the literal is false.

Parameters

literal : int: The solver literal.

Returns

bool

def is_fixed(self, literal:int) -> bool

Determine if the literal is assigned on the top level.

Parameters

literal : int: The solver literal.

Returns

bool

def is_true(self, literal:int) -> bool

Determine if the literal is true.

Parameters

literal : int: The solver literal.

Returns

bool

def level(self, literal:int) -> int

The decision level of the given literal.

Parameters

literal : int: The solver literal.

Returns

int

Notes

Note that the returned value is only meaningful if the literal is assigned - i.e., value(lit) is not None.

def value(self, literal) -> Optional[bool]

Get the truth value of the given literal or None if it has none.

Parameters

literal : int: The solver literal.

Returns

Optional[bool]

class Backend

Backend object providing a low level interface to extend a logic program.

This class allows for adding statements in ASPIF format.

Notes

The Backend is a context manager and must be used with Python's with statement.

Statements added with the backend are added directly to the solver. For example, the grounding component will not be aware if facts were added to a program via the backend. The only exception are atoms added with Backend.add_atom(), which will subsequently be used to instantiate rules. Furthermore, the Control.cleanup() method can be used to transfer information about facts back to the grounder.

Examples

The following example shows how to add a fact to a program and the effect of the Control.cleanup() function:

>>> import clingo
>>> ctl = clingo.Control()
>>> sym_a = clingo.Function("a")
>>> with ctl.backend() as backend:
...     atm_a = backend.add_atom(sym_a)
...     backend.add_rule([atm_a])
...
>>> ctl.symbolic_atoms[sym_a].is_fact
False
>>> ctl.cleanup()
>>> ctl.symbolic_atoms[sym_a].is_fact
True
>>> ctl.solve(on_model=lambda m: print("Answer: {}".format(m)))
Answer: a
SAT

Methods

def add_acyc_edge(self, node_u:int, node_v:int, condition:List[int]) -> None

Add an edge directive to the program.

Parameters

node_u : int: The start node represented as an unsigned integer.
node_v : int: The end node represented as an unsigned integer.
condition : List[int]: List of program literals.

Returns

None

def add_assume(self, literals:List[int]) -> None

Add assumptions to the program.

Parameters

literals : List[int]: The list of literals to assume true.

Returns

None

def add_atom(self, symbol:Optional[Symbol]=None) -> int

Return a fresh program atom or the atom associated with the given symbol.

If the given symbol does not exist in the atom base, it is added first. Such atoms will be used in subequents calls to ground for instantiation.

Parameters

symbol : Optional[Symbol]=None: The symbol associated with the atom.

Returns

int: The program atom representing the atom.

def add_external(self, atom:int, value:TruthValue=TruthValue.False_) -> None

Mark a program atom as external optionally fixing its truth value.

Parameters

atom : int: The program atom to mark as external.
value : TruthValue=TruthValue.False_: Optional truth value.

Returns

None

Notes

Can also be used to release an external atom using TruthValue.Release.

def add_heuristic(self, atom:int, type:HeuristicType, bias:int, priority:int, condition:List[int]) -> None

Add a heuristic directive to the program.

Parameters

atom : int: Program atom to heuristically modify.
type : HeuristicType: The type of modification.
bias : int: A signed integer.
priority : int: An unsigned integer.
condition : List[int]: List of program literals.

Returns

None

def add_minimize(self, priority:int, literals:List[Tuple[int,int]]) -> None

Add a minimize constraint to the program.

Parameters

priority : int: Integer for the priority.
literals : List[Tuple[int,int]]: List of pairs of program literals and weights.

Returns

None

def add_project(self, atoms:List[int]) -> None

Add a project statement to the program.

Parameters

atoms : List[int]: List of program atoms to project on.

Returns

None

def add_rule(self, head:List[int], body:List[int]=[], choice:bool=False) -> None

Add a disjuntive or choice rule to the program.

Parameters

head : List[int]: The program atoms forming the rule head.
body : List[int]=[]: The program literals forming the rule body.
choice : bool=False: Whether to add a disjunctive or choice rule.

Returns

None

Notes

Integrity constraints and normal rules can be added by using an empty or singleton head list, respectively.

def add_weight_rule(self, head:List[int], lower:int, body:List[Tuple[int,int]], choice:bool=False) -> None

Add a disjuntive or choice rule with one weight constraint with a lower bound in the body to the program.

Parameters

head : List[int]: The program atoms forming the rule head.
lower : int: The lower bound.
body : List[Tuple[int,int]]: The pairs of program literals and weights forming the elements of the weight constraint.
choice : bool=False: Whether to add a disjunctive or choice rule.

Returns

None

class Configuration

Allows for changing the configuration of the underlying solver.

Options are organized hierarchically. To change and inspect an option use:

config.group.subgroup.option = "value"
value = config.group.subgroup.option

There are also arrays of option groups that can be accessed using integer indices:

config.group.subgroup[0].option = "value1"
config.group.subgroup[1].option = "value2"

To list the subgroups of an option group, use the Configuration.keys member. Array option groups, like solver, have a non-negative length and can be iterated. Furthermore, there are meta options having key configuration. Assigning a meta option sets a number of related options. To get further information about an option or option group <opt>, use property __desc_<opt> to retrieve a description.

Notes

When integers are assigned to options, they are automatically converted to strings. The value of an option is always a string.

Examples

The following example shows how to modify the configuration to enumerate all models:

>>> import clingo
>>> prg = clingo.Control()
>>> prg.configuration.solve.__desc_models
'Compute at most %A models (0 for all)\n'
>>> prg.configuration.solve.models = 0
>>> prg.add("base", [], "{a;b}.")
>>> prg.ground([("base", [])])
>>> prg.solve(on_model=lambda m: print("Answer: {}".format(m)))
Answer:
Answer: a
Answer: b
Answer: a b
SAT

Instance variables

var keys : Optional[List[str]]: The list of names of sub-option groups or options.

The list is None if the current object is not an option group.

class Control(arguments:List[str]=[], logger:Callback[[MessageCode,str],None]=None, message_limit:int=20)

Control object for the grounding/solving process.

Parameters

arguments : List[str]: Arguments to the grounder and solver.
logger : Callback[[MessageCode,str],None]=None: Function to intercept messages normally printed to standard error.
message_limit : int: The maximum number of messages passed to the logger.

Notes

Note that only gringo options (without --text) and clasp's search options are supported. Furthermore, a Control object is blocked while a search call is active; you must not call any member function during search.

Instance variables

var configuration : Configuration

Configuration object to change the configuration.

var is_conflicting : bool

Whether the internal program representation is conflicting.

If this (read-only) property is true, solve calls return immediately with an unsatisfiable solve result.

Notes

Conflicts first have to be detected, e.g., initial unit propagation results in an empty clause, or later if an empty clause is resolved during solving. Hence, the property might be false even if the problem is unsatisfiable.

var statistics : dict

A dict containing solve statistics of the last solve call.

Notes

The statistics correspond to the --stats output of clingo. The detail of the statistics depends on what level is requested on the command line.

This property is only available in clingo.

Examples

The following example shows how to dump the solving statistics in json format:

>>> import json
>>> import clingo
>>> ctl = clingo.Control()
>>> ctl.add("base", [], "{a}.")
>>> ctl.ground([("base", [])])
>>> ctl.solve()
SAT
>>> print(json.dumps(ctl.statistics['solving'], sort_keys=True, indent=4,
... separators=(',', ': ')))
{
    "solvers": {
        "choices": 1.0,
        "conflicts": 0.0,
        "conflicts_analyzed": 0.0,
        "restarts": 0.0,
        "restarts_last": 0.0
    }
}

var symbolic_atoms : SymbolicAtoms

SymbolicAtoms object to inspect the symbolic atoms.

var theory_atoms : TheoryAtomIter

A TheoryAtomIter object, which can be used to iterate over the theory atoms.

var use_enumeration_assumption : bool

Whether do discard or keep learnt information from enumeration modes.

If the enumeration assumption is enabled, then all information learnt from clasp's various enumeration modes is removed after a solve call. This includes enumeration of cautious or brave consequences, enumeration of answer sets with or without projection, or finding optimal models; as well as clauses added with SolveControl.add_clause().

Notes

Initially the enumeration assumption is enabled.

In general, the enumeration assumption should be enabled whenever there are multiple calls to solve. Otherwise, the behavior of the solver will be unpredictable because there are no guarantees which information exactly is kept. There might be small speed benefits when disabling the enumeration assumption for single shot solving.

Methods

def add(self, name:str, parameters:List[str], program:str) -> None

Extend the logic program with the given non-ground logic program in string form.

Parameters

name : str: The name of program block to add.
parameters : List[str]: The parameters of the program block to add.
program : str: The non-ground program in string form.

Returns

None

Parameters

external : Union[Symbol,int]: A symbol or program literal representing the external atom.
truth : Optional[bool]: A Boolean fixes the external to the respective truth value; and None leaves its truth value open.

Returns

None

Notes

The truth value of an external atom can be changed before each solve call. An atom is treated as external if it has been declared using an #external directive, and has not been released by calling release_external() or defined in a logic program with some rule. If the given atom is not external, then the function has no effect.

For convenience, the truth assigned to atoms over negative program literals is inverted.

def backend(self) -> Backend

Returns a Backend object providing a low level interface to extend a logic program.

Returns

Backend

def builder(self) -> ProgramBuilder

Return a builder to construct a non-ground logic programs.

Returns

ProgramBuilder

Returns

None

Notes

Any atoms falsified are completely removed from the logic program. Hence, a definition for such an atom in a successive step introduces a fresh atom.

def get_const(self, name:str) -> Optional[Symbol]

Return the symbol for a constant definition of form: #const name = symbol.

Parameters

name : str: The name of the constant to retrieve.

Returns

Optional[Symbol]: The function returns None if no matching constant definition exists.

def ground(self, parts:List[Tuple[str,List[Symbol]]], context:Any=None) -> None

Ground the given list of program parts specified by tuples of names and arguments.

Parameters

parts : List[Tuple[str,List[Symbol]]]: List of tuples of program names and program arguments to ground.
context : Any=None: A context object whose methods are called during grounding using the @-syntax (if omitted methods, from the main module are used).

Notes

Note that parts of a logic program without an explicit #program specification are by default put into a program called base without arguments.

Examples

>>> import clingo
>>> ctl = clingo.Control()
>>> ctl.add("p", ["t"], "q(t).")
>>> parts = []
>>> parts.append(("p", [1]))
>>> parts.append(("p", [2]))
>>> ctl.ground(parts)
>>> ctl.solve(on_model=lambda m: print("Answer: {}".format(m)))
Answer: q(1) q(2)
SAT

def interrupt(self) -> None

Interrupt the active solve call.

Returns

None

Notes

This function is thread-safe and can be called from a signal handler. If no search is active, the subsequent call to Control.solve() is interrupted. The result of the Control.solve() method can be used to query if the search was interrupted.

def load(self, path:str) -> None

Extend the logic program with a (non-ground) logic program in a file.

Parameters

path : str: The path of the file to load.

Returns

None

def register_observer(self, observer:Observer, replace:bool=False) -> None

Registers the given observer to inspect the produced grounding.

Parameters

observer : Observer: The observer to register. See below for a description of the requirede interface.
replace : bool=False: If set to true, the output is just passed to the observer and nolonger to the underlying solver (or any previously registered observers).

Returns

None

Notes

An observer should be a class of the form below. Not all functions have to be implemented and can be omitted if not needed.

class Observer:
    def init_program(self, incremental: bool) -> None:
        """
        Called once in the beginning.

        Parameters
        ----------
        incremental : bool
            Whether the program is incremental. If the incremental flag is
            true, there can be multiple calls to `Control.solve`.

        Returns
        -------
        None
        """

    def begin_step(self) -> None:
        """
        Marks the beginning of a block of directives passed to the solver.

        Returns
        -------
        None
        """

    def rule(self, choice: bool, head: List[int], body: List[int]) -> None:
        """
        Observe rules passed to the solver.

        Parameters
        ----------
        choice : bool
            Determines if the head is a choice or a disjunction.
        head : List[int]
            List of program atoms forming the rule head.
        body : List[int]
            List of program literals forming the rule body.

        Returns
        -------
        None
        """

    def weight_rule(self, choice: bool, head: List[int], lower_bound: int,
                    body: List[Tuple[int,int]]) -> None:
        """
        Observe rules with one weight constraint in the body passed to the
        solver.

        Parameters
        ----------
        choice : bool
            Determines if the head is a choice or a disjunction.
        head : List[int]
            List of program atoms forming the head of the rule.
        lower_bound:
            The lower bound of the weight constraint in the rule body.
        body : List[Tuple[int,int]]
            List of weighted literals (pairs of literal and weight) forming the
            elements of the weight constraint.

        Returns
        -------
        None
        """

    def minimize(self, priority: int, literals: List[Tuple[int,int]]) -> None:
        """
        Observe minimize directives (or weak constraints) passed to the
        solver.

        Parameters
        ----------
        priority : int
            The priority of the directive.
        literals : List[Tuple[int,int]]
            List of weighted literals whose sum to minimize (pairs of literal
            and weight).

        Returns
        -------
        None
        """

    def project(self, atoms: List[int]) -> None:
        """
        Observe projection directives passed to the solver.

        Parameters
        ----------
        atoms : List[int]
            The program atoms to project on.

        Returns
        -------
        None
        """

    def output_atom(self, symbol: Symbol, atom: int) -> None:
        """
        Observe shown atoms passed to the solver.  Facts do not have an
        associated program atom. The value of the atom is set to zero.

        Parameters
        ----------
        symbol : Symbolic
            The symbolic representation of the atom.
        atom : int
            The associated program atom (0 for facts).

        Returns
        -------
        None
        """

    def output_term(self, symbol: Symbol, condition: List[int]) -> None:
        """
        Observe shown terms passed to the solver.

        Parameters
        ----------
        symbol : Symbol
            The symbolic representation of the term.
        condition : List[int]
            List of program literals forming the condition when to show the
            term.

        Returns
        -------
        None
        """

    def output_csp(self, symbol: Symbol, value: int,
                   condition: List[int]) -> None:
        """
        Observe shown csp variables passed to the solver.

        Parameters
        ----------
        symbol : Symbol
            The symbolic representation of the variable.
        value : int
            The integer value of the variable.
        condition : List[int]
            List of program literals forming the condition when to show the
            variable with its value.

        Returns
        -------
        None
        """

    def external(self, atom: int, value: TruthValue) -> None:
        """
        Observe external statements passed to the solver.

        Parameters
        ----------
        atom : int
            The external atom in form of a program literal.
        value : TruthValue
            The truth value of the external statement.

        Returns
        -------
        None
        """

    def assume(self, literals: List[int]) -> None:
        """
        Observe assumption directives passed to the solver.

        Parameters
        ----------
        literals : List[int]
            The program literals to assume (positive literals are true and
            negative literals false for the next solve call).

        Returns
        -------
        None
        """

    def heuristic(self, atom: int, type: HeuristicType, bias: int,
                  priority: int, condition: List[int]) -> None:
        """
        Observe heuristic directives passed to the solver.

        Parameters
        ----------
        atom : int
            The program atom heuristically modified.
        type : HeuristicType
            The type of the modification.
        bias : int
            A signed integer.
        priority : int
            An unsigned integer.
        condition : List[int]
            List of program literals.

        Returns
        -------
        None
        """

    def acyc_edge(self, node_u: int, node_v: int,
                  condition: List[int]) -> None:
        """
        Observe edge directives passed to the solver.

        Parameters
        ----------
        node_u : int
            The start vertex of the edge (in form of an integer).
        node_v : int
            Тhe end vertex of the edge (in form of an integer).
        condition : List[int]
            The list of program literals forming th condition under which to
            add the edge.

        Returns
        -------
        None
        """

    def theory_term_number(self, term_id: int, number: int) -> None:
        """
        Observe numeric theory terms.

        Parameters
        ----------
        term_id : int
            The id of the term.
        number : int
            The value of the term.

        Returns
        -------
        None
        """

    def theory_term_string(self, term_id : int, name : str) -> None:
        """
        Observe string theory terms.

        Parameters
        ----------
        term_id : int
            The id of the term.
        name : str
            The string value of the term.

        Returns
        -------
        None
        """

    def theory_term_compound(self, term_id: int, name_id_or_type: int,
                             arguments: List[int]) -> None:
        """
        Observe compound theory terms.

        Parameters
        ----------
        term_id : int
            The id of the term.
        name_id_or_type : int
            The name or type of the term where
            - if it is -1, then it is a tuple
            - if it is -2, then it is a set
            - if it is -3, then it is a list
            - otherwise, it is a function and name_id_or_type refers to the id
            of the name (in form of a string term)
        arguments : List[int]
            The arguments of the term in form of a list of term ids.

        Returns
        -------
        None
        """

    def theory_element(self, element_id: int, terms: List[int],
                       condition: List[int]) -> None:
        """
        Observe theory elements.

        Parameters
        ----------
        element_id : int
            The id of the element.
        terms : List[int]
            The term tuple of the element in form of a list of term ids.
        condition : List[int]
            The list of program literals forming the condition.

        Returns
        -------
        None
        """

    def theory_atom(self, atom_id_or_zero: int, term_id: int,
                    elements: List[int]) -> None:
        """
        Observe theory atoms without guard.

        Parameters
        ----------
        atom_id_or_zero : int
            The id of the atom or zero for directives.
        term_id : int
            The term associated with the atom.
        elements : List[int]
            The elements of the atom in form of a list of element ids.

        Returns
        -------
        None
        """

    def theory_atom_with_guard(self, atom_id_or_zero: int, term_id: int,
                               elements: List[int], operator_id: int,
                               right_hand_side_id: int) -> None:
        """
        Observe theory atoms with guard.

        Parameters
        ----------
        atom_id_or_zero : int
            The id of the atom or zero for directives.
        term_id : int
            The term associated with the atom.
        elements : List[int]
            The elements of the atom in form of a list of element ids.
        operator_id : int
            The id of the operator (a string term).
        right_hand_side_id : int
            The id of the term on the right hand side of the atom.

        Returns
        -------
        None
        """

    def end_step(self) -> None:
        """
        Marks the end of a block of directives passed to the solver.

        This function is called right before solving starts.

        Returns
        -------
        None
        """

def register_propagator(self, propagator:Propagator) -> None

Registers the given propagator with all solvers.

Parameters

propagator : Propagator: The propagator to register.

Returns

None

Notes

Each symbolic or theory atom is uniquely associated with a positive program atom in form of a positive integer. Program literals additionally have a sign to represent default negation. Furthermore, there are non-zero integer solver literals. There is a surjective mapping from program atoms to solver literals.

All methods called during propagation use solver literals whereas SymbolicAtom.literal and TheoryAtom.literal return program literals. The function PropagateInit.solver_literal() can be used to map program literals or condition ids to solver literals.

A propagator should be a class of the form below. Not all functions have to be implemented and can be omitted if not needed.

class Propagator:
    def init(self, init: PropagateInit) -> None:
        """
        This function is called once before each solving step.

        It is used to map relevant program literals to solver literals, add
        watches for solver literals, and initialize the data structures used
        during propagation.

        Parameters
        ----------
        init : PropagateInit
            Object to initialize the propagator.

        Returns
        -------
        None

        Notes
        -----
        This is the last point to access theory atoms.  Once the search has
        started, they are no longer accessible.
        """

    def propagate(self, control: PropagateControl, changes: List[int]) -> None:
        """
        Can be used to propagate solver literals given a partial assignment.

        Parameters
        ----------
        control : PropagateControl
            Object to control propagation.
        changes : List[int]
            List of watched solver literals assigned to true.

        Returns
        -------
        None

        Notes
        -----
        Called during propagation with a non-empty list of watched solver
        literals that have been assigned to true since the last call to either
        propagate, undo, (or the start of the search) - the change set. Only
        watched solver literals are contained in the change set. Each literal
        in the change set is true w.r.t. the current Assignment.
        `PropagateControl.add_clause` can be used to add clauses. If a clause
        is unit resulting, it can be propagated using
        `PropagateControl.propagate`. If either of the two methods returns
        False, the propagate function must return immediately.

            c = ...
            if not control.add_clause(c) or not control.propagate(c):
                return

        Note that this function can be called from different solving threads.
        Each thread has its own assignment and id, which can be obtained using
        `PropagateControl.id`.
        """

    def undo(self, thread_id: int, assignment: Assignment,
             changes: List[int]) -> None:
        """
        Called whenever a solver with the given id undos assignments to watched
        solver literals.

        Parameters
        ----------
        thread_id : int
            The solver thread id.
        assignment : Assignment
            Object for inspecting the partial assignment of the solver.
        changes : List[int]
            The list of watched solver literals whose assignment is undone.

        Returns
        -------
        None

        Notes
        -----
        This function is meant to update assignment dependent state in a
        propagator but not to modify the current state of the solver.
        """

    def check(self, control: PropagateControl) -> None:
        """
        This function is similar to propagate but is called without a change
        set on propagation fixpoints.

        When exactly this function is called, can be configured using the @ref
        PropagateInit.check_mode property.

        Parameters
        ----------
        control : PropagateControl
            Object to control propagation.

        Returns
        -------
        None

        Notes
        -----
        This function is called even if no watches have been added.
        """

    def decide(self, thread_id: int, assignment: Assignment, fallback: int) -> int:
        """
        This function allows a propagator to implement domain-specific
        heuristics.

        It is called whenever propagation reaches a fixed point.

        Parameters
        ----------
        thread_id : int
            The solver thread id.
        assignment : Assignment
            Object for inspecting the partial assignment of the solver.
        fallback : int
            The literal choosen by the solver's heuristic.

        Returns
        -------
        int
            Тhe next solver literal to make true.

        Notes
        -----
        This function should return a free solver literal that is to be
        assigned true. In case multiple propagators are registered, this
        function can return 0 to let a propagator registered later make a
        decision. If all propagators return 0, then the fallback literal is
        used.
        """

def release_external(self, symbol:Union[Symbol,int]) -> None

Release an external atom represented by the given symbol or program literal.

This function causes the corresponding atom to become permanently false if there is no definition for the atom in the program. Otherwise, the function has no effect.

Parameters

symbol : Union[Symbol,int]: The symbolic atom or program atom to release.

Returns

None

Notes

If the program literal is negative, the corresponding atom is released.

Examples

The following example shows the effect of assigning and releasing and external atom.

>>> import clingo
>>> ctl = clingo.Control()
>>> ctl.add("base", [], "a. #external b.")
>>> ctl.ground([("base", [])])
>>> ctl.assign_external(clingo.Function("b"), True)
>>> ctl.solve(on_model=lambda m: print("Answer: {}".format(m)))
Answer: b a
SAT
>>> ctl.release_external(clingo.Function("b"))
>>> ctl.solve(on_model=lambda m: print("Answer: {}".format(m)))
Answer: a
SAT

def solve(self, assumptions:List[Union[Tuple[Symbol,bool],int]]=[], on_model:Callback[[Model],Optional[bool]]=None, on_statistics:Callback[[StatisticsMap,StatisticsMap],None]=None, on_finish:Callback[[SolveResult],None]=None, yield_:bool=False, async_:bool=False) -> Union[SolveHandle,SolveResult]

Starts a search.

Parameters

assumptions : List[Union[Tuple[Symbol,bool],int]]=[]: List of (atom, boolean) tuples or program literals that serve as assumptions for the solve call, e.g., solving under assumptions [(Function("a"), True)] only admits answer sets that contain atom a.
on_model : Callback[[Model],Optional[bool]]=None: Optional callback for intercepting models. A Model object is passed to the callback. The search can be interruped from the model callback by returning False.
on_statistics : Callback[[StatisticsMap,StatisticsMap],None]=None: Optional callback to update statistics. The step and accumulated statistics are passed as arguments.
on_finish : Callback[[SolveResult],None]=None: Optional callback called once search has finished. A SolveResult also indicating whether the solve call has been intrrupted is passed to the callback.
yield_ : bool=False: The resulting SolveHandle is iterable yielding Model objects.
async_ : bool=False: The solve call and the method SolveHandle.resume() of the returned handle are non-blocking.

Returns

Union[SolveHandle,SolveResult]: The return value depends on the parameters. If either yield_ or async_ is true, then a handle is returned. Otherwise, a SolveResult is returned.

Notes

If neither yield_ nor async_ is set, the function returns a SolveResult right away.

Note that in gringo or in clingo with lparse or text output enabled this function just grounds and returns a SolveResult where SolveResult.unknown is true.

If this function is used in embedded Python code, you might want to start clingo using the --outf=3 option to disable all output from clingo.

Note that asynchronous solving is only available in clingo with thread support enabled. Furthermore, the on_model and on_finish callbacks are called from another thread. To ensure that the methods can be called, make sure to not use any functions that block Python's GIL indefinitely.

This function as well as blocking functions on the SolveHandle release the GIL but are not thread-safe.

Examples

The following example shows how to intercept models with a callback:

>>> import clingo
>>> ctl = clingo.Control("0")
>>> ctl.add("p", [], "1 { a; b } 1.")
>>> ctl.ground([("p", [])])
>>> ctl.solve(on_model=lambda m: print("Answer: {}".format(m)))
Answer: a
Answer: b
SAT

The following example shows how to yield models:

>>> import clingo
>>> ctl = clingo.Control("0")
>>> ctl.add("p", [], "1 { a; b } 1.")
>>> ctl.ground([("p", [])])
>>> with ctl.solve(yield_=True) as handle:
...     for m in handle: print("Answer: {}".format(m))
...     handle.get()
...
Answer: a
Answer: b
SAT

The following example shows how to solve asynchronously:

>>> import clingo
>>> ctl = clingo.Control("0")
>>> ctl.add("p", [], "1 { a; b } 1.")
>>> ctl.ground([("p", [])])
>>> with ctl.solve(on_model=lambda m: print("Answer: {}".format(m)), async_=True) as handle:
...     while not handle.wait(0): pass
...     handle.get()
...
Answer: a
Answer: b
SAT

class Flag(value:bool=False)

Helper object to parse command-line flags.

Parameters

value : bool=False: The initial value of the flag.

Instance variables

var value : bool: The value of the flag.

class HeuristicType

Enumeration of the different heuristic types.

HeuristicType objects have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Furthermore, they cannot be constructed from Python. Instead the following preconstructed class attributes are available:

Attributes

Level : HeuristicType: Heuristic modification to set the level of an atom.
Sign : HeuristicType: Heuristic modification to set the sign of an atom.
Factor : HeuristicType: Heuristic modification to set the decaying factor of an atom.
Init : HeuristicType: Heuristic modification to set the inital score of an atom.
True_ : HeuristicType: Heuristic modification to make an atom true.
False_ : HeuristicType: Heuristic modification to make an atom false.

Class variables

var Factor
var False_
var Init
var Level
var Sign
var True_

class MessageCode

Enumeration of the different types of messages.

MessageCode objects have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Furthermore, they cannot be constructed from Python. Instead the following preconstructed class attributes are available:

Attributes

OperationUndefined : MessageCode: Inform about an undefined arithmetic operation or unsupported weight of an aggregate.
RuntimeError : MessageCode: To report multiple errors; a corresponding runtime error is raised later.
AtomUndefined : MessageCode: Informs about an undefined atom in program.
FileIncluded : MessageCode: Indicates that the same file was included multiple times.
VariableUnbounded : MessageCode: Informs about a CSP variable with an unbounded domain.
GlobalVariable : MessageCode: Informs about a global variable in a tuple of an aggregate element.
Other : MessageCode: Reports other kinds of messages.

Class variables

var AtomUndefined
var FileIncluded
var GlobalVariable
var OperationUndefined
var Other
var RuntimeError
var VariableUnbounded

class Model

Provides access to a model during a solve call and provides a SolveContext object to provided limited support to influence the running search.

Notes

The string representation of a model object is similar to the output of models by clingo using the default output.

Model objects cannot be constructed from Python. Instead they are obained during solving (see Control.solve()). Furthermore, the lifetime of a model object is limited to the scope of the callback it was passed to or until the search for the next model is started. They must not be stored for later use.

Examples

The following example shows how to store atoms in a model for usage after solving:

>>> import clingo
>>> ctl = clingo.Control()
>>> ctl.add("base", [], "{a;b}.")
>>> ctl.ground([("base", [])])
>>> ctl.configuration.solve.models="0"
>>> models = []
>>> with ctl.solve(yield_=True) as handle:
...     for model in handle:
...         models.append(model.symbols(atoms=True))
...
>>> sorted(models)
[[], [a], [a, b], [b]]

Instance variables

var context : SolveControl: Object that allows for controlling the running search.
var cost : List[int]: Return the list of integer cost values of the model.

The return values correspond to clasp's cost output.
var number : int: The running number of the model.
var optimality_proven : bool: Whether the optimality of the model has been proven.
var thread_id : int: The id of the thread which found the model.
var type : ModelType: The type of the model.

Methods

def contains(self, atom:Symbol) -> bool

Efficiently check if an atom is contained in the model.

Parameters

atom : Symbol: The atom to lookup.

Returns

bool: Whether the given atom is contained in the model.

Notes

The atom must be represented using a function symbol.

def extend(self, symbols:List[Symbol]) -> None

Extend a model with the given symbols.

Parameters

symbols : List[Symbol]: The symbols to add to the model.

Returns

None

Notes

This only has an effect if there is an underlying clingo application, which will print the added symbols.

def is_true(self, literal:int) -> bool

Check if the given program literal is true.

Parameters

literal : int: The given program literal.

Returns

bool: Whether the given program literal is true.

def symbols(self, atoms:bool=False, terms:bool=False, shown:bool=False, csp:bool=False, complement:bool=False) -> List[Symbol]

Return the list of atoms, terms, or CSP assignments in the model.

Parameters

atoms : bool=False: Select all atoms in the model (independent of #show statements).
terms : bool=False: Select all terms displayed with #show statements in the model.
shown : bool: Select all atoms and terms as outputted by clingo.
csp : bool: Select all csp assignments (independent of #show statements).
complement : bool: Return the complement of the answer set w.r.t. to the atoms known to the grounder. (Does not affect csp assignments.)

Returns

List[Symbol]: The selected symbols.

Notes

Atoms are represented using functions (Symbol objects), and CSP assignments are represented using functions with name "$" where the first argument is the name of the CSP variable and the second its value.

class ModelType

Enumeration of the different types of models.

ModelType objects have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Furthermore, they cannot be constructed from Python. Instead the following preconstructed class attributes are available:

Attributes

StableModel : ModelType: The model captures a stable model.
BraveConsequences : ModelType: The model stores the set of brave consequences.
CautiousConsequences : ModelType: The model stores the set of cautious consequences.

Class variables

var BraveConsequences
var CautiousConsequences
var StableModel

class ProgramBuilder

Object to build non-ground programs.

Notes

A ProgramBuilder is a context manager and must be used with Python's with statement.

Examples

The following example parses a program from a string and passes the resulting AST to the builder:

>>> import clingo
>>> ctl = clingo.Control()
>>> prg = "a."
>>> with ctl.builder() as bld:
...    clingo.parse_program(prg, lambda stm: bld.add(stm))
...
>>> ctl.ground([("base", [])])
>>> ctl.solve(on_model=lambda m: print("Answer: {}".format(m)))
Answer: a
SAT

Methods

def add(self, statement:AST) -> None

Adds a statement in form of an AST node to the program.

Parameters

statement : AST: The statement to add.

Returns

None

class PropagateControl

This object can be used to add clauses and to propagate them.

Parameters

clause : List[int]: List of solver literals forming the clause.
tag : bool=False: If true, the clause applies only in the current solving step.
lock : bool=False: If true, exclude clause from the solver's regular clause deletion policy.

Returns

bool: This method returns false if the current propagation must be stopped.

def add_literal(self) -> int

Adds a new positive volatile literal to the underlying solver thread.

The literal is only valid within the current solving step and solver thread. All volatile literals and clauses involving a volatile literal are deleted after the current search.

Returns

int: The added solver literal.

def add_nogood(self, clause:List[int], tag:bool=False, lock:bool=False) -> bool

Equivalent to self.add_clause([-lit for lit in clause], tag, lock).

def add_watch(self, literal:int) -> None

Add a watch for the solver literal in the given phase.

Parameters

literal : int: The target solver literal.

Returns

None

Notes

Unlike PropagateInit.add_watch() this does not add a watch to all solver threads but just the current one.

def has_watch(self, literal:int) -> bool

Check whether a literal is watched in the current solver thread.

Parameters

literal : int: The target solver literal.

Returns

bool: Whether the literal is watched.

def propagate(self) -> bool

Propagate literals implied by added clauses.

Returns

bool: This method returns false if the current propagation must be stopped.

def remove_watch(self, literal:int) -> None

Removes the watch (if any) for the given solver literal.

Parameters

literal : int: The target solver literal.

Returns

None

class PropagateInit

Object that is used to initialize a propagator before each solving step.

Parameters

clause : List[int]: The clause over solver literals to add.

Returns

bool: Returns false if the clause is conflicting.

def add_watch(self, literal:int, thread_id:Optional[int]=None) -> None

Add a watch for the solver literal in the given phase.

Parameters

literal : int: The solver literal to watch.
thread_id : Optional[int]: The id of the thread to watch the literal. If the is None then all active threads will watch the literal.

Returns

None

def solver_literal(self, literal:int) -> int

Maps the given program literal or condition id to its solver literal.

Parameters

literal : int: A program literal or condition id.

Returns

int: A solver literal.

class PropagatorCheckMode

Enumeration of supported check modes for propagators.

PropagatorCheckMode objects have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Furthermore, they cannot be constructed from Python. Instead the following preconstructed class attributes are available:

Attributes

Off : PropagatorCheckMode: Do not call Propagator.check at all.
Total : PropagatorCheckMode: Call Propagator.check on total assignments.
Fixpoint : PropagatorCheckMode: Call Propagator.check on propagation fixpoints.

Class variables

var Fixpoint
var Off
var Total

class SolveControl

Object that allows for controlling a running search.

SolveControl objects cannot be constructed from Python. Instead they are available via Model.context.

Instance variables

var symbolic_atoms : SymbolicAtoms: SymbolicAtoms object to inspect the symbolic atoms.

Methods

def add_clause(self, literals:List[Union[Tuple[Symbol,bool],int]]) -> None

Add a clause that applies to the current solving step during the search.

Parameters

literals : List[Union[Tuple[Symbol,bool],int]]: List of literals either represented as pairs of symbolic atoms and Booleans or as program literals.

Notes

This function can only be called in a model callback or while iterating when using a SolveHandle.

def add_nogood(self, literals:List[Union[Tuple[Symbol,bool],int]]) -> None

Equivalent to SolveControl.add_clause() with the literals inverted.

class SolveHandle

Handle for solve calls.

SolveHandle objects cannot be created from Python. Instead they are returned by Control.solve(). They can be used to control solving, like, retrieving models or cancelling a search.

Notes

A SolveHandle is a context manager and must be used with Python's with statement.

Blocking functions in this object release the GIL. They are not thread-safe though.

Methods

def cancel(self) -> None

Cancel the running search.

Returns

None

Returns

SolveResult

def resume(self) -> None

Discards the last model and starts searching for the next one.

Notes

If the search has been started asynchronously, this function also starts the search in the background. A model that was not yet retrieved by calling __next__ is not discared.

def wait(self, timeout:Optional[float]=None) -> Optional[bool]

Wait for solve call to finish with an optional timeout.

Parameters

timeout : Optional[float]=None: If a timeout is given, the function blocks for at most timeout seconds.

Returns

Optional[bool]: If a timout is given, returns a Boolean indicating whether the search has finished. Otherwise, the function blocks until the search is finished and returns nothing.

class SolveResult

Captures the result of a solve call.

SolveResult objects cannot be constructed from Python. Instead they are returned by the solve methods of the Control object.

Instance variables

var exhausted : bool: True if the search space was exhausted.
var interrupted : bool: True if the search was interrupted.
var satisfiable : Optional[bool]: True if the problem is satisfiable, False if the problem is unsatisfiable, or None if the satisfiablity is not known.
var unknown : bool: True if the satisfiablity is not known.

This is equivalent to satisfiable is None.
var unsatisfiable : Optional[bool]: True if the problem is unsatisfiable, false if the problem is satisfiable, or None if the satisfiablity is not known.

class StatisticsArray

Object to modify statistics stored in an array.

This class implements Sequence[Union[StatisticsArray,StatisticsMap,float]] but only supports inplace concatenation and does not support deletion.

Notes

The StatisticsArray.update() function provides convenient means to initialize and modify a statistics array.

Methods

def append(self, value:Any) -> None

Append a value.

Parameters

value : Any: A nested structure composed of floats, sequences, and mappings.

Returns

None

def extend(self, values:Sequence[Any]) -> None

Extend the statistics array with the given values.

Paremeters

values : Sequence[Any]: A sequence of nested structures composed of floats, sequences, and mappings.

Returns

None

Parameters

values : Sequence[Any]: A sequence of nested structures composed of floats, callable, sequences, and mappings. A callable can be used to update an existing value, it receives the previous numeric value (or None if absent) as argument and must return an updated numeric value.

Returns

None

class StatisticsMap

Object to capture statistics stored in a map.

This class implements Mapping[str,Union[StatisticsArray,StatisticsMap,float]] but does not support item deletion.

Notes

The StatisticsMap.update() function provides convenient means to initialize and modify a statistics map.

Methods

def items(self) -> List[Tuple[str,Union[StatisticsArray,StatisticsMap,float]]]

Return the items of the map.

Returns

List[Tuple[str, Union[StatisticsArray,StatisticsMap,float]]]: The items of the map.

def keys(self) -> List[str]

Return the keys of the map.

Returns

List[str]: The keys of the map.

def update(self, values:Mappping[str,Any]) -> None

Update the map with the given values.

Parameters

values : Mapping[Any]: A mapping of nested structures composed of floats, callable, sequences, and mappings. A callable can be used to update an existing value, it receives the previous numeric value (or None if absent) as argument and must return an updated numeric value.

Returns

None

def values(self) -> List[Union[StatisticsArray,StatisticsMap,float]]

Return the values of the map.

Returns

List[Union[StatisticsArray,StatisticsMap,float]]: The values of the map.

class Symbol

Represents a gringo symbol.

This includes numbers, strings, functions (including constants with len(arguments) == 0 and tuples with len(name) == 0), #inf and #sup.

Symbol objects implemente Python's rich comparison operators and are ordered like in gringo. They can also be used as keys in dictionaries. Their string representation corresponds to their gringo representation.

Notes

Note that this class does not have a constructor. Instead there are the functions Number(), String(), and Function() to construct symbol objects or the preconstructed symbols Infimum and Supremum.

Instance variables

var arguments : List[Symbol]: The arguments of a function.
var name : str: The name of a function.
var negative : bool: The inverted sign of a function.
var number : int: The value of a number.
var positive : bool: The sign of a function.
var string : str: The value of a string.
var type : SymbolType: The type of the symbol.

Methods

def match(self, name:str, arity:int) -> bool

Check if this is a function symbol with the given signature.

Parameters

name : str: The name of the function.
arity : int: The arity of the function.

Returns

bool: Whether the function matches.

class SymbolType

Enumeration of the different types of symbols.

SymbolType objects have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Furthermore, they cannot be constructed from Python. Instead the following preconstructed objects are available:

Attributes

Number : SymbolType: A numeric symbol, e.g., 1.
String : SymbolType: A string symbol, e.g., "a".
Function : SymbolType: A function symbol, e.g., c, (1, "a"), or f(1,"a").
Infimum : SymbolType: The #inf symbol.
Supremum : SymbolType: The #sup symbol

Class variables

var Function
var Infimum
var Number
var String
var Supremum

class SymbolicAtom

Captures a symbolic atom and provides properties to inspect its state.

Instance variables

var is_external : bool: Whether the atom is an external atom.
var is_fact : bool: Whether the atom is a fact.
var literal : int: The program literal associated with the atom.
var symbol : Symbol: The representation of the atom in form of a symbol.

Methods

def match(self, name:str, arity:int) -> bool

Check if the atom matches the given signature.

Parameters

name : str: The name of the function.
arity : int: The arity of the function.

Returns

bool: Whether the function matches.

Examples

>>> import clingo
>>> prg = clingo.Control()
>>> prg.add('base', [], '''\
... p(1).
... { p(3) }.
... #external p(1..3).
...
... q(X) :- p(X).
... ''')
>>> prg.ground([("base", [])])
>>> len(prg.symbolic_atoms)
6
>>> prg.symbolic_atoms[clingo.Function("p", [2])] is not None
True
>>> prg.symbolic_atoms[clingo.Function("p", [4])] is None
True
>>> prg.symbolic_atoms.signatures
[('p', 1L, True), ('q', 1L, True)]
>>> [(x.symbol, x.is_fact, x.is_external)
...  for x in prg.symbolic_atoms.by_signature("p", 1)]
[(p(1), True, False), (p(3), False, False), (p(2), False, True)]

Instance variables

var signatures : List[Tuple[str,int,bool]]: The list of predicate signatures occurring in the program.

The Boolean indicates the sign of the signature.

Methods

def by_signature(self, name:str, arity:int, positive:bool=True) -> Iterator[Symbol]

Return an iterator over the symbolic atoms with the given signature.

Arguments

name : str: The name of the signature.
arity : int: The arity of the signature.
positive : bool=True: The sign of the signature.

Returns

Iterator[Symbol]

class TheoryAtom

Class to represent theory atoms.

Theory atoms have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Instance variables

var elements : List[TheoryElement]: The elements of the atom.
var guard : Tuple[str,TheoryTerm]: The guard of the atom or None if the atom has no guard.
var literal : int: The program literal associated with the atom.
var term : TheoryTerm: The term of the atom.

class TheoryAtomIter

Implements Iterator[SymbolicAtom].

class TheoryElement

Class to represent theory elements.

Theory elements have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Instance variables

var condition : List[TheoryTerm]: The condition of the element.
var condition_id : int: Each condition has an id. This id can be passed to PropagateInit.solver_literal() to obtain a solver literal equivalent to the condition.
var terms : List[TheoryTerm]: The tuple of the element.

class TheoryTerm

TheoryTerm objects represent theory terms.

Theory terms have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Instance variables

var arguments : List[Symbol]: The arguments of the term (for functions, tuples, list, and sets).
var name : str: The name of the term (for symbols and functions).
var number : int: The numeric representation of the term (for numbers).
var type : TheoryTermType: The type of the theory term.

class TheoryTermType

Enumeration of the different types of theory terms.

TheoryTermType objects have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Furthermore, they cannot be constructed from Python. Instead the following preconstructed objects are available:

Attributes

Function : TheoryTermType: For a function theory terms.
Number : TheoryTermType: For numeric theory terms.
Symbol : TheoryTermType: For symbolic theory terms.
List : TheoryTermType: For list theory terms.
Tuple : TheoryTermType: For tuple theory terms.
Set : TheoryTermType: For set theory terms.

Class variables

var Function
var List
var Number
var Set
var Symbol
var Tuple

class TruthValue

Enumeration of the different truth values.

TruthValue objects have a readable string representation, implement Python's rich comparison operators, and can be used as dictionary keys.

Furthermore, they cannot be constructed from Python. Instead the following preconstructed class attributes are available:

Attributes

True_ : TruthValue: Represents truth value true.
False_ : TruthValue: Represents truth value true.
Free : TruthValue: Represents absence of a truth value.
Release : TruthValue: Indicates that an atom is to be released.

Class variables

var False_
var Free
var Release
var True_

Examples

Overview

Sub-modules

Global variables

Functions

Parameters

Returns

Parameters

Returns

Parameters

Returns

Parameters

Returns

See Also

Parameters

Returns

Notes

Examples

Parameters

Returns

See Also

Parameters

Returns

Examples

Classes

Methods

Parameters

Returns

Raises

Notes

Parameters

Returns

Instance variables

Methods

Parameters

Returns

Parameters

Returns

Parameters

Returns

Parameters

Returns

Parameters

Returns

Parameters

Returns

Notes

Parameters

Returns

See Also

Notes

Examples

Methods

Parameters

Returns

Parameters

Returns

Parameters

Returns

Parameters

Returns

Notes

Parameters

Returns

Parameters

Returns

Parameters

Returns

Parameters

Returns

Notes

Parameters

Returns

Notes

Examples

Instance variables

Parameters

Notes

Instance variables

Notes