1 /********************* */
2 /*! \file simple_vc_compat_c.c
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief A simple demonstration of the C compatibility interface
13 ** (quite similar to the old CVC3 C interface)
15 ** A simple demonstration of the C compatibility interface
16 ** (quite similar to the old CVC3 C interface).
22 /* #include <cvc4/bindings/compat/c/c_interface.h> /* use this after CVC4 is properly installed */
23 #include "bindings/compat/c/c_interface.h"
26 VC vc
= vc_createValidityChecker(NULL
);
28 /* Prove that for integers x and y:
29 * x > 0 AND y > 0 => 2x + y >= 3 */
31 Type integer
= vc_intType(vc
);
33 Expr x
= vc_varExpr(vc
, "x", integer
);
34 Expr y
= vc_varExpr(vc
, "y", integer
);
35 Expr zero
= vc_ratExpr(vc
, 0, 1);
37 Expr x_positive
= vc_gtExpr(vc
, x
, zero
);
38 Expr y_positive
= vc_gtExpr(vc
, y
, zero
);
40 Expr two
= vc_ratExpr(vc
, 2, 1);
41 Expr twox
= vc_multExpr(vc
, two
, x
);
42 Expr twox_plus_y
= vc_plusExpr(vc
, twox
, y
);
44 Expr three
= vc_ratExpr(vc
, 3, 1);
45 Expr twox_plus_y_geq_3
= vc_geExpr(vc
, twox_plus_y
, three
);
47 Expr formula
= vc_impliesExpr(vc
, vc_andExpr(vc
, x_positive
, y_positive
),
50 char* formulaString
= vc_printExprString(vc
, formula
);
52 printf("Checking validity of formula %s with CVC4.\n", formulaString
);
53 printf("CVC4 should return 1 (meaning VALID).\n");
54 printf("Result from CVC4 is: %d\n", vc_query(vc
, formula
));