diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-12-06 13:24:01 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-12-06 13:26:24 -0600 |
| commit | c4410c3123f7dc73bb0296ebe01c172e96b210cc (patch) | |
| tree | e585487fee95d2098c9229b84db236b008fcba4c /examples/api/java | |
| parent | 5e2eef449c11b0be6b25942bccf7b0712ebe2d20 (diff) | |
Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.
Diffstat (limited to 'examples/api/java')
| -rw-r--r-- | examples/api/java/Makefile.am | 6 | ||||
| -rw-r--r-- | examples/api/java/Strings.java | 67 |
2 files changed, 71 insertions, 2 deletions
diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am index 7216d758e..d12f2877e 100644 --- a/examples/api/java/Makefile.am +++ b/examples/api/java/Makefile.am @@ -9,7 +9,8 @@ noinst_DATA += \ HelloWorld.class \ LinearArith.class \ Datatypes.class \ - PipedInput.class + PipedInput.class \ + Strings.class endif %.class: %.java @@ -23,7 +24,8 @@ EXTRA_DIST = \ HelloWorld.java \ LinearArith.java \ Datatypes.java \ - PipedInput.java + PipedInput.java \ + Strings.java # for installation examplesdir = $(docdir)/$(subdir) diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java new file mode 100644 index 000000000..293118d62 --- /dev/null +++ b/examples/api/java/Strings.java @@ -0,0 +1,67 @@ +/********************* */
+/*! \file Strings.java
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Reasoning about strings with CVC4 via Java API.
+ **
+ ** A simple demonstration of reasoning about strings with CVC4 via Jave API.
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+
+public class Strings {
+ public static void main(String[] args) {
+ System.loadLibrary("cvc4jni");
+
+ ExprManager em = new ExprManager();
+ SmtEngine smt = new SmtEngine(em);
+
+ // Set the logic
+ smt.setLogic("S");
+
+ // Produce models
+ smt.setOption("produce-models", new SExpr(true));
+ // The option strings-exp is needed
+ smt.setOption("strings-exp", new SExpr(true));
+ // output-language
+ smt.setOption("output-language", new SExpr("smt2"));
+
+ // String type
+ Type string = em.stringType();
+
+ // Variables
+ Expr x = em.mkVar("x", string);
+ Expr y = em.mkVar("y", string);
+ Expr z = em.mkVar("z", string);
+
+ // String concatenation: x.y
+ Expr lhs = em.mkExpr(Kind.STRING_CONCAT, x, y);
+ // String concatenation: z.z
+ Expr rhs = em.mkExpr(Kind.STRING_CONCAT, z, z);;
+ // x.y = z.z
+ Expr formula1 = em.mkExpr(Kind.EQUAL, lhs, rhs);
+
+ // Length of y: |y|
+ Expr leny = em.mkExpr(Kind.STRING_LENGTH, y);
+ // |y| >= 1
+ Expr formula2 = em.mkExpr(Kind.GEQ, leny, em.mkConst(new Rational(1)));
+
+ // Make a query
+ Expr q = em.mkExpr(Kind.AND,
+ formula1,
+ formula2);
+
+ // check sat
+ Result result = smt.checkSat(q);
+ System.out.println("CVC4 reports: " + q + " is " + result + ".");
+
+ System.out.println(" x = " + smt.getValue(x));
+ }
+}
|