Enum Logic

pub enum Logic {
    QF_UF,
    QF_LIA,
    QF_NIA,
    QF_LRA,
    QF_AUFLIA,
    AUFLIA,
    AUFLIRA,
    AUFNIRA,
    LRA,
    QF_BV,
    QF_UFBV,
    QF_ABV,
    QF_AUFBV,
}

SMT-LIB 2 logics, used with Solver::set_logic.

Variants

QF_UF

Quantifier-free uninterpreted functions.

QF_LIA

Quantifier-free linear integer arithmetic.

QF_NIA

Quantifier-free non-linear integer arithmetic.

QF_LRA

Quantifier-free linear real arithmetic.

QF_AUFLIA

Quantifier-free arrays, uninterpreted functions, linear integer arithmetic.

AUFLIA

Arrays, uninterpreted functions, linear integer arithmetic.

AUFLIRA

Arrays, uninterpreted functions, linear integer/real arithmetic.

AUFNIRA

arrays, uninterpreted functions, non-linear integer/real arithmetic.

LRA

Linear real arithmetic.

QF_BV

Quantifier-free fixed-size bitvectors.

QF_UFBV

Quantifier-free uninterpreted functions, fixed-size bitvectors.

QF_ABV

Quantifier-free arrays, fixed-size bitvectors.

QF_AUFBV

Quantifier-free arrays, uninterpreted functions, fixed-size bitvectors.

Implementations

impl Logic

pub fn to_smt2<W: Write>(self, writer: &mut W, _: ()) -> SmtRes<()>

Prints the logic in a writer in SMT-LIB 2 format.

Trait Implementations

impl Clone for Logic

fn clone(&self) -> Logic

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Display for Logic

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

Formats the value using the given formatter.

impl Copy for Logic