Struct rsmt2::actlit::Actlit

pub struct Actlit { /* private fields */ }

An activation literal is an opaque wrapper around a usize.

Obtained by a call to Solver::get_actlit.

Implementations

impl Actlit

pub fn uid(&self) -> usize

Unique number of this actlit.

pub fn write<W>(&self, w: &mut W) -> SmtRes<()>where
    W: Write,

Writes the actlit as an SMT-LIB 2 symbol.

pub fn implies<Expr>(&self, expr: Expr) -> CondExpr<Expr>

Builds an implication between an actlit and an expression.

Allows to use normal assert function over Solver.

let mut solver = Solver::default_z3(()).expect("failed to spawn solver");
let actlit = solver.get_actlit().expect("failed to declare actlit");
let conditional = actlit.implies("(> 0 1)");
solver.assert(&conditional).expect("failed to assert conditional expr");
let is_sat = solver.check_sat_assuming(Some(&actlit)).expect("failed to perform check-sat");
assert!(!is_sat);

Methods from Deref<Target = usize>

pub const MIN: usize = 0usize

pub const MAX: usize = 4_294_967_295usize

pub const BITS: u32 = 32u32

Trait Implementations

impl AsRef<Actlit> for Actlit

fn as_ref(&self) -> &Self

Converts this type into a shared reference of the (usually inferred) input type.

impl Debug for Actlit

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

Formats the value using the given formatter.

impl Deref for Actlit

type Target = usize

The resulting type after dereferencing.

fn deref(&self) -> &usize

Dereferences the value.

impl Expr2Smt<()> for Actlit

fn expr_to_smt2<Writer>(&self, w: &mut Writer, _: ()) -> SmtRes<()>where
    Writer: Write,

Prints an expression to a writer given some info.

fn to_smt_named<Sym>(self, name: Sym) -> NamedExpr<Sym, Self, Info>where
    Sym: Sym2Smt,
    Self: Sized,

Gives a name to an expression (owned version).

fn as_smt_named<Sym>(&self, name: Sym) -> NamedExpr<Sym, &Self, Info>where
    Sym: Sym2Smt,
    Self: Sized,

Gives a name to an expression (borrowed version).

impl Sym2Smt<()> for Actlit

fn sym_to_smt2<Writer>(&self, w: &mut Writer, _: ()) -> SmtRes<()>where
    Writer: Write,

Prints a symbol to a writer given some info.