mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
58d7c6d556
This introduces a TermManager object, which will, in the future, be the sole object responsible for handling/managing terms and sorts. For now, all corresponding functions in `cvc5::Solver` are marked as deprecated, as is constructor `cvc5::Solver::Solver()`, since in the future a solver instance must be constructed from a term manager instance. Currently, we maintain a static thread_local term manager instance to not break the API and continue providing constructor `cvc5::Solver::Solver()`. Note that this already converts all C++ unit tests to use the TermManager except for a single test `getStatistics()` in `test/unit/api/cpp/solver_black.cpp`. Statistics handling is currently still maintained on the solver level. The statistics we maintain, however, concern terms only and will eventually be refactored to be tracked in the NodeManager. Further note that the Java and Python APIs will be refactored in separate PRs.
69 lines
2.0 KiB
C++
69 lines
2.0 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Andres Noetzli, Mathias Preiner, Aina Niemetz
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2022 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 cvc5 via C++ API.
|
|
*/
|
|
|
|
#include <cvc5/cvc5.h>
|
|
|
|
#include <iostream>
|
|
|
|
using namespace cvc5;
|
|
|
|
int main()
|
|
{
|
|
TermManager tm;
|
|
Solver slv(tm);
|
|
|
|
// 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 = tm.mkSequenceSort(tm.getIntegerSort());
|
|
|
|
// Sequence variables
|
|
Term x = tm.mkConst(intSeq, "x");
|
|
Term y = tm.mkConst(intSeq, "y");
|
|
|
|
// Empty sequence
|
|
Term empty = tm.mkEmptySequence(tm.getIntegerSort());
|
|
// Sequence concatenation: x.y.empty
|
|
Term concat = tm.mkTerm(Kind::SEQ_CONCAT, {x, y, empty});
|
|
// Sequence length: |x.y.empty|
|
|
Term concat_len = tm.mkTerm(Kind::SEQ_LENGTH, {concat});
|
|
// |x.y.empty| > 1
|
|
Term formula1 = tm.mkTerm(Kind::GT, {concat_len, tm.mkInteger(1)});
|
|
// Sequence unit: seq(1)
|
|
Term unit = tm.mkTerm(Kind::SEQ_UNIT, {tm.mkInteger(1)});
|
|
// x = seq(1)
|
|
Term formula2 = tm.mkTerm(Kind::EQUAL, {x, unit});
|
|
|
|
// Make a query
|
|
Term q = tm.mkTerm(Kind::AND, {formula1, formula2});
|
|
|
|
// check sat
|
|
Result result = slv.checkSatAssuming(q);
|
|
std::cout << "cvc5 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;
|
|
}
|
|
}
|