1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * EXAMPLE USE OF THE MCSAT SOLVER
21 */
22
23 #include <assert.h>
24 #include <stdbool.h>
25 #include <stdio.h>
26 #include <inttypes.h>
27 #include <stdlib.h>
28
29 #include <poly/algebraic_number.h>
30
31 #include "yices.h"
32
33 /*
34 * Print an error message then exit
35 */
print_error(void)36 static void print_error(void) {
37 char *s;
38
39 s = yices_error_string();
40 fprintf(stderr, "Yices error: %s\n", s);
41 yices_free_string(s);
42 exit(1);
43 }
44
45 /*
46 * Convert to string
47 */
term_to_string(term_t term)48 static char *term_to_string(term_t term) {
49 char *s;
50
51 s = yices_term_to_string(term, 80, 20, 0);
52 if (s == NULL) print_error();
53 return s;
54 }
55
56 /*
57 * Create a real variable.
58 */
declare_var(const char * name)59 static term_t declare_var(const char *name) {
60 term_t x;
61
62 x = yices_new_uninterpreted_term(yices_real_type());
63 if (x < 0) print_error();
64 yices_set_term_name(x, name);
65 return x;
66 }
67
68
69 /*
70 * Create a context for QF_NRA
71 */
make_context(void)72 static context_t *make_context(void) {
73 ctx_config_t *cfg;
74 context_t *ctx;
75 int32_t code;
76
77 /*
78 * We set the logic to QF_NRA and mode to "one-shot"
79 * (one-shot is currently required when MCSAT is used).
80 */
81 cfg = yices_new_config();
82 code = yices_default_config_for_logic(cfg, "QF_NRA");
83 if (code < 0) print_error();
84 code = yices_set_config(cfg, "mode", "one-shot");
85 if (code < 0) print_error();
86
87 ctx = yices_new_context(cfg);
88 if (ctx == NULL) print_error();
89 yices_free_config(cfg);
90
91 return ctx;
92 }
93
94
95 /*
96 * Print the value of term t in mdl as an algebraic number
97 */
show_algebraic_value(model_t * mdl,term_t t)98 static void show_algebraic_value(model_t *mdl, term_t t) {
99 lp_algebraic_number_t n;
100 int32_t code;
101
102 code = yices_get_algebraic_number_value(mdl, t, &n);
103 if (code < 0) print_error();
104 lp_algebraic_number_print(&n, stdout);
105 fflush(stdout);
106 lp_algebraic_number_destruct(&n);
107 }
108
109
test_mcsat(void)110 static void test_mcsat(void) {
111 context_t *ctx;
112 model_t *mdl;
113 term_t x, p;
114 char *s;
115 int32_t code;
116 smt_status_t status;
117 double root;
118
119 x = declare_var("x");
120 p = yices_parse_term("(= (* x x) 2)");
121 if (p < 0) print_error();
122
123 s = term_to_string(p);
124 printf("Assertion: %s\n", s);
125 fflush(stdout);
126 yices_free_string(s);
127
128 ctx = make_context();
129 code = yices_assert_formula(ctx, p);
130 if (code < 0) print_error();
131
132 status = yices_check_context(ctx, NULL);
133 if (status != STATUS_SAT) {
134 fprintf(stderr, "Test failed: status != STATUS_SAT\n");
135 exit(1);
136 }
137
138 printf("Satisfiable\n");
139 mdl = yices_get_model(ctx, true);
140 if (mdl == NULL) print_error();
141 printf("Model:\n");
142 yices_pp_model(stdout, mdl, 80, 20, 0);
143 printf("\n");
144
145 // test: get value as a double
146 code = yices_get_double_value(mdl, x, &root);
147 if (code < 0) print_error();
148 printf("double value of x = %f\n", root);
149
150 // test use the lp_algebraic_number interface
151 printf("algebraic value of x = ");
152 show_algebraic_value(mdl, x);
153 printf("\n");
154
155 printf("Test succeeded\n");
156
157 // cleanup
158 yices_free_model(mdl);
159 yices_free_context(ctx);
160 }
161
main(void)162 int main(void) {
163 if (yices_has_mcsat()) {
164 yices_init();
165 test_mcsat();
166 yices_exit();
167 } else {
168 fprintf(stderr, "MCSAT is not supported by this Yices build\n");
169 }
170
171 return 0;
172 }
173