3#include <clingo/symbol.hh>
5#include <clingo/base.h>
31 return Detail::call<clingo_atom_base_literal>(base_, index_);
38 return Symbol{Detail::call<clingo_atom_base_symbol>(base_, index_),
true};
47 [[nodiscard]]
auto hash() const noexcept ->
size_t {
return Detail::hash_value(index_); }
55 assert(a.base_ == b.base_);
56 return a.index_ == b.index_;
65 assert(a.base_ == b.base_);
66 return a.index_ <=> b.index_;
90 using pointer = Detail::ArrowProxy<value_type>;
92 using iterator = Detail::RandomAccessIterator<AtomBase>;
104 [[nodiscard]]
auto size() const ->
size_type {
return Detail::call<clingo_atom_base_size>(base_); }
111 if (
auto atom =
Atom{base_, index}; index <
size()) {
114 throw std::out_of_range{
"index out of range"};
122 return Detail::call<clingo_atom_base_find>(base_, *c_cast(&
symbol)) <
size();
130 [[nodiscard]]
auto get(
key_type const &
symbol, std::optional<mapped_type> def = std::nullopt)
const
131 -> std::optional<mapped_type> {
132 auto index = Detail::call<clingo_atom_base_find>(base_, *c_cast(&
symbol));
133 return index < size() ? std::make_optional<mapped_type>(base_, index) : def;
149static_assert(std::random_access_iterator<AtomBase::iterator>);
164 return Symbol{Detail::call<clingo_term_base_symbol>(base_, index_),
true};
171 size_t const *sizes =
nullptr;
176 auto res = std::vector<ProgramLiteralVector>{};
178 for (
size_t i = 0; i < size; ++i) {
180 res.emplace_back(lits[i], lits[i] + sizes[i]);
191 [[nodiscard]]
auto hash() const noexcept ->
size_t {
return Detail::hash_value(index_); }
199 assert(a.base_ == b.base_);
200 return a.index_ == b.index_;
209 assert(a.base_ == b.base_);
210 return a.index_ <=> b.index_;
234 using pointer = Detail::ArrowProxy<value_type>;
236 using iterator = Detail::RandomAccessIterator<TermBase>;
246 [[nodiscard]]
auto size() const ->
size_type {
return Detail::call<clingo_term_base_size>(base_); }
253 auto term =
Term{*base_, index};
254 return index <
size() ?
value_type{term.symbol(), term} :
throw std::out_of_range{
"index out of range"};
262 return Detail::call<clingo_term_base_find>(base_, *c_cast(&
symbol)) <
size();
270 [[nodiscard]]
auto get(
key_type const &
symbol, std::optional<mapped_type> def = std::nullopt)
const
271 -> std::optional<mapped_type> {
272 auto index = Detail::call<clingo_term_base_find>(base_, *c_cast(&
symbol));
273 return index < size() ? std::make_optional<mapped_type>(*base_, index) : def;
289static_assert(std::random_access_iterator<TermBase::iterator>);
316 return static_cast<TheoryTermType>(Detail::call<clingo_theory_base_term_type>(base_, index_));
322 [[nodiscard]]
auto number() const ->
int {
return Detail::call<clingo_theory_base_term_number>(base_, index_); }
327 [[nodiscard]]
auto name() const -> std::string_view {
328 auto [
name, size] = Detail::call<clingo_theory_base_term_name>(base_, index_);
339 return Detail::transform(std::span{args, size}, [
this](
clingo_id_t id) {
return TheoryTerm{*base_,
id}; });
348 return std::string{bld.str()};
357 [[nodiscard]]
auto hash() const noexcept ->
size_t {
return Detail::hash_value(index_); }
365 assert(a.base_ == b.base_);
366 return a.index_ == b.index_;
375 assert(a.base_ == b.base_);
376 return a.index_ <=> b.index_;
414 return std::span{cond, size};
428 auto ret = Detail::call<clingo_theory_base_element_condition_id>(base_, index_);
429 return ret != 0 ? std::optional(ret) : std::nullopt;
438 return std::string{bld.str()};
447 [[nodiscard]]
auto hash() const noexcept ->
size_t {
return Detail::hash_value(index_); }
455 assert(a.base_ == b.base_);
456 return a.index_ == b.index_;
465 assert(a.base_ == b.base_);
466 return a.index_ <=> b.index_;
487 return TheoryTerm{*base_, Detail::call<clingo_theory_base_atom_term>(base_, index_)};
504 return Detail::call<clingo_theory_base_atom_literal>(base_, index_);
510 [[nodiscard]]
auto guard() const -> std::optional<std::pair<std::string_view,
TheoryTerm>> {
511 auto has_guard = Detail::call<clingo_theory_base_atom_has_guard>(base_, index_);
527 return std::string{bld.str()};
536 [[nodiscard]]
auto hash() const noexcept ->
size_t {
return Detail::hash_value(index_); }
544 assert(a.base_ == b.base_);
545 return a.index_ == b.index_;
554 assert(a.base_ == b.base_);
555 return a.index_ <=> b.index_;
575 using pointer = Detail::ArrowProxy<value_type>;
577 using iterator = Detail::RandomAccessIterator<TheoryBase>;
587 [[nodiscard]]
auto size() const ->
size_type {
return Detail::call<clingo_theory_base_size>(base_); }
593 return index <
size() ?
TheoryAtom{*base_, index} :
throw std::out_of_range{
"atom index out of range"};
609static_assert(std::random_access_iterator<TheoryBase::iterator>);
615 using key_type = std::tuple<std::string_view, size_t, bool>;
627 using pointer = Detail::ArrowProxy<value_type>;
629 using iterator = Detail::RandomAccessIterator<Base>;
641 return Detail::call<clingo_base_is_external>(base_, lit);
649 return Detail::call<clingo_base_is_fact>(base_, lit);
657 return Detail::call<clingo_base_is_shown>(base_, lit);
665 return Detail::call<clingo_base_is_fact>(base_, lit);
673 return Detail::call<clingo_base_is_current>(base_, lit);
679 [[nodiscard]]
auto size() const ->
size_type {
return Detail::call<clingo_base_atoms_size>(base_); }
686 if (index <
size()) {
690 return std::pair{std::tuple{sig.name, sig.arity, sig.is_positive},
AtomBase{
atoms}};
692 throw std::out_of_range{
"index out of range"};
702 return Detail::call<clingo_base_atoms_find>(base_, &csig,
nullptr);
712 [[nodiscard]]
auto contains(std::pair<std::string_view, size_t>
const &sig)
const ->
bool {
713 return contains({std::get<0>(sig), std::get<1>(sig),
true});
721 if (
auto sig = sym.signature(); sig) {
722 if (
auto base =
get(*sig)) {
723 return base->contains(sym);
734 [[nodiscard]]
auto get(
key_type const &sig, std::optional<mapped_type> def = std::nullopt)
const
735 -> std::optional<mapped_type> {
741 return found ? std::make_optional<AtomBase>(
atoms) : def;
749 [[nodiscard]]
auto get(std::pair<std::string_view, size_t>
const &sig,
750 std::optional<mapped_type> def = std::nullopt)
const -> std::optional<mapped_type> {
751 return get({std::get<0>(sig), std::get<1>(sig),
true}, def);
759 [[nodiscard]]
auto get(
Symbol const &sym, std::optional<Atom> def = std::nullopt)
const -> std::optional<Atom> {
760 if (
auto sig = sym.signature(); sig) {
761 if (
auto base =
get(*sig)) {
762 return base->get(sym, def);
791static_assert(std::random_access_iterator<Base::iterator>);
800template <>
struct hash<Clingo::Atom> {
802 auto operator()(
Clingo::Atom const &x)
const noexcept ->
size_t {
return x.hash(); }
806template <>
struct hash<Clingo::
Term> {
808 auto operator()(
Clingo::Term const &x)
const noexcept ->
size_t {
return x.hash(); }
814 auto operator()(
Clingo::TheoryTerm const &x)
const noexcept ->
size_t {
return x.hash(); }
818template <>
struct hash<Clingo::TheoryElement> {
824template <>
struct hash<Clingo::TheoryAtom> {
826 auto operator()(
Clingo::TheoryAtom const &x)
const noexcept ->
size_t {
return x.hash(); }
An atom base that maps symbols to atoms.
Definition base.hh:75
Detail::ArrowProxy< value_type > pointer
The pointer type.
Definition base.hh:90
std::size_t size_type
The size type.
Definition base.hh:84
auto size() const -> size_type
The size of the atom base.
Definition base.hh:104
value_type reference
The reference type.
Definition base.hh:88
AtomBase(clingo_atom_base_t const *base)
Construct an atom base from its C representation.
Definition base.hh:99
auto at(size_t index) const -> value_type
Get the symbol atom pair at the given index.
Definition base.hh:110
std::pair< key_type, mapped_type > value_type
The value type.
Definition base.hh:82
auto get(key_type const &symbol, std::optional< mapped_type > def=std::nullopt) const -> std::optional< mapped_type >
Get the atom for the given symbol.
Definition base.hh:130
auto contains(key_type const &symbol) const -> bool
Whether the atom base contains the given symbol.
Definition base.hh:121
auto end() const -> iterator
Get an iterator pointing to the end of the atom base.
Definition base.hh:144
std::ptrdiff_t difference_type
The difference type.
Definition base.hh:86
auto begin() const -> iterator
Get an iterator pointing to the first element of the atom base.
Definition base.hh:139
Detail::RandomAccessIterator< AtomBase > iterator
The iterator type.
Definition base.hh:92
Class to provide access to symbolic atoms.
Definition base.hh:17
friend auto operator==(Atom const &a, Atom const &b) noexcept -> bool
Compare two atoms for equality.
Definition base.hh:54
auto hash() const noexcept -> size_t
Get the header of the atom.
Definition base.hh:47
auto symbol() const -> Symbol
Get the atom's symbol.
Definition base.hh:37
auto literal() const -> ProgramLiteral
Get the program literal of the atom.
Definition base.hh:30
Atom(clingo_atom_base_t const *base, size_t index)
Construct an atom from its C representation.
Definition base.hh:25
friend auto operator<=>(Atom const &a, Atom const &b) noexcept -> std::strong_ordering
Compare two atoms.
Definition base.hh:64
A base that maps signatures to atom bases, and captures term and theory bases.
Definition base.hh:612
auto at(size_t index) const -> value_type
Get the signature atom base pair at the given index.
Definition base.hh:685
auto is_fact(ProgramLiteral lit) const -> bool
Check whether the given program literal is a fact.
Definition base.hh:648
auto size() const -> size_type
Get the number of atom bases in the base.
Definition base.hh:679
auto terms() const -> TermBase
Get the term base of the program.
Definition base.hh:771
std::tuple< std::string_view, size_t, bool > key_type
The key type.
Definition base.hh:615
Detail::ArrowProxy< value_type > pointer
The pointer type.
Definition base.hh:627
auto is_external(ProgramLiteral lit) const -> bool
Check whether the given program literal is external.
Definition base.hh:640
std::pair< key_type, mapped_type > value_type
The value type.
Definition base.hh:619
value_type reference
The reference type.
Definition base.hh:625
auto theory() const -> TheoryBase
Get the theory base of the program.
Definition base.hh:776
std::size_t size_type
The size type.
Definition base.hh:621
auto contains(Symbol const &sym) const -> bool
Check whether the base contains the given symbol.
Definition base.hh:720
auto is_projected(ProgramLiteral lit) const -> bool
Check whether the (atom of the) given program literal is projected.
Definition base.hh:664
Base(clingo_base_t const *base)
Construct a base from its C representation.
Definition base.hh:634
auto get(Symbol const &sym, std::optional< Atom > def=std::nullopt) const -> std::optional< Atom >
Get the atom base for the given symbol.
Definition base.hh:759
auto is_current(ProgramLiteral lit) const -> bool
Check whether the program literals belongs to the current solving step.
Definition base.hh:672
auto is_shown(ProgramLiteral lit) const -> bool
Check whether the given program literal is shown.
Definition base.hh:656
std::ptrdiff_t difference_type
The difference type.
Definition base.hh:623
auto end() const -> iterator
Get an iterator pointing to the end of the base.
Definition base.hh:786
Detail::RandomAccessIterator< Base > iterator
The iterator type.
Definition base.hh:629
auto begin() const -> iterator
Get an iterator pointing to the first element of the base.
Definition base.hh:781
auto contains(key_type const &sig) const -> bool
Check whether the base contains the given signature.
Definition base.hh:699
auto get(key_type const &sig, std::optional< mapped_type > def=std::nullopt) const -> std::optional< mapped_type >
Get the atom base for the given signature.
Definition base.hh:734
auto contains(std::pair< std::string_view, size_t > const &sig) const -> bool
Check whether the base contains the given short signature.
Definition base.hh:712
auto get(std::pair< std::string_view, size_t > const &sig, std::optional< mapped_type > def=std::nullopt) const -> std::optional< mapped_type >
Get the atom base for the given short signature.
Definition base.hh:749
A string builder for constructing strings.
Definition core.hh:619
Class modeling a symbol in Clingo.
Definition symbol.hh:68
A term base that maps symbols to terms.
Definition base.hh:219
auto size() const -> size_type
The size of the term base.
Definition base.hh:246
auto begin() const -> iterator
Get an iterator pointing to the first element of the term base.
Definition base.hh:279
auto at(size_t index) const -> value_type
Get the symbol term pair at the given index.
Definition base.hh:252
auto end() const -> iterator
Get an iterator pointing to the end of the term base.
Definition base.hh:284
Detail::ArrowProxy< value_type > pointer
The pointer type.
Definition base.hh:234
std::ptrdiff_t difference_type
The difference type.
Definition base.hh:230
auto contains(key_type const &symbol) const -> bool
Whether the term base contains the given symbol.
Definition base.hh:261
std::pair< key_type, mapped_type > value_type
The value type.
Definition base.hh:226
Detail::RandomAccessIterator< TermBase > iterator
The iterator type.
Definition base.hh:236
auto get(key_type const &symbol, std::optional< mapped_type > def=std::nullopt) const -> std::optional< mapped_type >
Get the term for the given symbol.
Definition base.hh:270
value_type reference
The reference type.
Definition base.hh:232
TermBase(clingo_term_base_t const &base)
Construct a term base from its C representation.
Definition base.hh:241
std::size_t size_type
The size type.
Definition base.hh:228
Class to provide access to terms in a program.
Definition base.hh:152
friend auto operator==(Term const &a, Term const &b) noexcept -> bool
Compare two terms for equality.
Definition base.hh:198
auto condition() const -> std::vector< ProgramLiteralVector >
Get the condition of the term.
Definition base.hh:170
friend auto operator<=>(Term const &a, Term const &b) noexcept -> std::strong_ordering
Compare two terms.
Definition base.hh:208
Term(clingo_term_base_t const &base, size_t index)
Construct a term from its C representation.
Definition base.hh:158
auto symbol() const -> Symbol
Get the symbol of the term.
Definition base.hh:163
auto hash() const noexcept -> size_t
Get the hash of the term.
Definition base.hh:191
Class to provide access to theory atoms.
Definition base.hh:475
friend auto operator<=>(TheoryAtom const &a, TheoryAtom const &b) noexcept -> std::strong_ordering
Compare two theory atoms.
Definition base.hh:553
TheoryAtom(clingo_theory_base_t const &base, size_t index)
Constructor from C representation.
Definition base.hh:481
auto hash() const noexcept -> size_t
Get the hash of the theory atom.
Definition base.hh:536
auto to_string() const -> std::string
Convert the theory atom to a string representation.
Definition base.hh:524
auto guard() const -> std::optional< std::pair< std::string_view, TheoryTerm > >
Get the guard of the theory atom.
Definition base.hh:510
friend auto operator==(TheoryAtom const &a, TheoryAtom const &b) noexcept -> bool
Compare two theory atoms for equality.
Definition base.hh:543
auto literal() const -> ProgramLiteral
Get the literal of the theory atom.
Definition base.hh:503
auto elements() const -> TheoryElementVector
Get the elements of the theory atom.
Definition base.hh:493
auto name() const -> TheoryTerm
Get the name of the theory atom.
Definition base.hh:486
A theory base that maps theory atoms.
Definition base.hh:564
std::size_t size_type
The size type.
Definition base.hh:569
auto begin() const -> iterator
Get an iterator pointing to the first element of the theory base.
Definition base.hh:599
TheoryAtom value_type
The value type.
Definition base.hh:567
TheoryBase(clingo_theory_base_t const &base)
Construct a theory base from its C representation.
Definition base.hh:582
auto at(size_t index) const -> value_type
Get the theory atom at the given index.
Definition base.hh:592
std::ptrdiff_t difference_type
The difference type.
Definition base.hh:571
Detail::RandomAccessIterator< TheoryBase > iterator
The iterator type.
Definition base.hh:577
auto size() const -> size_type
Get the size of the theory base.
Definition base.hh:587
Detail::ArrowProxy< value_type > pointer
The pointer type.
Definition base.hh:575
auto end() const -> iterator
Get an iterator pointing to the end of the theory base.
Definition base.hh:604
Class to provide access to theory elements.
Definition base.hh:389
auto tuple() const -> TheoryTermVector
Get the tuple of the theory element.
Definition base.hh:400
auto to_string() const -> std::string
Convert the theory element to a string representation.
Definition base.hh:435
auto hash() const noexcept -> size_t
Get the hash of the theory element.
Definition base.hh:447
auto condition_id() const -> std::optional< ProgramLiteral >
Get a program literal for the condition of the theory element.
Definition base.hh:427
friend auto operator<=>(TheoryElement const &a, TheoryElement const &b) noexcept -> std::strong_ordering
Compare two theory elements.
Definition base.hh:464
auto condition() const -> ProgramLiteralSpan
Get the condition of the theory element.
Definition base.hh:410
TheoryElement(clingo_theory_base_t const &base, size_t index)
Constructor from C representation.
Definition base.hh:395
friend auto operator==(TheoryElement const &a, TheoryElement const &b) noexcept -> bool
Compare two theory elements for equality.
Definition base.hh:454
Class to provide access to theory terms.
Definition base.hh:306
auto number() const -> int
Get the numeric value of the term if it is a number term.
Definition base.hh:322
auto arguments() const -> std::vector< TheoryTerm >
Get the arguments of the term if it is a function term.
Definition base.hh:335
friend auto operator<=>(TheoryTerm const &a, TheoryTerm const &b) noexcept -> std::strong_ordering
Compare two theory terms.
Definition base.hh:374
auto name() const -> std::string_view
Get the name of the term if it is a constant or function term.
Definition base.hh:327
auto hash() const noexcept -> size_t
Get the hash of the term.
Definition base.hh:357
auto type() const -> TheoryTermType
Get the type of the theory term.
Definition base.hh:315
TheoryTerm(clingo_theory_base_t const &base, size_t index)
Construct a theory term from its C representation.
Definition base.hh:312
friend auto operator==(TheoryTerm const &a, TheoryTerm const &b) noexcept -> bool
Compare two theory terms for equality.
Definition base.hh:364
auto to_string() const -> std::string
Convert the term to a string representation.
Definition base.hh:345
CLINGO_VISIBILITY_DEFAULT bool clingo_theory_base_element_to_string(clingo_theory_base_t const *theory, clingo_id_t element, clingo_string_builder_t *builder)
Get the string representation of the given theory element.
CLINGO_VISIBILITY_DEFAULT bool clingo_theory_base_atom_elements(clingo_theory_base_t const *theory, clingo_id_t atom, clingo_id_t const **elements, size_t *size)
Get the theory elements associated with the theory atom.
struct clingo_theory_base clingo_theory_base_t
Object to inspect theory atoms.
Definition base.h:93
struct clingo_atom_base clingo_atom_base_t
Object to inspect the symbolic atoms in a program.
Definition base.h:75
CLINGO_VISIBILITY_DEFAULT bool clingo_theory_base_atom_to_string(clingo_theory_base_t const *theory, clingo_id_t atom, clingo_string_builder_t *builder)
Get the string representation of the given theory atom.
CLINGO_VISIBILITY_DEFAULT bool clingo_theory_base_atom_guard(clingo_theory_base_t const *theory, clingo_id_t atom, clingo_string_t *connective, clingo_id_t *term)
Get the guard consisting of a theory operator and a theory term of the given theory atom.
CLINGO_VISIBILITY_DEFAULT bool clingo_base_atoms_find(clingo_base_t const *base, clingo_signature_t const *signature, clingo_atom_base_t const **atoms, bool *found)
Find the atom base wit the given signature.
CLINGO_VISIBILITY_DEFAULT bool clingo_theory_base_term_arguments(clingo_theory_base_t const *theory, clingo_id_t term, clingo_id_t const **arguments, size_t *size)
Get the arguments of the given function theory term.
CLINGO_VISIBILITY_DEFAULT bool clingo_theory_base_term_to_string(clingo_theory_base_t const *theory, clingo_id_t term, clingo_string_builder_t *builder)
Get the string representation of the given theory term.
struct clingo_term_base clingo_term_base_t
Object to inspect the shown terms in a program.
Definition base.h:78
CLINGO_VISIBILITY_DEFAULT bool clingo_base_atoms_at(clingo_base_t const *base, size_t index, clingo_signature_t *signature, clingo_atom_base_t const **atoms)
Get the signature and atom base at the given index.
CLINGO_VISIBILITY_DEFAULT bool clingo_theory_base_element_tuple(clingo_theory_base_t const *theory, clingo_id_t element, clingo_id_t const **tuple, size_t *size)
Get the tuple (array of theory terms) of the given theory element.
struct clingo_base clingo_base_t
Object to inspect symbolic atoms in a program—the relevant Herbrand base gringo uses to instantiate p...
Definition base.h:70
CLINGO_VISIBILITY_DEFAULT bool clingo_term_base_condition(clingo_term_base_t const *terms, size_t index, size_t const **sizes, clingo_literal_t const *const **literals, size_t *size)
Get the conditions of a show directive.
CLINGO_VISIBILITY_DEFAULT bool clingo_theory_base_element_condition(clingo_theory_base_t const *theory, clingo_id_t element, clingo_literal_t const **condition, size_t *size)
Get the condition (array of aspif literals) of the given theory element.
@ clingo_theory_term_type_symbol
a symbol term, e.g., c
Definition base.h:87
@ clingo_theory_term_type_set
a set term, e.g., {1,2,3}
Definition base.h:84
@ clingo_theory_term_type_list
a list term, e.g., [1,2,3]
Definition base.h:83
@ clingo_theory_term_type_number
a number term, e.g., 42
Definition base.h:86
@ clingo_theory_term_type_function
a function term, e.g., f(1,2,3)
Definition base.h:85
@ clingo_theory_term_type_tuple
a tuple term, e.g., (1,2,3)
Definition base.h:82
int32_t clingo_literal_t
Signed integer type used for aspif and solver literals.
Definition core.h:73
uint32_t clingo_id_t
Unsigned integer type used in various places.
Definition core.h:77
@ tuple
Theory tuples "(t1,...,tn)".
@ list
Theory lists "[t1,...,tn]".
@ set
Theory sets "{t1,...,tn}".
std::vector< TheoryTerm > TheoryTermVector
A vector of theory terms.
Definition base.hh:303
std::vector< TheoryElement > TheoryElementVector
A vector of theory elements.
Definition base.hh:386
TheoryTermType
Enumeration of theory term types.
Definition base.hh:292
@ symbol
a symbol term, e.g., c
@ number
a number term, e.g., 42
@ function
a function term, e.g., f(1,2,3)
std::vector< ProgramLiteral > ProgramLiteralVector
A vector of program literals.
Definition core.hh:491
clingo_literal_t ProgramLiteral
A program literal.
Definition core.hh:487
std::span< ProgramLiteral const > ProgramLiteralSpan
A span of program literals.
Definition core.hh:489
Represents a predicate signature.
Definition base.h:58
size_t size
the size of the name
Definition base.h:60
Struct to capture strings that are not null-terminated.
Definition core.h:86
size_t size
the length of the string
Definition core.h:88
char const * data
pointer to the beginning of the string
Definition core.h:87