diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-26 17:58:39 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-26 19:43:25 -0400 |
commit | ad5e31e2031349c9b9d0bf5d9fcaa1ea7950db58 (patch) | |
tree | dd3e7e943628f1410f4a8d2f260c994d62be308d /examples/api | |
parent | a9912269ab2b47b783a66f381b14148c0ac73e93 (diff) |
Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/java/Makefile.am | 6 | ||||
-rw-r--r-- | examples/api/java/PipedInput.java | 69 |
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); + } + } +} |