Library combining input, ground, and output. More...

Classes
class	CppClingo::Control::ProfileProgram
	Class storing profiling data for a program. More...

class	CppClingo::Control::BuildContext
	Context object holding necessary data for translating from input to ground representation. More...

class	CppClingo::Control::Grounder
	A grounder for logic programs. More...

class	CppClingo::Control::ParseHelper
	A helper for parsing. More...

class	CppClingo::Control::Script
	Script providing code execution, main, and callbacks. More...

class	CppClingo::Control::Scripts
	Helper to run specific code and callbacks. More...

struct	CppClingo::Control::SolverOptions
	Options for the solver. More...

class	CppClingo::Control::TermBaseMap
	Map from symbols to show term ids. More...

class	CppClingo::Control::BaseView
	Interface providing the necessary data to inspect atom, term, and theory bases. More...

class	CppClingo::Control::SolveControl
	Simple control class to add clauses while enumerating models. More...

class	CppClingo::Control::Model
	The model class. More...

class	CppClingo::Control::SolveHandle
	A handle to control a running search. More...

class	CppClingo::Control::EventHandler
	The event handler interface. More...

class	CppClingo::Control::BackendHandle
	Object to provide access to the backend. More...

class	CppClingo::Control::Propagator
	The propagator interface. More...

class	CppClingo::Control::CallbackLock
	This lock ensures that callbacks during solving are called in lock-step. More...

class	CppClingo::Control::unlock_guard< M >
	RAII helper to unlock a mutex. More...

class	CppClingo::Control::SymbolTable
	Helper to output symbols. More...

class	CppClingo::Control::Grounded
	Event emitted by a solver after the program is grounded. More...

class	CppClingo::Control::Solver
	A grounder and solver for logic programs. More...

Typedefs
using	CppClingo::Control::ProjectMap = CppClingo::Ground::ProjectMap
	A map from a terms with projections associated state used during grounding.

using	CppClingo::Control::BaseMap = CppClingo::Ground::BaseMap
	A map from signatures to atom bases.

using	CppClingo::Control::VarMap = Util::unordered_map< String, size_t >
	A map from variable names (input) to their indices (ground).

using	CppClingo::Control::DefMap = Util::unordered_map< Input::Term const *, std::vector< size_t > >
	A map from terms to the indices defining them.

using	CppClingo::Control::ProgramParams = std::pair< CppClingo::Input::Precedence, std::optional< ProgramParamVec > >
	A pair capturing a program `#parts` directive.

using	CppClingo::Control::UScript = std::unique_ptr< Script >
	A unique pointer to a script.

using	CppClingo::Control::UModel = std::unique_ptr< Model >
	A unique pointer to a model.

using	CppClingo::Control::USolveHandle = std::unique_ptr< SolveHandle >
	A unique pointer for a solve handle.

using	CppClingo::Control::UEventHandler = std::unique_ptr< EventHandler >
	A unique pointer for an event handler.

using	CppClingo::Control::UBackendHandle = std::unique_ptr< BackendHandle >
	A unique pointer to a backend handle.

using	CppClingo::Control::UPropagator = std::unique_ptr< Propagator >
	A unique pointer to a propagator.

using	CppClingo::Control::USymbolTable = std::unique_ptr< SymbolTable >
	A unique pointer to a symbol table.

Enumerations
enum class	CppClingo::Control::BuiltinIncludes : uint8_t { BuiltinIncludes::empty = 0 , BuiltinIncludes::incmode = 1 }
	Bitset of enabled builtin includes. More...

enum class	CppClingo::Control::IStop : uint8_t { IStop::none , IStop::sat , IStop::unsat , IStop::unknown }
	Stop condition for incremental mode. More...

enum class	CppClingo::Control::AppMode : uint8_t { AppMode::parse , AppMode::rewrite , AppMode::ground , AppMode::solve }
	Enumeration of available application modes. More...

enum class	CppClingo::Control::SymbolSelectFlags : uint8_t { SymbolSelectFlags::none = 0 , SymbolSelectFlags::shown = 1 , SymbolSelectFlags::atoms = 2 , SymbolSelectFlags::terms = 4 , SymbolSelectFlags::theory = 8 , SymbolSelectFlags::all = 15 }
	A bit set of symbol selection flags. More...

enum class	CppClingo::Control::ModelType : uint8_t { ModelType::model = 0 , ModelType::brave_consequences = 1 , ModelType::cautious_consequences = 2 }
	Enumeration of available model flags. More...

enum class	CppClingo::Control::ConsequenceType : uint8_t { ConsequenceType::false_ = 0 , ConsequenceType::true_ = 1 , ConsequenceType::unknown = 2 }
	Enumeration of available consequence types. More...

enum class	CppClingo::Control::SolveResult : uint8_t { SolveResult::empty = 0 , SolveResult::satisfiable = 1 , SolveResult::unsatisfiable = 2 , SolveResult::exhausted = 4 , SolveResult::interrupted = 8 }
	The solve result. More...

enum class	CppClingo::Control::SolveMode : uint8_t { SolveMode::none = 0 , SolveMode::async = 1 , SolveMode::yield = 2 }
	The available solve modes. More...

Functions
void	CppClingo::Control::build_hd_lit (BuildContext &ctx, Input::HdLitAggregate const &lit, Ground::ProfileNodeInternal *node)
	Translate head aggregates.

void	CppClingo::Control::build_bd_lit (BuildContext &ctx, Input::BdLitAggregate const &lit, Ground::ProfileNodeInternal *node)
	Translate body aggregates.

void	CppClingo::Control::build_hd_lit (BuildContext &ctx, Input::HdLitDisjunction const &lit, Ground::ProfileNodeInternal *node)
	Translate disjunctions.

