Theory of Strings

examples/api/cpp/strings.cpp

 1/******************************************************************************
 2 * Top contributors (to current version):
 3 *   Tianyi Liang, Aina Niemetz, Mathias Preiner
 4 *
 5 * This file is part of the cvc5 project.
 6 *
 7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
 8 * in the top-level source directory and their institutional affiliations.
 9 * All rights reserved.  See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about strings with cvc5 via C++ API.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20using namespace cvc5;
21
22int main()
23{
24  Solver slv;
25
26  // Set the logic
27  slv.setLogic("QF_SLIA");
28  // Produce models
29  slv.setOption("produce-models", "true");
30  // The option strings-exp is needed
31  slv.setOption("strings-exp", "true");
32  // Set output language to SMTLIB2
33  slv.setOption("output-language", "smt2");
34
35  // String type
36  Sort string = slv.getStringSort();
37
38  // std::string
39  std::string str_ab("ab");
40  // String constants
41  Term ab  = slv.mkString(str_ab);
42  Term abc = slv.mkString("abc");
43  // String variables
44  Term x = slv.mkConst(string, "x");
45  Term y = slv.mkConst(string, "y");
46  Term z = slv.mkConst(string, "z");
47
48  // String concatenation: x.ab.y
49  Term lhs = slv.mkTerm(STRING_CONCAT, {x, ab, y});
50  // String concatenation: abc.z
51  Term rhs = slv.mkTerm(STRING_CONCAT, {abc, z});
52  // x.ab.y = abc.z
53  Term formula1 = slv.mkTerm(EQUAL, {lhs, rhs});
54
55  // Length of y: |y|
56  Term leny = slv.mkTerm(STRING_LENGTH, {y});
57  // |y| >= 0
58  Term formula2 = slv.mkTerm(GEQ, {leny, slv.mkInteger(0)});
59
60  // Regular expression: (ab[c-e]*f)|g|h
61  Term r = slv.mkTerm(
62      REGEXP_UNION,
63
64      {slv.mkTerm(
65           REGEXP_CONCAT,
66           {slv.mkTerm(STRING_TO_REGEXP, {slv.mkString("ab")}),
67            slv.mkTerm(REGEXP_STAR,
68                       {slv.mkTerm(REGEXP_RANGE,
69                                   {slv.mkString("c"), slv.mkString("e")})}),
70            slv.mkTerm(STRING_TO_REGEXP, {slv.mkString("f")})}),
71       slv.mkTerm(STRING_TO_REGEXP, {slv.mkString("g")}),
72       slv.mkTerm(STRING_TO_REGEXP, {slv.mkString("h")})});
73
74  // String variables
75  Term s1 = slv.mkConst(string, "s1");
76  Term s2 = slv.mkConst(string, "s2");
77  // String concatenation: s1.s2
78  Term s = slv.mkTerm(STRING_CONCAT, {s1, s2});
79
80  // s1.s2 in (ab[c-e]*f)|g|h
81  Term formula3 = slv.mkTerm(STRING_IN_REGEXP, {s, r});
82
83  // Make a query
84  Term q = slv.mkTerm(AND, {formula1, formula2, formula3});
85
86  // check sat
87  Result result = slv.checkSatAssuming(q);
88  std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
89
90  if(result.isSat())
91  {
92    std::cout << "  x  = " << slv.getValue(x) << std::endl;
93    std::cout << "  s1.s2 = " << slv.getValue(s) << std::endl;
94  }
95}