Enum Logic

pub enum Logic {
    AUFLIA,
    AUFLIRA,
    AUFNIRA,
    LIA,
    LRA,
    QF_ABV,
    QF_AUFBV,
    QF_AUFLIA,
    QF_AX,
    QF_BV,
    QF_IDL,
    QF_LIA,
    QF_LRA,
    QF_NIA,
    QF_NRA,
    QF_RDL,
    QF_UF,
    QF_UFBV,
    QF_UFIDL,
    QF_UFLIA,
    QF_UFLRA,
    QF_UFNRA,
    UFLRA,
    UFNIA,
    Custom(String),
}

Logics allow specifictation of which (sub-)logic should be used by a solver.

A more detailed description of logics can be found on the SMT-LIB website.

Variants

AUFLIA

Closed formulas built over arbitrary expansions of the Ints and ArraysEx signatures with free sort and function symbols, but with the following restrictions:

• all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes;
• all array terms have sort (Array Int Int).

AUFLIRA

Closed formulas built over arbitrary expansions of the Reals_Ints and ArraysEx signatures with free sort and function symbols, but with the following restrictions:

• all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes;
• all terms of sort Real are linear, that is, have no occurrences of the function symbols * and /, except as specified in the :extensions attribute;
• all array terms have sort (Array Int Real) or (Array Int (Array Int Real)).

AUFNIRA

Closed formulas built over arbitrary expansions of the Reals_Ints and ArraysEx signatures with free sort and function symbols.

LIA

Closed formulas built over an arbitrary expansion of the Ints signature with free constant symbols, but whose terms of sort Int are all linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified the :extensions attribute.

LRA

Closed formulas built over arbitrary expansions of the Reals signature with free constant symbols, but containing only linear atoms, that is, atoms with no occurrences of the function symbols * and /, except as specified the :extensions attribute.

QF_ABV

Closed quantifier-free formulas built over the FixedSizeBitVectors and ArraysEx signatures, with the restriction that all array terms have sort of the form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.

QF_AUFBV

Closed quantifier-free formulas built over an arbitrary expansion of the FixedSizeBitVectors and ArraysEx signatures with free sort and function symbols, but with the restriction that all array terms have sort of the form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.

QF_AUFLIA

Closed quantifier-free formulas built over arbitrary expansions of the Ints and ArraysEx signatures with free sort and function symbols, but with the following restrictions:

• all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes;
• all array terms have sort (Array Int Int).

QF_AX

Closed quantifier-free formulas built over an arbitrary expansion of the ArraysEx signature with free sort and constant symbols.

QF_BV

Closed quantifier-free formulas built over an arbitrary expansion of the FixedSizeBitVectors signature with free constant symbols over the sorts (_ BitVec m) for 0 < m. Formulas in ite terms must satisfy the same restriction as well, with the exception that they need not be closed (because they may be in the scope of a let binder).

QF_IDL

Closed quantifier-free formulas with atoms of the form:

• q
• (op (- x y) n),
• (op (- x y) (- n)), or
• (op x y) where
  • q is a variable or free constant symbol of sort Bool,
  • op is <, <=, >, >=, =, or distinct,
  • x, y are free constant symbols of sort Int,
  • n is a numeral.

QF_LIA

Closed quantifier-free formulas built over an arbitrary expansion of the Ints signature with free constant symbols, but whose terms of sort Int are all linear, that is, have no occurrences of the function symbols /, div, mod, and abs, and no occurrences of the function symbol *, except as specified in the :extensions attribute.

QF_LRA

Closed quantifier-free formulas built over arbitrary expansions of the Reals signature with free constant symbols, but containing only linear atoms, that is, atoms with no occurrences of the function symbols * and /, except as specified the :extensions attribute.

QF_NIA

Closed quantifier-free formulas built over an arbitrary expansion of the Ints signature with free constant symbols.

QF_NRA

Closed quantifier-free formulas built over arbitrary expansions of the Reals signature with free constant symbols.

QF_RDL

Closed quantifier-free formulas with atoms of the form:

• p
• (op (- x y) c),
• (op x y),
• (op (- (+ x … x) (+ y … y)) c) with n > 1 occurrences of x and of y, where
  • p is a variable or free constant symbol of sort Bool,
  • c is an expression of the form m or (- m) for some numeral m,
  • op is <, <=, >, >=, =, or distinct,
  • x, y are free constant symbols of sort Real.

QF_UF

Closed quantifier-free formulas built over an arbitrary expansion of the Core signature with free sort and function symbols.

QF_UFBV

Closed quantifier-free formulas built over arbitrary expansions of the FixedSizeBitVectors signature with free sort and function symbols.

QF_UFIDL

Closed quantifier-free formulas built over an arbitrary expansion with free sort and function symbols of the signature consisting of

• all the sort and function symbols of Core and

• the following symbols of Int:

  :sorts ((Int 0)) :funs ((NUMERAL Int) (- Int Int Int) (+ Int Int Int) (<= Int Int Bool) (< Int Int Bool) (>= Int Int Bool) (> Int Int Bool) )

Additionally, for every term of the form (op t1 t2) with op in {+, -}, at least one of t1 and t2 is a numeral.

QF_UFLIA

Closed quantifier-free formulas built over arbitrary expansions of the Ints signatures with free sort and function symbols, but with the following restrictions:

• all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes;

QF_UFLRA

Closed quantifier-free formulas built over arbitrary expansions of the Reals signature with free sort and function symbols, but containing only linear atoms, that is, atoms with no occurrences of the function symbols * and /, except as specified the :extensions attribute.

QF_UFNRA

Closed quantifier-free formulas built over arbitrary expansions of the Reals signature with free sort and function symbols.

UFLRA

Closed formulas built over arbitrary expansions of the Reals signature with free sort and function symbols, but containing only linear atoms, that is, atoms with no occurrences of the function symbols * and /, except as specified the :extensions attribute.

UFNIA

Closed formulas built over an arbitrary expansion of the Ints signature with free sort and function symbols.

Custom(String)

A fallback variant in case the user wants to specify some logic which is not part of the predefined collection.

Implementations

impl Logic

pub fn name(&self) -> Cow<'static, str>

Returns the name of the logic.

Trait Implementations

impl Display for Logic

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

Formats the value using the given formatter.