`reify-defined.lp`¶

Adds defined directives for the reification predicates to avoid warnings when using clingo. Check the How to build your own ASP system?! paper for more details on the reification predicates and their semantics.

Predicate Summary ¶

Name	Definition	Type
`atom_tuple/1`	Represents a tuple or set of atoms identified by `H`, without a specified order
`atom_tuple/2`	Atom `A` is part of the atom tuple identified by `H`
`literal_tuple/1`	Represents a tuple or set of literals identified by `B`, without a specified order
`literal_tuple/2`	Literal `L` is part of the literal tuple identified by `B`
`output/2`	Specifies that `O` will be output when the literal tuple `B` is true
`rule/2`	Represents a rule in ASP, with `HEAD` being either a disjunction or choice of atoms, and `BODY` a conjunction of literals
`theory_atom/3`	Represents a theory atom without a guard
`theory_atom/5`	Represents a theory atom with a guard
`theory_function/3`	Represents a theory function symbol
`theory_number/2`	Represents a theory number symbol
`theory_sequence/0`	tuple: Constant atom indicating this is a tuple (function without name)
`theory_string/2`	Represents a theory string symbol
`theory_tuple/1`	Defines a theory tuple
`theory_tuple/3`	Specifies the symbol at a position in a theory tuple
`weighted_literal_tuple/1`	Represents a tuple or set of weighted literals identified by `B`, without a specified order
`weighted_literal_tuple/3`	Literal `L` is part of the literal tuple identified by `B` and has a weight of `W`

Glossary ¶

`atom_tuple(H)` ¶

Represents a tuple or set of atoms identified by H, without a specified order.

Parameter	Description
`H`	Numerical identifier unique within its class.

`atom_tuple(H, A)` ¶

Atom A is part of the atom tuple identified by H.

Parameter	Description
`H`	Numerical identifier for the atom tuple.
`A`	Numerical identifier for the atom.

`literal_tuple(B)` ¶

Represents a tuple or set of literals identified by B, without a specified order. A literal can be an atom or a negated atom.

Parameter	Description
`B`	Numerical identifier unique within its class.

`literal_tuple(B, L)` ¶

Literal L is part of the literal tuple identified by B.

Parameter	Description
`B`	Numerical identifier for the literal tuple.
`L`	Numerical identifier for the literal. It is either `-A` or `A`, where `A` is the atom, and the negative symbol represents negation.

`output(O, B)` ¶

Specifies that O will be output when the literal tuple B is true.

Parameter	Description
`O`	Value to be output.
`B`	Numerical identifier of the literal tuple.

`rule(HEAD, BODY)` ¶

Represents a rule in ASP, with HEAD being either a disjunction or choice of atoms, and BODY a conjunction of literals.

Parameter	Description
`HEAD`	One of the following `disjunction(H)`: Disjunction of atoms. `choice(H)`: Choice among atoms.
`BODY`	One of the following `normal(B)`: Normal body with literals. `sum(B, G)`: Sum body with literals and a threshold.

`theory_atom(ID, ID_STR, ID_ET)` ¶

Represents a theory atom without a guard.

Parameter	Description
`ID`	Unique identifier for the theory atom.
`ID_STR`	Identifier of the theory_string for the atom name.
`ID_ET`	Identifier of the theory_element_tuple for the elements inside the brackets.

`theory_atom(ID, ID_STR, ID_ET, ID_GUARD, ID_SYMBOL)` ¶

Represents a theory atom with a guard.

Parameter	Description
`ID`	Unique identifier for the theory atom.
`ID_STR`	Identifier of the theory_string for the atom name.
`ID_ET`	Identifier of the theory_element_tuple for the elements inside the brackets (left-hand side).
`ID_GUARD`	Identifier of the theory_string for the guard name (e.g., `=`).
`ID_SYMBOL`	Identifier of the theory symbol for the right-hand side of the guard.

`theory_function(ID, ID_STR, ID_TUPLE)` ¶

Represents a theory function symbol.

