Module mikino_api::prelude

Common imports throughout this project.

Re-exports

pub use crate::ast;

pub use crate::build_decls;

pub use crate::build_expr;

pub use crate::build_trans;

pub use crate::build_typ;

pub use crate::check;

pub use crate::err::*;

pub use crate::expr;

pub use crate::expr::HasTyp;

pub use crate::expr::Typ;

pub use crate::parse;

pub use crate::parse::Span;

pub use crate::parse::Spn;

pub use crate::script;

pub use crate::solver::SFSolver;

pub use crate::solver::SLSolver;

pub use crate::trans;

Macros

bail

Exits a function early with an error

Structs

Int

A big signed integer type.

RSmtParser

SMT-LIB 2.0 parser.

SmtConf

Configuration and solver specific info.

SmtSolver

Solver providing most of the SMT-LIB 2.5 commands.

Enums

Either

The enum Either with variants Left and Right is a general purpose sum type with two cases.

Sign

A Sign is a BigInt’s composing element.

Traits

One

Defines a multiplicative identity element for Self.

Style

Style trait.

Zero

Defines an additive identity element for Self.

Functions

z3_cmd_to_conf

Generates an SmtConf from a Z3 command with arguments.

Type Definitions

Rat

Alias for arbitrary precision rationals.

SmtRes

Convenient wrapper around std::Result.

Unroll

Step index.