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