Struct clingo::PropagateControl

pub struct PropagateControl(_);

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

Methods

impl PropagateControl

pub fn thread_id(&mut self) -> u32

Get the id of the underlying solver thread.

Thread ids are consecutive numbers starting with zero.

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

Get the assignment associated with the underlying solver.

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

Get the assignment associated with the underlying solver.

pub fn add_literal(&mut self, result: &mut Literal) -> 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:

• ErrorType::BadAlloc
• ErrorType::Logic if the assignment is conflicting

pub fn add_watch(&mut self, literal: Literal) -> 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:

• ErrorType::BadAlloc
• ErrorType::Logic if the literal is invalid

See: PropagateControl::remove_watch()

pub fn has_watch(&self, literal: Literal) -> 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: Literal)

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: &[Literal],
    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

Errors

• ErrorType::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

• ErrorType::BadAlloc

Trait Implementations

impl Debug for PropagateControl

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Copy for PropagateControl

impl Clone for PropagateControl

fn clone(&self) -> PropagateControl

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.