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.