1 files changed, 101 insertions, 0 deletions
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;
+  }
+}