Struct clingo::GenericControl
source · pub struct GenericControl<L: Logger, P: Propagator, O: GroundProgramObserver, F: FunctionHandler> { /* private fields */ }Expand description
Control object holding grounding and solving state.
Implementations§
source§impl<L: Logger, P: Propagator, O: GroundProgramObserver, F: FunctionHandler> GenericControl<L, P, O, F>
impl<L: Logger, P: Propagator, O: GroundProgramObserver, F: FunctionHandler> GenericControl<L, P, O, F>
sourcepub fn ground(&mut self, parts: &[Part]) -> Result<(), ClingoError>
pub fn ground(&mut self, parts: &[Part]) -> Result<(), ClingoError>
Ground the selected parts of the current (non-ground) logic program.
After grounding, logic programs can be solved with solve().
Note: Parts of a logic program without an explicit #program
specification are by default put into a program called base - without
arguments.
Arguments
parts- array of parts to ground
Errors
sourcepub fn register_function_handler<T: FunctionHandler>(
self,
function_handler: T
) -> GenericControl<L, P, O, T>
pub fn register_function_handler<T: FunctionHandler>( self, function_handler: T ) -> GenericControl<L, P, O, T>
Register a handler for external functions
Arguments
function_handler- implementing the traitFunctionHandler
sourcepub fn solve(
self,
mode: SolveMode,
assumptions: &[SolverLiteral]
) -> Result<GenericSolveHandle<L, P, O, F, Non>, ClingoError>
pub fn solve( self, mode: SolveMode, assumptions: &[SolverLiteral] ) -> Result<GenericSolveHandle<L, P, O, F, Non>, ClingoError>
Solve the currently grounded logic program enumerating its models.
Arguments
mode- configures the search modeassumptions- array of assumptions to solve under
Errors
ClingoError::InternalErrorwithErrorCode::BadAllocorErrorCode::Runtimeif solving could not be started
sourcepub fn solve_with_event_handler<T: SolveEventHandler>(
self,
mode: SolveMode,
assumptions: &[SolverLiteral],
event_handler: T
) -> Result<GenericSolveHandle<L, P, O, F, T>, ClingoError>
pub fn solve_with_event_handler<T: SolveEventHandler>( self, mode: SolveMode, assumptions: &[SolverLiteral], event_handler: T ) -> Result<GenericSolveHandle<L, P, O, F, T>, ClingoError>
Solve the currently grounded logic program enumerating its models.
Arguments
mode- configures the search modeassumptions- array of assumptions to solve underhandler- implementing the traitSolveEventHandler
Errors
ClingoError::InternalErrorwithErrorCode::BadAllocorErrorCode::Runtimeif solving could not be started
sourcepub fn add(
&mut self,
name: &str,
parameters: &[&str],
program: &str
) -> Result<(), ClingoError>
pub fn add( &mut self, name: &str, parameters: &[&str], program: &str ) -> Result<(), ClingoError>
Extend the logic program with the given non-ground logic program in string form.
This function puts the given program into a block of form: #program name(parameters).
After extending the logic program, the corresponding program parts are typically grounded
with ground().
Arguments
name- name of the program blockparameters- string array of parameters of the program blockprogram- string representation of the program
Errors
ClingoError::NulError- if a any argument contains a nul byteClingoError::InternalErrorwithErrorCode::BadAllocorErrorCode::Runtimeif parsing fails
sourcepub fn cleanup(&mut self) -> Result<(), ClingoError>
pub fn cleanup(&mut self) -> Result<(), ClingoError>
sourcepub fn assign_external(
&mut self,
literal: SolverLiteral,
value: TruthValue
) -> Result<(), ClingoError>
pub fn assign_external( &mut self, literal: SolverLiteral, value: TruthValue ) -> Result<(), ClingoError>
sourcepub fn release_external(
&mut self,
SolverLiteral: SolverLiteral
) -> Result<(), ClingoError>
pub fn release_external( &mut self, SolverLiteral: SolverLiteral ) -> Result<(), ClingoError>
sourcepub fn register_propagator<T: Propagator>(
self,
propagator: T,
sequential: bool
) -> Result<GenericControl<L, T, O, F>, ClingoError>
pub fn register_propagator<T: Propagator>( self, propagator: T, sequential: bool ) -> Result<GenericControl<L, T, O, F>, ClingoError>
Register a custom propagator with the control object.
If the sequential flag is set to true, the propagator is called sequentially when solving with multiple threads.
Arguments
propagator- implementing the traitPropagatorsequential- whether the propagator should be called sequentially
Errors
sourcepub fn is_conflicting(&self) -> bool
pub fn is_conflicting(&self) -> bool
Check if the solver has determined that the internal program representation is conflicting.
If this function returns true, solve calls will return immediately with an unsatisfiable solve result. Note that conflicts first have to be detected, e.g. - initial unit propagation results in an empty clause, or later if an empty clause is resolved during solving. Hence, the function might return false even if the problem is unsatisfiable.
sourcepub fn statistics(&self) -> Result<&Statistics, ClingoError>
pub fn statistics(&self) -> Result<&Statistics, ClingoError>
Get a statistics object to inspect solver statistics.
Statistics are updated after a solve call.
Attention:
The level of detail of the statistics depends on the stats option
(which can be set using Configuration or passed as an
option when creating the control object).
The default level zero only provides basic statistics,
level one provides extended and accumulated statistics,
and level two provides per-thread statistics.
Furthermore, the statistics object is best accessed right after solving.
Otherwise, not all of its entries have valid values.
Errors
sourcepub fn interrupt(&mut self)
pub fn interrupt(&mut self)
Interrupt the active solve call (or the following solve call right at the beginning).
sourcepub fn configuration_mut(&mut self) -> Result<&mut Configuration, ClingoError>
pub fn configuration_mut(&mut self) -> Result<&mut Configuration, ClingoError>
Get a configuration object to change the solver configuration.
sourcepub fn configuration(&self) -> Result<&Configuration, ClingoError>
pub fn configuration(&self) -> Result<&Configuration, ClingoError>
Get a configuration object to change the solver configuration.
sourcepub fn set_enable_enumeration_assumption(
&mut self,
enable: bool
) -> Result<(), ClingoError>
pub fn set_enable_enumeration_assumption( &mut self, enable: bool ) -> Result<(), ClingoError>
Configure how learnt constraints are handled during enumeration.
If the enumeration assumption is enabled, then all information learnt from
the solver’s various enumeration modes is removed after a solve call. This
includes enumeration of cautious or brave consequences, enumeration of
answer sets with or without projection, or finding optimal models, as well
as clauses added with SolveControl::add_clause().
Attention: For practical purposes, this option is only interesting for single-shot solving or before the last solve call to squeeze out a tiny bit of performance. Initially, the enumeration assumption is enabled.
Arguments
enable- whether to enable the assumption
sourcepub fn get_enable_enumeration_assumption(&self) -> bool
pub fn get_enable_enumeration_assumption(&self) -> bool
Check whether the enumeration assumption is enabled.
See Control::set_enable_assumption()
Returns using the enumeration assumption is enabled
sourcepub fn set_enable_cleanup(&mut self, enable: bool) -> bool
pub fn set_enable_cleanup(&mut self, enable: bool) -> bool
Enable automatic cleanup after solving.
Note: Cleanup is enabled by default.
Arguments
enable- whether to enable cleanups
Returns whether the call was successful
sourcepub fn get_enable_cleanup(&self) -> bool
pub fn get_enable_cleanup(&self) -> bool
Check whether automatic cleanup is enabled.
sourcepub fn get_const(&self, name: &str) -> Result<Symbol, ClingoError>
pub fn get_const(&self, name: &str) -> Result<Symbol, ClingoError>
Return the symbol for a constant definition of form: #const name = symbol.
Arguments
name- the name of the constant if it exists
Errors
ClingoError::NulError- ifnamecontains a nul byteClingoError::InternalError
sourcepub fn has_const(&self, name: &str) -> Result<bool, ClingoError>
pub fn has_const(&self, name: &str) -> Result<bool, ClingoError>
Check if there is a constant definition for the given constant.
Arguments
name- the name of the constant
Errors
ClingoError::NulError- ifnamecontains a nul byteClingoError::InternalError
See: Part::get_const()
sourcepub fn symbolic_atoms<'a>(&self) -> Result<&'a SymbolicAtoms, ClingoError>
pub fn symbolic_atoms<'a>(&self) -> Result<&'a SymbolicAtoms, ClingoError>
Get an object to inspect symbolic atoms (the relevant Herbrand base) used
sourcepub fn theory_atoms(&self) -> Result<&TheoryAtoms, ClingoError>
pub fn theory_atoms(&self) -> Result<&TheoryAtoms, ClingoError>
Get an object to inspect theory atoms that occur in the grounding.
sourcepub fn register_observer<T: GroundProgramObserver>(
self,
observer: T,
replace: bool
) -> Result<GenericControl<L, P, T, F>, ClingoError>
pub fn register_observer<T: GroundProgramObserver>( self, observer: T, replace: bool ) -> Result<GenericControl<L, P, T, F>, ClingoError>
Register a program observer with the control object.
Arguments
observer- the observer to registerreplace- just pass the grounding to the observer but not the solver
Returns whether the call was successful
sourcepub fn backend(&mut self) -> Result<Backend<'_>, ClingoError>
pub fn backend(&mut self) -> Result<Backend<'_>, ClingoError>
Get an object to add ground directives to the program.
Errors
pub fn add_facts(&mut self, facts: &FactBase) -> Result<(), ClingoError>
sourcepub fn all_models(self) -> Result<AllModels<L, P, O, F, Non>, ClingoError>
pub fn all_models(self) -> Result<AllModels<L, P, O, F, Non>, ClingoError>
Covenience function that returns an iterator over the models.
Uses solve() with SolveMode::Yield and empty assumptions.
Errors
ClingoError::InternalErrorwithErrorCode::BadAllocorErrorCode::Runtimeif solving could not be started
sourcepub fn optimal_models(
self
) -> Result<OptimalModels<L, P, O, F, Non>, ClingoError>
pub fn optimal_models( self ) -> Result<OptimalModels<L, P, O, F, Non>, ClingoError>
Covenience function that returns an iterator over the optimal models.
Uses solve() with SolveMode::Yield and empty assumptions.
Errors
ClingoError::InternalErrorwithErrorCode::BadAllocorErrorCode::Runtimeif solving could not be started