test/java/HelloWorld.java

   1 /*********************                                                        */
   2 /*! \file HelloWorld.java
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Pat Hawks
   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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 import static org.junit.Assert.assertEquals;
  19 import org.junit.Before;
  20 import org.junit.Test;
  21
  22 import edu.nyu.acsys.CVC4.*;
  23
  24 public class HelloWorld {
  25   static {
  26     System.loadLibrary("cvc4jni");
  27   }
  28   ExprManager em;
  29   SmtEngine smt;
  30
  31   @Before
  32   public void initialize() {
  33     em = new ExprManager();
  34     smt = new SmtEngine(em);
  35   }
  36
  37   @Test
  38   public void evaluatesExpression() {
  39     Expr helloworld = em.mkVar("Hello World!", em.booleanType());
  40     Result.Validity expect = Result.Validity.INVALID;
  41     Result.Validity actual = smt.query(helloworld).isValid();
  42     assertEquals(actual, expect);
  43   }
  44 }