Clingo
Loading...
Searching...
No Matches
Clingo::TheoryBackend Class Reference

Theory backend to build theory atoms. More...

#include <backend.hh>

Inheritance diagram for Clingo::TheoryBackend:
Clingo::ProgramBackend

Public Member Functions

auto number (int number) const -> ProgramId
 Add a numeric theory term.
 
auto string (std::string_view string) const -> ProgramId
 Add a string theory term.
 
auto symbol (Symbol const &symbol) const -> ProgramId
 Convert the given symbol into a theory term.
 
auto sequence (TheorySequenceType type, ProgramIdSpan elements) const -> ProgramId
 Add a theory term sequence.
 
auto function (std::string_view name, ProgramIdSpan elements) const -> ProgramId
 Add a theory function.
 
auto element (ProgramIdSpan tuple, ProgramLiteralSpan condition) const -> ProgramId
 Add a theory element.
 
auto atom (std::optional< ProgramAtom > atom, Symbol const &name, ProgramIdSpan elements={}, std::optional< std::pair< std::string_view, ProgramId > > const &guard=std::nullopt) const -> ProgramAtom
 Add a theory atom.
 

Friends

class ProgramBackend
 

Detailed Description

Theory backend to build theory atoms.

Member Function Documentation

◆ atom()

auto Clingo::TheoryBackend::atom ( std::optional< ProgramAtom atom,
Symbol const name,
ProgramIdSpan  elements = {},
std::optional< std::pair< std::string_view, ProgramId > > const guard = std::nullopt 
) const -> ProgramAtom
inline

Add a theory atom.

If an equivalent theory atom already exists, the function returns its associated program atom. If no equivalent theory atom exists and the provided program atom is engaged, a new theory atom is created using this program atom, and the function returns it. If the provided program atom is not engaged, a new theory atom is created and assigned a fresh program atom, and the function returns the newly created program atom.

Parameters
atoman optional program atom to assign
namethe symbol representing the name of the atom
elementsthe theory elements of the atom
guardthe optional guard of the atom
Returns
the resulting term id

◆ element()

auto Clingo::TheoryBackend::element ( ProgramIdSpan  tuple,
ProgramLiteralSpan  condition 
) const -> ProgramId
inline

Add a theory element.

Parameters
tuplethe theory term tuple of the element
conditionthe program literals forming the condition
Returns
the resulting term id

◆ function()

auto Clingo::TheoryBackend::function ( std::string_view  name,
ProgramIdSpan  elements 
) const -> ProgramId
inline

Add a theory function.

Parameters
namethe name of the function
elementsthe arguments of the function
Returns
the resulting term id

◆ number()

auto Clingo::TheoryBackend::number ( int  number) const -> ProgramId
inline

Add a numeric theory term.

Parameters
numberthe value of the term
Returns
the resulting term id

◆ sequence()

auto Clingo::TheoryBackend::sequence ( TheorySequenceType  type,
ProgramIdSpan  elements 
) const -> ProgramId
inline

Add a theory term sequence.

Parameters
typethe type of the sequence
elementsthe elements of the sequence
Returns
the resulting term id

◆ string()

auto Clingo::TheoryBackend::string ( std::string_view  string) const -> ProgramId
inline

Add a string theory term.

Includes constants as well as quoted strings.

Parameters
stringthe value of the term
Returns
the resulting term id

◆ symbol()

auto Clingo::TheoryBackend::symbol ( Symbol const symbol) const -> ProgramId
inline

Convert the given symbol into a theory term.

Parameters
symbolthe symbol to convert
Returns
the resulting term id

The documentation for this class was generated from the following file: