ATSLIB/contrib/SMT/Z3/z3

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


  • Z3_mk_int_symbol
  • Z3_mk_string_symbol

  • 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#%"