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