Theory of Strings ¶
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
20 using namespace cvc5;
21
22 int 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 }
examples/api/java/Strings.java
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Tianyi Liang, Andres Noetzli
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 import static io.github.cvc5.Kind.*;
17
18 import io.github.cvc5.*;
19
20 public class Strings
21 {
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 try (Solver slv = new Solver())
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 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(REGEXP_UNION,
62 slv.mkTerm(REGEXP_CONCAT,
63 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")),
64 slv.mkTerm(
65 REGEXP_STAR, slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))),
66 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))),
67 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")),
68 slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
69
70 // String variables
71 Term s1 = slv.mkConst(string, "s1");
72 Term s2 = slv.mkConst(string, "s2");
73 // String concatenation: s1.s2
74 Term s = slv.mkTerm(STRING_CONCAT, s1, s2);
75
76 // s1.s2 in (ab[c-e]*f)|g|h
77 Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r);
78
79 // Make a query
80 Term q = slv.mkTerm(AND, formula1, formula2, formula3);
81
82 // check sat
83 Result result = slv.checkSatAssuming(q);
84 System.out.println("cvc5 reports: " + q + " is " + result + ".");
85
86 if (result.isSat())
87 {
88 System.out.println(" x = " + slv.getValue(x));
89 System.out.println(" s1.s2 = " + slv.getValue(s));
90 }
91 }
92 }
93 }
examples/api/python/strings.py
1 #!/usr/bin/env python
2 ###############################################################################
3 # Top contributors (to current version):
4 # Makai Mann, Aina Niemetz, Alex Ozdemir
5 #
6 # This file is part of the cvc5 project.
7 #
8 # Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
9 # in the top-level source directory and their institutional affiliations.
10 # All rights reserved. See the file COPYING in the top-level source
11 # directory for licensing information.
12 # #############################################################################
13 #
14 # A simple demonstration of the solving capabilities of the cvc5 strings solver
15 # through the Python API. This is a direct translation of strings-new.cpp.
16 ##
17
18 import cvc5
19 from cvc5 import Kind
20
21 if __name__ == "__main__":
22 slv = cvc5.Solver()
23 # Set the logic
24 slv.setLogic("QF_SLIA")
25 # Produce models
26 slv.setOption("produce-models", "true")
27 # The option strings-exp is needed
28 slv.setOption("strings-exp", "true")
29 # Set output language to SMTLIB2
30 slv.setOption("output-language", "smt2")
31
32 # String type
33 string = slv.getStringSort()
34
35 # std::string
36 str_ab = "ab"
37 # String constants
38 ab = slv.mkString(str_ab)
39 abc = slv.mkString("abc")
40 # String variables
41 x = slv.mkConst(string, "x")
42 y = slv.mkConst(string, "y")
43 z = slv.mkConst(string, "z")
44
45 # String concatenation: x.ab.y
46 lhs = slv.mkTerm(Kind.STRING_CONCAT, x, ab, y)
47 # String concatenation: abc.z
48 rhs = slv.mkTerm(Kind.STRING_CONCAT, abc, z)
49 # x.ab.y = abc.z
50 formula1 = slv.mkTerm(Kind.EQUAL, lhs, rhs)
51
52 # Length of y: |y|
53 leny = slv.mkTerm(Kind.STRING_LENGTH, y)
54 # |y| >= 0
55 formula2 = slv.mkTerm(Kind.GEQ, leny, slv.mkInteger(0))
56
57 # Regular expression: (ab[c-e]*f)|g|h
58 r = slv.mkTerm(Kind.REGEXP_UNION,
59 slv.mkTerm(Kind.REGEXP_CONCAT,
60 slv.mkTerm(Kind.STRING_TO_REGEXP,
61 slv.mkString("ab")),
62 slv.mkTerm(Kind.REGEXP_STAR,
63 slv.mkTerm(Kind.REGEXP_RANGE,
64 slv.mkString("c"),
65 slv.mkString("e"))),
66 slv.mkTerm(Kind.STRING_TO_REGEXP,
67 slv.mkString("f"))),
68 slv.mkTerm(Kind.STRING_TO_REGEXP, slv.mkString("g")),
69 slv.mkTerm(Kind.STRING_TO_REGEXP, slv.mkString("h")))
70
71 # String variables
72 s1 = slv.mkConst(string, "s1")
73 s2 = slv.mkConst(string, "s2")
74 # String concatenation: s1.s2
75 s = slv.mkTerm(Kind.STRING_CONCAT, s1, s2)
76
77 # s1.s2 in (ab[c-e]*f)|g|h
78 formula3 = slv.mkTerm(Kind.STRING_IN_REGEXP, s, r)
79
80 # Make a query
81 q = slv.mkTerm(Kind.AND,
82 formula1,
83 formula2,
84 formula3)
85
86 # check sat
87 result = slv.checkSatAssuming(q)
88 print("cvc5 reports:", q, "is", result)
89
90 if result:
91 print("x = ", slv.getValue(x))
92 print(" s1.s2 =", slv.getValue(s))
examples/api/smtlib/strings.smt2
1 (set-logic QF_SLIA)
2 (set-option :produce-models true)
3
4 (define-const ab String "ab")
5 (define-const abc String "abc")
6
7 (declare-const x String)
8 (declare-const y String)
9 (declare-const z String)
10
11 ; x.ab.y = abc.z
12 (assert (= (str.++ x ab y) (str.++ abc z)))
13 ; |y| >= 0
14 (assert (>= (str.len y) 0))
15
16 ; Regular expression: (ab[c-e]*f)|g|h
17 (define-const r RegLan
18 (re.union
19 (re.++ (str.to_re "ab") (re.* (re.range "c" "e")) (str.to_re "f"))
20 (str.to_re "f")
21 (str.to_re "h")
22 )
23 )
24
25 ; s1.s2 in (ab[c-e]*f)|g|h
26 (assert (str.in_re (str.++ "s1" "s2") r))
27
28 (check-sat)