1 /********************* */
2 /*! \file strings-new.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Makai Mann
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Reasoning about strings with CVC4 via C++ API.
13 **
14 ** A simple demonstration of reasoning about strings with CVC4 via C++ API.
15 **/
16
17 #include <iostream>
18
19 // #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
20 #include "api/cvc4cpp.h"
21
22 using namespace CVC4::api;
23
main()24 int main()
25 {
26 Solver slv;
27
28 // Set the logic
29 slv.setLogic("S");
30 // Produce models
31 slv.setOption("produce-models", "true");
32 // The option strings-exp is needed
33 slv.setOption("strings-exp", "true");
34 // Set output language to SMTLIB2
35 slv.setOption("output-language", "smt2");
36
37 // String type
38 Sort string = slv.getStringSort();
39
40 // std::string
41 std::string str_ab("ab");
42 // String constants
43 Term ab = slv.mkString(str_ab);
44 Term abc = slv.mkString("abc");
45 // String variables
46 Term x = slv.mkVar(string, "x");
47 Term y = slv.mkVar(string, "y");
48 Term z = slv.mkVar(string, "z");
49
50 // String concatenation: x.ab.y
51 Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y);
52 // String concatenation: abc.z
53 Term rhs = slv.mkTerm(STRING_CONCAT, abc, z);
54 // x.ab.y = abc.z
55 Term formula1 = slv.mkTerm(EQUAL, lhs, rhs);
56
57 // Length of y: |y|
58 Term leny = slv.mkTerm(STRING_LENGTH, y);
59 // |y| >= 0
60 Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0));
61
62 // Regular expression: (ab[c-e]*f)|g|h
63 Term r = slv.mkTerm(REGEXP_UNION,
64 slv.mkTerm(REGEXP_CONCAT,
65 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")),
66 slv.mkTerm(REGEXP_STAR,
67 slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))),
68 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))),
69 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")),
70 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
71
72 // String variables
73 Term s1 = slv.mkVar(string, "s1");
74 Term s2 = slv.mkVar(string, "s2");
75 // String concatenation: s1.s2
76 Term s = slv.mkTerm(STRING_CONCAT, s1, s2);
77
78 // s1.s2 in (ab[c-e]*f)|g|h
79 Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r);
80
81 // Make a query
82 Term q = slv.mkTerm(AND,
83 formula1,
84 formula2,
85 formula3);
86
87 // check sat
88 Result result = slv.checkSatAssuming(q);
89 std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;
90
91 if(result.isSat())
92 {
93 std::cout << " x = " << slv.getValue(x) << std::endl;
94 std::cout << " s1.s2 = " << slv.getValue(s) << std::endl;
95 }
96 }
97