examples/SimpleVC.java

   1 /*********************                                                        */
   2 /*! \file SimpleVC.java
   3  ** \verbatim
   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
  13  **
  14  ** \brief A simple demonstration of the Java interface
  15  **
  16  ** A simple demonstration of the Java interface.
  17  **
  18  ** To run the resulting class file, you need to do something like the
  19  ** following:
  20  **
  21  **   java \
  22  **     -classpath path/to/CVC4.jar \
  23  **     -Djava.library.path=/dir/containing/java/CVC4.so \
  24  **     SimpleVC
  25  **
  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:
  29  **
  30  **   java \
  31  **     -classpath builds/examples:builds/src/bindings/CVC4.jar \
  32  **     -Djava.library.path=builds/src/bindings/java/.libs \
  33  **     SimpleVC
  34  **/
  35
  36 import edu.nyu.acsys.CVC4.*;
  37
  38 public class SimpleVC {
  39   public static void main(String[] args) {
  40     System.loadLibrary("cvc4jni");
  41
  42     ExprManager em = new ExprManager();
  43     SmtEngine smt = new SmtEngine(em);
  44
  45     // Prove that for integers x and y:
  46     //   x > 0 AND y > 0  =>  2x + y >= 3
  47
  48     Type integer = em.integerType();
  49
  50     Expr x = em.mkVar("x", integer);
  51     Expr y = em.mkVar("y", integer);
  52     Expr zero = em.mkConst(new Rational(0));
  53
  54     Expr x_positive = em.mkExpr(Kind.GT, x, zero);
  55     Expr y_positive = em.mkExpr(Kind.GT, y, zero);
  56
  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);
  60
  61     Expr three = em.mkConst(new Rational(3));
  62     Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three);
  63
  64     BoolExpr formula =
  65       new BoolExpr(em.mkExpr(Kind.AND, x_positive, y_positive)).
  66       impExpr(new BoolExpr(twox_plus_y_geq_3));
  67
  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));
  71   }
  72 }