Module default 

Defines a default crate::semantics::Computation implementation called computation::SynthesizedComputation.

Modules

builder

Builder for Exprs.

codegen

Provides CodeGenerator, a trait for code generation.

computation

Various kinds of computations.

ops

Defines all operations supported by computations, as well as functions to execute the operations.

smtgen

Provides Z3Model and ConcreteZ3Model, SMT models that can be generated for uninstantiated encodings.

Macros

expr

A helper macro that defines an crate::semantics::default::Expr.

Structs

Expr

The expression used in computations. Non-owned version of Expression.

Expression

An owned expression.

Constants

FALSE

An Expr that always returns 0.

MAX_TEMPLATE_ARGS

The maximum number of holes in a single template.

TRUE

An Expr that always returns 1.