ATSLIB/contrib/SMT/Z3/z3

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

Z3_mk_int_symbol

Synopsis

fun Z3_mk_int_symbol
  (ctx: !Z3_context, i: int): Z3_symbol = "mac#%"

Z3_mk_string_symbol

Synopsis

fun Z3_mk_string_symbol
  (ctx: !Z3_context, str: Z3_string): Z3_symbol = "mac#%"