diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-21 03:26:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-21 03:26:13 +0000 |
commit | 3b1689612bb2ff984aa90cd84093ffc043d78ba9 (patch) | |
tree | 872cf423273a331e110ff3868cd5281c960dd3b1 /test/system/CVC4JavaTest.java | |
parent | 69d8f8da6bbb856964d47a583ceb4e50060e9457 (diff) |
considerable bindings interface work, some improvements to build
Diffstat (limited to 'test/system/CVC4JavaTest.java')
-rw-r--r-- | test/system/CVC4JavaTest.java | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java new file mode 100644 index 000000000..8151300f4 --- /dev/null +++ b/test/system/CVC4JavaTest.java @@ -0,0 +1,50 @@ +import edu.nyu.acsys.CVC4.CVC4; + +import edu.nyu.acsys.CVC4.SmtEngine; +import edu.nyu.acsys.CVC4.ExprManager; +import edu.nyu.acsys.CVC4.Expr; +import edu.nyu.acsys.CVC4.Type; +import edu.nyu.acsys.CVC4.BoolExpr; +import edu.nyu.acsys.CVC4.Kind; +import edu.nyu.acsys.CVC4.Configuration; + +//import edu.nyu.acsys.CVC4.Exception; + +import edu.nyu.acsys.CVC4.Parser; +import edu.nyu.acsys.CVC4.ParserBuilder; + +public class CVC4JavaTest { + public static void main(String[] args) { + try { + System.loadLibrary("cvc4bindings_java"); + + CVC4.getDebugChannel().on("current"); + +System.out.println(Configuration.about()); +System.out.println("constructing"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + +System.out.println("getting type"); + Type t = em.booleanType(); +System.out.println("making vars"); + Expr a = em.mkVar("a", em.booleanType()); + Expr b = em.mkVar("b", em.booleanType()); +System.out.println("making sausage"); + BoolExpr e = new BoolExpr(em.mkExpr(Kind.AND, a, b)); + +System.out.println("about to check"); + + System.out.println(smt.checkSat(e)); + + System.out.println(smt.getStatisticsRegistry()); + + System.exit(1); + } catch(Exception e) { + System.err.println(e); + System.exit(1); + } + } +} + |