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 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  // Sequence sort
35  Sort intSeq = tm.mkSequenceSort(tm.getIntegerSort());
36
37  // Sequence variables
38  Term x = tm.mkConst(intSeq, "x");
39  Term y = tm.mkConst(intSeq, "y");
40
41  // Empty sequence
42  Term empty = tm.mkEmptySequence(tm.getIntegerSort());
43  // Sequence concatenation: x.y.empty
44  Term concat = tm.mkTerm(Kind::SEQ_CONCAT, {x, y, empty});
45  // Sequence length: |x.y.empty|
46  Term concat_len = tm.mkTerm(Kind::SEQ_LENGTH, {concat});
47  // |x.y.empty| > 1
48  Term formula1 = tm.mkTerm(Kind::GT, {concat_len, tm.mkInteger(1)});
49  // Sequence unit: seq(1)
50  Term unit = tm.mkTerm(Kind::SEQ_UNIT, {tm.mkInteger(1)});
51  // x = seq(1)
52  Term formula2 = tm.mkTerm(Kind::EQUAL, {x, unit});
53
54  // Make a query
55  Term q = tm.mkTerm(Kind::AND, {formula1, formula2});
56
57  // check sat
58  Result result = slv.checkSatAssuming(q);
59  std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl;
60
61  if (result.isSat())
62  {
63    std::cout << "  x = " << slv.getValue(x) << std::endl;
64    std::cout << "  y = " << slv.getValue(y) << std::endl;
65  }
66}