z3-example.c

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <z3.h>

int main(int argc, char** argv)
{
  Z3_config cfg = Z3_mk_config();
  Z3_context ctx = Z3_mk_context(cfg);
  Z3_solver solver = Z3_mk_solver(ctx);

  Z3_sort s = Z3_mk_int_sort(ctx);
  Z3_ast x = Z3_mk_fresh_const(ctx, "x", s);
  /*Z3_func_decl d = Z3_mk_fresh_func_decl(ctx, NULL, 0, 0, Z3_mk_int_sort(ctx));*/
  /*Z3_ast x = Z3_mk_app(ctx, d, 0, 0);*/

  Z3_symbol y_name = Z3_mk_string_symbol(ctx, "y");
  Z3_ast y = Z3_mk_const(ctx, y_name, s);
  Z3_ast zero = Z3_mk_int64(ctx, 0, s);

  Z3_symbol z_name = Z3_mk_int_symbol(ctx, 2);
  Z3_ast z = Z3_mk_const(ctx, z_name, s);

  Z3_solver_inc_ref(ctx, solver);

  Z3_ast ast = Z3_mk_gt(ctx, x, zero);
  Z3_ast ast2 = Z3_mk_gt(ctx, y, zero);
  Z3_ast ast3 = Z3_mk_gt(ctx, z, zero);
  Z3_solver_assert(ctx, solver, ast);
  Z3_solver_assert(ctx, solver, ast2);
  Z3_solver_assert(ctx, solver, ast3);

  int result = Z3_solver_check(ctx, solver) == Z3_L_TRUE;
  printf("result: %d\n", result);
  if (!result) { return 127; }

  Z3_model model = Z3_solver_get_model(ctx, solver);
  Z3_model_inc_ref(ctx, model);

  Z3_string modelAsString;
  modelAsString = Z3_model_to_string(ctx, model);
  printf("Model:\n%s\n", modelAsString);


	return 0;
}