63 lines · cpp
1#include <cassert>2#include <dlfcn.h>3#include <cstdio>4#include <cstdlib>5#include <cstring>6 7#include <z3.h>8 9static char *Z3ResultsBegin;10static char *Z3ResultsCursor;11 12static __attribute__((constructor)) void init() {13 const char *Env = getenv("Z3_SOLVER_RESULTS");14 if (!Env) {15 fprintf(stderr, "Z3_SOLVER_RESULTS envvar must be defined; abort\n");16 abort();17 }18 Z3ResultsBegin = strdup(Env);19 Z3ResultsCursor = Z3ResultsBegin;20 if (!Z3ResultsBegin) {21 fprintf(stderr, "strdup failed; abort\n");22 abort();23 }24}25 26static __attribute__((destructor)) void finit() {27 if (strlen(Z3ResultsCursor) > 0) {28 fprintf(stderr, "Z3_SOLVER_RESULTS should have been completely consumed "29 "by the end of the test; abort\n");30 abort();31 }32 free(Z3ResultsBegin);33}34 35static bool consume_token(char **pointer_to_cursor, const char *token) {36 assert(pointer_to_cursor);37 int len = strlen(token);38 if (*pointer_to_cursor && strncmp(*pointer_to_cursor, token, len) == 0) {39 *pointer_to_cursor += len;40 return true;41 }42 return false;43}44 45Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s) {46 consume_token(&Z3ResultsCursor, ",");47 48 if (consume_token(&Z3ResultsCursor, "UNDEF")) {49 printf("Z3_solver_check returns UNDEF\n");50 return Z3_L_UNDEF;51 }52 if (consume_token(&Z3ResultsCursor, "SAT")) {53 printf("Z3_solver_check returns SAT\n");54 return Z3_L_TRUE;55 }56 if (consume_token(&Z3ResultsCursor, "UNSAT")) {57 printf("Z3_solver_check returns UNSAT\n");58 return Z3_L_FALSE;59 }60 fprintf(stderr, "Z3_SOLVER_RESULTS was exhausted; abort\n");61 abort();62}63