Struct PropagateControl

pub struct PropagateControl(/* private fields */);

This object can be used to add clauses and propagate literals while solving.

Implementations

impl PropagateControl

pub fn thread_id(&self) -> u32

Get the id of the underlying solver thread.

Thread ids are consecutive numbers starting with zero.

pub fn assignment(&self) -> Result<&Assignment, ClingoError>

Get the assignment associated with the underlying solver.

pub fn assignment_mut(&self) -> Result<&mut Assignment, ClingoError>

Get the assignment associated with the underlying solver.

pub fn add_literal( &mut self, result: &mut SolverLiteral, ) -> Result<(), ClingoError>

Adds a new volatile literal to the underlying solver thread.

Attention: The literal is only valid within the current solving step and solver thread. All volatile literals and clauses involving a volatile literal are deleted after the current search.

Arguments

• result - the (positive) solver literal

Errors:

• ClingoError::InternalError with ErrorCode::BadAlloc or ErrorCode::Logic if the assignment is conflicting

pub fn add_watch(&mut self, literal: SolverLiteral) -> Result<(), ClingoError>

Add a watch for the solver literal in the given phase.

Note: Unlike PropagateInit::add_watch() this does not add a watch to all solver threads but just the current one.

Arguments

• literal - the literal to watch

Errors:

• ClingoError::InternalError with ErrorCode::BadAlloc or ErrorCode::Logic if the literal is invalid

See: PropagateControl::remove_watch()

pub fn has_watch(&self, literal: SolverLiteral) -> bool

Check whether a literal is watched in the current solver thread.

Arguments

• literal - the literal to check

pub fn remove_watch(&mut self, literal: SolverLiteral)

Removes the watch (if any) for the given solver literal.

Note: Similar to PropagateInit::add_watch() this just removes the watch in the current solver thread.

Arguments

• literal - the literal to remove

pub fn add_clause( &mut self, clause: &[SolverLiteral], ctype: ClauseType, ) -> Result<bool, ClingoError>

Add the given clause to the solver.

This method sets its result to false if the current propagation must be stopped for the solver to backtrack.

Attention: No further calls on the control object or functions on the assignment should be called when the result of this method is false.

Arguments

• clause - the clause to add
• ctype - the clause type determining its lifetime

Returns result indicating whether propagation has to be stopped

Errors

• ClingoError::InternalError with ErrorCode::BadAlloc

pub fn propagate(&mut self) -> Result<bool, ClingoError>

Propagate implied literals (resulting from added clauses).

This method sets its result to false if the current propagation must be stopped for the solver to backtrack.

Attention: No further calls on the control object or functions on the assignment should be called when the result of this method is false.

Returns result indicating whether propagation has to be stopped

Errors

• ClingoError::InternalError with ErrorCode::BadAlloc

Trait Implementations

impl Debug for PropagateControl

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.