examples/SimpleVC.java

   1 /*********************                                                        */
   2 /*! \file SimpleVC.java
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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  **     -cp path/to/CVC4.jar:SimpleVC.jar \
  21  **     -Djava.library.path=/dir/containing/libcvc4jni.so \
  22  **     SimpleVC
  23  **
  24  **/
  25
  26 import edu.stanford.CVC4.*;
  27
  28 public class SimpleVC {
  29   public static void main(String[] args) {
  30     System.loadLibrary("cvc4jni");
  31
  32     ExprManager em = new ExprManager();
  33     SmtEngine smt = new SmtEngine(em);
  34
  35     // Prove that for integers x and y:
  36     //   x > 0 AND y > 0  =>  2x + y >= 3
  37
  38     Type integer = em.integerType();
  39
  40     Expr x = em.mkVar("x", integer);
  41     Expr y = em.mkVar("y", integer);
  42     Expr zero = em.mkConst(new Rational(0));
  43
  44     Expr x_positive = em.mkExpr(Kind.GT, x, zero);
  45     Expr y_positive = em.mkExpr(Kind.GT, y, zero);
  46
  47     Expr two = em.mkConst(new Rational(2));
  48     Expr twox = em.mkExpr(Kind.MULT, two, x);
  49     Expr twox_plus_y = em.mkExpr(Kind.PLUS, twox, y);
  50
  51     Expr three = em.mkConst(new Rational(3));
  52     Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three);
  53
  54     Expr formula =
  55       new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)).
  56       impExpr(new Expr(twox_plus_y_geq_3));
  57
  58     System.out.println(
  59         "Checking entailment of formula " + formula + " with CVC4.");
  60     System.out.println("CVC4 should report ENTAILED.");
  61     System.out.println("Result from CVC4 is: " + smt.checkEntailed(formula));
  62   }
  63 }