Struct rsmt2::actlit::Actlit

pub struct Actlit { /* fields omitted */ }

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.

Trait Implementations

impl Debug for Actlit

pub 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.

pub fn deref(&self) -> &usize

Dereferences the value.

impl Expr2Smt<()> for Actlit

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

Prints an expression to a writer given some info.