ATSLIB/contrib/SMT/Z3/z3

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

Z3_set_ast_print_mode

Synopsis

fun Z3_set_ast_print_mode
  (ctx: !Z3_context, mode: Z3_ast_print_mode): void

Z3_ast_to_string

Synopsis

fun Z3_ast_to_string (ctx: !Z3_context, a: !Z3_ast): vStrptr1

Z3_pattern_to_string

Synopsis

fun Z3_pattern_to_string (ctx: !Z3_context, p: !Z3_pattern): vStrptr1

Z3_func_decl_to_string

Synopsis

fun Z3_func_decl_to_string (ctx: !Z3_context, d: !Z3_func_decl): vStrptr1

Z3_model_to_string

Synopsis

fun Z3_model_to_string (ctx: !Z3_context, m: !Z3_model): vStrptr1