diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/api/java/CVC4Streams.java | 59 | ||||
| -rw-r--r-- | examples/api/java/Makefile.am | 2 |
2 files changed, 61 insertions, 0 deletions
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 \ |