///////////////////////////////////////////////////////////////////////////////
// //
// File: main.cpp //
// Author: Clark Barrett //
// Created: Sat Apr 19 01:47:47 2003 //
// //
///////////////////////////////////////////////////////////////////////////////
#include "c_interface.h"
#include <stdio.h>
#define TRUE 1
#define FALSE 0
#define FatalAssert(b,msg) \
if (!(b)) { \
fprintf(stderr, "Assertion Failure: %s\n", msg); \
exit(1); }
// Check whether e is valid
void check_error(char* msg) {
if(get_error_status() < 0) {
fprintf(stderr, "%s\n", msg);
fprintf(stderr, "%s\n", get_error_string());
exit(1);
}
}
void check(VC vc, Expr e)
{
printf("Query: ");
vc_printExpr(vc, e);
check_error("Error occured during query");
switch (vc_query(vc, e)) {
case 0:
printf("Invalid\n\n");
break;
case 1:
printf("Valid\n\n");
break;
}
}
// Make a new assertion
void newAssertion(VC vc, Expr e)
{
// Testing printing to file descriptor. Turns out, we need to flush
// the file in C before printing through C++ (they apparently use
// different buffers, and text may come out of order).
printf("Assert: "); fflush(stdout);
vc_printExprFile(vc, e, 1);
vc_assertFormula(vc, e);
check_error("Error occured during assertion");
}
void test1()
{
Flags flags = vc_createFlags();
VC vc;
Type b;
Expr p, np, e;
Type r, real2real;
Expr x, y, fx, fy, xeqy, fxeqfy, w, z, weqx, yeqz, one, two, xeqone, xeqtwo,
simp, simp2;
Op f;
Expr* assertions;
int i, size;
vc_setStringFlag(flags, "dump-log", ".testc1.cvc");
vc = vc_createValidityChecker(flags);
// Check p OR ~p
b = vc_boolType(vc);
p = vc_varExpr(vc, "p", vc_boolType(vc));
np = vc_notExpr(vc, p);
e = vc_orExpr(vc, p, np);
check(vc, e);
vc_deleteType(b);
vc_deleteExpr(p);
vc_deleteExpr(np);
vc_deleteExpr(e);
/* Check x = y -> f(x) = f(y) */
r = vc_realType(vc);
x = vc_varExpr(vc, "x", r);
y = vc_varExpr(vc, "y", r);
real2real = vc_funType1(vc, r, r);
f = vc_createOp(vc, "f", real2real);
fx = vc_funExpr1(vc, f, x);
fy = vc_funExpr1(vc, f, y);
xeqy = vc_eqExpr(vc, x, y);
fxeqfy = vc_eqExpr(vc, fx, fy);
e = vc_impliesExpr(vc, xeqy, fxeqfy);
check(vc, e);
vc_deleteType(real2real);
vc_deleteExpr(e);
// Check f(x) = f(y) -> x = y
e = vc_impliesExpr(vc, fxeqfy, xeqy);
check(vc, e);
vc_deleteExpr(e);
// Get counter-example
printf("Scope level: %d\n", vc_scopeLevel(vc));
printf("Counter-example:\n");
assertions = vc_getCounterExample(vc, &size);
for (i = 0; i < size; ++i) {
vc_printExpr(vc, assertions[i]);
}
printf("End of counter-example\n\n");
// Reset to initial scope
printf("Resetting\n");
vc_popto(vc, 1);
printf("Scope level: %d\n\n", vc_scopeLevel(vc));
// Check w = x & x = y & y = z & f(x) = f(y) & x = 1 & z = 2
w = vc_varExpr(vc, "w", r);
z = vc_varExpr(vc, "z", r);
printf("Push Scope\n\n");
vc_push(vc);
weqx = vc_eqExpr(vc, w, x);
yeqz = vc_eqExpr(vc, y, z);
one = vc_ratExpr(vc, 1, 1);
two = vc_ratExpr(vc, 2, 1);
xeqone = vc_eqExpr(vc, x, one);
xeqtwo = vc_eqExpr(vc, x, two);
newAssertion(vc, weqx);
newAssertion(vc, xeqy);
newAssertion(vc, yeqz);
newAssertion(vc, fxeqfy);
newAssertion(vc, xeqone);
newAssertion(vc, xeqtwo);
printf("\nsimplify(w) = ");
simp = vc_simplify(vc, w);
vc_printExpr(vc, simp);
printf("\n");
printf("Inconsistent?: %d\n", vc_inconsistent(vc, &assertions, &size));
check_error("Error occured during inconsistency check");
printf("Assumptions Used:\n");
for (i = 0; i < size; ++i) {
vc_printExpr(vc, assertions[i]);
}
printf("\nPop Scope\n\n");
vc_pop(vc);
printf("simplify(w) = ");
simp2 = vc_simplify(vc, w);
vc_printExpr(vc, simp2);
printf("\n");
printf("Inconsistent?: %d\n", vc_inconsistent(vc, &assertions, &size));
vc_deleteType(r);
vc_deleteExpr(x);
vc_deleteExpr(y);
vc_deleteOp(f);
vc_deleteExpr(fx);
vc_deleteExpr(fy);
vc_deleteExpr(xeqy);
vc_deleteExpr(fxeqfy);
vc_deleteExpr(w);
vc_deleteExpr(z);
vc_deleteExpr(weqx);
vc_deleteExpr(yeqz);
vc_deleteExpr(one);
vc_deleteExpr(two);
vc_deleteExpr(xeqone);
vc_deleteExpr(xeqtwo);
vc_deleteExpr(simp);
vc_deleteExpr(simp2);
vc_destroyValidityChecker(vc);
vc_deleteFlags(flags);
}
void test2()
{
VC vc = vc_createValidityChecker(NULL);
// Check x = y -> g(x,y) = g(y,x)
Type r = vc_realType(vc);
Expr x = vc_varExpr(vc, "x", r);
Expr y = vc_varExpr(vc, "y", r);
Type realxreal2real = vc_funType2(vc, r, r, r);
Op g = vc_createOp(vc, "g", realxreal2real);
Expr gxy = vc_funExpr2(vc, g, x, y);
Expr gyx = vc_funExpr2(vc, g, y, x);
Expr xeqy = vc_eqExpr(vc, x, y);
Expr gxyeqgyx = vc_eqExpr(vc, gxy, gyx);
Expr e = vc_impliesExpr(vc, xeqy, gxyeqgyx);
Type v[2];
Op h;
Expr hxy, hyx, hxyeqhyx;
check(vc, e);
vc_deleteType(realxreal2real);
vc_deleteOp(g);
vc_deleteExpr(gxy);
vc_deleteExpr(gyx);
vc_deleteExpr(gxyeqgyx);
vc_deleteExpr(e);
v[0] = r;
v[1] = r;
realxreal2real = vc_funTypeN(vc, v, r, 2);
h = vc_createOp(vc, "h", realxreal2real);
hxy = vc_funExpr2(vc, h, x, y);
hyx = vc_funExpr2(vc, h, y, x);
hxyeqhyx = vc_eqExpr(vc, hxy, hyx);
e = vc_impliesExpr(vc, xeqy, hxyeqhyx);
check(vc, e);
vc_deleteType(r);
vc_deleteExpr(x);
vc_deleteExpr(y);
vc_deleteType(realxreal2real);
vc_deleteExpr(hxy);
vc_deleteExpr(hxyeqhyx);
vc_deleteExpr(e);
vc_destroyValidityChecker(vc);
}
/* void test3() */
/* { */
/* VC vc = vc_createValidityChecker(NULL); */
/* // Check x = y -> g(x,y) = g(y,x) */
/* Type r = vc_realType(vc); */
/* Expr x = vc_varExpr(vc, "x", r); */
/* Expr y = vc_varExpr(vc, "y", r); */
/* Type realxreal2real = vc_funType2(vc, r, r, r); */
/* Op g = vc_createOp(vc, "g", realxreal2real); */
/* Expr gxy = vc_parseExpr(vc, "g(x,y)"); */
/* Expr gxy2; */
/* vc_printExpr(vc, gxy); */
/* gxy2 = vc_funExpr2(vc, g, x, y); */
/* vc_printExpr(vc, gxy2); */
/* FatalAssert((gxy == gxy2), "Should be equal"); */
/* vc_deleteType(r); */
/* vc_deleteExpr(x); */
/* vc_deleteExpr(y); */
/* vc_deleteType(realxreal2real); */
/* vc_deleteOp(g); */
/* vc_deleteExpr(gxy); */
/* vc_deleteExpr(gxy2); */
/* vc_destroyValidityChecker(vc); */
/* } */
void test4(int regressLevel)
{
VC vc = vc_createValidityChecker(NULL);
// Check x >= 10 /\ x >= 40 /\ y <= 0 -->
// x >= 1 /\ y < 10
Type r = vc_realType(vc);
Expr x = vc_varExpr(vc, "x", r);
Expr y = vc_varExpr(vc, "y", r);
Expr ten = vc_ratExpr(vc, 10, 1);
Expr ge = vc_geExpr(vc, x, ten);
Expr forty = vc_ratExpr(vc, 40, 1);
Expr ge2 = vc_geExpr(vc, x, forty);
Expr zero = vc_ratExpr(vc, 0, 1);
Expr ge3 = vc_leExpr(vc, y, zero);
Expr children[3];
Expr hyp, one, conc, query;
int i;
children[0] = ge;
children[1] = ge2;
children[2] = ge3;
hyp = vc_andExprN(vc, children, 3);
vc_deleteType(r);
vc_deleteExpr(ge);
vc_deleteExpr(forty);
vc_deleteExpr(ge2);
vc_deleteExpr(zero);
vc_deleteExpr(ge3);
one = vc_ratExpr(vc, 1, 1);
ge = vc_geExpr(vc, x, one);
ge2 = vc_ltExpr(vc, y, ten);
conc = vc_andExpr(vc, ge, ge2);
query = vc_impliesExpr(vc, hyp, conc);
vc_deleteExpr(x);
vc_deleteExpr(y);
vc_deleteExpr(ten);
vc_deleteExpr(hyp);
vc_deleteExpr(one);
vc_deleteExpr(ge);
vc_deleteExpr(ge2);
vc_deleteExpr(conc);
for (i = 0; i < 100*regressLevel; i++)
vc_query(vc, query);
vc_deleteExpr(query);
vc_destroyValidityChecker(vc);
}
void test5()
{
Flags flags = vc_createFlags();
VC vc;
Type r;
Expr x, xEQx, p;
vc_setBoolFlag(flags, "proofs", TRUE);
vc = vc_createValidityChecker(flags);
r = vc_realType(vc);
x = vc_varExpr(vc, "x", r);
xEQx = vc_eqExpr(vc, x, x);
vc_query(vc, xEQx);
p = vc_getProof(vc);
vc_printExpr(vc, p);
vc_deleteType(r);
vc_deleteExpr(x);
vc_deleteExpr(xEQx);
vc_deleteExpr(p);
vc_destroyValidityChecker(vc);
vc_deleteFlags(flags);
}
void test6()
{
Flags flags = vc_createFlags();
VC vc;
Expr p, p3, p32;
char *x;
vc_setBoolFlag(flags, "proofs", 1);
vc_setBoolFlag(flags, "dagify-exprs", 0);
vc = vc_createValidityChecker(flags);
p = vc_getProofOfFile(vc,"benchmarks/add1.cvc");
check_error("Failed to check file");
/* p3 = getChild(p,3); */
/* p32 = getChild(p3,2); */
/* if (isLambda(p32)) */
/* printf("The expression is Lambda\n"); */
/* else */
/* printf("The expression is not Lambda\n"); */
/* x = exprString(p32); */
/* printf("Test expr,%s",x);*/
}
int printImpliedLiterals(VC vc)
{
int count = 0;
Expr impLit = vc_getImpliedLiteral(vc);
printf("Implied Literals:\n");
while (impLit) {
++count;
vc_printExpr(vc, impLit);
vc_deleteExpr(impLit);
impLit = vc_getImpliedLiteral(vc);
}
return count;
}
void test7()
{
VC vc = vc_createValidityChecker(NULL);
Type r = vc_realType(vc);
Type b = vc_boolType(vc);
Expr x = vc_varExpr(vc, "x", r);
Expr y = vc_varExpr(vc, "y", r);
Expr z = vc_varExpr(vc, "z", r);
Type real2real = vc_funType1(vc, r, r);
Type real2bool = vc_funType1(vc, r, b);
Op f = vc_createOp(vc, "f", real2real);
Op p = vc_createOp(vc, "p", real2bool);
Expr fx = vc_funExpr1(vc, f, x);
Expr fy = vc_funExpr1(vc, f, y);
Expr fxeqfy = vc_eqExpr(vc, fx, fy);
Expr px = vc_funExpr1(vc, p, x);
Expr py = vc_funExpr1(vc, p, y);
Expr xeqy = vc_eqExpr(vc, x, y);
Expr yeqx = vc_eqExpr(vc, y, x);
Expr xeqz = vc_eqExpr(vc, x, z);
Expr zeqx = vc_eqExpr(vc, z, x);
Expr yeqz = vc_eqExpr(vc, y, z);
Expr zeqy = vc_eqExpr(vc, z, y);
Expr notxeqz = vc_notExpr(vc, xeqz);
int c;
vc_registerAtom(vc, xeqy);
vc_registerAtom(vc, yeqx);
vc_registerAtom(vc, xeqz);
vc_registerAtom(vc, zeqx);
vc_registerAtom(vc, yeqz);
vc_registerAtom(vc, zeqy);
vc_registerAtom(vc, px);
vc_registerAtom(vc, py);
vc_registerAtom(vc, fxeqfy);
printf("Push\n");
vc_push(vc);
printf("Assert x = y\n");
vc_assertFormula(vc, xeqy);
c = printImpliedLiterals(vc);
FatalAssert(c==3,"Implied literal error 0");
printf("Push\n");
vc_push(vc);
printf("Assert x /= z\n");
vc_assertFormula(vc, notxeqz);
c = printImpliedLiterals(vc);
FatalAssert(c==4,"Implied literal error 1");
printf("Pop\n");
vc_pop(vc);
printf("Pop\n");
vc_pop(vc);
vc_deleteExpr(notxeqz);
vc_deleteExpr(zeqy);
vc_deleteExpr(yeqz);
vc_deleteExpr(zeqx);
vc_deleteExpr(xeqz);
vc_deleteExpr(yeqx);
vc_deleteExpr(xeqy);
vc_deleteExpr(py);
vc_deleteExpr(px);
vc_deleteExpr(fxeqfy);
vc_deleteExpr(fy);
vc_deleteExpr(fx);
vc_deleteOp(p);
vc_deleteOp(f);
vc_deleteType(real2bool);
vc_deleteType(real2real);
vc_deleteExpr(z);
vc_deleteExpr(y);
vc_deleteExpr(x);
vc_deleteType(b);
vc_deleteType(r);
vc_destroyValidityChecker(vc);
}
int main(int argc, char** argv)
{
int regressLevel = 2;
if (argc > 1) regressLevel = atoi(argv[1]);
printf("Running C API test, regress level = %d\n", regressLevel);
printf("\ntest1() {\n");
test1();
check_error("test1");
printf("\n}\n\ntest2() {\n");
test2();
check_error("test2");
/* TODO: implement parseExpr */
/* test3(); */
/* check_error("test3"); */
test4(regressLevel);
check_error("test4");
printf("\n}\n\ntest5() {\n");
test5();
check_error("test5");
if (regressLevel > 0) {
printf("\n}\ntest6()\n");
test6();
check_error("test6");
}
printf("\n}\ntest7()\n");
test7();
check_error("test7");
return 0;
}
syntax highlighted by Code2HTML, v. 0.9.1