Java streams example I forgot to add a long time ago

diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java
new file mode 100644 (file)
index 0000000..0b0984b
--- /dev/null
+++ b/examples/api/java/CVC4Streams.java
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file CVC4Streams.java
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Example of driving CVC4 parsing from Java streams
+ **
+ ** This example shows how CVC4 can be driven from Java streams.
+ **/
+
+import java.io.*;
+import edu.nyu.acsys.CVC4.*;
+
+public class CVC4Streams {
+  public static void main(String[] args) throws IOException {
+    System.loadLibrary("cvc4jni");
+    ExprManager exprMgr = new ExprManager();
+    SmtEngine smt = new SmtEngine(exprMgr);
+    smt.setOption("incremental", new SExpr(true));
+    smt.setOption("output-language", new SExpr("smt2"));
+
+    PipedOutputStream solverPipe = new PipedOutputStream();
+    PrintWriter toSolver = new PrintWriter(solverPipe);
+    PipedInputStream stream = new PipedInputStream(solverPipe);
+
+    toSolver.println("(set-logic QF_LIA)");
+    toSolver.println("(declare-fun x () Int)");
+    toSolver.println("(assert (= x 5))");
+    toSolver.println("(check-sat)");
+    toSolver.flush();
+
+    ParserBuilder pbuilder =
+      new ParserBuilder(exprMgr, "<string 1>")
+      .withInputLanguage(InputLanguage.INPUT_LANG_SMTLIB_V2)
+      .withLineBufferedStreamInput((java.io.InputStream)stream);
+    Parser parser = pbuilder.build();
+
+    Command cmd;
+    while((cmd = parser.nextCommand()) != null) {
+      System.out.println(cmd);
+      cmd.invoke(smt, System.out);
+    }
+
+    toSolver.println("(assert (= x 10))");
+    toSolver.println("(check-sat)");
+    toSolver.flush();
+
+    while((cmd = parser.nextCommand()) != null) {
+      System.out.println(cmd);
+      cmd.invoke(smt, System.out);
+    }
+  }
+}

diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am
index 84c818737f727eb8a75273c00b7750cd35be8a01..f4b8f104340918444e5e267f7ce1b274edf2043b 100644 (file)
--- a/examples/api/java/Makefile.am
+++ b/examples/api/java/Makefile.am
@@ -2,6 +2,7 @@ noinst_DATA =
 
 if CVC4_LANGUAGE_BINDING_JAVA
 noinst_DATA += \
+       CVC4Streams.class \
        BitVectors.class \
        BitVectorsAndArrays.class \
        Combination.class \
@@ -14,6 +15,7 @@ endif
        $(AM_V_JAVAC)$(JAVAC) -classpath "@builddir@/../../../src/bindings/CVC4.jar" -d "@builddir@" $<
 
 EXTRA_DIST = \
+       CVC4Streams.java \
        BitVectors.java \
        BitVectorsAndArrays.java \
        Combination.java \