test/java/HelloWorld.java


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

import static org.junit.Assert.assertEquals;
import org.junit.Before;
import org.junit.Test;

import edu.nyu.acsys.CVC4.*;

public class HelloWorld {
  static {
    System.loadLibrary("cvc4jni");
  }
  ExprManager em;
  SmtEngine smt;

  @Before
  public void initialize() {
    em = new ExprManager();
    smt = new SmtEngine(em);
  }

  @Test
  public void evaluatesExpression() {
    Expr helloworld = em.mkVar("Hello World!", em.booleanType());
    Result.Validity expect = Result.Validity.INVALID;
    Result.Validity actual = smt.query(helloworld).isValid();
    assertEquals(actual, expect);
  }
}