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-2012 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 interface
14 ** A simple demonstration of the Java interface.
16 ** To run the resulting class file, you need to do something like the
20 ** -classpath path/to/CVC4.jar \
21 ** -Djava.library.path=/dir/containing/java/CVC4.so \
24 ** For example, if you are building CVC4 without specifying your own
25 ** build directory, the build process puts everything in builds/, and
26 ** you can run this example (after building it with "make") like this:
29 ** -classpath builds/examples:builds/src/bindings/CVC4.jar \
30 ** -Djava.library.path=builds/src/bindings/java/.libs \
34 import edu
.nyu
.acsys
.CVC4
.*;
36 public class SimpleVC
{
37 public static void main(String
[] args
) {
38 System
.loadLibrary("cvc4jni");
40 ExprManager em
= new ExprManager();
41 SmtEngine smt
= new SmtEngine(em
);
43 // Prove that for integers x and y:
44 // x > 0 AND y > 0 => 2x + y >= 3
46 Type integer
= em
.integerType();
48 Expr x
= em
.mkVar("x", integer
);
49 Expr y
= em
.mkVar("y", integer
);
50 Expr zero
= em
.mkConst(new Rational(0));
52 Expr x_positive
= em
.mkExpr(Kind
.GT
, x
, zero
);
53 Expr y_positive
= em
.mkExpr(Kind
.GT
, y
, zero
);
55 Expr two
= em
.mkConst(new Rational(2));
56 Expr twox
= em
.mkExpr(Kind
.MULT
, two
, x
);
57 Expr twox_plus_y
= em
.mkExpr(Kind
.PLUS
, twox
, y
);
59 Expr three
= em
.mkConst(new Rational(3));
60 Expr twox_plus_y_geq_3
= em
.mkExpr(Kind
.GEQ
, twox_plus_y
, three
);
63 new Expr(em
.mkExpr(Kind
.AND
, x_positive
, y_positive
)).
64 impExpr(new Expr(twox_plus_y_geq_3
));
66 System
.out
.println("Checking validity of formula " + formula
+ " with CVC4.");
67 System
.out
.println("CVC4 should report VALID.");
68 System
.out
.println("Result from CVC4 is: " + smt
.query(formula
));