diff options
Diffstat (limited to 'examples/api/cpp/sequences.cpp')
-rw-r--r-- | examples/api/cpp/sequences.cpp | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/examples/api/cpp/sequences.cpp b/examples/api/cpp/sequences.cpp new file mode 100644 index 000000000..5ee66048f --- /dev/null +++ b/examples/api/cpp/sequences.cpp @@ -0,0 +1,67 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Aina Niemetz, Tianyi Liang + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of reasoning about sequences with CVC4 via C++ API. + */ + +#include <cvc5/cvc5.h> + +#include <iostream> + +using namespace cvc5::api; + +int main() +{ + Solver slv; + + // Set the logic + slv.setLogic("QF_SLIA"); + // Produce models + slv.setOption("produce-models", "true"); + // The option strings-exp is needed + slv.setOption("strings-exp", "true"); + // Set output language to SMTLIB2 + slv.setOption("output-language", "smt2"); + + // Sequence sort + Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort()); + + // Sequence variables + Term x = slv.mkConst(intSeq, "x"); + Term y = slv.mkConst(intSeq, "y"); + + // Empty sequence + Term empty = slv.mkEmptySequence(slv.getIntegerSort()); + // Sequence concatenation: x.y.empty + Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty); + // Sequence length: |x.y.empty| + Term concat_len = slv.mkTerm(SEQ_LENGTH, concat); + // |x.y.empty| > 1 + Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1)); + // Sequence unit: seq(1) + Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1)); + // x = seq(1) + Term formula2 = slv.mkTerm(EQUAL, x, unit); + + // Make a query + Term q = slv.mkTerm(AND, formula1, formula2); + + // check sat + Result result = slv.checkSatAssuming(q); + std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + + if (result.isSat()) + { + std::cout << " x = " << slv.getValue(x) << std::endl; + std::cout << " y = " << slv.getValue(y) << std::endl; + } +} |