pub struct Assignment(/* private fields */);Expand description
Represents a (partial) assignment of a particular solver.
An assignment assigns truth values to a set of literals.
A literal is assigned to either true or false, or is unassigned (Assignment::truth_value()).
Furthermore, each assigned literal is associated with a decision level (Assignment::level()).
There is exactly one decision literal (Assignment::decision()) for each decision level greater than zero.
Assignments to all other literals on the same level are consequences implied by the current and possibly previous decisions.
Assignments on level zero are immediate consequences of the current program.
Decision levels are consecutive numbers starting with zero up to and including the current decision level (Assignment::decision_level()).
Implementations§
Source§impl Assignment
impl Assignment
Sourcepub fn decision_level(&self) -> u32
pub fn decision_level(&self) -> u32
Get the current decision level.
Sourcepub fn root_level(&self) -> u32
pub fn root_level(&self) -> u32
Get the current root level.
Decisions levels smaller or equal to the root level are not backtracked during solving.
Sourcepub fn has_conflict(&self) -> bool
pub fn has_conflict(&self) -> bool
Check whether the given assignment is conflicting.
Sourcepub fn has_literal(&self, literal: SolverLiteral) -> bool
pub fn has_literal(&self, literal: SolverLiteral) -> bool
Sourcepub fn level(&self, literal: SolverLiteral) -> Result<u32, ClingoError>
pub fn level(&self, literal: SolverLiteral) -> Result<u32, ClingoError>
Determine the decision level of a given literal.
§Arguments
literal- the literal
Returns the decision level of the given literal
Sourcepub fn decision(&self, level: u32) -> Result<SolverLiteral, ClingoError>
pub fn decision(&self, level: u32) -> Result<SolverLiteral, ClingoError>
Determine the decision literal given a decision level.
§Arguments
level- the level
Returns the decision literal for the given decision level
Sourcepub fn is_fixed(&self, literal: SolverLiteral) -> Result<bool, ClingoError>
pub fn is_fixed(&self, literal: SolverLiteral) -> Result<bool, ClingoError>
Check if a literal has a fixed truth value.
§Arguments
literal- the literal
Returns whether the literal is fixed
Sourcepub fn is_true(&self, literal: SolverLiteral) -> Result<bool, ClingoError>
pub fn is_true(&self, literal: SolverLiteral) -> Result<bool, ClingoError>
Check if a literal is true.
§Arguments
literal- the literal Returns whether the literal is true (seeAssignment::truth_value()
Sourcepub fn is_false(&self, literal: SolverLiteral) -> Result<bool, ClingoError>
pub fn is_false(&self, literal: SolverLiteral) -> Result<bool, ClingoError>
Check if a literal has a fixed truth value.
§Arguments
literal- the literal
Returns whether the literal is false (see Assignment::truth_value()
Sourcepub fn truth_value(
&self,
literal: SolverLiteral,
) -> Result<TruthValue, ClingoError>
pub fn truth_value( &self, literal: SolverLiteral, ) -> Result<TruthValue, ClingoError>
Determine the truth value of a given literal.
§Arguments
literal- the literalvalue- the resulting truth value
Returns whether the call was successful
Sourcepub fn at(&self, offset: usize) -> Result<SolverLiteral, ClingoError>
pub fn at(&self, offset: usize) -> Result<SolverLiteral, ClingoError>
The (positive) literal at the given offset in the assignment.
§Arguments
offset- the offset of the literal
Returns the literal
Sourcepub fn is_total(&self) -> bool
pub fn is_total(&self) -> bool
Check if the assignmen is total, i.e. there are no free literal.
Sourcepub fn trail_size(&self) -> Result<u32, ClingoError>
pub fn trail_size(&self) -> Result<u32, ClingoError>
Returns the number of literals in the trail, i.e., the number of assigned literals.
Sourcepub fn trail_begin(&self, level: u32) -> Result<u32, ClingoError>
pub fn trail_begin(&self, level: u32) -> Result<u32, ClingoError>
Returns the offset of the decision literal with the given decision level in the trail.
**Note:**SolverLiterals in the trail are ordered by decision levels, where the first literal with a larger level than the previous literals is a decision; the following literals with same level are implied by this decision literal. Each decision level up to and including the current decision level has a valid offset in the trail.
§Arguments
level- the decision level
Returns the offset of the decision literal
Sourcepub fn trail_end(&self, level: u32) -> Result<u32, ClingoError>
pub fn trail_end(&self, level: u32) -> Result<u32, ClingoError>
Returns the offset following the last literal with the given decision level.
Note: This function is the counter part to clingo_assignment_trail_begin().
§Arguments
level- the decision level
Returns the offset
Sourcepub fn trail_at(&self, offset: u32) -> Result<SolverLiteral, ClingoError>
pub fn trail_at(&self, offset: u32) -> Result<SolverLiteral, ClingoError>
Returns the literal at the given position in the trail.
§Arguments
offset- the offset of the literal
Returns the literal