1 /********************* */
2 /*! \file SimpleVC.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 interface
16 ** A simple demonstration of the Java interface.
18 ** To run the resulting class file, you need to do something like the
22 ** -classpath path/to/CVC4.jar \
23 ** -Djava.library.path=/dir/containing/java/CVC4.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/CVC4.jar \
32 ** -Djava.library.path=builds/src/bindings/java/.libs \
36 import edu
.nyu
.acsys
.CVC4
.*;
38 public class SimpleVC
{
39 public static void main(String
[] args
) {
40 System
.loadLibrary("cvc4jni");
42 ExprManager em
= new ExprManager();
43 SmtEngine smt
= new SmtEngine(em
);
45 // Prove that for integers x and y:
46 // x > 0 AND y > 0 => 2x + y >= 3
48 Type integer
= em
.integerType();
50 Expr x
= em
.mkVar("x", integer
);
51 Expr y
= em
.mkVar("y", integer
);
52 Expr zero
= em
.mkConst(new Rational(0));
54 Expr x_positive
= em
.mkExpr(Kind
.GT
, x
, zero
);
55 Expr y_positive
= em
.mkExpr(Kind
.GT
, y
, zero
);
57 Expr two
= em
.mkConst(new Rational(2));
58 Expr twox
= em
.mkExpr(Kind
.MULT
, two
, x
);
59 Expr twox_plus_y
= em
.mkExpr(Kind
.PLUS
, twox
, y
);
61 Expr three
= em
.mkConst(new Rational(3));
62 Expr twox_plus_y_geq_3
= em
.mkExpr(Kind
.GEQ
, twox_plus_y
, three
);
65 new BoolExpr(em
.mkExpr(Kind
.AND
, x_positive
, y_positive
)).
66 impExpr(new BoolExpr(twox_plus_y_geq_3
));
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: " + smt
.query(formula
));