1 /********************* */
2 /*! \file SimpleVCCompat.java
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief A simple demonstration of the Java compatibility interface
15 ** (quite similar to the old CVC3 Java interface)
17 ** A simple demonstration of the Java compatibility interface
18 ** (quite similar to the old CVC3 Java interface).
20 ** To run the resulting class file, you need to do something like the
24 ** -classpath path/to/CVC4compat.jar \
25 ** -Djava.library.path=/dir/containing/libcvc4bindings_java_compat.so \
28 ** For example, if you are building CVC4 without specifying your own
29 ** build directory, the build process puts everything in builds/, and
30 ** you can run this example (after building it with "make") like this:
33 ** -classpath builds/examples:builds/src/bindings/compat/java/CVC4compat.jar \
34 ** -Djava.library.path=builds/src/bindings/compat/java/.libs \
40 public class SimpleVCCompat
{
41 public static void main(String
[] args
) {
42 //System.loadLibrary("cvc4bindings_java_compat");
44 ValidityChecker vc
= ValidityChecker
.create();
46 // Prove that for integers x and y:
47 // x > 0 AND y > 0 => 2x + y >= 3
49 Type integer
= vc
.intType();
51 Expr x
= vc
.varExpr("x", integer
);
52 Expr y
= vc
.varExpr("y", integer
);
53 Expr zero
= vc
.ratExpr(0);
55 Expr x_positive
= vc
.gtExpr(x
, zero
);
56 Expr y_positive
= vc
.gtExpr(y
, zero
);
58 Expr two
= vc
.ratExpr(2);
59 Expr twox
= vc
.multExpr(two
, x
);
60 Expr twox_plus_y
= vc
.plusExpr(twox
, y
);
62 Expr three
= vc
.ratExpr(3);
63 Expr twox_plus_y_geq_3
= vc
.geExpr(twox_plus_y
, three
);
65 Expr formula
= vc
.impliesExpr(vc
.andExpr(x_positive
, y_positive
),
68 System
.out
.println("Checking validity of formula " + formula
+ " with CVC4.");
69 System
.out
.println("CVC4 should report VALID.");
70 System
.out
.println("Result from CVC4 is: " + vc
.query(formula
));