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 | |
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')
-rw-r--r-- | examples/api/Makefile.am | 8 | ||||
-rw-r--r-- | examples/api/java/Makefile.am | 6 | ||||
-rw-r--r-- | examples/api/java/Strings.java | 67 | ||||
-rw-r--r-- | examples/api/strings.cpp | 101 |
4 files changed, 179 insertions, 3 deletions
diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am index a1455d168..1b3e0b086 100644 --- a/examples/api/Makefile.am +++ b/examples/api/Makefile.am @@ -12,7 +12,8 @@ noinst_PROGRAMS = \ datatypes \ helloworld \ linear_arith \ - sets + sets \ + strings noinst_DATA = @@ -53,6 +54,11 @@ sets_SOURCES = \ sets_LDADD = \ @builddir@/../../src/libcvc4.la +strings_SOURCES = \ + strings.cpp +strings_LDADD = \ + @builddir@/../../src/libcvc4.la + # for installation examplesdir = $(docdir)/$(subdir) examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST) 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));
+ }
+}
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp new file mode 100644 index 000000000..a424c654a --- /dev/null +++ b/examples/api/strings.cpp @@ -0,0 +1,101 @@ +/********************* */
+/*! \file sets.cpp
+ ** \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 C++ API.
+ **
+ ** A simple demonstration of reasoning about strings with CVC4 via C++ API.
+ **/
+
+#include <iostream>
+
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+
+int main() {
+ ExprManager em;
+ SmtEngine smt(&em);
+
+ // Set the logic
+ smt.setLogic("S");
+
+ // Produce models
+ smt.setOption("produce-models", true);
+
+ // The option strings-exp is needed
+ smt.setOption("strings-exp", true);
+
+ // Set output language to SMTLIB2
+ std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+
+ // String type
+ Type string = em.stringType();
+
+ // std::string
+ std::string std_str_ab("ab");
+ // CVC4::String
+ CVC4::String cvc4_str_ab(std_str_ab);
+ CVC4::String cvc4_str_abc("abc");
+ // String constants
+ Expr ab = em.mkConst(cvc4_str_ab);
+ Expr abc = em.mkConst(CVC4::String("abc"));
+ // String variables
+ Expr x = em.mkVar("x", string);
+ Expr y = em.mkVar("y", string);
+ Expr z = em.mkVar("z", string);
+
+ // String concatenation: x.ab.y
+ Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y);
+ // String concatenation: abc.z
+ Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z);
+ // x.ab.y = abc.z
+ Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs);
+
+ // Length of y: |y|
+ Expr leny = em.mkExpr(kind::STRING_LENGTH, y);
+ // |y| >= 0
+ Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0)));
+
+ // Regular expression: (ab[c-e]*f)|g|h
+ Expr r = em.mkExpr(kind::REGEXP_UNION,
+ em.mkExpr(kind::REGEXP_CONCAT,
+ em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))),
+ em.mkExpr(kind::REGEXP_STAR,
+ em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))),
+ em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))),
+ em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))),
+ em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("h"))));
+
+ // String variables
+ Expr s1 = em.mkVar("s1", string);
+ Expr s2 = em.mkVar("s2", string);
+ // String concatenation: s1.s2
+ Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2);
+
+ // s1.s2 in (ab[c-e]*f)|g|h
+ Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r);
+
+ // Make a query
+ Expr q = em.mkExpr(kind::AND,
+ formula1,
+ formula2,
+ formula3);
+
+ // check sat
+ Result result = smt.checkSat(q);
+ std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;
+
+ if(result == Result::SAT) {
+ std::cout << " x = " << smt.getValue(x) << std::endl;
+ std::cout << " s1.s2 = " << smt.getValue(s) << std::endl;
+ }
+}
|