Lines Matching refs:vc
35 int check(VC vc, Expr e) in check() argument
39 vc_printExpr(vc, e); in check()
41 res = vc_query(vc, e); in check()
55 void newAssertion(VC vc, Expr e) in newAssertion() argument
61 vc_printExprFile(vc, e, 1); in newAssertion()
62 vc_assertFormula(vc, e); in newAssertion()
70 VC vc; in test1() local
84 vc = vc_createValidityChecker(flags); in test1()
88 b = vc_boolType(vc); in test1()
89 p = vc_varExpr(vc, "p", vc_boolType(vc)); in test1()
90 np = vc_notExpr(vc, p); in test1()
91 e = vc_orExpr(vc, p, np); in test1()
93 res = check(vc, e); in test1()
97 FatalAssert(vc_getKind(vc_getType(vc, e)) == BOOLEAN, "Expected TRUE for type kind check"); in test1()
106 r = vc_realType(vc); in test1()
108 x = vc_varExpr(vc, "x", r); in test1()
109 y = vc_varExpr(vc, "y", r); in test1()
111 real2real = vc_funType1(vc, r, r); in test1()
112 f = vc_createOp(vc, "f", real2real); in test1()
114 fx = vc_funExpr1(vc, f, x); in test1()
115 fy = vc_funExpr1(vc, f, y); in test1()
117 xeqy = vc_eqExpr(vc, x, y); in test1()
118 fxeqfy = vc_eqExpr(vc, fx, fy); in test1()
120 e = vc_impliesExpr(vc, xeqy, fxeqfy); in test1()
121 res = check(vc, e); in test1()
129 e = vc_impliesExpr(vc, fxeqfy, xeqy); in test1()
130 vc_push(vc); in test1()
131 res = check(vc, e); in test1()
137 printf("Stack level: %d\n", vc_stackLevel(vc)); in test1()
139 assertions = vc_getCounterExample(vc, &size); in test1()
142 vc_printExpr(vc, assertions[i]); in test1()
148 assertions = vc_getConcreteModel(vc, &size); in test1()
151 vc_printExpr(vc, assertions[i]); in test1()
158 vc_pop(vc); in test1()
159 printf("Stack level: %d\n\n", vc_stackLevel(vc)); in test1()
163 w = vc_varExpr(vc, "w", r); in test1()
164 z = vc_varExpr(vc, "z", r); in test1()
167 vc_push(vc); in test1()
169 weqx = vc_eqExpr(vc, w, x); in test1()
170 yeqz = vc_eqExpr(vc, y, z); in test1()
172 one = vc_ratExpr(vc, 1, 1); in test1()
173 two = vc_ratExpr(vc, 2, 1); in test1()
174 xeqone = vc_eqExpr(vc, x, one); in test1()
175 xeqtwo = vc_eqExpr(vc, x, two); in test1()
177 newAssertion(vc, weqx); in test1()
178 newAssertion(vc, xeqy); in test1()
179 newAssertion(vc, yeqz); in test1()
180 newAssertion(vc, fxeqfy); in test1()
181 newAssertion(vc, xeqone); in test1()
182 newAssertion(vc, xeqtwo); in test1()
186 simp = vc_simplify(vc, w); in test1()
188 char* str = vc_printExprString(vc, simp); in test1()
192 printf("Inconsistent?: %d\n", vc_inconsistent(vc, &assertions, &size)); in test1()
197 vc_printExpr(vc, assertions[i]); in test1()
202 vc_pop(vc); in test1()
206 simp2 = vc_simplify(vc, w); in test1()
207 vc_printExpr(vc, simp2); in test1()
210 printf("Inconsistent?: %d\n", vc_inconsistent(vc, &assertions, &size)); in test1()
232 vc_destroyValidityChecker(vc); in test1()
239 VC vc = vc_createValidityChecker(NULL); in test2() local
243 Type r = vc_realType(vc); in test2()
245 Expr x = vc_varExpr(vc, "x", r); in test2()
246 Expr y = vc_varExpr(vc, "y", r); in test2()
248 Type realxreal2real = vc_funType2(vc, r, r, r); in test2()
249 Op g = vc_createOp(vc, "g", realxreal2real); in test2()
251 Expr gxy = vc_funExpr2(vc, g, x, y); in test2()
252 Expr gyx = vc_funExpr2(vc, g, y, x); in test2()
254 Expr xeqy = vc_eqExpr(vc, x, y); in test2()
255 Expr gxyeqgyx = vc_eqExpr(vc, gxy, gyx); in test2()
257 Expr e = vc_impliesExpr(vc, xeqy, gxyeqgyx); in test2()
263 res = check(vc, e); in test2()
276 realxreal2real = vc_funTypeN(vc, v, r, 2); in test2()
277 h = vc_createOp(vc, "h", realxreal2real); in test2()
279 hxy = vc_funExpr2(vc, h, x, y); in test2()
280 hyx = vc_funExpr2(vc, h, y, x); in test2()
281 hxyeqhyx = vc_eqExpr(vc, hxy, hyx); in test2()
283 e = vc_impliesExpr(vc, xeqy, hxyeqhyx); in test2()
284 res = check(vc, e); in test2()
295 vc_destroyValidityChecker(vc); in test2()
333 VC vc = vc_createValidityChecker(NULL); in test4() local
338 Type r = vc_realType(vc); in test4()
339 Expr x = vc_varExpr(vc, "x", r); in test4()
340 Expr y = vc_varExpr(vc, "y", r); in test4()
342 Expr ten = vc_ratExpr(vc, 10, 1); in test4()
343 Expr ge = vc_geExpr(vc, x, ten); in test4()
345 Expr forty = vc_ratExpr(vc, 40, 1); in test4()
346 Expr ge2 = vc_geExpr(vc, x, forty); in test4()
348 Expr zero = vc_ratExpr(vc, 0, 1); in test4()
349 Expr ge3 = vc_leExpr(vc, y, zero); in test4()
359 hyp = vc_andExprN(vc, children, 3); in test4()
368 one = vc_ratExpr(vc, 1, 1); in test4()
369 ge = vc_geExpr(vc, x, one); in test4()
371 ge2 = vc_ltExpr(vc, y, ten); in test4()
373 conc = vc_andExpr(vc, ge, ge2); in test4()
374 query = vc_impliesExpr(vc, hyp, conc); in test4()
386 vc_query(vc, query); in test4()
390 vc_destroyValidityChecker(vc); in test4()
397 VC vc; in test5() local
402 vc = vc_createValidityChecker(flags); in test5()
404 r = vc_realType(vc); in test5()
405 x = vc_varExpr(vc, "x", r); in test5()
406 xEQx = vc_eqExpr(vc, x, x); in test5()
408 vc_query(vc, xEQx); in test5()
419 vc_destroyValidityChecker(vc); in test5()
427 VC vc; in test6() local
433 vc = vc_createValidityChecker(flags); in test6()
439 vc_destroyValidityChecker(vc); in test6()
457 int printImpliedLiterals(VC vc) in printImpliedLiterals() argument
460 Expr impLit = vc_getImpliedLiteral(vc); in printImpliedLiterals()
464 vc_printExpr(vc, impLit); in printImpliedLiterals()
466 impLit = vc_getImpliedLiteral(vc); in printImpliedLiterals()
474 VC vc = vc_createValidityChecker(NULL); in test7() local
476 Type r = vc_realType(vc); in test7()
477 Type b = vc_boolType(vc); in test7()
479 Expr x = vc_varExpr(vc, "x", r); in test7()
480 Expr y = vc_varExpr(vc, "y", r); in test7()
481 Expr z = vc_varExpr(vc, "z", r); in test7()
483 Type real2real = vc_funType1(vc, r, r); in test7()
484 Type real2bool = vc_funType1(vc, r, b); in test7()
486 Op f = vc_createOp(vc, "f", real2real); in test7()
487 Op p = vc_createOp(vc, "p", real2bool); in test7()
489 Expr fx = vc_funExpr1(vc, f, x); in test7()
490 Expr fy = vc_funExpr1(vc, f, y); in test7()
491 Expr fxeqfy = vc_eqExpr(vc, fx, fy); in test7()
493 Expr px = vc_funExpr1(vc, p, x); in test7()
494 Expr py = vc_funExpr1(vc, p, y); in test7()
496 Expr xeqy = vc_eqExpr(vc, x, y); in test7()
497 Expr yeqx = vc_eqExpr(vc, y, x); in test7()
498 Expr xeqz = vc_eqExpr(vc, x, z); in test7()
499 Expr zeqx = vc_eqExpr(vc, z, x); in test7()
500 Expr yeqz = vc_eqExpr(vc, y, z); in test7()
501 Expr zeqy = vc_eqExpr(vc, z, y); in test7()
503 Expr notxeqz = vc_notExpr(vc, xeqz); in test7()
507 vc_registerAtom(vc, xeqy); in test7()
508 vc_registerAtom(vc, yeqx); in test7()
509 vc_registerAtom(vc, xeqz); in test7()
510 vc_registerAtom(vc, zeqx); in test7()
511 vc_registerAtom(vc, yeqz); in test7()
512 vc_registerAtom(vc, zeqy); in test7()
513 vc_registerAtom(vc, px); in test7()
514 vc_registerAtom(vc, py); in test7()
515 vc_registerAtom(vc, fxeqfy); in test7()
518 vc_push(vc); in test7()
521 vc_assertFormula(vc, xeqy); in test7()
522 c = printImpliedLiterals(vc); in test7()
526 vc_push(vc); in test7()
528 vc_assertFormula(vc, notxeqz); in test7()
529 c = printImpliedLiterals(vc); in test7()
532 vc_pop(vc); in test7()
534 vc_pop(vc); in test7()
558 vc_destroyValidityChecker(vc); in test7()
570 VC vc = vc_createValidityChecker (flags); in test8() local
571 Type bv32 = vc_bvType (vc, 32); in test8()
572 Expr zero = vc_bvConstExprFromInt (vc, 32, 0); in test8()
573 Expr one = vc_bvConstExprFromInt (vc, 32, 1); in test8()
574 Expr a = vc_varExpr (vc, "a", bv32); in test8()
575 Expr three = vc_bvConstExprFromInt (vc, 32, 3); in test8()
576 Expr prod = vc_bvMultExpr (vc, 32, a, three); in test8()
578 Expr a64 = vc_bvSignExtend (vc, a, 64); in test8()
579 Expr three64 = vc_bvSignExtend (vc, three, 64); in test8()
580 Expr prod64 = vc_bvMultExpr (vc, 64, a64, three64); in test8()
581 Expr max = vc_bvConstExprFromInt (vc, 32, 2147483647); in test8()
582 Expr min = vc_bvConstExprFromInt (vc, 32, (-2147483647 - 1)); in test8()
583 Expr prod64_sge_min = vc_bvSGeExpr (vc, prod64, min); in test8()
584 Expr prod64_sle_max = vc_bvSLeExpr (vc, prod64, max); in test8()
586 vc_andExpr (vc, prod64_sge_min, prod64_sle_max); in test8()
587 vc_assertFormula (vc, prod64_sge_min_and_sle_max); in test8()
589 Expr D4 = vc_varExpr (vc, "D4", bv32); in test8()
591 Expr cond = vc_bvSLtExpr (vc, a, prod); in test8()
592 Expr test = vc_iteExpr (vc, cond, one, zero); in test8()
593 Expr D4_eq_test = vc_eqExpr (vc, D4, test); in test8()
594 vc_assertFormula (vc, D4_eq_test); in test8()
596 Expr D6 = vc_varExpr (vc, "D6", bv32); in test8()
598 Expr cond = vc_bvSLeExpr (vc, a, prod); in test8()
599 Expr test = vc_iteExpr (vc, cond, one, zero); in test8()
600 Expr D6_eq_test = vc_eqExpr (vc, D6, test); in test8()
601 vc_assertFormula (vc, D6_eq_test); in test8()
603 vc_push (vc); in test8()
604 vc_pop (vc); in test8()
605 vc_push (vc); in test8()
607 Expr cond = vc_bvSLtExpr (vc, a, zero); in test8()
608 Expr test = vc_iteExpr (vc, cond, one, zero); in test8()
609 Expr test_eq_one = vc_eqExpr (vc, test, one); in test8()
610 vc_assertFormula (vc, test_eq_one); in test8()
611 vc_push (vc); in test8()
613 Expr D4_eq_one = vc_eqExpr (vc, D4, one); in test8()
614 vc_query (vc, D4_eq_one); in test8()
616 vc_pop (vc); in test8()
617 vc_push (vc); in test8()
618 vc_pop (vc); in test8()
619 vc_push (vc); in test8()
620 vc_pop (vc); in test8()
622 vc_pop (vc); in test8()
624 Expr cond = vc_eqExpr (vc, a, zero); in test8()
625 Expr test = vc_iteExpr (vc, cond, one, zero); in test8()
626 Expr test_eq_one = vc_eqExpr (vc, test, one); in test8()
627 vc_assertFormula (vc, test_eq_one); in test8()
628 vc_push (vc); in test8()
629 vc_pop (vc); in test8()
631 Expr zero_eq_one = vc_eqExpr (vc, zero, one); in test8()
632 vc_query (vc, zero_eq_one); in test8()
635 vc_destroyValidityChecker(vc); in test8()
641 VC vc = vc_createValidityChecker (((void *) 0)); in test9() local
642 Type bv32 = vc_bvType (vc, 32); in test9()
643 Expr zero = vc_bvConstExprFromInt (vc, 32, 0); in test9()
644 Expr one = vc_bvConstExprFromInt (vc, 32, 1); in test9()
645 Expr a = vc_varExpr (vc, "a", bv32); in test9()
646 Expr three = vc_bvConstExprFromInt (vc, 32, 3); in test9()
647 Expr three64 = vc_bvSignExtend (vc, three, 64); in test9()
648 Expr a64 = vc_bvSignExtend (vc, a, 64); in test9()
649 Expr prod64 = vc_bvMultExpr (vc, 64, a64, three64); in test9()
650 Expr min = vc_bvConstExprFromInt (vc, 32, (-2147483647 - 1)); in test9()
651 Expr max = vc_bvConstExprFromInt (vc, 32, 2147483647); in test9()
652 Expr prod64_sge_min = vc_bvSGeExpr (vc, prod64, min); in test9()
653 Expr prod64_sle_max = vc_bvSLeExpr (vc, prod64, max); in test9()
655 vc_andExpr (vc, prod64_sge_min, prod64_sle_max); in test9()
656 vc_assertFormula (vc, prod64_sge_min_and_sle_max); in test9()
657 Expr D3 = vc_varExpr (vc, "D3", bv32); in test9()
658 Expr prod = vc_bvMultExpr (vc, 32, a, three); in test9()
659 Expr D3_eq_prod = vc_eqExpr (vc, D3, prod); in test9()
660 vc_assertFormula (vc, D3_eq_prod); in test9()
661 Expr D4 = vc_varExpr (vc, "D4", bv32); in test9()
662 Expr D3_sle_a_cond = vc_bvSLeExpr (vc, D3, a); in test9()
663 Expr D3_sle_a_expr = vc_iteExpr (vc, D3_sle_a_cond, one, zero); in test9()
664 Expr D4_eq_D3_sle_a_expr = vc_eqExpr (vc, D4, D3_sle_a_expr); in test9()
665 vc_assertFormula (vc, D4_eq_D3_sle_a_expr); in test9()
666 Expr D6 = vc_varExpr (vc, "D6", bv32); in test9()
667 Expr D3_slt_a_cond = vc_bvSLtExpr (vc, D3, a); in test9()
668 Expr D3_slt_a_expr = vc_iteExpr (vc, D3_slt_a_cond, one, zero); in test9()
669 Expr D6_eq_D3_slt_a_expr = vc_eqExpr (vc, D6, D3_slt_a_expr); in test9()
670 vc_assertFormula (vc, D6_eq_D3_slt_a_expr); in test9()
671 Expr zero_lt_a = vc_bvSLtExpr (vc, zero, a); in test9()
672 vc_assertFormula (vc, zero_lt_a); in test9()
673 Expr D4_eq_one = vc_eqExpr (vc, D4, one); in test9()
674 Expr not_D4_eq_one = vc_notExpr (vc, D4_eq_one); in test9()
675 vc_query (vc, not_D4_eq_one); in test9()
676 Expr D6_eq_one = vc_eqExpr (vc, D6, one); in test9()
677 Expr not_D6_eq_one = vc_notExpr (vc, D6_eq_one); in test9()
678 vc_query (vc, not_D6_eq_one); in test9()
679 vc_destroyValidityChecker(vc); in test9()
686 VC vc = vc_createValidityChecker(flags); in test10() local
687 Type a = vc_createType(vc, "a"); in test10()
688 Type aa = vc_funType1(vc, a, a); in test10()
689 Op f1 = vc_createOp(vc, "f", aa); in test10()
691 Op f2 = vc_lookupOp(vc, "f", &aa2); in test10()
694 Expr x = vc_varExpr(vc, "x", a); in test10()
695 Expr f1x = vc_funExpr1(vc, f1, x); in test10()
696 Expr f2x = vc_funExpr1(vc, f2, x); in test10()
697 Expr eq = vc_eqExpr(vc, f1x, f2x); in test10()
698 int res = vc_query(vc, eq); in test10()
700 vc_destroyValidityChecker(vc); in test10()
707 VC vc = vc_createValidityChecker(flags); in test11() local
708 Type a = vc_createType(vc, "a"); in test11()
709 Type aa = vc_funType1(vc, a, a); in test11()
710 Op f = vc_createOp(vc, "f", aa); in test11()
711 Expr x = vc_varExpr(vc, "x", a); in test11()
712 Expr fx = vc_funExpr1(vc, f, x); in test11()
713 Expr ffx = vc_funExpr1(vc, f, fx); in test11()
714 Expr e = vc_eqExpr(vc, x, fx); in test11()
715 Expr expectE = vc_eqExpr(vc, fx, ffx); in test11()
716 Expr newE = vc_substExpr(vc, e, &x, 1, &fx, 1); in test11()
718 vc_destroyValidityChecker(vc); in test11()