Clingo
Loading...
Searching...
No Matches
CppClingo::TheoryBackend Class Referenceabstract

Abstract class connecting grounder and theory data. More...

#include <backend.hh>

Public Member Functions

virtual ~TheoryBackend ()=default
 Destroy the backend.
 
void num (prg_id_t id, prg_weight_t num)
 Add a theory number.
 
void str (prg_id_t id, std::string_view str)
 Add a theory string.
 
void fun (prg_id_t id, prg_id_t name, PrgIdSpan args)
 Add a theory function.
 
void tup (prg_id_t id, TheoryTermTupleType type, PrgIdSpan args)
 Add a theory tuple.
 
void elem (prg_id_t id, PrgIdSpan terms, PrgLitSpan cond)
 Add a theory element.
 
void atom (prg_lit_t atom_or_zero, prg_id_t name, PrgIdSpan elems, std::optional< std::pair< prg_id_t, prg_id_t > > guard)
 Add a theory atom.
 
void end ()
 Finalize the theory.
 

Detailed Description

Abstract class connecting grounder and theory data.

Member Function Documentation

◆ atom()

void CppClingo::TheoryBackend::atom ( prg_lit_t  atom_or_zero,
prg_id_t  name,
PrgIdSpan  elems,
std::optional< std::pair< prg_id_t, prg_id_t > >  guard 
)
inline

Add a theory atom.

Parameters
atom_or_zerothe literal of the atom (zero for directives)
namethe name of the atom (must be a function or symbol)
elemsthe elements of the atom
guardthe optional guard of the atom

◆ elem()

void CppClingo::TheoryBackend::elem ( prg_id_t  id,
PrgIdSpan  terms,
PrgLitSpan  cond 
)
inline

Add a theory element.

Note
The caller is responsible to assign unique ids.
Parameters
idthe unique element id
termsthe terms forming the tuple
condthe condition of the element

◆ fun()

void CppClingo::TheoryBackend::fun ( prg_id_t  id,
prg_id_t  name,
PrgIdSpan  args 
)
inline

Add a theory function.

Note
The caller is responsible to assign unique ids.
Precondition
The name must be an id to a string.
Parameters
idthe unique term id
namethe term id of the function name
argsthe term ids of the arguments

◆ num()

void CppClingo::TheoryBackend::num ( prg_id_t  id,
prg_weight_t  num 
)
inline

Add a theory number.

Note
The caller is responsible to assign unique ids.
Parameters
idthe unique term id
numthe number

◆ str()

void CppClingo::TheoryBackend::str ( prg_id_t  id,
std::string_view  str 
)
inline

Add a theory string.

Note
The caller is responsible to assign unique ids.
Parameters
idthe unique term id
strthe string

◆ tup()

void CppClingo::TheoryBackend::tup ( prg_id_t  id,
TheoryTermTupleType  type,
PrgIdSpan  args 
)
inline

Add a theory tuple.

Note
The caller is responsible to assign unique ids.
Parameters
idthe unique term id
typethe type of the tuple
argsthe term ids of the arguments

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