Parameter	Description
`ID`	Unique identifier for the theory symbol.
`ID_STR`	Identifier of the theory_string for the function name.
`ID_TUPLE`	Identifier of the theory_tuple for the function arguments.

`theory_number(ID, N)` ¶

Represents a theory number symbol.

Parameter	Description
`ID`	Unique identifier for the theory symbol.
`N`	Integer value of the number.

`theory_sequence()` ¶

tuple: Constant atom indicating this is a tuple (function without name). - ID_TUPLE: Identifier of the theory_tuple for the arguments.

`theory_string(ID, STR)` ¶

Represents a theory string symbol.

Parameter	Description
`ID`	Unique identifier for the theory symbol.
`STR`	String value. Used for function names, operators, or string content.

`theory_tuple(ID)` ¶

Defines a theory tuple.

Parameter	Description
`ID`	Unique identifier for the theory tuple.

`theory_tuple(ID, POS, ID_SYMBOL)` ¶

Specifies the symbol at a position in a theory tuple.

Parameter	Description
`ID`	Identifier of the theory tuple.
`POS`	Position index.
`ID_SYMBOL`	Identifier of the theory symbol at this position.

`weighted_literal_tuple(B)` ¶

Represents a tuple or set of weighted literals identified by B, without a specified order.

Parameter	Description
`B`	Numerical identifier for the weighted literal tuple.

`weighted_literal_tuple(B, L, W)` ¶

Literal L is part of the literal tuple identified by B and has a weight of W.

Parameter	Description
`B`	Numerical identifier for the literal tuple.
`L`	Numerical identifier for the literal. It is either `-A` or `A`, where `A` is the atom, and the negative symbol represents negation.
`W`	Weight of the literal.

Examples¶

Example

For the following program

f.lp

{a;b}.
c :- a, not b.
:- b.

The reified output will be:

gringo f.lp --output=reify

atom_tuple(0).                  % at0 := {a,b}
atom_tuple(0,1).                % (a1 := a) in at0
atom_tuple(0,2).                % (a2 := b) in at0
literal_tuple(0).               % lt0 := {} (Literal tuple of arity 0)
rule(choice(0),normal(0)).      % choice(at0) :- and(lt0)   <->   {a;b} :- #true.

atom_tuple(1).                  % at1 := {} (Atom tuple of arity 0)
literal_tuple(1).               % lt1 := {b}
literal_tuple(1,2).             % (a2 := b) in lt1
rule(disjunction(1),normal(1)). % disjunction(at1) :- and(lt1)   <->  #false :- b.

atom_tuple(2).                  % at2 := {c}
atom_tuple(2,3).                % a3 := c in at2
literal_tuple(2).               % lt2 := {a, not b}
literal_tuple(2,-2).            % (a-2 := not b) in lt2
literal_tuple(2,1).             % (a1 := a) in lt2
rule(disjunction(2),normal(2)). % disjunction(at2) :- and(lt2)   <->  c :- a, not b.

literal_tuple(3).               % lt3 := {a}
literal_tuple(3,1).             % (a1 := a) in lt3
output(a,3).                    % Show a if lt3

output(b,1).                    % Show b if lt1

literal_tuple(4).               % lt4 := {b}
literal_tuple(4,3).             % (a3 := c) in lt3
output(c,4).                    % Show c if lt4

reify-defined.lp¶

Predicate Summary ¶

Glossary ¶

atom_tuple(H) ¶

atom_tuple(H, A) ¶

literal_tuple(B) ¶

literal_tuple(B, L) ¶

output(O, B) ¶

rule(HEAD, BODY) ¶

theory_atom(ID, ID_STR, ID_ET) ¶

theory_atom(ID, ID_STR, ID_ET, ID_GUARD, ID_SYMBOL) ¶

theory_function(ID, ID_STR, ID_TUPLE) ¶

theory_number(ID, N) ¶

theory_sequence() ¶

theory_string(ID, STR) ¶

theory_tuple(ID) ¶

theory_tuple(ID, POS, ID_SYMBOL) ¶

weighted_literal_tuple(B) ¶

weighted_literal_tuple(B, L, W) ¶