Struct Axiom 

pub struct Axiom<T: Types> {
    pub name: String,
    pub args: Vec<(T::Var, Sort<T>)>,
    pub body: Expr<T>,
    pub patterns: Vec<Expr<T>>,
}

A fact that is asserted to the SMT solver, universally quantified over args.

Fields

name: String

args: Vec<(T::Var, Sort<T>)>

body: Expr<T>

patterns: Vec<Expr<T>>

The terms of the (multi-)pattern used by the SMT solver to instantiate the axiom, i.e., the axiom is instantiated when all of them are matched.

Trait Implementations

impl<T: Types> Clone for Axiom<T>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T: Types> Debug for Axiom<T>

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

Formats the value using the given formatter.

impl<T: Types> Display for Axiom<T>

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

Formats the value using the given formatter.

impl<T: Types> Hash for Axiom<T>

fn hash<__H: Hasher>(&self, __state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.