mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
7440f0568b
This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details: - for consistency, all cpp examples are moved from examples/api to examples/api/cpp - add capabilities for SMT-LIB examples, and two simple smt2 examples - more docs/examples/*.rst files - two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)
68 lines
2.0 KiB
C++
68 lines
2.0 KiB
C++
/******************************************************************************
|
|
* 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;
|
|
}
|
|
}
|