1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2018 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 #include <stdlib.h>
20 #include <stdio.h>
21 #include <stdbool.h>
22 #include <inttypes.h>
23
24 #include "yices.h"
25
26
27 /*
28 * How to call the pretty printer
29 * - this also shows how to check for errors
30 * and print an error message if something goes wrong
31 */
print_term(term_t term)32 static void print_term(term_t term) {
33 int32_t code;
34
35 code = yices_pp_term(stdout, term, 80, 20, 0);
36 if (code < 0) {
37 // An error occurred
38 fprintf(stderr, "Error in print_term: ");
39 yices_print_error(stderr);
40 exit(1);
41 }
42 }
43
44
45 /*
46 * Small example: equivalent to
47 *
48 * (define x::int)
49 * (define y::int)
50 * (assert (and (>= x 0) (>= y 0)(= (+ x y) 100)))
51 * (check)
52 *
53 * Then we query the model to get the values of x and y.
54 */
simple_test(void)55 static void simple_test(void) {
56 int32_t code;
57
58 /*
59 * Build the formula
60 */
61 // Create two uninterpreted terms of type int.
62 type_t int_type = yices_int_type();
63 term_t x = yices_new_uninterpreted_term(int_type);
64 term_t y = yices_new_uninterpreted_term(int_type);
65
66 // Assign names "x" and "y" to these terms.
67 // This is optional, but we need the names in yices_parse_term
68 // and it makes pretty printing nicer.
69 yices_set_term_name(x, "x");
70 yices_set_term_name(y, "y");
71
72 // Build the formula (and (>= x 0) (>= y 0) (= (+ x y) 100))
73 term_t f = yices_and3(yices_arith_geq0_atom(x), // x >= 0
74 yices_arith_geq0_atom(y), // y >= 0
75 yices_arith_eq_atom(yices_add(x, y), yices_int32(100))); // x + y = 100
76
77
78 // Another way to do it
79 term_t f_var = yices_parse_term("(and (>= x 0) (>= y 0) (= (+ x y) 100))");
80
81
82 /*
83 * Print the formulas: f and f_var should be identical
84 */
85 printf("Formula f\n");
86 print_term(f);
87 printf("Formula f_var\n");
88 print_term(f_var);
89
90
91 /*
92 * To check whether f is satisfiable
93 * - first build a context
94 * - assert f in the context
95 * - call check_context
96 * - if check_context returns SAT, build a model
97 * and make queries about the model.
98 */
99 context_t *ctx = yices_new_context(NULL); // NULL means 'use default configuration'
100 code = yices_assert_formula(ctx, f);
101 if (code < 0) {
102 fprintf(stderr, "Assert failed: code = %"PRId32", error = %"PRId32"\n", code, yices_error_code());
103 yices_print_error(stderr);
104 }
105
106 switch (yices_check_context(ctx, NULL)) { // call check_context, NULL means 'use default heuristics'
107 case STATUS_SAT:
108 printf("The formula is satisfiable\n");
109 model_t* model = yices_get_model(ctx, true); // get the model
110 if (model == NULL) {
111 fprintf(stderr, "Error in get_model\n");
112 yices_print_error(stderr);
113 } else {
114 printf("Model\n");
115 code = yices_pp_model(stdout, model, 80, 4, 0); // print the model
116
117 int32_t v;
118 code = yices_get_int32_value(model, x, &v); // get the value of x, we know it fits int32
119 if (code < 0) {
120 fprintf(stderr, "Error in get_int32_value for 'x'\n");
121 yices_print_error(stderr);
122 } else {
123 printf("Value of x = %"PRId32"\n", v);
124 }
125
126 code = yices_get_int32_value(model, y, &v); // get the value of y
127 if (code < 0) {
128 fprintf(stderr, "Error in get_int32_value for 'y'\n");
129 yices_print_error(stderr);
130 } else {
131 printf("Value of y = %"PRId32"\n", v);
132 }
133
134 yices_free_model(model); // clean up: delete the model
135 }
136 break;
137
138 case STATUS_UNSAT:
139 printf("The formula is not satisfiable\n");
140 break;
141
142 case STATUS_UNKNOWN:
143 printf("The status is unknown\n");
144 break;
145
146 case STATUS_IDLE:
147 case STATUS_SEARCHING:
148 case STATUS_INTERRUPTED:
149 case STATUS_ERROR:
150 fprintf(stderr, "Error in check_context\n");
151 yices_print_error(stderr);
152 break;
153 }
154
155 yices_free_context(ctx); // delete the context
156 }
157
158
main(void)159 int main(void) {
160 yices_init(); // Always call this first
161 simple_test();
162 yices_exit(); // Cleanup
163
164 return 0;
165 }
166