void	CppClingo::Control::build_bd_lit (BuildContext &ctx, Input::BdLitConjunction const &lit, Ground::ProfileNodeInternal *node)
	Translate conditional literals.

template<class F >
void	CppClingo::Control::build_lit (BuildContext &ctx, Input::Lit const &lit, F &&fun)
	Translate input literals to their ground representation.

template<class F >
void	CppClingo::Control::build_stratified_lit (BuildContext &ctx, Input::Lit const &lit, F &&fun)
	Translate input literals to their ground representation.

	CppClingo::Control::CLINGO_ENABLE_BITSET_ENUM (BuiltinIncludes)
	Indicate that the builtin includes type is a bitset.

	CppClingo::Control::CLINGO_ENABLE_BITSET_ENUM (SymbolSelectFlags)
	Enable bit set operations.

	CppClingo::Control::CLINGO_ENABLE_BITSET_ENUM (SolveResult)
	Enable bit set operations.

	CppClingo::Control::CLINGO_ENABLE_BITSET_ENUM (SolveMode)
	Enable bit set operations.

void	CppClingo::Control::build_stm (BuildContext &ctx, Input::Stm const &stm, Input::Stm const *src)
	Translate input statements to their ground representation.

auto	CppClingo::Control::build_term (Util::unordered_map< String, size_t > const &var_map, Input::Term const &term, bool &has_projection) -> Ground::UTerm
	Translates input theory terms to their ground representation.

auto	CppClingo::Control::build_term (Util::unordered_map< String, size_t > const &var_map, Input::Term const &term) -> Ground::UTerm
	Translates input theory terms to their ground representation.

auto	CppClingo::Control::build_theory_term (Util::unordered_map< String, size_t > const &var_map, Input::TheoryTerm const &term) -> Ground::UTheoryTerm
	Translates input theory terms to their ground representation.

void	CppClingo::Control::build_hd_lit (BuildContext &ctx, Input::HdLitTheoryAtom const &lit, Ground::ProfileNodeInternal *node)
	Translate a head theory atom.

void	CppClingo::Control::build_bd_lit (BuildContext &ctx, Input::BdLitTheoryAtom const &lit, Ground::ProfileNodeInternal *node)
	Translate a body theory atom.

Detailed Description

Library combining input, ground, and output.

Typedef Documentation

◆ ProjectMap

using CppClingo::Control::ProjectMap = typedef CppClingo::Ground::ProjectMap

A map from a terms with projections associated state used during grounding.

The terms represent a class of similar terms that can reuse the same projection state.

Enumeration Type Documentation

◆ AppMode

enum class CppClingo::Control::AppMode : uint8_t

strong

Enumeration of available application modes.

Enumerator
parse	Stop processing after parsing.
rewrite	Stop processing after rewriting.
ground	Stop processing after grounding.
solve	Stop processing after solving.

◆ BuiltinIncludes

enum class CppClingo::Control::BuiltinIncludes : uint8_t

strong

Bitset of enabled builtin includes.

Enumerator
empty	The empty set.
incmode	Enable the incremental mode.

◆ ConsequenceType

enum class CppClingo::Control::ConsequenceType : uint8_t

strong

Enumeration of available consequence types.

Enumerator
false_	The literal is not a consequence.
true_	The literal is a consequence.
unknown	The literal might or might not be a consequence.

◆ IStop

enum class CppClingo::Control::IStop : uint8_t

strong

Stop condition for incremental mode.

Enumerator
none	Do not consider solve result.
sat	Stop when satisfiable.
unsat	Stop when unsat.
unknown	Stop when interrupted.

◆ ModelType

enum class CppClingo::Control::ModelType : uint8_t

strong

Enumeration of available model flags.

Enumerator
model	The model represents a stable model.
brave_consequences	The model represents a set of brave consequences.
cautious_consequences	The model represents a set of cautious consequences.

◆ SolveMode

enum class CppClingo::Control::SolveMode : uint8_t

strong

The available solve modes.

This is a bitset.

Enumerator
none	Default synchronous callback-based solving.
async	Solve asynchronously in background threads.
yield	Yield models while solving via `SolveHandle::model()`.

◆ SolveResult

enum class CppClingo::Control::SolveResult : uint8_t

strong

The solve result.

This is a bitset. For example, a model can be both satisfiable and interrupted.

Enumerator
empty	No flags set.
satisfiable	The search produced at least one model.
unsatisfiable	The search finished and no model was produced.
exhausted	The search has been exhausted.
interrupted	The search has been interrupted.

◆ SymbolSelectFlags

enum class CppClingo::Control::SymbolSelectFlags : uint8_t

strong

A bit set of symbol selection flags.

Enumerator
none	Select nothing.
shown	Select shown atoms and terms.
atoms	Select all atoms.
terms	Select all terms.
theory	Select symbols added by theory.
all	Select everything.

Function Documentation

◆ build_lit()

template<class F >

void CppClingo::Control::build_lit	(	BuildContext &	ctx,
		Input::Lit const &	lit,
		F &&	fun
	)

Translate input literals to their ground representation.

Assumes that literals have been rewritten.

◆ build_stratified_lit()

template<class F >

void CppClingo::Control::build_stratified_lit	(	BuildContext &	ctx,
		Input::Lit const &	lit,
		F &&	fun
	)

Translate input literals to their ground representation.

Assumes that literals have been rewritten.

Classes

Typedefs

Enumerations

Functions

Detailed Description

Typedef Documentation

◆ ProjectMap

Enumeration Type Documentation

◆ AppMode

◆ BuiltinIncludes

◆ ConsequenceType

◆ IStop

◆ ModelType

◆ SolveMode

◆ SolveResult

◆ SymbolSelectFlags

Function Documentation

◆ build_lit()

◆ build_stratified_lit()