Theory of Strings
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about strings via the C++ API.
11 */
12
13#include <cvc5/cvc5.h>
14
15#include <iostream>
16
17using namespace cvc5;
18
19int main()
20{
21 TermManager tm;
22 Solver slv(tm);
23
24 // Set the logic
25 slv.setLogic("QF_SLIA");
26 // Produce models
27 slv.setOption("produce-models", "true");
28 // The option strings-exp is needed
29 slv.setOption("strings-exp", "true");
30
31 // String type
32 Sort string = tm.getStringSort();
33
34 // std::string
35 std::string str_ab("ab");
36 // String constants
37 Term ab = tm.mkString(str_ab);
38 Term abc = tm.mkString("abc");
39 // String variables
40 Term x = tm.mkConst(string, "x");
41 Term y = tm.mkConst(string, "y");
42 Term z = tm.mkConst(string, "z");
43
44 // String concatenation: x.ab.y
45 Term lhs = tm.mkTerm(Kind::STRING_CONCAT, {x, ab, y});
46 // String concatenation: abc.z
47 Term rhs = tm.mkTerm(Kind::STRING_CONCAT, {abc, z});
48 // x.ab.y = abc.z
49 Term formula1 = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
50
51 // Length of y: |y|
52 Term leny = tm.mkTerm(Kind::STRING_LENGTH, {y});
53 // |y| >= 0
54 Term formula2 = tm.mkTerm(Kind::GEQ, {leny, tm.mkInteger(0)});
55
56 // Regular expression: (ab[c-e]*f)|g|h
57 Term r = tm.mkTerm(
58 Kind::REGEXP_UNION,
59
60 {tm.mkTerm(Kind::REGEXP_CONCAT,
61 {tm.mkTerm(Kind::STRING_TO_REGEXP, {tm.mkString("ab")}),
62 tm.mkTerm(Kind::REGEXP_STAR,
63 {tm.mkTerm(Kind::REGEXP_RANGE,
64 {tm.mkString("c"), tm.mkString("e")})}),
65 tm.mkTerm(Kind::STRING_TO_REGEXP, {tm.mkString("f")})}),
66 tm.mkTerm(Kind::STRING_TO_REGEXP, {tm.mkString("g")}),
67 tm.mkTerm(Kind::STRING_TO_REGEXP, {tm.mkString("h")})});
68
69 // String variables
70 Term s1 = tm.mkConst(string, "s1");
71 Term s2 = tm.mkConst(string, "s2");
72 // String concatenation: s1.s2
73 Term s = tm.mkTerm(Kind::STRING_CONCAT, {s1, s2});
74
75 // s1.s2 in (ab[c-e]*f)|g|h
76 Term formula3 = tm.mkTerm(Kind::STRING_IN_REGEXP, {s, r});
77
78 // Make a query
79 Term q = tm.mkTerm(Kind::AND, {formula1, formula2, formula3});
80
81 // check sat
82 Result result = slv.checkSatAssuming(q);
83 std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
84
85 if(result.isSat())
86 {
87 std::cout << " x = " << slv.getValue(x) << std::endl;
88 std::cout << " s1.s2 = " << slv.getValue(s) << std::endl;
89 }
90}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about strings via the C API.
11 */
12
13#include <cvc5/c/cvc5.h>
14#include <stdio.h>
15
16int main()
17{
18 Cvc5TermManager* tm = cvc5_term_manager_new();
19 Cvc5* slv = cvc5_new(tm);
20
21 // Set the logic
22 cvc5_set_logic(slv, "QF_SLIA");
23 // Produce models
24 cvc5_set_option(slv, "produce-models", "true");
25 // The option strings-exp is needed
26 cvc5_set_option(slv, "strings-exp", "true");
27
28 // String type
29 Cvc5Sort string_sort = cvc5_get_string_sort(tm);
30
31 // String constants
32 Cvc5Term ab = cvc5_mk_string(tm, "ab", false);
33 Cvc5Term abc = cvc5_mk_string(tm, "abc", false);
34 // String variables
35 Cvc5Term x = cvc5_mk_const(tm, string_sort, "x");
36 Cvc5Term y = cvc5_mk_const(tm, string_sort, "y");
37 Cvc5Term z = cvc5_mk_const(tm, string_sort, "z");
38
39 // String concatenation: x.ab.y
40 Cvc5Term args3[3] = {x, ab, y};
41 Cvc5Term lhs = cvc5_mk_term(tm, CVC5_KIND_STRING_CONCAT, 3, args3);
42 // String concatenation: abc.z
43 Cvc5Term args2[2] = {abc, z};
44 Cvc5Term rhs = cvc5_mk_term(tm, CVC5_KIND_STRING_CONCAT, 2, args2);
45 // x.ab.y = abc.z
46 args2[0] = lhs;
47 args2[1] = rhs;
48 Cvc5Term formula1 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
49
50 // Length of y: |y|
51 Cvc5Term args1[1] = {y};
52 Cvc5Term len_y = cvc5_mk_term(tm, CVC5_KIND_STRING_LENGTH, 1, args1);
53 // |y| >= 0
54 args2[0] = len_y;
55 args2[1] = cvc5_mk_integer_int64(tm, 0);
56 Cvc5Term formula2 = cvc5_mk_term(tm, CVC5_KIND_GEQ, 2, args2);
57
58 // Regular expression: (ab[c-e]*f)|g|h
59 args2[0] = cvc5_mk_string(tm, "c", false);
60 args2[1] = cvc5_mk_string(tm, "e", false);
61 Cvc5Term range = cvc5_mk_term(tm, CVC5_KIND_REGEXP_RANGE, 2, args2);
62 args1[0] = range;
63 Cvc5Term reg_star = cvc5_mk_term(tm, CVC5_KIND_REGEXP_STAR, 1, args1);
64 args1[0] = cvc5_mk_string(tm, "ab", false);
65 args3[0] = cvc5_mk_term(tm, CVC5_KIND_STRING_TO_REGEXP, 1, args1);
66 args3[1] = reg_star;
67 args1[0] = cvc5_mk_string(tm, "f", false);
68 args3[2] = cvc5_mk_term(tm, CVC5_KIND_STRING_TO_REGEXP, 1, args1);
69 Cvc5Term concat = cvc5_mk_term(tm, CVC5_KIND_REGEXP_CONCAT, 3, args3);
70 args3[0] = concat;
71 args1[0] = cvc5_mk_string(tm, "g", false);
72 args3[1] = cvc5_mk_term(tm, CVC5_KIND_STRING_TO_REGEXP, 1, args1);
73 args1[0] = cvc5_mk_string(tm, "h", false);
74 args3[2] = cvc5_mk_term(tm, CVC5_KIND_STRING_TO_REGEXP, 1, args1);
75 Cvc5Term r = cvc5_mk_term(tm, CVC5_KIND_REGEXP_UNION, 3, args3);
76
77 // String variables
78 Cvc5Term s1 = cvc5_mk_const(tm, string_sort, "s1");
79 Cvc5Term s2 = cvc5_mk_const(tm, string_sort, "s2");
80 // String concatenation: s1.s2
81 args2[0] = s1;
82 args2[1] = s2;
83 Cvc5Term s = cvc5_mk_term(tm, CVC5_KIND_STRING_CONCAT, 2, args2);
84
85 // s1.s2 in (ab[c-e]*f)|g|h
86 args2[0] = s;
87 args2[1] = r;
88 Cvc5Term formula3 = cvc5_mk_term(tm, CVC5_KIND_STRING_IN_REGEXP, 2, args2);
89
90 // Make a query
91 args3[0] = formula1;
92 args3[1] = formula2;
93 args3[2] = formula3;
94 Cvc5Term q = cvc5_mk_term(tm, CVC5_KIND_AND, 3, args3);
95
96 // check sat
97 Cvc5Term assumptions[1] = {q};
98 Cvc5Result result = cvc5_check_sat_assuming(slv, 1, assumptions);
99 printf("cvc5 reports: %s is %s.\n",
100 cvc5_term_to_string(q),
101 cvc5_result_to_string(result));
102
103 if (cvc5_result_is_sat(result))
104 {
105 printf(" x = %s\n", cvc5_term_to_string(cvc5_get_value(slv, x)));
106 printf(" s1.s2 = %s\n", cvc5_term_to_string(cvc5_get_value(slv, s)));
107 }
108
109 cvc5_delete(slv);
110 cvc5_term_manager_delete(tm);
111}
examples/api/java/Strings.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about strings with cvc5 via C++ API.
11 */
12
13import static io.github.cvc5.Kind.*;
14
15import io.github.cvc5.*;
16
17public class Strings
18{
19 public static void main(String args[]) throws CVC5ApiException
20 {
21 TermManager tm = new TermManager();
22 Solver slv = new Solver(tm);
23 {
24 // Set the logic
25 slv.setLogic("QF_SLIA");
26 // Produce models
27 slv.setOption("produce-models", "true");
28 // The option strings-exp is needed
29 slv.setOption("strings-exp", "true");
30 // Set output language to SMTLIB2
31 slv.setOption("output-language", "smt2");
32
33 // String type
34 Sort string = tm.getStringSort();
35
36 // std::string
37 String str_ab = "ab";
38 // String constants
39 Term ab = tm.mkString(str_ab);
40 Term abc = tm.mkString("abc");
41 // String variables
42 Term x = tm.mkConst(string, "x");
43 Term y = tm.mkConst(string, "y");
44 Term z = tm.mkConst(string, "z");
45
46 // String concatenation: x.ab.y
47 Term lhs = tm.mkTerm(STRING_CONCAT, x, ab, y);
48 // String concatenation: abc.z
49 Term rhs = tm.mkTerm(STRING_CONCAT, abc, z);
50 // x.ab.y = abc.z
51 Term formula1 = tm.mkTerm(EQUAL, lhs, rhs);
52
53 // Length of y: |y|
54 Term leny = tm.mkTerm(STRING_LENGTH, y);
55 // |y| >= 0
56 Term formula2 = tm.mkTerm(GEQ, leny, tm.mkInteger(0));
57
58 // Regular expression: (ab[c-e]*f)|g|h
59 Term r = tm.mkTerm(REGEXP_UNION,
60 tm.mkTerm(REGEXP_CONCAT,
61 tm.mkTerm(STRING_TO_REGEXP, tm.mkString("ab")),
62 tm.mkTerm(REGEXP_STAR, tm.mkTerm(REGEXP_RANGE, tm.mkString("c"), tm.mkString("e"))),
63 tm.mkTerm(STRING_TO_REGEXP, tm.mkString("f"))),
64 tm.mkTerm(STRING_TO_REGEXP, tm.mkString("g")),
65 tm.mkTerm(STRING_TO_REGEXP, tm.mkString("h")));
66
67 // String variables
68 Term s1 = tm.mkConst(string, "s1");
69 Term s2 = tm.mkConst(string, "s2");
70 // String concatenation: s1.s2
71 Term s = tm.mkTerm(STRING_CONCAT, s1, s2);
72
73 // s1.s2 in (ab[c-e]*f)|g|h
74 Term formula3 = tm.mkTerm(STRING_IN_REGEXP, s, r);
75
76 // Make a query
77 Term q = tm.mkTerm(AND, formula1, formula2, formula3);
78
79 // check sat
80 Result result = slv.checkSatAssuming(q);
81 System.out.println("cvc5 reports: " + q + " is " + result + ".");
82
83 if (result.isSat())
84 {
85 System.out.println(" x = " + slv.getValue(x));
86 System.out.println(" s1.s2 = " + slv.getValue(s));
87 }
88 }
89 Context.deletePointers();
90 }
91}
examples/api/python/pythonic/strings.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the solving capabilities of the cvc5 strings
12# solver. A simple translation of the base python API.
13# example.
14##
15
16from cvc5.pythonic import *
17
18if __name__ == "__main__":
19
20 str_ab = "ab"
21 # String constants
22 ab = StringVal(str_ab)
23 abc = StringVal("abc")
24 # String variables
25 x = String("x")
26 y = String("y")
27 z = String("z")
28
29 # String concatenation: x.ab.y
30 lhs = Concat(x, ab, y)
31 # String concatenation: abc.z
32 rhs = Concat(abc, z)
33 # x.ab.y = abc.z
34 formula1 = (lhs == rhs)
35
36 # Length of y: |y|
37 leny = Length(y)
38 # |y| >= 0
39 formula2 = leny >= 0
40
41 # Regular expression: (ab[c-e]*f)|g|h
42 r = Union(Concat(Re("ab"), Star(Range("c", "e")), Re("f")), Re("g"), Re("h"))
43
44
45 # String variables
46 s1 = String("s1")
47 s2 = String("s2")
48 # String concatenation: s1.s2
49 s = Concat(s1, s2)
50
51 # s1.s2 in (ab[c-e]*f)|g|h
52 formula3 = InRe(s,r)
53
54 # Make a query
55 q = And(formula1, formula2, formula3)
56
57 # check sat
58 s = Solver()
59 s.add(q)
60 assert sat == s.check()
61 m = s.model()
62 print("x = ", m[x])
63 print(" s1.s2 =", m[Concat(s1, s2)])
examples/api/python/strings.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the solving capabilities of the cvc5 strings solver
12# through the Python API. This is a direct translation of strings-new.cpp.
13##
14
15import cvc5
16from cvc5 import Kind
17
18if __name__ == "__main__":
19 tm = cvc5.TermManager()
20 slv = cvc5.Solver(tm)
21 # Set the logic
22 slv.setLogic("QF_SLIA")
23 # Produce models
24 slv.setOption("produce-models", "true")
25 # The option strings-exp is needed
26 slv.setOption("strings-exp", "true")
27 # Set output language to SMTLIB2
28 slv.setOption("output-language", "smt2")
29
30 # String type
31 string = tm.getStringSort()
32
33 # std::string
34 str_ab = "ab"
35 # String constants
36 ab = tm.mkString(str_ab)
37 abc = tm.mkString("abc")
38 # String variables
39 x = tm.mkConst(string, "x")
40 y = tm.mkConst(string, "y")
41 z = tm.mkConst(string, "z")
42
43 # String concatenation: x.ab.y
44 lhs = tm.mkTerm(Kind.STRING_CONCAT, x, ab, y)
45 # String concatenation: abc.z
46 rhs = tm.mkTerm(Kind.STRING_CONCAT, abc, z)
47 # x.ab.y = abc.z
48 formula1 = tm.mkTerm(Kind.EQUAL, lhs, rhs)
49
50 # Length of y: |y|
51 leny = tm.mkTerm(Kind.STRING_LENGTH, y)
52 # |y| >= 0
53 formula2 = tm.mkTerm(Kind.GEQ, leny, tm.mkInteger(0))
54
55 # Regular expression: (ab[c-e]*f)|g|h
56 r = tm.mkTerm(Kind.REGEXP_UNION,
57 tm.mkTerm(Kind.REGEXP_CONCAT,
58 tm.mkTerm(Kind.STRING_TO_REGEXP,
59 tm.mkString("ab")),
60 tm.mkTerm(Kind.REGEXP_STAR,
61 tm.mkTerm(Kind.REGEXP_RANGE,
62 tm.mkString("c"),
63 tm.mkString("e"))),
64 tm.mkTerm(Kind.STRING_TO_REGEXP,
65 tm.mkString("f"))),
66 tm.mkTerm(Kind.STRING_TO_REGEXP, tm.mkString("g")),
67 tm.mkTerm(Kind.STRING_TO_REGEXP, tm.mkString("h")))
68
69 # String variables
70 s1 = tm.mkConst(string, "s1")
71 s2 = tm.mkConst(string, "s2")
72 # String concatenation: s1.s2
73 s = tm.mkTerm(Kind.STRING_CONCAT, s1, s2)
74
75 # s1.s2 in (ab[c-e]*f)|g|h
76 formula3 = tm.mkTerm(Kind.STRING_IN_REGEXP, s, r)
77
78 # Make a query
79 q = tm.mkTerm(Kind.AND, formula1, formula2, formula3)
80
81 # check sat
82 result = slv.checkSatAssuming(q)
83 print("cvc5 reports:", q, "is", result)
84
85 if result:
86 print("x = ", slv.getValue(x))
87 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)