1 /********************* */
2 /*! \file SimpleVCCompat.java
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-2013 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 Java compatibility interface
13 ** (quite similar to the old CVC3 Java interface)
15 ** A simple demonstration of the Java compatibility interface
16 ** (quite similar to the old CVC3 Java interface).
18 ** To run the resulting class file, you need to do something like the
22 ** -classpath path/to/CVC4compat.jar \
23 ** -Djava.library.path=/dir/containing/libcvc4bindings_java_compat.so \
26 ** For example, if you are building CVC4 without specifying your own
27 ** build directory, the build process puts everything in builds/, and
28 ** you can run this example (after building it with "make") like this:
31 ** -classpath builds/examples:builds/src/bindings/compat/java/CVC4compat.jar \
32 ** -Djava.library.path=builds/src/bindings/compat/java/.libs \
38 public class SimpleVCCompat
{
39 public static void main(String
[] args
) {
40 ValidityChecker vc
= ValidityChecker
.create();
42 // Prove that for integers x and y:
43 // x > 0 AND y > 0 => 2x + y >= 3
45 Type integer
= vc
.intType();
47 Expr x
= vc
.varExpr("x", integer
);
48 Expr y
= vc
.varExpr("y", integer
);
49 Expr zero
= vc
.ratExpr(0);
51 Expr x_positive
= vc
.gtExpr(x
, zero
);
52 Expr y_positive
= vc
.gtExpr(y
, zero
);
54 Expr two
= vc
.ratExpr(2);
55 Expr twox
= vc
.multExpr(two
, x
);
56 Expr twox_plus_y
= vc
.plusExpr(twox
, y
);
58 Expr three
= vc
.ratExpr(3);
59 Expr twox_plus_y_geq_3
= vc
.geExpr(twox_plus_y
, three
);
61 Expr formula
= vc
.impliesExpr(vc
.andExpr(x_positive
, y_positive
),
64 System
.out
.println("Checking validity of formula " + formula
+ " with CVC4.");
65 System
.out
.println("CVC4 should report VALID.");
66 System
.out
.println("Result from CVC4 is: " + vc
.query(formula
));