From f183843fa211b05dbe7af157c1418744079a208b Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Tue, 31 Oct 2023 23:09:30 -0700 Subject: [PATCH] api test --- tests/api/test_model_hint.c | 233 ++++++++++++++++++++++++++++++++++++ 1 file changed, 233 insertions(+) create mode 100644 tests/api/test_model_hint.c diff --git a/tests/api/test_model_hint.c b/tests/api/test_model_hint.c new file mode 100644 index 000000000..2a5da6273 --- /dev/null +++ b/tests/api/test_model_hint.c @@ -0,0 +1,233 @@ +/* + * Examples of check_with_model and model interpolants + */ + +#include +#include +#include + +#include "assert.h" + +#include + +/* + * Create an MCSAT context that supports model interpolants + */ +static context_t *make_mcsat_context(void) { + ctx_config_t *config; + context_t *context; + int32_t code; + + config = yices_new_config(); + code = yices_set_config(config, "solver-type", "mcsat"); + if (code < 0) goto error; + code = yices_set_config(config, "model-interpolation", "true"); + if (code < 0) goto error; + context = yices_new_context(config); + if (context == NULL) goto error; + yices_free_config(config); + return context; + + error: + yices_print_error(stderr); + yices_free_config(config); + return NULL; +} + +/* + * Create assertion x^2 + y^2 < 1 + * - return terms x and y in var: + * var[0] = x + * var[1] = y + */ +static term_t make_circle_constraint(term_t var[2]) { + type_t real; + term_t x, y, p; + + real = yices_real_type(); + x = yices_new_uninterpreted_term(real); + yices_set_term_name(x, "x"); + y = yices_new_uninterpreted_term(real); + yices_set_term_name(y, "y"); + + var[0] = x; + var[1] = y; + + p = yices_add(yices_square(x), yices_square(y)); // p is x^2 + y^2 + return yices_arith_lt_atom(p, yices_int32(1)); // p < 1 +} + +/* + * Create an unsat assertion: x^2 + y^2 < 1 AND x>2 + * - return variables x and y in var[0] and var[1], respectively. + */ +static term_t make_unsat_constraint(term_t var[2]) { + term_t p1, p2; + + p1 = make_circle_constraint(var); // x^2 + y^2 < 1 + p2 = yices_arith_gt_atom(var[0], yices_int32(2)); // x>2 + return yices_and2(p1, p2); +} + + +/* + * Check with model + */ +static smt_status_t check_with_model_and_hint(context_t *ctx, model_t *model, term_t assertion, uint32_t n, const term_t t[], uint32_t m) { + int32_t code = yices_assert_formula(ctx, assertion); + if (code < 0) { + yices_print_error(stderr); + exit(1); + } + + return yices_check_context_with_model_and_hint(ctx, NULL, model, n, t, m); +} + + +static void check_with_sat_model(bool use_hint) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + int32_t code; + + ctx = make_mcsat_context(); + assertion = make_circle_constraint(vars); // x^2 + y^2 < 1 + + model = yices_new_model(); + code = yices_model_set_int32(model, vars[0], 0); // x == 0 + if (code < 0) { + yices_print_error(stderr); + exit(1); + } + + smt_status_t status; + if (use_hint) { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 0); + assert(status == STATUS_SAT); + } else { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 1); + assert(status == STATUS_SAT); + } + yices_free_model(model); + yices_free_context(ctx); +} + + +static void check_with_unsat_model(bool use_hint) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + int32_t code; + + ctx = make_mcsat_context(); + assertion = make_circle_constraint(vars); // x^2 + y^2 < 1 + + model = yices_new_model(); + code = yices_model_set_int32(model, vars[0], 1); // x == 1 + if (code < 0) { + yices_print_error(stderr); + exit(1); + } + + smt_status_t status; + if (use_hint) { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 0); + assert(status == STATUS_SAT); + } else { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 1); + assert(status == STATUS_UNSAT); + } + yices_free_model(model); + yices_free_context(ctx); +} + +static void check_sat_with_empty_model(void) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + + ctx = make_mcsat_context(); + assertion = make_circle_constraint(vars); // x^2 + y^2 < 1 + + model = yices_new_model(); + + smt_status_t status; + status = check_with_model_and_hint(ctx, model, assertion, 0, vars, 0); + assert(status == STATUS_SAT); + yices_free_model(model); + yices_free_context(ctx); +} + +static void check_unsat_with_empty_model(void) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + + ctx = make_mcsat_context(); + assertion = make_unsat_constraint(vars); + + model = yices_new_model(); + + smt_status_t status; + status = check_with_model_and_hint(ctx, model, assertion, 0, vars, 0); + assert(status == STATUS_UNSAT); + + yices_free_model(model); + yices_free_context(ctx); +} + +static void check_unsat_with_model(bool use_hint) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + int32_t code; + + ctx = make_mcsat_context(); + assertion = make_unsat_constraint(vars); + + model = yices_new_model(); + code = yices_model_set_int32(model, vars[0], 0); // x == 0 + if (code < 0) { + yices_print_error(stderr); + exit(1); + } + + smt_status_t status; + if (use_hint) { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 0); + assert(status == STATUS_UNSAT); + } else { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 1); + assert(status == STATUS_UNSAT); + } + + yices_free_model(model); + yices_free_context(ctx); +} + + +int main(void) { + yices_init(); + if (yices_has_mcsat()) { + printf("MCSAT supported\n"); + check_with_sat_model(false); + check_with_sat_model(true); + check_with_unsat_model(false); + check_with_unsat_model(true); + check_sat_with_empty_model(); + check_unsat_with_empty_model(); + check_unsat_with_model(false); + check_unsat_with_model(true); + } else { + printf("MCSAT not supported\n"); + } + yices_exit(); + + return 0; +} +