1 ///////////////////////////////////////////////////////////////////////////////
2 // //
3 // File: main.cpp //
4 // Author: Clark Barrett //
5 // Created: Sat Apr 19 01:47:47 2003 //
6 // //
7 ///////////////////////////////////////////////////////////////////////////////
8
9
10 #include "c_interface.h"
11 #include <stdio.h>
12 #include <stdlib.h>
13
14
15 #define TRUE 1
16 #define FALSE 0
17
18
19 #define FatalAssert(b,msg) \
20 if (!(b)) { \
21 fprintf(stderr, "Assertion Failure: %s\n", msg); \
22 exit(1); }
23
24
25 // Check whether e is valid
26
check_error(char * msg)27 void check_error(char* msg) {
28 if(vc_get_error_status() < 0) {
29 fprintf(stderr, "%s\n", msg);
30 fprintf(stderr, "%s\n", vc_get_error_string());
31 exit(1);
32 }
33 }
34
check(VC vc,Expr e)35 int check(VC vc, Expr e)
36 {
37 int res;
38 printf("Query: ");
39 vc_printExpr(vc, e);
40 check_error("Error occured during query");
41 res = vc_query(vc, e);
42 switch (res) {
43 case 0:
44 printf("Invalid\n\n");
45 break;
46 case 1:
47 printf("Valid\n\n");
48 break;
49 }
50 return res;
51 }
52
53
54 // Make a new assertion
newAssertion(VC vc,Expr e)55 void newAssertion(VC vc, Expr e)
56 {
57 // Testing printing to file descriptor. Turns out, we need to flush
58 // the file in C before printing through C++ (they apparently use
59 // different buffers, and text may come out of order).
60 printf("Assert: "); fflush(stdout);
61 vc_printExprFile(vc, e, 1);
62 vc_assertFormula(vc, e);
63 check_error("Error occured during assertion");
64 }
65
66
test1()67 void test1()
68 {
69 Flags flags = vc_createFlags();
70 VC vc;
71 Type b;
72 Expr p, np, e;
73 Type r, real2real;
74 Expr x, y, fx, fy, xeqy, fxeqfy, w, z, weqx, yeqz, one, two, xeqone, xeqtwo,
75 simp, simp2;
76 Op f;
77 Expr* assertions;
78 int i, size, res;
79 Kind k;
80
81 vc_setStringFlag(flags, "dump-log", ".testc1.cvc");
82 vc_setStrSeqFlag(flags, "trace", "pushpop", 1);
83
84 vc = vc_createValidityChecker(flags);
85
86 // Check p OR ~p
87
88 b = vc_boolType(vc);
89 p = vc_varExpr(vc, "p", vc_boolType(vc));
90 np = vc_notExpr(vc, p);
91 e = vc_orExpr(vc, p, np);
92
93 res = check(vc, e);
94 FatalAssert(res == 1, "Expected Valid");
95
96 FatalAssert(vc_getKind(e) == OR, "Expected TRUE for kind check");
97 FatalAssert(vc_getKind(vc_getType(vc, e)) == BOOLEAN, "Expected TRUE for type kind check");
98
99 vc_deleteType(b);
100 vc_deleteExpr(p);
101 vc_deleteExpr(np);
102 vc_deleteExpr(e);
103
104 /* Check x = y -> f(x) = f(y) */
105
106 r = vc_realType(vc);
107
108 x = vc_varExpr(vc, "x", r);
109 y = vc_varExpr(vc, "y", r);
110
111 real2real = vc_funType1(vc, r, r);
112 f = vc_createOp(vc, "f", real2real);
113
114 fx = vc_funExpr1(vc, f, x);
115 fy = vc_funExpr1(vc, f, y);
116
117 xeqy = vc_eqExpr(vc, x, y);
118 fxeqfy = vc_eqExpr(vc, fx, fy);
119
120 e = vc_impliesExpr(vc, xeqy, fxeqfy);
121 res = check(vc, e);
122 FatalAssert(res == 1, "Expected Valid");
123
124 vc_deleteType(real2real);
125 vc_deleteExpr(e);
126
127 // Check f(x) = f(y) -> x = y
128
129 e = vc_impliesExpr(vc, fxeqfy, xeqy);
130 vc_push(vc);
131 res = check(vc, e);
132 FatalAssert(res == 0, "Expected Invalid");
133 vc_deleteExpr(e);
134
135 // Get counter-example
136
137 printf("Stack level: %d\n", vc_stackLevel(vc));
138 printf("Counter-example:\n");
139 assertions = vc_getCounterExample(vc, &size);
140
141 for (i = 0; i < size; ++i) {
142 vc_printExpr(vc, assertions[i]);
143 }
144 vc_deleteVector(assertions);
145 printf("End of counter-example\n\n");
146
147 printf("Concrete model:\n");
148 assertions = vc_getConcreteModel(vc, &size);
149
150 for (i = 0; i < size; ++i) {
151 vc_printExpr(vc, assertions[i]);
152 }
153 vc_deleteVector(assertions);
154 printf("End of concrete model\n\n");
155
156 // Reset to initial scope
157 printf("Resetting\n");
158 vc_pop(vc);
159 printf("Stack level: %d\n\n", vc_stackLevel(vc));
160
161 // Check w = x & x = y & y = z & f(x) = f(y) & x = 1 & z = 2
162
163 w = vc_varExpr(vc, "w", r);
164 z = vc_varExpr(vc, "z", r);
165
166 printf("Push Scope\n\n");
167 vc_push(vc);
168
169 weqx = vc_eqExpr(vc, w, x);
170 yeqz = vc_eqExpr(vc, y, z);
171
172 one = vc_ratExpr(vc, 1, 1);
173 two = vc_ratExpr(vc, 2, 1);
174 xeqone = vc_eqExpr(vc, x, one);
175 xeqtwo = vc_eqExpr(vc, x, two);
176
177 newAssertion(vc, weqx);
178 newAssertion(vc, xeqy);
179 newAssertion(vc, yeqz);
180 newAssertion(vc, fxeqfy);
181 newAssertion(vc, xeqone);
182 newAssertion(vc, xeqtwo);
183
184 printf("\nsimplify(w) = ");
185
186 simp = vc_simplify(vc, w);
187
188 char* str = vc_printExprString(vc, simp);
189 printf("%s\n", str);
190 vc_deleteString(str);
191
192 printf("Inconsistent?: %d\n", vc_inconsistent(vc, &assertions, &size));
193 check_error("Error occured during inconsistency check");
194
195 printf("Assumptions Used:\n");
196 for (i = 0; i < size; ++i) {
197 vc_printExpr(vc, assertions[i]);
198 }
199 vc_deleteVector(assertions);
200
201 printf("\nPop Scope\n\n");
202 vc_pop(vc);
203
204 printf("simplify(w) = ");
205
206 simp2 = vc_simplify(vc, w);
207 vc_printExpr(vc, simp2);
208 printf("\n");
209
210 printf("Inconsistent?: %d\n", vc_inconsistent(vc, &assertions, &size));
211 vc_deleteVector(assertions);
212
213 vc_deleteType(r);
214 vc_deleteExpr(x);
215 vc_deleteExpr(y);
216 vc_deleteOp(f);
217 vc_deleteExpr(fx);
218 vc_deleteExpr(fy);
219 vc_deleteExpr(xeqy);
220 vc_deleteExpr(fxeqfy);
221 vc_deleteExpr(w);
222 vc_deleteExpr(z);
223 vc_deleteExpr(weqx);
224 vc_deleteExpr(yeqz);
225 vc_deleteExpr(one);
226 vc_deleteExpr(two);
227 vc_deleteExpr(xeqone);
228 vc_deleteExpr(xeqtwo);
229 vc_deleteExpr(simp);
230 vc_deleteExpr(simp2);
231
232 vc_destroyValidityChecker(vc);
233 vc_deleteFlags(flags);
234 }
235
236
test2()237 void test2()
238 {
239 VC vc = vc_createValidityChecker(NULL);
240
241 // Check x = y -> g(x,y) = g(y,x)
242
243 Type r = vc_realType(vc);
244
245 Expr x = vc_varExpr(vc, "x", r);
246 Expr y = vc_varExpr(vc, "y", r);
247
248 Type realxreal2real = vc_funType2(vc, r, r, r);
249 Op g = vc_createOp(vc, "g", realxreal2real);
250
251 Expr gxy = vc_funExpr2(vc, g, x, y);
252 Expr gyx = vc_funExpr2(vc, g, y, x);
253
254 Expr xeqy = vc_eqExpr(vc, x, y);
255 Expr gxyeqgyx = vc_eqExpr(vc, gxy, gyx);
256
257 Expr e = vc_impliesExpr(vc, xeqy, gxyeqgyx);
258 Type v[2];
259 Op h;
260 Expr hxy, hyx, hxyeqhyx;
261 int res;
262
263 res = check(vc, e);
264 FatalAssert(res == 1, "Expected Valid");
265
266 vc_deleteType(realxreal2real);
267 vc_deleteOp(g);
268 vc_deleteExpr(gxy);
269 vc_deleteExpr(gyx);
270 vc_deleteExpr(gxyeqgyx);
271 vc_deleteExpr(e);
272
273 v[0] = r;
274 v[1] = r;
275
276 realxreal2real = vc_funTypeN(vc, v, r, 2);
277 h = vc_createOp(vc, "h", realxreal2real);
278
279 hxy = vc_funExpr2(vc, h, x, y);
280 hyx = vc_funExpr2(vc, h, y, x);
281 hxyeqhyx = vc_eqExpr(vc, hxy, hyx);
282
283 e = vc_impliesExpr(vc, xeqy, hxyeqhyx);
284 res = check(vc, e);
285 FatalAssert(res == 1, "Expected Valid");
286
287 vc_deleteType(r);
288 vc_deleteExpr(x);
289 vc_deleteExpr(y);
290 vc_deleteType(realxreal2real);
291 vc_deleteExpr(hxy);
292 vc_deleteExpr(hxyeqhyx);
293 vc_deleteExpr(e);
294
295 vc_destroyValidityChecker(vc);
296 }
297
298
299 /* void test3() */
300 /* { */
301 /* VC vc = vc_createValidityChecker(NULL); */
302 /* // Check x = y -> g(x,y) = g(y,x) */
303
304 /* Type r = vc_realType(vc); */
305 /* Expr x = vc_varExpr(vc, "x", r); */
306 /* Expr y = vc_varExpr(vc, "y", r); */
307
308 /* Type realxreal2real = vc_funType2(vc, r, r, r); */
309 /* Op g = vc_createOp(vc, "g", realxreal2real); */
310
311 /* Expr gxy = vc_parseExpr(vc, "g(x,y)"); */
312 /* Expr gxy2; */
313
314 /* vc_printExpr(vc, gxy); */
315
316 /* gxy2 = vc_funExpr2(vc, g, x, y); */
317 /* vc_printExpr(vc, gxy2); */
318 /* FatalAssert((gxy == gxy2), "Should be equal"); */
319
320 /* vc_deleteType(r); */
321 /* vc_deleteExpr(x); */
322 /* vc_deleteExpr(y); */
323 /* vc_deleteType(realxreal2real); */
324 /* vc_deleteOp(g); */
325 /* vc_deleteExpr(gxy); */
326 /* vc_deleteExpr(gxy2); */
327
328 /* vc_destroyValidityChecker(vc); */
329 /* } */
330
test4(int regressLevel)331 void test4(int regressLevel)
332 {
333 VC vc = vc_createValidityChecker(NULL);
334
335 // Check x >= 10 /\ x >= 40 /\ y <= 0 -->
336 // x >= 1 /\ y < 10
337
338 Type r = vc_realType(vc);
339 Expr x = vc_varExpr(vc, "x", r);
340 Expr y = vc_varExpr(vc, "y", r);
341
342 Expr ten = vc_ratExpr(vc, 10, 1);
343 Expr ge = vc_geExpr(vc, x, ten);
344
345 Expr forty = vc_ratExpr(vc, 40, 1);
346 Expr ge2 = vc_geExpr(vc, x, forty);
347
348 Expr zero = vc_ratExpr(vc, 0, 1);
349 Expr ge3 = vc_leExpr(vc, y, zero);
350
351 Expr children[3];
352 Expr hyp, one, conc, query;
353 int i;
354
355 children[0] = ge;
356 children[1] = ge2;
357 children[2] = ge3;
358
359 hyp = vc_andExprN(vc, children, 3);
360
361 vc_deleteType(r);
362 vc_deleteExpr(ge);
363 vc_deleteExpr(forty);
364 vc_deleteExpr(ge2);
365 vc_deleteExpr(zero);
366 vc_deleteExpr(ge3);
367
368 one = vc_ratExpr(vc, 1, 1);
369 ge = vc_geExpr(vc, x, one);
370
371 ge2 = vc_ltExpr(vc, y, ten);
372
373 conc = vc_andExpr(vc, ge, ge2);
374 query = vc_impliesExpr(vc, hyp, conc);
375
376 vc_deleteExpr(x);
377 vc_deleteExpr(y);
378 vc_deleteExpr(ten);
379 vc_deleteExpr(hyp);
380 vc_deleteExpr(one);
381 vc_deleteExpr(ge);
382 vc_deleteExpr(ge2);
383 vc_deleteExpr(conc);
384
385 for (i = 0; i < 100*regressLevel; i++)
386 vc_query(vc, query);
387
388 vc_deleteExpr(query);
389
390 vc_destroyValidityChecker(vc);
391 }
392
393
test5()394 void test5()
395 {
396 Flags flags = vc_createFlags();
397 VC vc;
398 Type r;
399 Expr x, xEQx, p;
400
401 // vc_setBoolFlag(flags, "proofs", TRUE);
402 vc = vc_createValidityChecker(flags);
403
404 r = vc_realType(vc);
405 x = vc_varExpr(vc, "x", r);
406 xEQx = vc_eqExpr(vc, x, x);
407
408 vc_query(vc, xEQx);
409
410 // p = vc_getProof(vc);
411
412 // vc_printExpr(vc, p);
413
414 vc_deleteType(r);
415 vc_deleteExpr(x);
416 vc_deleteExpr(xEQx);
417 // vc_deleteExpr(p);
418
419 vc_destroyValidityChecker(vc);
420 vc_deleteFlags(flags);
421 }
422
423
test6()424 void test6()
425 {
426 Flags flags = vc_createFlags();
427 VC vc;
428 Expr p, p3, p32;
429 char *x;
430
431 // vc_setBoolFlag(flags, "proofs", 1);
432 vc_setBoolFlag(flags, "dagify-exprs", 0);
433 vc = vc_createValidityChecker(flags);
434
435 // p = vc_getProofOfFile(vc,"benchmarks/add1.cvc");
436 check_error("Failed to check file");
437
438 // vc_deleteExpr(p);
439 vc_destroyValidityChecker(vc);
440 vc_deleteFlags(flags);
441
442 /* p3 = getChild(p,3); */
443 /* p32 = getChild(p3,2); */
444
445 /* if (isLambda(p32)) */
446 /* printf("The expression is Lambda\n"); */
447 /* else */
448 /* printf("The expression is not Lambda\n"); */
449
450 /* x = exprString(p32); */
451
452 /* printf("Test expr,%s",x);*/
453
454 }
455
456
printImpliedLiterals(VC vc)457 int printImpliedLiterals(VC vc)
458 {
459 int count = 0;
460 Expr impLit = vc_getImpliedLiteral(vc);
461 printf("Implied Literals:\n");
462 while (impLit) {
463 ++count;
464 vc_printExpr(vc, impLit);
465 vc_deleteExpr(impLit);
466 impLit = vc_getImpliedLiteral(vc);
467 }
468 return count;
469 }
470
471
test7()472 void test7()
473 {
474 VC vc = vc_createValidityChecker(NULL);
475
476 Type r = vc_realType(vc);
477 Type b = vc_boolType(vc);
478
479 Expr x = vc_varExpr(vc, "x", r);
480 Expr y = vc_varExpr(vc, "y", r);
481 Expr z = vc_varExpr(vc, "z", r);
482
483 Type real2real = vc_funType1(vc, r, r);
484 Type real2bool = vc_funType1(vc, r, b);
485
486 Op f = vc_createOp(vc, "f", real2real);
487 Op p = vc_createOp(vc, "p", real2bool);
488
489 Expr fx = vc_funExpr1(vc, f, x);
490 Expr fy = vc_funExpr1(vc, f, y);
491 Expr fxeqfy = vc_eqExpr(vc, fx, fy);
492
493 Expr px = vc_funExpr1(vc, p, x);
494 Expr py = vc_funExpr1(vc, p, y);
495
496 Expr xeqy = vc_eqExpr(vc, x, y);
497 Expr yeqx = vc_eqExpr(vc, y, x);
498 Expr xeqz = vc_eqExpr(vc, x, z);
499 Expr zeqx = vc_eqExpr(vc, z, x);
500 Expr yeqz = vc_eqExpr(vc, y, z);
501 Expr zeqy = vc_eqExpr(vc, z, y);
502
503 Expr notxeqz = vc_notExpr(vc, xeqz);
504
505 int c;
506
507 vc_registerAtom(vc, xeqy);
508 vc_registerAtom(vc, yeqx);
509 vc_registerAtom(vc, xeqz);
510 vc_registerAtom(vc, zeqx);
511 vc_registerAtom(vc, yeqz);
512 vc_registerAtom(vc, zeqy);
513 vc_registerAtom(vc, px);
514 vc_registerAtom(vc, py);
515 vc_registerAtom(vc, fxeqfy);
516
517 printf("Push\n");
518 vc_push(vc);
519
520 printf("Assert x = y\n");
521 vc_assertFormula(vc, xeqy);
522 c = printImpliedLiterals(vc);
523 FatalAssert(c==3,"Implied literal error 0");
524
525 printf("Push\n");
526 vc_push(vc);
527 printf("Assert x /= z\n");
528 vc_assertFormula(vc, notxeqz);
529 c = printImpliedLiterals(vc);
530 FatalAssert(c==4,"Implied literal error 1");
531 printf("Pop\n");
532 vc_pop(vc);
533 printf("Pop\n");
534 vc_pop(vc);
535
536 vc_deleteExpr(notxeqz);
537 vc_deleteExpr(zeqy);
538 vc_deleteExpr(yeqz);
539 vc_deleteExpr(zeqx);
540 vc_deleteExpr(xeqz);
541 vc_deleteExpr(yeqx);
542 vc_deleteExpr(xeqy);
543 vc_deleteExpr(py);
544 vc_deleteExpr(px);
545 vc_deleteExpr(fxeqfy);
546 vc_deleteExpr(fy);
547 vc_deleteExpr(fx);
548 vc_deleteOp(p);
549 vc_deleteOp(f);
550 vc_deleteType(real2bool);
551 vc_deleteType(real2real);
552 vc_deleteExpr(z);
553 vc_deleteExpr(y);
554 vc_deleteExpr(x);
555 vc_deleteType(b);
556 vc_deleteType(r);
557
558 vc_destroyValidityChecker(vc);
559 }
560
561
test8(void)562 void test8 (void)
563 {
564 Flags flags = vc_createFlags();
565 /* vc_setStrSeqFlag(flags, "trace", "pushpop", 1); */
566 /* vc_setStrSeqFlag(flags, "trace", "assertLit", 1); */
567 /* vc_setStrSeqFlag(flags, "trace", "assertFactCore", 1); */
568 /* vc_setStrSeqFlag(flags, "trace", "assertFormula", 1); */
569
570 VC vc = vc_createValidityChecker (flags);
571 Type bv32 = vc_bvType (vc, 32);
572 Expr zero = vc_bvConstExprFromInt (vc, 32, 0);
573 Expr one = vc_bvConstExprFromInt (vc, 32, 1);
574 Expr a = vc_varExpr (vc, "a", bv32);
575 Expr three = vc_bvConstExprFromInt (vc, 32, 3);
576 Expr prod = vc_bvMultExpr (vc, 32, a, three);
577 {
578 Expr a64 = vc_bvSignExtend (vc, a, 64);
579 Expr three64 = vc_bvSignExtend (vc, three, 64);
580 Expr prod64 = vc_bvMultExpr (vc, 64, a64, three64);
581 Expr max = vc_bvConstExprFromInt (vc, 32, 2147483647);
582 Expr min = vc_bvConstExprFromInt (vc, 32, (-2147483647 - 1));
583 Expr prod64_sge_min = vc_bvSGeExpr (vc, prod64, min);
584 Expr prod64_sle_max = vc_bvSLeExpr (vc, prod64, max);
585 Expr prod64_sge_min_and_sle_max =
586 vc_andExpr (vc, prod64_sge_min, prod64_sle_max);
587 vc_assertFormula (vc, prod64_sge_min_and_sle_max);
588 }
589 Expr D4 = vc_varExpr (vc, "D4", bv32);
590 {
591 Expr cond = vc_bvSLtExpr (vc, a, prod);
592 Expr test = vc_iteExpr (vc, cond, one, zero);
593 Expr D4_eq_test = vc_eqExpr (vc, D4, test);
594 vc_assertFormula (vc, D4_eq_test);
595 }
596 Expr D6 = vc_varExpr (vc, "D6", bv32);
597 {
598 Expr cond = vc_bvSLeExpr (vc, a, prod);
599 Expr test = vc_iteExpr (vc, cond, one, zero);
600 Expr D6_eq_test = vc_eqExpr (vc, D6, test);
601 vc_assertFormula (vc, D6_eq_test);
602 }
603 vc_push (vc);
604 vc_pop (vc);
605 vc_push (vc);
606 {
607 Expr cond = vc_bvSLtExpr (vc, a, zero);
608 Expr test = vc_iteExpr (vc, cond, one, zero);
609 Expr test_eq_one = vc_eqExpr (vc, test, one);
610 vc_assertFormula (vc, test_eq_one);
611 vc_push (vc);
612 {
613 Expr D4_eq_one = vc_eqExpr (vc, D4, one);
614 vc_query (vc, D4_eq_one);
615 }
616 vc_pop (vc);
617 vc_push (vc);
618 vc_pop (vc);
619 vc_push (vc);
620 vc_pop (vc);
621 }
622 vc_pop (vc);
623 {
624 Expr cond = vc_eqExpr (vc, a, zero);
625 Expr test = vc_iteExpr (vc, cond, one, zero);
626 Expr test_eq_one = vc_eqExpr (vc, test, one);
627 vc_assertFormula (vc, test_eq_one);
628 vc_push (vc);
629 vc_pop (vc);
630 {
631 Expr zero_eq_one = vc_eqExpr (vc, zero, one);
632 vc_query (vc, zero_eq_one);
633 }
634 }
635 vc_destroyValidityChecker(vc);
636 }
637
638
test9(void)639 void test9 (void)
640 {
641 VC vc = vc_createValidityChecker (((void *) 0));
642 Type bv32 = vc_bvType (vc, 32);
643 Expr zero = vc_bvConstExprFromInt (vc, 32, 0);
644 Expr one = vc_bvConstExprFromInt (vc, 32, 1);
645 Expr a = vc_varExpr (vc, "a", bv32);
646 Expr three = vc_bvConstExprFromInt (vc, 32, 3);
647 Expr three64 = vc_bvSignExtend (vc, three, 64);
648 Expr a64 = vc_bvSignExtend (vc, a, 64);
649 Expr prod64 = vc_bvMultExpr (vc, 64, a64, three64);
650 Expr min = vc_bvConstExprFromInt (vc, 32, (-2147483647 - 1));
651 Expr max = vc_bvConstExprFromInt (vc, 32, 2147483647);
652 Expr prod64_sge_min = vc_bvSGeExpr (vc, prod64, min);
653 Expr prod64_sle_max = vc_bvSLeExpr (vc, prod64, max);
654 Expr prod64_sge_min_and_sle_max =
655 vc_andExpr (vc, prod64_sge_min, prod64_sle_max);
656 vc_assertFormula (vc, prod64_sge_min_and_sle_max);
657 Expr D3 = vc_varExpr (vc, "D3", bv32);
658 Expr prod = vc_bvMultExpr (vc, 32, a, three);
659 Expr D3_eq_prod = vc_eqExpr (vc, D3, prod);
660 vc_assertFormula (vc, D3_eq_prod);
661 Expr D4 = vc_varExpr (vc, "D4", bv32);
662 Expr D3_sle_a_cond = vc_bvSLeExpr (vc, D3, a);
663 Expr D3_sle_a_expr = vc_iteExpr (vc, D3_sle_a_cond, one, zero);
664 Expr D4_eq_D3_sle_a_expr = vc_eqExpr (vc, D4, D3_sle_a_expr);
665 vc_assertFormula (vc, D4_eq_D3_sle_a_expr);
666 Expr D6 = vc_varExpr (vc, "D6", bv32);
667 Expr D3_slt_a_cond = vc_bvSLtExpr (vc, D3, a);
668 Expr D3_slt_a_expr = vc_iteExpr (vc, D3_slt_a_cond, one, zero);
669 Expr D6_eq_D3_slt_a_expr = vc_eqExpr (vc, D6, D3_slt_a_expr);
670 vc_assertFormula (vc, D6_eq_D3_slt_a_expr);
671 Expr zero_lt_a = vc_bvSLtExpr (vc, zero, a);
672 vc_assertFormula (vc, zero_lt_a);
673 Expr D4_eq_one = vc_eqExpr (vc, D4, one);
674 Expr not_D4_eq_one = vc_notExpr (vc, D4_eq_one);
675 vc_query (vc, not_D4_eq_one);
676 Expr D6_eq_one = vc_eqExpr (vc, D6, one);
677 Expr not_D6_eq_one = vc_notExpr (vc, D6_eq_one);
678 vc_query (vc, not_D6_eq_one);
679 vc_destroyValidityChecker(vc);
680 }
681
682
test10()683 void test10()
684 {
685 Flags flags = vc_createFlags();
686 VC vc = vc_createValidityChecker(flags);
687 Type a = vc_createType(vc, "a");
688 Type aa = vc_funType1(vc, a, a);
689 Op f1 = vc_createOp(vc, "f", aa);
690 Type aa2;
691 Op f2 = vc_lookupOp(vc, "f", &aa2);
692 FatalAssert(f2 != NULL, "Expected f2 not NULL");
693 FatalAssert(f1 == f2, "Expected equal");
694 Expr x = vc_varExpr(vc, "x", a);
695 Expr f1x = vc_funExpr1(vc, f1, x);
696 Expr f2x = vc_funExpr1(vc, f2, x);
697 Expr eq = vc_eqExpr(vc, f1x, f2x);
698 int res = vc_query(vc, eq);
699 printf("eq: %d\n", res);
700 vc_destroyValidityChecker(vc);
701 }
702
703
test11()704 void test11()
705 {
706 Flags flags = vc_createFlags();
707 VC vc = vc_createValidityChecker(flags);
708 Type a = vc_createType(vc, "a");
709 Type aa = vc_funType1(vc, a, a);
710 Op f = vc_createOp(vc, "f", aa);
711 Expr x = vc_varExpr(vc, "x", a);
712 Expr fx = vc_funExpr1(vc, f, x);
713 Expr ffx = vc_funExpr1(vc, f, fx);
714 Expr e = vc_eqExpr(vc, x, fx);
715 Expr expectE = vc_eqExpr(vc, fx, ffx);
716 Expr newE = vc_substExpr(vc, e, &x, 1, &fx, 1);
717 FatalAssert(expectE == newE, "Expected equal");
718 vc_destroyValidityChecker(vc);
719 }
720
721
main(int argc,char ** argv)722 int main(int argc, char** argv)
723 {
724 int regressLevel = 2;
725 if (argc > 1) regressLevel = atoi(argv[1]);
726 printf("Running C API test, regress level = %d\n", regressLevel);
727 printf("\ntest1() {\n");
728 test1();
729 check_error("test1");
730 printf("\n}\ntest2() {\n");
731 test2();
732 check_error("test2");
733 /* TODO: implement parseExpr */
734 /* test3(); */
735 /* check_error("test3"); */
736
737 printf("\n}\ntest4() {\n");
738 test4(regressLevel);
739 check_error("test4");
740 printf("\n}\ntest5() {\n");
741 test5();
742 check_error("test5");
743 if (regressLevel > 0) {
744 printf("\n}\ntest6() {\n");
745 test6();
746 check_error("test6");
747 }
748 printf("\n}\ntest7() {\n");
749 test7();
750 check_error("test7");
751 if (regressLevel > 0) {
752 printf("\n}\ntest8() {\n");
753 test8();
754 check_error("test8");
755 printf("\n}\ntest9() {\n");
756 test9();
757 check_error("test9");
758 }
759 printf("\n}");
760 printf("\ntest10() {\n");
761 test10();
762 printf("\n}");
763 printf("\ntest11() {\n");
764 test11();
765 printf("\n}\n");
766 return 0;
767 }
768