From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 17 Jun 2013 22:36:26 +0000 (-0400)
Subject: Java streams example I forgot to add a long time ago
X-Git-Tag: cvc5-1.0.0~7287^2~96
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5177b11ad8cc5287fa7a8e65f78d5f6cfe23ead;p=cvc5.git

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
index 000000000..0b0984bf3
--- /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 84c818737..f4b8f1043 100644
--- 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 \