Module uvls::smt::smt_lib

Structs

• Assert
• AssertInfo
• SMTBuilder 🔒
• SMTModule
  This is a helper module, to use SMT (and in that sense Z3) for every UVL Module A smt-lib module equivalent to some UVL source module.

Enums

• AssertName
• Expr

Functions

• translate_constraint 🔒
  Translates the constraints into Expressions which can be converted to Z3 Statements
• translate_expr 🔒
  Translates expr into Expressions which can be converted to Z3 Statements
• uvl2smt
  Converts a UVL Module into a SMT Module
• uvl2smt_constraints
  create an SMTModule, but the asserts are only constraints