Struct PropagateInit 

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

Object to initialize a user-defined propagator before each solving step.

Each symbolic (SymbolicAtoms) or theory atom (TheoryAtoms) is uniquely associated with an aspif atom in form of a positive integer (SolverLiteral). Aspif literals additionally are signed to represent default negation. Furthermore, there are non-zero integer solver literals (also represented using SolverLiteral. There is a surjective mapping from program atoms to solver literals.

All methods called during propagation use solver literals whereas SymbolicAtom::literal() and TheoryAtoms::atom_literal() return program literals. The function PropagateInit::solver_literal() can be used to map program literals or condition ids(TheoryAtoms::element_condition_id()) to solver literals.

Implementations

impl PropagateInit

pub fn solver_literal( &self, SolverLiteral: SolverLiteral, ) -> Result<SolverLiteral, ClingoError>

Map the given program literal or condition id to its solver literal.

Arguments

• aspif_literal - the aspif literal to map

Returns the corresponding solver literal

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

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

Arguments

• solver_literal - the solver literal

pub fn add_watch_to_thread( &mut self, SolverLiteral: SolverLiteral, thread_id: u32, ) -> Result<(), ClingoError>

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

Arguments

• solver_literal - the solver literal
• thread_id - the id of the solver thread

pub fn symbolic_atoms(&self) -> Result<&SymbolicAtoms, ClingoError>

Get an object to inspect the symbolic atoms.

pub fn theory_atoms(&self) -> Result<&TheoryAtoms, ClingoError>

Get an object to inspect the theory atoms.

pub fn number_of_threads(&self) -> usize

Get the number of threads used in subsequent solving.

See: PropagateControl::thread_id()

pub fn set_check_mode(&mut self, mode: PropagatorCheckMode)

Configure when to call the check method of the propagator.

Arguments

• mode - bitmask when to call the propagator

See: Propagator::check()

pub fn get_check_mode(&self) -> Result<PropagatorCheckMode, ClingoError>

Get the current check mode of the propagator.

Returns bitmask when to call the propagator

See: PropagateInit::set_check_mode()

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

Get the top level assignment solver.

Returns the assignment

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

Add a literal to the solver.

To be able to use the variable in clauses during propagation or add watches to it, it has to be frozen. Otherwise, it might be removed during preprocessing.

Attention If varibales were added, subsequent calls to functions adding constraints or ::clingo_propagate_init_propagate() are expensive. It is best to add varables in batches.

Arguments

• freeze - whether to freeze the literal Returns the added literal

Errors

• ClingoError::InternalError with ErrorCode::BadAlloc

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

Add the given clause to the solver.

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

Arguments

• clause - the clause to add

Returns whether the problem became unsatisfiable

Errors

• ClingoError::InternalError with ErrorCode::BadAlloc

pub fn add_weight_constraint( &mut self, literal: SolverLiteral, literals: &[WeightedLiteral], bound: i32, wctype: WeigthConstraintType, compare_equal: bool, ) -> Result<bool, ClingoError>

Add the given weight constraint to the solver.

This function adds a constraint of form literal <=> { lit=weight | (lit, weight) in literals } >= bound to the solver. Depending on the type the <=> connective can be either a left implication, right implication, or equivalence.

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

• literal - the literal of the constraint
• literals - the weighted literals
• bound - the bound of the constraint
• wctype - the type of the weight constraint
• compare_equal - if true compare equal instead of less than equal

Returns result indicating whether the problem became unsatisfiable

Errors

• ClingoError::InternalError with ErrorCode::BadAlloc

pub fn add_minimize( &mut self, literal: SolverLiteral, weight: i32, priority: i32, ) -> Result<(), ClingoError>

Add the given literal to minimize to the solver.

This corresponds to a weak constraint of form :~ literal. [weight@priority].

• literal - the literal to minimize
• weight - the weight of the literal
• priority - the priority of the literal

Errors

• ClingoError::InternalError with ErrorCode::BadAlloc

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

Propagates consequences of the underlying problem excluding registered propagators.

Note The function has no effect if SAT-preprocessing is enabled.

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

Returns result indicating whether the problem became unsatisfiable

Errors

• ClingoError::InternalError with ErrorCode::BadAlloc

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

Remove the watch for the solver literal in the given phase.

Arguments

• literal - the solver literal

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

Remove the watch for the solver literal in the given phase from the given solver thread.

• literal - the solver literal
• thread_id- the id of the solver thread

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

Freeze the given solver literal.

Any solver literal that is not frozen is subject to simplification and might be removed in a preprocessing step after propagator initialization. A propagator should freeze all literals over which it might add clauses during propagation. Note that any watched literal is automatically frozen and that it does not matter which phase of the literal is frozen.

• literal - the solver literal

Trait Implementations

impl Debug for PropagateInit

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

Formats the value using the given formatter.