Clingo::Theory Class Reference

Theory class to represent a theory in Clingo. More...

#include <theory.hh>

Public Member Functions
	Theory (Library const &lib, bool(*create)(clingo_lib_t *lib, clingo_theory_t *theory))
	Constructor for the Theory class.
	Theory (Theory &&other)=delete
	Disable copy and move operations for the Theory class.
	~Theory ()
	Destructor for the Theory class.
void	prepare (Control const &ctl) const
	Prepare the theory for solving.
template<class F >
void	rewrite (AST::Node const &stm, F fun) const
	Rewrite the given AST node using the theory's rewrite function.
void	rewrite (Library const &lib, Control const &ctl, std::string_view str) const
	Rewrite the given program using the theory's rewrite function.
void	rewrite (Library const &lib, Control const &ctl, StringSpan files) const
	Rewrite the programs in the files using the theory's rewrite function.
auto	assignment (uint32_t thread_id) const -> TheoryAssignment
	Get the theory assignment for the given thread id.
void	stats (Stats step, Stats accu) const
	Incorporate statistics from the theory into the solver's statistics.
void	model (Model model) const
	Incorporate theory symbols into the model.
void	register_theory (Control const &ctl) const
	Register the theory with the control object.
void	register_options (Options const &opts) const
	Add theory related options to the given options object.
void	validate_options () const
	Validate previously parsed the theory options.
void	configure (std::string_view key, std::string_view value) const
	Configure the theory with the given key and value.

Friends
auto	c_cast (Theory const &x) -> clingo_theory_t const *
	Get the underlying C representation of the theory.

Detailed Description

Theory class to represent a theory in Clingo.

Constructor & Destructor Documentation

Theory()

Clingo::Theory::Theory ( Library const &  lib, bool(*)(clingo_lib_t *lib, clingo_theory_t *theory)  create  )

inline

Constructor for the Theory class.

Parameters

lib	the library to store symbols
create	the function to create the theory

Member Function Documentation

assignment()

auto Clingo::Theory::assignment ( uint32_t  thread_id ) const -> TheoryAssignment

inline

Get the theory assignment for the given thread id.

Parameters

thread_id

the thread id for which to get the assignment

Returns

the theory assignment for the given thread id

configure()

void Clingo::Theory::configure ( std::string_view  key, std::string_view  value  ) const

inline

Configure the theory with the given key and value.

It is theory dependent at which point this function can be called. Some theories might require configuration before theory registration, while others might allow configuration at any time.

Parameters

key	the key to configure
value	the value to configure

model()

void Clingo::Theory::model ( Model  model ) const

inline

Incorporate theory symbols into the model.

Parameters

model

the model to extend with theory symbols

prepare()

void Clingo::Theory::prepare ( Control const &  ctl ) const

inline

Prepare the theory for solving.

Must be called before solve calls.

Parameters

ctl	the control object to prepare the theory with

register_options()

void Clingo::Theory::register_options ( Options const &  opts ) const

inline

Add theory related options to the given options object.

Should be called from the Clingo::App::register_options() method.

Parameters

opts	the options object to register the theory options with

register_theory()

void Clingo::Theory::register_theory ( Control const &  ctl ) const

inline

Register the theory with the control object.

This gives a theory the possibility to register propagators. Hence, it must be called before grounding and solving.

Parameters

ctl	the control object to register the theory with

rewrite() [1/3]

template<class F >

void Clingo::Theory::rewrite ( AST::Node const &  stm, F  fun  ) const

inline

Rewrite the given AST node using the theory's rewrite function.

Rewritten asts are passed to the given function.

Parameters

stm	the AST node to rewrite
fun	the function to call with the rewritten AST nodes

rewrite() [2/3]

void Clingo::Theory::rewrite ( Library const &  lib, Control const &  ctl, std::string_view  str  ) const

inline

Rewrite the given program using the theory's rewrite function.

Parameters

lib	the library to store symbols
ctl	the control object to add statements to
str	the string to parse and rewrite

rewrite() [3/3]

void Clingo::Theory::rewrite ( Library const &  lib, Control const &  ctl, StringSpan  files  ) const

inline

Rewrite the programs in the files using the theory's rewrite function.

Parameters

lib	the library to store symbols
ctl	the control object to add statements to
files	the files to parse and rewrite

stats()

void Clingo::Theory::stats ( Stats  step, Stats  accu  ) const

inline

Incorporate statistics from the theory into the solver's statistics.

Parameters

step	the current step of the solver
accu	the accumulated statistics

validate_options()

void Clingo::Theory::validate_options ( ) const

inline

Validate previously parsed the theory options.

Should be called from the Clingo::App::validate_options() method.

Friends And Related Symbol Documentation

c_cast

auto c_cast ( Theory const &  x ) -> clingo_theory_t const *

friend

Get the underlying C representation of the theory.

Parameters

x	the theory to cast

Returns

the C representation of the theory

---

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

• clingo/theory.hh