Clingo
|
State storing all necessary information to ground theory atoms. More...
#include <theory_atom.hh>
Classes | |
class | ElementKey |
Keys for aggregate elements storing their tuple and their aggregate index. More... | |
Public Types | |
using | AtomMap = BaseTheory::AtomMap |
Map containing the atoms. | |
using | ElementMap = Util::ordered_map< ElementKey *, Util::small_vector< size_t > > |
Map capturing the elements of theory atoms. | |
Public Member Functions | |
StateTheory (std::pmr::monotonic_buffer_resource &mbr, VariableVec global, UTerm name, TheoryRGuard guard, OutputTheory::AtomType type) | |
Construct the state. | |
auto | find_atom (Assignment &ass) -> AtomMap::iterator |
Find a previously grounded theory atom. | |
auto | insert_atom (Symbol name, std::optional< size_t > rhs, Assignment &ass) -> std::pair< AtomMap::iterator, bool > |
Insert a theory atom. | |
void | insert_elem (EvalContext const &ctx, AtomMap::iterator it, UTheoryTermVec const &tuple, ElementKey *&elem_key, auto const &get_cond) |
Insert a theory atom element. | |
void | print (std::ostream &out) |
Print a debug representation of the theory atom. | |
void | output (Logger &log, SymbolStore &store, OutputStm &out) override |
Output all previously output theory atoms. | |
auto | global () const -> VariableVec const & |
Get the global variables of the theory atom. | |
auto | name () const -> UTerm const & |
Get the name of the theory atom. | |
auto | guard () const -> TheoryRGuard const & |
Get the guard of the theory atom. | |
auto | base () -> BaseTheory & |
Get the associated base. | |
void | elems (UStmVec elems) |
Set the theory elements. | |
![]() | |
virtual | ~State ()=default |
Destructor. | |
State storing all necessary information to ground theory atoms.
auto CppClingo::Ground::StateTheory::find_atom | ( | Assignment & | ass | ) | -> AtomMap::iterator |
Find a previously grounded theory atom.
Assumes that the assignment binds the global variables of the atom.
auto CppClingo::Ground::StateTheory::insert_atom | ( | Symbol | name, |
std::optional< size_t > | rhs, | ||
Assignment & | ass | ||
) | -> std::pair< AtomMap::iterator, bool > |
Insert a theory atom.
Assumes that the assignment binds the global variables of the atom.
void CppClingo::Ground::StateTheory::insert_elem | ( | EvalContext const & | ctx, |
AtomMap::iterator | it, | ||
UTheoryTermVec const & | tuple, | ||
ElementKey *& | elem_key, | ||
auto const & | get_cond | ||
) |
Insert a theory atom element.
Assumes that the assignment binds the global/local variables of the element.
|
overridevirtual |
Output all previously output theory atoms.
Implements CppClingo::Ground::State.