summaryrefslogtreecommitdiff
path: root/examples
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-03-26 17:58:39 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-03-26 19:43:25 -0400
commitad5e31e2031349c9b9d0bf5d9fcaa1ea7950db58 (patch)
treedd3e7e943628f1410f4a8d2f260c994d62be308d /examples
parenta9912269ab2b47b783a66f381b14148c0ac73e93 (diff)
Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac
Diffstat (limited to 'examples')
-rw-r--r--examples/api/java/Makefile.am6
-rw-r--r--examples/api/java/PipedInput.java69
2 files changed, 73 insertions, 2 deletions
diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am
index 55f637604..84c818737 100644
--- a/examples/api/java/Makefile.am
+++ b/examples/api/java/Makefile.am
@@ -6,7 +6,8 @@ noinst_DATA += \
BitVectorsAndArrays.class \
Combination.class \
HelloWorld.class \
- LinearArith.class
+ LinearArith.class \
+ PipedInput.class
endif
%.class: %.java
@@ -17,7 +18,8 @@ EXTRA_DIST = \
BitVectorsAndArrays.java \
Combination.java \
HelloWorld.java \
- LinearArith.java
+ LinearArith.java \
+ PipedInput.java
# for installation
examplesdir = $(docdir)/$(subdir)
diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java
new file mode 100644
index 000000000..3a5470914
--- /dev/null
+++ b/examples/api/java/PipedInput.java
@@ -0,0 +1,69 @@
+/********************* */
+/*! \file PipedInput.java
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** 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 A simple demonstration of the input parsing capabilities of CVC4
+ ** when used from Java
+ **
+ ** A simple demonstration of the input parsing capabilities of CVC4 when
+ ** used from Java.
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+import java.io.*;
+
+public class PipedInput {
+ public static void main(String[] args) throws IOException {
+ System.loadLibrary("cvc4jni");
+
+ // Boilerplate setup for CVC4
+ ExprManager exprMgr = new ExprManager();
+ SmtEngine smt = new SmtEngine(exprMgr);
+ smt.setOption("incremental", new SExpr(true));
+ smt.setOption("output-language", new SExpr("smt2"));
+
+ // Set up a pair of connected Java streams
+ PipedOutputStream solverPipe = new PipedOutputStream();
+ PrintWriter toSolver = new PrintWriter(solverPipe);
+ PipedInputStream stream = new PipedInputStream(solverPipe);
+
+ // Write some things to CVC4's input stream, making sure to flush()
+ toSolver.println("(set-logic QF_LIA)");
+ toSolver.println("(declare-fun x () Int)");
+ toSolver.println("(assert (= x 5))");
+ toSolver.println("(check-sat)");
+ toSolver.flush();
+
+ // Set up the CVC4 parser
+ ParserBuilder pbuilder =
+ new ParserBuilder(exprMgr, "<string 1>")
+ .withInputLanguage(InputLanguage.INPUT_LANG_SMTLIB_V2)
+ .withLineBufferedStreamInput((java.io.InputStream)stream);
+ Parser parser = pbuilder.build();
+
+ // Read all the commands thus far
+ Command cmd;
+ while((cmd = parser.nextCommand()) != null) {
+ System.out.println(cmd);
+ cmd.invoke(smt, System.out);
+ }
+
+ // Write some more things to CVC4's input stream, making sure to flush()
+ toSolver.println("(assert (= x 10))");
+ toSolver.println("(check-sat)");
+ toSolver.flush();
+
+ // Read all the commands thus far
+ while((cmd = parser.nextCommand()) != null) {
+ System.out.println(cmd);
+ cmd.invoke(smt, System.out);
+ }
+ }
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback