Clingo
Loading...
Searching...
No Matches
CppClingo::Ground::StateTheory Class Reference

State storing all necessary information to ground theory atoms. More...

#include <theory_atom.hh>

Inheritance diagram for CppClingo::Ground::StateTheory:
CppClingo::Ground::State

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.
 
- Public Member Functions inherited from CppClingo::Ground::State
virtual ~State ()=default
 Destructor.
 

Detailed Description

State storing all necessary information to ground theory atoms.

Member Function Documentation

◆ find_atom()

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.

◆ insert_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.

◆ insert_elem()

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.

◆ output()

void CppClingo::Ground::StateTheory::output ( Logger log,
SymbolStore store,
OutputStm out 
)
overridevirtual

Output all previously output theory atoms.

Implements CppClingo::Ground::State.


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