Theory of Sequences
examples/api/cpp/sequences.cpp
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Andres Noetzli, Tianyi Liang
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 sequences 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 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 // Set output language to SMTLIB2
34 slv.setOption("output-language", "smt2");
35
36 // Sequence sort
37 Sort intSeq = tm.mkSequenceSort(tm.getIntegerSort());
38
39 // Sequence variables
40 Term x = tm.mkConst(intSeq, "x");
41 Term y = tm.mkConst(intSeq, "y");
42
43 // Empty sequence
44 Term empty = tm.mkEmptySequence(tm.getIntegerSort());
45 // Sequence concatenation: x.y.empty
46 Term concat = tm.mkTerm(Kind::SEQ_CONCAT, {x, y, empty});
47 // Sequence length: |x.y.empty|
48 Term concat_len = tm.mkTerm(Kind::SEQ_LENGTH, {concat});
49 // |x.y.empty| > 1
50 Term formula1 = tm.mkTerm(Kind::GT, {concat_len, tm.mkInteger(1)});
51 // Sequence unit: seq(1)
52 Term unit = tm.mkTerm(Kind::SEQ_UNIT, {tm.mkInteger(1)});
53 // x = seq(1)
54 Term formula2 = tm.mkTerm(Kind::EQUAL, {x, unit});
55
56 // Make a query
57 Term q = tm.mkTerm(Kind::AND, {formula1, formula2});
58
59 // check sat
60 Result result = slv.checkSatAssuming(q);
61 std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
62
63 if (result.isSat())
64 {
65 std::cout << " x = " << slv.getValue(x) << std::endl;
66 std::cout << " y = " << slv.getValue(y) << std::endl;
67 }
68}
examples/api/java/Sequences.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, 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 sequences with cvc5 via C++ API.
14 */
15
16import static io.github.cvc5.Kind.*;
17
18import io.github.cvc5.*;
19
20public class Sequences
21{
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 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 // Sequence sort
36 Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort());
37
38 // Sequence variables
39 Term x = slv.mkConst(intSeq, "x");
40 Term y = slv.mkConst(intSeq, "y");
41
42 // Empty sequence
43 Term empty = slv.mkEmptySequence(slv.getIntegerSort());
44 // Sequence concatenation: x.y.empty
45 Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty);
46 // Sequence length: |x.y.empty|
47 Term concat_len = slv.mkTerm(SEQ_LENGTH, concat);
48 // |x.y.empty| > 1
49 Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1));
50 // Sequence unit: seq(1)
51 Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1));
52 // x = seq(1)
53 Term formula2 = slv.mkTerm(EQUAL, x, unit);
54
55 // Make a query
56 Term q = slv.mkTerm(AND, formula1, formula2);
57
58 // check sat
59 Result result = slv.checkSatAssuming(q);
60 System.out.println("cvc5 reports: " + q + " is " + result + ".");
61
62 if (result.isSat())
63 {
64 System.out.println(" x = " + slv.getValue(x));
65 System.out.println(" y = " + slv.getValue(y));
66 }
67 }
68 Context.deletePointers();
69 }
70}
examples/api/python/pythonic/sequences.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 x = Const("x", SeqSort(IntSort()))
22 y = Const("y", SeqSort(IntSort()))
23
24 # Empty sequence
25 empty = Empty(SeqSort(IntSort()))
26 # Sequence concatenation: x.y.empty
27 concat = Concat( x, y, empty)
28 # Sequence length: |x.y.empty|
29 concat_len = Length(concat)
30 # |x.y.empty| > 1
31 formula1 = (concat_len > 1)
32 # Sequence unit: seq(1)
33 unit = Unit(IntVal(1))
34 # x = seq(1)
35 formula2 = (x == unit)
36
37 # Make a query
38 q = And(formula1, formula2)
39
40 # Check satisfiability
41 s = Solver()
42 result = s.check([q])
43 assert result == sat
44 m = s.model()
45 print("x = {}".format(m[x]))
46 print("y = {}".format(m[y]))
examples/api/python/sequences.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Andres Noetzli, Makai Mann, Aina Niemetz
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 sequences.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 # Sequence sort
34 int_seq = tm.mkSequenceSort(tm.getIntegerSort())
35
36 # Sequence variables
37 x = tm.mkConst(int_seq, "x")
38 y = tm.mkConst(int_seq, "y")
39
40 # Empty sequence
41 empty = tm.mkEmptySequence(tm.getIntegerSort())
42 # Sequence concatenation: x.y.empty
43 concat = tm.mkTerm(Kind.SEQ_CONCAT, x, y, empty)
44 # Sequence length: |x.y.empty|
45 concat_len = tm.mkTerm(Kind.SEQ_LENGTH, concat)
46 # |x.y.empty| > 1
47 formula1 = tm.mkTerm(Kind.GT, concat_len, tm.mkInteger(1))
48 # Sequence unit: seq(1)
49 unit = tm.mkTerm(Kind.SEQ_UNIT, tm.mkInteger(1))
50 # x = seq(1)
51 formula2 = tm.mkTerm(Kind.EQUAL, x, unit)
52
53 # Make a query
54 q = tm.mkTerm(Kind.AND, formula1, formula2)
55
56 # Check satisfiability
57 result = slv.checkSatAssuming(q)
58 print("cvc5 reports:", q, "is", result)
59
60 if result:
61 print("x = {}".format(slv.getValue(x)))
62 print("y = {}".format(slv.getValue(y)))
examples/api/smtlib/sequences.smt2
1(set-logic QF_SLIA)
2(set-option :produce-models true)
3
4; create integer sequence constants
5(declare-const x (Seq Int))
6(declare-const y (Seq Int))
7
8; |x.y.empty| > 1
9(assert (> (seq.len (seq.++ x y (as seq.empty (Seq Int)))) 1))
10; x = seq(1)
11(assert (= x (seq.unit 1)))
12
13(check-sat)
14(get-value (x y))