mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
52 lines
1.7 KiB
C++
52 lines
1.7 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Aina Niemetz, Mathias Preiner, Andrew Reynolds
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2025 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.
|
|
* ****************************************************************************
|
|
*
|
|
* Test for project issue #382.
|
|
*/
|
|
#include <cvc5/cvc5.h>
|
|
|
|
using namespace cvc5;
|
|
|
|
int main(void)
|
|
{
|
|
TermManager tm;
|
|
Solver solver(tm);
|
|
|
|
Sort s1 = tm.getBooleanSort();
|
|
Sort psort = tm.mkParamSort("_x1");
|
|
DatatypeConstructorDecl ctor = tm.mkDatatypeConstructorDecl("_x20");
|
|
ctor.addSelector("_x19", psort);
|
|
DatatypeDecl dtdecl = tm.mkDatatypeDecl("_x0", {psort});
|
|
dtdecl.addConstructor(ctor);
|
|
Sort s2 = tm.mkDatatypeSort(dtdecl);
|
|
Sort s6 = s2.instantiate({s1});
|
|
Term t13 = tm.mkVar(s6, "_x58");
|
|
Term t18 = tm.mkConst(s6, "_x63");
|
|
Term t52 = tm.mkVar(s6, "_x70");
|
|
Term t53 = tm.mkTerm(Kind::MATCH_BIND_CASE,
|
|
{tm.mkTerm(Kind::VARIABLE_LIST, {t52}), t52, t18});
|
|
Term t73 = tm.mkVar(s1, "_x78");
|
|
Term t81 = tm.mkTerm(
|
|
Kind::MATCH_BIND_CASE,
|
|
{tm.mkTerm(Kind::VARIABLE_LIST, {t73}),
|
|
tm.mkTerm(
|
|
Kind::APPLY_CONSTRUCTOR,
|
|
{s6.getDatatype().getConstructor("_x20").getInstantiatedTerm(s6),
|
|
t73}),
|
|
t18});
|
|
Term t82 = tm.mkTerm(Kind::MATCH, {t13, t53, t53, t53, t81});
|
|
Term t325 = tm.mkTerm(
|
|
Kind::APPLY_SELECTOR,
|
|
{t82.getSort().getDatatype().getSelector("_x19").getTerm(), t82});
|
|
solver.simplify(t325);
|
|
}
|