ATSLIB/contrib/SMT/Z3/z3

This package contains an API for programming the SMT-solver Z3 in ATS.

Z3_mk_true

Synopsis

fun Z3_mk_true (ctx: !Z3_context): Z3_ast = "mac#%"

Z3_mk_false

Synopsis

fun Z3_mk_false (ctx: !Z3_context): Z3_ast = "mac#%"

Z3_mk_eq

Synopsis

fun Z3_mk_eq
(
  ctx: !Z3_context, left: !Z3_ast, right: !Z3_ast
) : Z3_ast = "mac#%" // end of [Z3_mk_eq]

Z3_mk_or2

Synopsis

fun Z3_mk_or2
  (ctx: !Z3_context, a1: !Z3_ast, a2: !Z3_ast): Z3_ast = "mac#%"

Z3_mk_and2

Synopsis

fun Z3_mk_and2
  (ctx: !Z3_context, a1: !Z3_ast, a2: !Z3_ast): Z3_ast = "mac#%"