1 /********************* */
2 /*! \file sequences.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Reasoning about sequences with CVC4 via C++ API.
14 ** A simple demonstration of reasoning about sequences with CVC4 via C++ API.
17 #include <cvc4/api/cvc4cpp.h>
21 using namespace CVC4::api
;
28 slv
.setLogic("QF_SLIA");
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");
37 Sort intSeq
= slv
.mkSequenceSort(slv
.getIntegerSort());
40 Term x
= slv
.mkConst(intSeq
, "x");
41 Term y
= slv
.mkConst(intSeq
, "y");
44 Term empty
= slv
.mkEmptySequence(slv
.getIntegerSort());
45 // Sequence concatenation: x.y.empty
46 Term concat
= slv
.mkTerm(SEQ_CONCAT
, x
, y
, empty
);
47 // Sequence length: |x.y.empty|
48 Term concat_len
= slv
.mkTerm(SEQ_LENGTH
, concat
);
50 Term formula1
= slv
.mkTerm(GT
, concat_len
, slv
.mkReal(1));
51 // Sequence unit: seq(1)
52 Term unit
= slv
.mkTerm(SEQ_UNIT
, slv
.mkReal(1));
54 Term formula2
= slv
.mkTerm(EQUAL
, x
, unit
);
57 Term q
= slv
.mkTerm(AND
, formula1
, formula2
);
60 Result result
= slv
.checkSatAssuming(q
);
61 std::cout
<< "CVC4 reports: " << q
<< " is " << result
<< "." << std::endl
;
65 std::cout
<< " x = " << slv
.getValue(x
) << std::endl
;
66 std::cout
<< " y = " << slv
.getValue(y
) << std::endl
;