Struct satoxid::constraints::Expr

pub struct Expr<V> { /* fields omitted */ }

Tseytin Encoding of propositional logic formulas.

Allows encoding of arbitrary boolean formulas. It implements the BitAnd, BitOr and Not traits, which should be used for the construction of boolean formulas.

Example

let expr = !(Expr::new("a") | "b") & "c"; // encoding the formula !(a | b) & c
encoder.add_constraint(expr);

if let Some(model) = encoder.solve() {
    assert!(model.lit(Lit::Neg("a")).unwrap());
    assert!(model.lit(Lit::Neg("b")).unwrap());
    assert!(model.lit(Lit::Pos("c")).unwrap());
}

NOTE: If you just want to ‘and’ or ‘or’ a bunch of literals use And or Or for more efficient encodings.

Implementations

impl<V: SatVar> Expr<V>

pub fn from_constraint<C>(constraint: C) -> Self where
    C: ConstraintRepr<V> + 'static, 

Create new Expr from given constraint.

impl<V: SatVar> Expr<V>

pub fn new<L>(l: L) -> Self where
    L: Into<VarType<V>>, 

Create new Expr from literal.

Trait Implementations

impl<V, R: Into<Self>> BitAnd<R> for Expr<V>

type Output = Expr<V>

The resulting type after applying the & operator.

fn bitand(self, rhs: R) -> Self::Output

Performs the & operation.

impl<V, R: Into<Self>> BitOr<R> for Expr<V>

type Output = Expr<V>

The resulting type after applying the | operator.

fn bitor(self, rhs: R) -> Self::Output

Performs the | operation.

impl<V: Clone> Clone for Expr<V>

fn clone(&self) -> Expr<V>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<V: SatVar> Constraint<V> for Expr<V>

fn encode<B: Backend>(self, backend: &mut B, varmap: &mut VarMap<V>)

Encode Self as an constraint using solver.

impl<V: SatVar> ConstraintRepr<V> for Expr<V>

fn encode_constraint_implies_repr<B: Backend>(
    self,
    repr: Option<i32>,
    backend: &mut B,
    varmap: &mut VarMap<V>
) -> i32

Encode if Self is satisified, that repr is true. Otherwise repr is not constrained and can be true or false.

fn encode_constraint_equals_repr<B: Backend>(
    self,
    repr: Option<i32>,
    backend: &mut B,
    varmap: &mut VarMap<V>
) -> i32

Encode if and only if Self is satisified, that repr is true.

fn encode_constraint_repr_cheap<B: Backend>(
    self,
    repr: Option<i32>,
    backend: &mut B,
    varmap: &mut VarMap<V>
) -> i32

Encode that repr is true if the constraint is satisfied. The implementation can decide if it has the semantics of encode_constraint_implies_repr or encode_constraint_equals_repr, depending on what is cheaper to encode.

impl<V: Debug> Debug for Expr<V>

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

Formats the value using the given formatter.

impl<V: SatVar, L: Into<VarType<V>>> From<L> for Expr<V>

fn from(l: L) -> Self

Performs the conversion.

impl<V> Not for Expr<V>

type Output = Self

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.