ATSLIB/contrib/SMT/Z3/z3

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

Z3_solver_get_model

Synopsis

fun
Z3_solver_get_model
  {l:addr}
(
  ctx: !Z3_context, s: !Z3_solver l
) : [l2:addr]
(
  minus (Z3_solver l, Z3_model l2) | Z3_model l2
) // end of [Z3_solver_get_model]