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 * TEST OF BASIC EGRAPH + CORE FUNCTIONS
21 */
22
23 #include <stdio.h>
24 #include <stdint.h>
25 #include <stdbool.h>
26 #include <inttypes.h>
27
28
29 #include "api/yices_globals.h"
30 #include "solvers/cdcl/smt_core.h"
31 #include "solvers/cdcl/smt_core_printer.h"
32 #include "solvers/egraph/egraph.h"
33 #include "solvers/egraph/egraph_printer.h"
34
35 #include "yices.h"
36
37
38
39 /*
40 * Build egraph and core
41 */
42 #define DEFAULT_NVARS 100
43
init_solver(egraph_t * egraph,smt_core_t * core)44 static void init_solver(egraph_t *egraph, smt_core_t *core) {
45 init_egraph(egraph, __yices_globals.types);
46 init_smt_core(core, DEFAULT_NVARS, egraph, egraph_ctrl_interface(egraph),
47 egraph_smt_interface(egraph), SMT_MODE_PUSHPOP);
48 egraph_attach_core(egraph, core);
49 }
50
51 /*
52 * Delete both
53 */
delete_solver(egraph_t * egraph,smt_core_t * core)54 static void delete_solver(egraph_t *egraph, smt_core_t *core) {
55 delete_egraph(egraph);
56 delete_smt_core(core);
57 }
58
59 /*
60 * Reset both
61 */
reset_solver(egraph_t * egraph,smt_core_t * core)62 static void reset_solver(egraph_t *egraph, smt_core_t *core) {
63 reset_smt_core(core);
64 }
65
66
67 /*
68 * Print both
69 */
print_solver(egraph_t * egraph,smt_core_t * core)70 static void print_solver(egraph_t *egraph, smt_core_t *core) {
71 printf("--- Terms ---\n");
72 print_egraph_terms(stdout, egraph);
73 printf("--- Atoms ---\n");
74 print_egraph_atoms(stdout, egraph);
75 print_egraph_congruence_roots(stdout, egraph);
76 printf("--- Classes ---\n");
77 print_egraph_root_classes(stdout, egraph);
78 printf("--- Clauses ---\n");
79 print_clauses(stdout, core);
80 }
81
82
83 #if 0
84
85 /*
86 * More details (not used)
87 */
88 static void print_solver_details(egraph_t *egraph, smt_core_t *core) {
89 print_egraph_terms_details(stdout, egraph);
90 print_egraph_root_classes_details(stdout, egraph);
91 print_egraph_atoms(stdout, egraph);
92 print_clauses(stdout, core);
93 }
94
95 #endif
96
97
98 /*
99 * Global variables: the core + the egraph
100 */
101 static egraph_t egraph;
102 static smt_core_t core;
103
104
105 /*
106 * Test 1: construct simple terms, push/pop
107 */
test1(void)108 static void test1(void) {
109 eterm_t tx, ty;
110 occ_t x, y;
111 type_t u;
112
113 printf("***********************\n"
114 "* TEST 1 *\n"
115 "***********************\n\n");
116
117 init_solver(&egraph, &core);
118
119 u = yices_new_uninterpreted_type();
120
121 // create x and y
122 printf("---> building x and y\n");
123 tx = egraph_make_variable(&egraph, u);
124 x = pos_occ(tx);
125
126 ty = egraph_make_variable(&egraph, u);
127 y = pos_occ(ty);
128
129 // test push/pop
130 printf("---> push\n");
131 smt_push(&core);
132
133 // create (eq x y)
134 printf("---> building (eq x y)\n");
135 (void) egraph_make_eq(&egraph, x, y);
136
137 // create (eq y y)
138 printf("---> building (eq x x)\n");
139 (void) egraph_make_eq(&egraph, y, y);
140
141 print_solver(&egraph, &core);
142
143 // empty push
144 printf("---> push\n");
145 smt_push(&core);
146
147 // start search + propagate + end_search
148 printf("---> propagation test 1\n");
149 start_search(&core, 0, NULL);
150 smt_process(&core);
151 end_search_unknown(&core);
152 print_solver(&egraph, &core);
153
154 printf("---> pop 1\n");
155 smt_pop(&core);
156 print_solver(&egraph, &core);
157
158 // start search + propagate + end_search
159 printf("---> propagation test 2\n");
160 start_search(&core, 0, NULL);
161 smt_process(&core);
162 end_search_unknown(&core);
163 print_solver(&egraph, &core);
164
165
166 printf("---> pop 2\n");
167 smt_pop(&core);
168 print_solver(&egraph, &core);
169
170 // reset
171 reset_solver(&egraph, &core);
172 print_solver(&egraph, &core);
173
174 delete_solver(&egraph, &core);
175 }
176
177
178 /*
179 * Test 2: build distinct terms
180 */
test2(void)181 static void test2(void) {
182 uint32_t i;
183 eterm_t aux;
184 occ_t a[50];
185 literal_t l;
186 type_t tau;
187
188 printf("***********************\n"
189 "* TEST 2 *\n"
190 "***********************\n\n");
191
192 init_solver(&egraph, &core);
193
194 tau = yices_new_uninterpreted_type();
195
196 printf("---> building a_0 ... a_49\n");
197 for (i=0; i<50; i++) {
198 aux = egraph_make_variable(&egraph, tau);
199 a[i] = pos_occ(aux);
200 }
201
202 for (i=0; i<40; i++) {
203 printf("---> creating (distinct a_%"PRIu32" ... a_%"PRIu32")\n", i, i+5);
204 l = egraph_make_distinct(&egraph, 5, a+i);
205 printf("---> result = ");
206 print_literal(stdout, l);
207 printf("\n");
208 }
209
210 print_solver(&egraph, &core);
211 delete_solver(&egraph, &core);
212 }
213
214
main(void)215 int main(void) {
216 yices_init();
217 test1();
218 test2();
219 yices_exit();
220 return 0;
221 }
222