Struct Assignment

pub struct Assignment {
    pub pos: HashSet<Variable>,
    pub neg: HashSet<Variable>,
}

An Assignment stores a set of positive and negative Variables.

Assignment stores all variables in HashSets, this allows for a fast evaluation of formulas. This might introduce additional costs when creating an assignment. An opposite approach has the Model data-structure. It also stores an assignment, but uses vectors instead of sets. Making it easier to create, but slower to use.

Conversion to Model and vice-versa

Depending of your use case it might be better to have a Model or an Assignment. Both data-structures implement the From trait, such that you can easily swap between both.

Convert from Model to Assignment:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");
let model = Model::new(vec![a], vec![b]);
let assignment = Assignment::from(model);

/// Convert from Assignment to Model:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");
let assignment = Assignment::from_variables(&[a], &[b]);
let model = Model::from(assignment);

Fields

pos: HashSet<Variable>

Set of all positive variables of this assignment.

neg: HashSet<Variable>

Set of all negative variables of this assignment.

Implementations

impl Assignment

pub const fn new(pos: HashSet<Variable>, neg: HashSet<Variable>) -> Self

Creates a new assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let pos = HashSet::from([a]);
let neg = HashSet::from([b]);

let assignment = Assignment::new(pos, neg);

pub fn from_variables(pos: &[Variable], neg: &[Variable]) -> Self

Creates a new assignment from slices.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let assignment = Assignment::from_variables(&[a], &[b]);

pub fn from_lit(lit: Literal) -> Self

Converts a literal into an assignment.

A positive literal is added to the positive variables, and a negative literal to the negative variables.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.lit("a", true);
let b = f.lit("b", false);

let assignment1 = Assignment::from_lit(a);
let assignment2 = Assignment::from_lit(b);

assert!(assignment1.contains_pos(a.variable()));
assert!(assignment2.contains_neg(b.variable()));

pub fn from_literals(literals: &[Literal]) -> Self

Creates an assignment from a single vector of literals.

All positive literals are added to the positive variables, and all negative literals to the negative variables.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.lit("a", true);
let b = f.lit("b", false);

let assignment = Assignment::from_literals(&[a, b]);

assert!(assignment.contains_pos(a.variable()));
assert!(assignment.contains_neg(b.variable()));

pub fn from_set(set: BTreeSet<Literal>) -> Self

Creates an assignment from a single set of literals.

All positive literals are added to the positive variables, and all negative literals to the negative variables.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.lit("a", true);
let b = f.lit("b", false);

let set = BTreeSet::from([a, b]);
let assignment = Assignment::from_set(set);

assert!(assignment.contains_pos(a.variable()));
assert!(assignment.contains_neg(b.variable()));

pub fn from_names( pos: &[&str], neg: &[&str], f: &FormulaFactory, ) -> Result<Self, String>

Creates a new assignment from slices of names.

Uses names of already existing variables and adds those variables to the assignment. If a name has no existing variable in the formula factory, the function will return an error.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let assignment = Assignment::from_names(&["a"], &["b"], &f)?;

assert!(assignment.contains_pos(a));
assert!(assignment.contains_neg(b));

pub const fn pos(&self) -> &HashSet<Variable>

Returns all positive variables of this assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let pos = HashSet::from([a]);
let neg = HashSet::from([b]);

let assignment = Assignment::new(pos.clone(), neg);

assert_eq!(assignment.pos(), &pos);

pub const fn neg(&self) -> &HashSet<Variable>

Returns all negative variables of this assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let pos = HashSet::from([a]);
let neg = HashSet::from([b]);

let assignment = Assignment::new(pos, neg.clone());

assert_eq!(assignment.neg(), &neg);

pub fn len(&self) -> usize

Returns the overall number of positive and negative variables.

A variable added as positive and negative is counted twice.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.len(), 2);

pub fn is_empty(&self) -> bool

Returns true if there is no variable in this assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let assignment1 = Assignment::from_variables(&[a], &[b]);
let assignment2 = Assignment::from_variables(&[], &[]);

assert_eq!(assignment1.is_empty(), false);
assert_eq!(assignment2.is_empty(), true);

