A grounder and solver for logic programs. More...

#include <solver.hh>

Inheritance diagram for CppClingo::Control::Solver:

Public Member Functions
	Solver (Clasp::ClaspFacade &clasp, Clasp::Cli::ClaspCliConfig &config, Logger &log, SymbolStore &store, Scripts &scripts, Input::RewriteOptions ropts, SolverOptions sopts, FILE *out=stdout)
	Create a solver object.

void	main (std::span< std::string_view const > const &files)
	Parse, ground, and solve a program.

void	main ()
	Ground and solve a program.

void	join (Input::UnprocessedProgram const &prg)
	Join with the given program.

void	parse (std::string_view str)
	Parse a program from the given string.

void	parse (std::span< std::string_view const > const &files)
	Parse the given files.

void	parse_with (std::function< void(ProgramBackend , TheoryBackend )> cb)
	Parse with optional backends.

void	add_const (String name, Symbol value)
	Define a constant.

auto	const_map () -> Input::ConstMap const &
	Get the const map.

void	ground (ProgramParamVec const &params, Ground::ScriptCallback *ctx)
	Ground the program.

auto	solve (UEventHandler handler={}, PrgLitSpan assumptions={}, SolveMode mode=SolveMode::none) -> USolveHandle
	Solve the program.

void	output_unprocessed_program (std::ostream &out)
	Output the current unprocessed program.

void	output_program (std::ostream &out)
	Output the current program.

auto	map_model (Clasp::Model const &mdl) -> Model &
	Map the given clasp model to the clingo one.

auto	buf () -> Util::OutputBuffer &
	Get the output buffer.

auto	backend () -> UBackendHandle
	Get a handle that provides access to the backend to add atoms and rules.

auto	clasp_facade () -> Clasp::ClaspFacade &
	Get a pointer to the underlying clasp facade.

auto	clasp_facade () const -> Clasp::ClaspFacade const &
	Get a pointer to the underlying clasp facade.

auto	clasp_config () -> Clasp::Cli::ClaspCliConfig &
	Only non-null in solving mode.

auto	clasp_stats () -> Potassco::AbstractStatistics const &
	Get the statistics.

void	register_propagator (UPropagator propagator)
	Register the given propagator with the control object.

auto	get_lock () -> CallbackLock &
	Get the solvers callback lock.

void	block_main (bool block)
	Block execution of the main function in scripts.

auto	get_mode () const -> AppMode
	Get the application mode.

auto	user_data () -> void *&
	Get user data for C integration.

void	interrupt () noexcept
	Interrupt the running (or next search).

auto	get_parts () -> std::optional< Input::StmParts > const &
	Get the program parts to ground.

void	set_parts (std::optional< Input::StmParts > parts)
	Set the program parts to ground.

void	set_parts (Input::ProgramParamVec parts)
	Set the program parts to ground.

void	show (Input::SharedSig const &sig)
	Show the given signature.

auto	sym_tab () -> SymbolTable &
	Get the symbol table.

Public Member Functions inherited from CppClingo::Control::BaseView
virtual	~BaseView ()=default
	The default destructor.

auto	bases () const -> Ground::Bases const &
	Get a reference to the underlying atom bases.

auto	term_base () const -> TermBaseMap const &
	Get a reference to the underlying term bases.

auto	clasp_program () const -> Clasp::Asp::LogicProgram const &
	Get a reference to the underlying facade.

auto	clasp_theory () const -> Potassco::TheoryData const &
	Get a reference to the underlying facade.

Detailed Description

A grounder and solver for logic programs.

Takes care of parsing, grounding, and solving.

Member Function Documentation

◆ backend()

auto CppClingo::Control::Solver::backend ( ) -> UBackendHandle

Get a handle that provides access to the backend to add atoms and rules.

While the handle is alive, the solver object should not be accessed. It can be seen like an active ground call.

◆ buf()

auto CppClingo::Control::Solver::buf ( ) -> Util::OutputBuffer &

inline

Get the output buffer.

If the control object has been constructed without a null output FILE, this buffer contains the output of the textoutput.

◆ register_propagator()

void CppClingo::Control::Solver::register_propagator ( UPropagator propagator )

Register the given propagator with the control object.

Parameters

propagator the propagator

◆ solve()

auto CppClingo::Control::Solver::solve	(	UEventHandler	handler = `{}`,
		PrgLitSpan	assumptions = `{}`,
		SolveMode	mode = `SolveMode::none`
	)		-> USolveHandle

Solve the program.