CppClingo::Output::TheoryData Class Reference

Class similar to Potassco::TheoryData but with automatic id generation. More...

#include <backend.hh>

Public Types
using	IdVec = Util::small_vector< prg_id_t, 4 >
	A vector of ids.
using	LitVec = Util::small_vector< prg_lit_t, 4 >
	A vector of literals.

Public Member Functions
	TheoryData (SymbolStore &store, UTheoryBackend backend)
	Construct a theory data object.
auto	num (prg_weight_t num) -> prg_id_t
	Add a number term.
auto	str (String str) -> prg_id_t
	Add a string term.
auto	fun (prg_id_t name, IdVec args) -> prg_id_t
	Add a function term.
auto	fun (String name, IdVec args) -> prg_id_t
	Overload for strings.
auto	fun (String name, PrgIdSpan args) -> prg_id_t
	Overload for strings and spans.
auto	tup (TheoryTermTupleType type, IdVec args) -> prg_id_t
	Add a tuple term.
auto	tup (TheoryTermTupleType type, PrgIdSpan args) -> prg_id_t
	Overload for spans.
auto	sym (Symbol sym) -> prg_id_t
	Convert a symbol into a theory term.
auto	elem (IdVec tuple, LitVec cond) -> prg_id_t
	Add a theory element.
auto	elem (PrgIdSpan tuple, PrgLitSpan cond) -> prg_id_t
	Overload for spans.
auto	atom (std::function< prg_lit_t()> const &atom, prg_id_t name, IdVec elems, std::optional< std::pair< prg_id_t, prg_id_t > > guard) -> prg_lit_t
	Add a theory atom.
auto	atom (std::function< prg_lit_t()> const &atom, Symbol name, IdVec elems, std::optional< std::pair< String, prg_id_t > > guard) -> prg_lit_t
	Overload for strings.
auto	atom (std::function< prg_lit_t()> const &atom, Symbol name, PrgIdSpan elems, std::optional< std::pair< String, prg_id_t > > guard) -> prg_lit_t
	Overload for strings and spans.
void	reset () noexcept
	Clear the theory data.

Detailed Description

Class similar to Potassco::TheoryData but with automatic id generation.

Constructor & Destructor Documentation

TheoryData()

CppClingo::Output::TheoryData::TheoryData ( SymbolStore &  store, UTheoryBackend  backend  )

inline

Construct a theory data object.

Parameters

store	the underlying symbol store
backend	the underlying backend

Member Function Documentation

atom()

auto CppClingo::Output::TheoryData::atom	(	std::function< prg_lit_t()> const &	atom,
		prg_id_t	name,
		IdVec	elems,
		std::optional< std::pair< prg_id_t, prg_id_t > >	guard
	)		-> prg_lit_t

Add a theory atom.

The first argument is a function to set the literal of the atom. It is only called if a fresh atom has been inserted. It must return a non-negative literal. The literal can be zero for directives.

Parameters

atom	function to set the literal
name	the name of the atom
elems	the element ids
guard	the optional guard of the atom

Returns

the literal of the theory atom

elem()

auto CppClingo::Output::TheoryData::elem	(	IdVec	tuple,
		LitVec	cond
	)		-> prg_id_t

Add a theory element.

Parameters

tuple	the ids of terms forming the tuple
cond	the condition

Returns

the element id

fun() [1/2]

auto CppClingo::Output::TheoryData::fun	(	prg_id_t	name,
		IdVec	args
	)		-> prg_id_t

Add a function term.

The given name must refer to a string.

Parameters

name	the name of the function
args	the arguments of the function

Returns

the term id

fun() [2/2]

auto CppClingo::Output::TheoryData::fun ( String  name, IdVec  args  ) -> prg_id_t

inline

Overload for strings.

Parameters

name	the name of the function
args	the arguments of the function

Returns

the term id

num()

auto CppClingo::Output::TheoryData::num

(

prg_weight_t

num

)

-> prg_id_t

Add a number term.

Parameters

num	the number

Returns

the term id

str()

auto CppClingo::Output::TheoryData::str

(

String

str

)

-> prg_id_t

Add a string term.

Parameters

str	the string

Returns

the term id

sym()

auto CppClingo::Output::TheoryData::sym

(

Symbol

sym

)

-> prg_id_t

Convert a symbol into a theory term.

Parameters

sym	the symbol to convert

Returns

the term id

tup()

auto CppClingo::Output::TheoryData::tup	(	TheoryTermTupleType	type,
		IdVec	args
	)		-> prg_id_t

Add a tuple term.

Parameters

type	the type of the tuple
args	the arguments of the tuple

Returns

the term id

---

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

• clingo/output/backend.hh