pub fn contains_pos(&self, var: Variable) -> bool

Returns true if the given variable is a positive variable in this assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");
let c = f.var("c");

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.contains_pos(a), true);
assert_eq!(assignment.contains_pos(b), false);
assert_eq!(assignment.contains_pos(c), false);

pub fn contains_neg(&self, var: Variable) -> bool

Returns true if the given variable is a negative variable in this assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");
let c = f.var("c");

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.contains_neg(a), false);
assert_eq!(assignment.contains_neg(b), true);
assert_eq!(assignment.contains_neg(c), false);

pub fn contains(&self, lit: Literal) -> bool

Returns true if the variable of the given literal is a variable with the same phase in this assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");
let c = f.var("c");

let lit1 = f.lit("a", true);
let lit2 = f.lit("b", true);
let lit3 = f.lit("c", false);

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.contains(lit1), true);
assert_eq!(assignment.contains(lit2), false);
assert_eq!(assignment.contains(lit3), false);

pub fn evaluate_lit(&self, lit: Literal) -> bool

Evaluates the given literals on this assignment.

It will return true, if the literal is positive and it’s variable is added as positive, or the literal is negative and it’s variable is added as negative or not contained in this assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");
let c = f.var("c");

let lit1 = f.lit("a", true);
let lit2 = f.lit("b", true);
let lit3 = f.lit("c", false);

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.evaluate_lit(lit1), true);
assert_eq!(assignment.evaluate_lit(lit2), false);
assert_eq!(assignment.evaluate_lit(lit3), true);

pub fn restrict_lit(&self, lit: Literal) -> EncodedFormula

Restricts the given literal in this assignment.

It will return a EncodedFormula, which is either a constant, if the variable is contained in the assignment, or it is the passed literal as a formula, if the variable is not in the assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");
let c = f.var("c");

let lit1 = f.lit("a", true);
let lit2 = f.lit("b", true);
let lit3 = f.lit("c", false);

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.restrict_lit(lit1), EncodedFormula::constant(true));
assert_eq!(assignment.restrict_lit(lit2), EncodedFormula::constant(false));
assert_eq!(assignment.restrict_lit(lit3), EncodedFormula::from(lit3));

pub fn blocking_clause( &self, f: &FormulaFactory, variables: Option<&[Variable]>, ) -> EncodedFormula

Creates the blocking clause for this assignment.

pub fn literals(&self) -> Vec<Literal>

Returns a vector of Literal representing this assignment.

All positive variables are returned as positive literals and all negative variables are returned as negative literals. The vector first consists of all positive literals and then of all negative literals.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let lit1 = f.lit("a", true);
let lit2 = f.lit("b", false);

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.literals(), vec![lit1, lit2]);

pub fn string_literals<'a>( &self, f: &'a FormulaFactory, ) -> Vec<StringLiteral<'a>>

Returns a vector of StringLiteral representing this assignment.

All positive variables are returned as positive literals and all negative variables are returned as negative literals. The vector first consists of all positive literals and then of all negative literals.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let lit1 = f.lit("a", true);
let lit2 = f.lit("b", false);

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.string_literals(&f), vec![lit1.to_string_lit(&f), lit2.to_string_lit(&f)]);

pub fn to_string(&self, f: &FormulaFactory) -> String

Creates a string representation of this assignment.

Examples

Basic usage:

let f = FormulaFactory::new();

let a = f.var("a");
let b = f.var("b");

let assignment = Assignment::from_variables(&[a], &[b]);

assert_eq!(assignment.to_string(&f), "Assignment{pos=[a], neg=[b]}");

Trait Implementations

impl Clone for Assignment

fn clone(&self) -> Assignment

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Assignment

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

Formats the value using the given formatter.

impl From<Assignment> for Model

fn from(assignment: Assignment) -> Self

Converts to this type from the input type.

impl<M: AsRef<Model>> From<M> for Assignment

fn from(model: M) -> Self

Converts to this type from the input type.

impl Hash for Assignment

fn hash<H: Hasher>(&self, state: &mut H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Assignment

fn eq(&self, other: &Self) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Assignment