Enum Logic

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

SMT Lib 2 logics.

See Solver::set_logic.

Variants

QF_UFBV

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

Quantifier-free 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.

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