ada/cvc5
0
0
Fork 0
mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
c86771fcffcbcb6e7aa032058c8dbcb29a714bc2
cvc5/test/unit/api/cpp/api_term_manager_black.cpp
Aina Niemetz fb407f4c06 c api: Add support/tests for some uncovered functions. (#10988) 
This is work towards full API coverage so that the C API tests can be
plugged into the nightlies coverage tests.
2024-07-09 23:27:42 +00:00

1241 lines
48 KiB
C++
Raw Blame History

/******************************************************************************
* Top contributors (to current version):
* Aina Niemetz, Mudathir Mohamed
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2024 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.
* ****************************************************************************
*
* Black box testing of the TermManager class of the C++ API.
*/
#include <gtest/gtest.h>
#include <cmath>
#include "test_api.h"
namespace cvc5::internal::test {
class TestApiBlackTermManager : public TestApi
{
};
TEST_F(TestApiBlackTermManager, getBooleanSort)
{
ASSERT_NO_THROW(d_tm.getBooleanSort());
}
TEST_F(TestApiBlackTermManager, getIntegerSort)
{
ASSERT_NO_THROW(d_tm.getIntegerSort());
}
TEST_F(TestApiBlackTermManager, getRealSort)
{
ASSERT_NO_THROW(d_tm.getRealSort());
}
TEST_F(TestApiBlackTermManager, getRegExpSort)
{
ASSERT_NO_THROW(d_tm.getRegExpSort());
}
TEST_F(TestApiBlackTermManager, getStringSort)
{
ASSERT_NO_THROW(d_tm.getStringSort());
}
TEST_F(TestApiBlackTermManager, getRoundingModeSort)
{
ASSERT_NO_THROW(d_tm.getRoundingModeSort());
}
TEST_F(TestApiBlackTermManager, mkArraySort)
{
Sort boolSort = d_tm.getBooleanSort();
Sort intSort = d_tm.getIntegerSort();
Sort realSort = d_tm.getRealSort();
Sort bvSort = d_tm.mkBitVectorSort(32);
ASSERT_NO_THROW(d_tm.mkArraySort(boolSort, boolSort));
ASSERT_NO_THROW(d_tm.mkArraySort(intSort, intSort));
ASSERT_NO_THROW(d_tm.mkArraySort(realSort, realSort));
ASSERT_NO_THROW(d_tm.mkArraySort(bvSort, bvSort));
ASSERT_NO_THROW(d_tm.mkArraySort(boolSort, intSort));
ASSERT_NO_THROW(d_tm.mkArraySort(realSort, bvSort));
Sort fpSort = d_tm.mkFloatingPointSort(3, 5);
ASSERT_NO_THROW(d_tm.mkArraySort(fpSort, fpSort));
ASSERT_NO_THROW(d_tm.mkArraySort(bvSort, fpSort));
ASSERT_NO_THROW(d_tm.mkArraySort(boolSort, boolSort));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(d_tm.mkArraySort(tm.getBooleanSort(), tm.getIntegerSort()));
}
TEST_F(TestApiBlackTermManager, mkBitVectorSort)
{
ASSERT_NO_THROW(d_tm.mkBitVectorSort(32));
ASSERT_THROW(d_tm.mkBitVectorSort(0), CVC5ApiException);
}
TEST_F(TestApiBlackTermManager, mkFiniteFieldSort)
{
ASSERT_NO_THROW(d_tm.mkFiniteFieldSort("31"));
ASSERT_THROW(d_tm.mkFiniteFieldSort("6"), CVC5ApiException);
ASSERT_THROW(d_tm.mkFiniteFieldSort("b"), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkFiniteFieldSort("1100101", 2));
ASSERT_NO_THROW(d_tm.mkFiniteFieldSort("10202", 3));
ASSERT_NO_THROW(d_tm.mkFiniteFieldSort("401", 5));
ASSERT_NO_THROW(d_tm.mkFiniteFieldSort("791a", 11));
ASSERT_NO_THROW(d_tm.mkFiniteFieldSort("970f", 16));
ASSERT_NO_THROW(d_tm.mkFiniteFieldSort("8CC5", 16));
ASSERT_THROW(d_tm.mkFiniteFieldSort("1100100", 2), CVC5ApiException);
ASSERT_THROW(d_tm.mkFiniteFieldSort("10201", 3), CVC5ApiException);
ASSERT_THROW(d_tm.mkFiniteFieldSort("400", 5), CVC5ApiException);
ASSERT_THROW(d_tm.mkFiniteFieldSort("7919", 11), CVC5ApiException);
ASSERT_THROW(d_tm.mkFiniteFieldSort("970e", 16), CVC5ApiException);
ASSERT_THROW(d_tm.mkFiniteFieldSort("8CC4", 16), CVC5ApiException);
}
TEST_F(TestApiBlackTermManager, mkFloatingPointSort)
{
ASSERT_NO_THROW(d_tm.mkFloatingPointSort(4, 8));
ASSERT_THROW(d_tm.mkFloatingPointSort(0, 8), CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPointSort(4, 0), CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPointSort(1, 8), CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPointSort(4, 1), CVC5ApiException);
}
TEST_F(TestApiBlackTermManager, mkDatatypeSort)
{
{
DatatypeDecl dtypeSpec = d_tm.mkDatatypeDecl("list");
DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_tm.getIntegerSort());
dtypeSpec.addConstructor(cons);
DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
ASSERT_NO_THROW(d_tm.mkDatatypeSort(dtypeSpec));
ASSERT_THROW(d_tm.mkDatatypeSort(dtypeSpec), CVC5ApiException);
ASSERT_THROW(d_tm.mkDatatypeSort(dtypeSpec), CVC5ApiException);
}
DatatypeDecl throwsDtypeSpec = d_tm.mkDatatypeDecl("list");
ASSERT_THROW(d_tm.mkDatatypeSort(throwsDtypeSpec), CVC5ApiException);
{
TermManager tm;
DatatypeDecl dtypeSpec = tm.mkDatatypeDecl("list");
DatatypeConstructorDecl cons = tm.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", tm.getIntegerSort());
dtypeSpec.addConstructor(cons);
DatatypeConstructorDecl nil = tm.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(d_tm.mkDatatypeSort(dtypeSpec));
}
}
TEST_F(TestApiBlackTermManager, mkDatatypeSorts)
{
{
DatatypeDecl dtypeSpec1 = d_tm.mkDatatypeDecl("list1");
DatatypeConstructorDecl cons1 = d_tm.mkDatatypeConstructorDecl("cons1");
cons1.addSelector("head1", d_tm.getIntegerSort());
dtypeSpec1.addConstructor(cons1);
DatatypeConstructorDecl nil1 = d_tm.mkDatatypeConstructorDecl("nil1");
dtypeSpec1.addConstructor(nil1);
DatatypeDecl dtypeSpec2 = d_tm.mkDatatypeDecl("list2");
DatatypeConstructorDecl cons2 = d_tm.mkDatatypeConstructorDecl("cons2");
cons2.addSelector("head2", d_tm.getIntegerSort());
dtypeSpec2.addConstructor(cons2);
DatatypeConstructorDecl nil2 = d_tm.mkDatatypeConstructorDecl("nil2");
dtypeSpec2.addConstructor(nil2);
std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
ASSERT_NO_THROW(d_tm.mkDatatypeSorts(decls));
ASSERT_THROW(d_tm.mkDatatypeSorts(decls), CVC5ApiException);
ASSERT_THROW(d_tm.mkDatatypeSorts(decls), CVC5ApiException);
}
DatatypeDecl throwsDtypeSpec = d_tm.mkDatatypeDecl("list");
std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
ASSERT_THROW(d_tm.mkDatatypeSorts(throwsDecls), CVC5ApiException);
/* with unresolved sorts */
Sort unresList = d_tm.mkUnresolvedDatatypeSort("ulist");
DatatypeDecl ulist = d_tm.mkDatatypeDecl("ulist");
DatatypeConstructorDecl ucons = d_tm.mkDatatypeConstructorDecl("ucons");
ucons.addSelector("car", unresList);
ucons.addSelector("cdr", unresList);
ulist.addConstructor(ucons);
DatatypeConstructorDecl unil = d_tm.mkDatatypeConstructorDecl("unil");
ulist.addConstructor(unil);
std::vector<DatatypeDecl> udecls = {ulist};
ASSERT_NO_THROW(d_tm.mkDatatypeSorts(udecls));
ASSERT_THROW(d_tm.mkDatatypeSorts(udecls), CVC5ApiException);
ASSERT_THROW(d_tm.mkDatatypeSorts(udecls), CVC5ApiException);
/* mutually recursive with unresolved parameterized sorts */
Sort p0 = d_tm.mkParamSort("p0");
Sort p1 = d_tm.mkParamSort("p1");
Sort u0 = d_tm.mkUnresolvedDatatypeSort("dt0", 1);
Sort u1 = d_tm.mkUnresolvedDatatypeSort("dt1", 1);
DatatypeDecl dtdecl0 = d_tm.mkDatatypeDecl("dt0", {p0});
DatatypeDecl dtdecl1 = d_tm.mkDatatypeDecl("dt1", {p1});
DatatypeConstructorDecl ctordecl0 = d_tm.mkDatatypeConstructorDecl("c0");
ctordecl0.addSelector("s0", u1.instantiate({p0}));
DatatypeConstructorDecl ctordecl1 = d_tm.mkDatatypeConstructorDecl("c1");
ctordecl1.addSelector("s1", u0.instantiate({p1}));
dtdecl0.addConstructor(ctordecl0);
dtdecl1.addConstructor(ctordecl1);
dtdecl1.addConstructor(d_tm.mkDatatypeConstructorDecl("nil"));
std::vector<Sort> dt_sorts = d_tm.mkDatatypeSorts({dtdecl0, dtdecl1});
Sort isort1 = dt_sorts[1].instantiate({d_tm.getBooleanSort()});
Term t1 = d_tm.mkConst(isort1, "t");
Term t0 =
d_tm.mkTerm(Kind::APPLY_SELECTOR,
{t1.getSort().getDatatype().getSelector("s1").getTerm(), t1});
ASSERT_EQ(dt_sorts[0].instantiate({d_tm.getBooleanSort()}), t0.getSort());
{
TermManager tm;
DatatypeDecl dtypeSpec1 = tm.mkDatatypeDecl("list1");
DatatypeConstructorDecl cons1 = tm.mkDatatypeConstructorDecl("cons1");
cons1.addSelector("head1", tm.getIntegerSort());
dtypeSpec1.addConstructor(cons1);
DatatypeConstructorDecl nil1 = tm.mkDatatypeConstructorDecl("nil1");
dtypeSpec1.addConstructor(nil1);
DatatypeDecl dtypeSpec2 = tm.mkDatatypeDecl("list2");
DatatypeConstructorDecl cons2 = tm.mkDatatypeConstructorDecl("cons2");
cons2.addSelector("head2", tm.getIntegerSort());
dtypeSpec2.addConstructor(cons2);
DatatypeConstructorDecl nil2 = tm.mkDatatypeConstructorDecl("nil2");
dtypeSpec2.addConstructor(nil2);
std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(d_tm.mkDatatypeSorts(decls));
}
/* Note: More tests are in datatype_api_black. */
}
TEST_F(TestApiBlackTermManager, mkFunctionSort)
{
ASSERT_NO_THROW(d_tm.mkFunctionSort({d_tm.mkUninterpretedSort("u")},
d_tm.getIntegerSort()));
Sort funSort = d_tm.mkFunctionSort({d_tm.mkUninterpretedSort("u")},
d_tm.getIntegerSort());
// function arguments are allowed
ASSERT_NO_THROW(d_tm.mkFunctionSort({funSort}, d_tm.getIntegerSort()));
// non-first-class arguments are not allowed
Sort reSort = d_tm.getRegExpSort();
ASSERT_THROW(d_tm.mkFunctionSort({reSort}, d_tm.getIntegerSort()),
CVC5ApiException);
ASSERT_THROW(d_tm.mkFunctionSort({d_tm.getIntegerSort()}, funSort),
CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkFunctionSort(
{d_tm.mkUninterpretedSort("u"), d_tm.getIntegerSort()},
d_tm.getIntegerSort()));
Sort funSort2 = d_tm.mkFunctionSort({d_tm.mkUninterpretedSort("u")},
d_tm.getIntegerSort());
// function arguments are allowed
ASSERT_NO_THROW(d_tm.mkFunctionSort({funSort2, d_tm.mkUninterpretedSort("u")},
d_tm.getIntegerSort()));
ASSERT_THROW(
d_tm.mkFunctionSort(
{d_tm.getIntegerSort(), d_tm.mkUninterpretedSort("u")}, funSort2),
CVC5ApiException);
std::vector<Sort> sorts1 = {
d_tm.getBooleanSort(), d_tm.getIntegerSort(), d_tm.getIntegerSort()};
std::vector<Sort> sorts2 = {d_tm.getBooleanSort(), d_tm.getIntegerSort()};
ASSERT_NO_THROW(d_tm.mkFunctionSort(sorts2, d_tm.getIntegerSort()));
ASSERT_NO_THROW(d_tm.mkFunctionSort(sorts1, d_tm.getIntegerSort()));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkFunctionSort(sorts2, tm.getIntegerSort()));
ASSERT_NO_THROW(tm.mkFunctionSort({tm.getBooleanSort(), tm.getIntegerSort()},
d_tm.getIntegerSort()));
}
TEST_F(TestApiBlackTermManager, mkParamSort)
{
ASSERT_NO_THROW(d_tm.mkParamSort("T"));
ASSERT_NO_THROW(d_tm.mkParamSort(""));
}
TEST_F(TestApiBlackTermManager, mkPredicateSort)
{
ASSERT_NO_THROW(d_tm.mkPredicateSort({d_tm.getIntegerSort()}));
ASSERT_THROW(d_tm.mkPredicateSort({}), CVC5ApiException);
Sort funSort = d_tm.mkFunctionSort({d_tm.mkUninterpretedSort("u")},
d_tm.getIntegerSort());
// functions as arguments are allowed
ASSERT_NO_THROW(d_tm.mkPredicateSort({d_tm.getIntegerSort(), funSort}));
ASSERT_NO_THROW(d_tm.mkPredicateSort({d_tm.getIntegerSort()}));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkPredicateSort({d_tm.getIntegerSort()}));
}
TEST_F(TestApiBlackTermManager, mkRecordSort)
{
std::vector<std::pair<std::string, Sort>> fields = {
std::make_pair("b", d_tm.getBooleanSort()),
std::make_pair("bv", d_tm.mkBitVectorSort(8)),
std::make_pair("i", d_tm.getIntegerSort())};
std::vector<std::pair<std::string, Sort>> empty;
ASSERT_NO_THROW(d_tm.mkRecordSort(fields));
ASSERT_NO_THROW(d_tm.mkRecordSort(empty));
Sort recSort = d_tm.mkRecordSort(fields);
ASSERT_NO_THROW(recSort.getDatatype());
ASSERT_NO_THROW(d_tm.mkRecordSort(fields));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkRecordSort({{"b", tm.getBooleanSort()},
{"bv", d_tm.mkBitVectorSort(8)},
{"i", tm.getIntegerSort()}}));
}
TEST_F(TestApiBlackTermManager, mkSetSort)
{
ASSERT_NO_THROW(d_tm.mkSetSort(d_tm.getBooleanSort()));
ASSERT_NO_THROW(d_tm.mkSetSort(d_tm.getIntegerSort()));
ASSERT_NO_THROW(d_tm.mkSetSort(d_tm.mkBitVectorSort(4)));
ASSERT_NO_THROW(d_tm.mkSetSort(d_tm.mkBitVectorSort(4)));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(d_tm.mkSetSort(tm.getBooleanSort()));
}
TEST_F(TestApiBlackTermManager, mkBagSort)
{
ASSERT_NO_THROW(d_tm.mkBagSort(d_tm.getBooleanSort()));
ASSERT_NO_THROW(d_tm.mkBagSort(d_tm.getIntegerSort()));
ASSERT_NO_THROW(d_tm.mkBagSort(d_tm.mkBitVectorSort(4)));
ASSERT_NO_THROW(d_tm.mkBagSort(d_tm.mkBitVectorSort(4)));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(d_tm.mkBagSort(tm.getBooleanSort()));
}
TEST_F(TestApiBlackTermManager, mkSequenceSort)
{
ASSERT_NO_THROW(d_tm.mkSequenceSort(d_tm.getBooleanSort()));
ASSERT_NO_THROW(
d_tm.mkSequenceSort(d_tm.mkSequenceSort(d_tm.getIntegerSort())));
ASSERT_NO_THROW(d_tm.mkSequenceSort(d_tm.getIntegerSort()));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(d_tm.mkSequenceSort(tm.getBooleanSort()));
}
TEST_F(TestApiBlackTermManager, mkAbstractSort)
{
ASSERT_NO_THROW(d_tm.mkAbstractSort(SortKind::ARRAY_SORT));
ASSERT_NO_THROW(d_tm.mkAbstractSort(SortKind::BITVECTOR_SORT));
ASSERT_NO_THROW(d_tm.mkAbstractSort(SortKind::TUPLE_SORT));
ASSERT_NO_THROW(d_tm.mkAbstractSort(SortKind::SET_SORT));
ASSERT_THROW(d_tm.mkAbstractSort(SortKind::BOOLEAN_SORT), CVC5ApiException);
}
TEST_F(TestApiBlackTermManager, mkUninterpretedSort)
{
ASSERT_NO_THROW(d_tm.mkUninterpretedSort("u"));
ASSERT_NO_THROW(d_tm.mkUninterpretedSort(""));
}
TEST_F(TestApiBlackTermManager, mkUnresolvedDatatypeSort)
{
ASSERT_NO_THROW(d_tm.mkUnresolvedDatatypeSort("u"));
ASSERT_NO_THROW(d_tm.mkUnresolvedDatatypeSort("u", 1));
ASSERT_NO_THROW(d_tm.mkUnresolvedDatatypeSort(""));
ASSERT_NO_THROW(d_tm.mkUnresolvedDatatypeSort("", 1));
}
TEST_F(TestApiBlackTermManager, mkUninterpretedSortConstructorSort)
{
ASSERT_NO_THROW(d_tm.mkUninterpretedSortConstructorSort(2, "s"));
ASSERT_NO_THROW(d_tm.mkUninterpretedSortConstructorSort(2, ""));
ASSERT_THROW(d_tm.mkUninterpretedSortConstructorSort(0), CVC5ApiException);
}
TEST_F(TestApiBlackTermManager, mkTupleSort)
{
ASSERT_NO_THROW(d_tm.mkTupleSort({d_tm.getIntegerSort()}));
Sort funSort = d_tm.mkFunctionSort({d_tm.mkUninterpretedSort("u")},
d_tm.getIntegerSort());
ASSERT_NO_THROW(d_tm.mkTupleSort({d_tm.getIntegerSort(), funSort}));
ASSERT_NO_THROW(d_tm.mkTupleSort({d_tm.getIntegerSort()}));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(d_tm.mkTupleSort({tm.getBooleanSort()}));
}
TEST_F(TestApiBlackTermManager, mkNullableSort)
{
ASSERT_NO_THROW(d_tm.mkNullableSort(d_tm.getIntegerSort()));
ASSERT_NO_THROW(d_tm.mkNullableSort(d_tm.getIntegerSort()));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(d_tm.mkNullableSort(tm.getIntegerSort()));
}
TEST_F(TestApiBlackTermManager, mkBitVector)
{
ASSERT_NO_THROW(d_tm.mkBitVector(8, 2));
ASSERT_NO_THROW(d_tm.mkBitVector(32, 2));
ASSERT_NO_THROW(d_tm.mkBitVector(8, "-1111111", 2));
ASSERT_NO_THROW(d_tm.mkBitVector(8, "0101", 2));
ASSERT_NO_THROW(d_tm.mkBitVector(8, "00000101", 2));
ASSERT_NO_THROW(d_tm.mkBitVector(8, "-127", 10));
ASSERT_NO_THROW(d_tm.mkBitVector(8, "255", 10));
ASSERT_NO_THROW(d_tm.mkBitVector(8, "-7f", 16));
ASSERT_NO_THROW(d_tm.mkBitVector(8, "a0", 16));
ASSERT_THROW(d_tm.mkBitVector(0, 2), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(0, "-127", 10), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(0, "a0", 16), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "", 2), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "101", 5), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "128", 11), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "a0", 21), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "-11111111", 2), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "101010101", 2), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "-256", 10), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "257", 10), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "-a0", 16), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "fffff", 16), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "10201010", 2), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "-25x", 10), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "2x7", 10), CVC5ApiException);
ASSERT_THROW(d_tm.mkBitVector(8, "fzff", 16), CVC5ApiException);
ASSERT_EQ(d_tm.mkBitVector(8, "0101", 2), d_tm.mkBitVector(8, "00000101", 2));
ASSERT_EQ(d_tm.mkBitVector(4, "-1", 2), d_tm.mkBitVector(4, "1111", 2));
ASSERT_EQ(d_tm.mkBitVector(4, "-1", 16), d_tm.mkBitVector(4, "1111", 2));
ASSERT_EQ(d_tm.mkBitVector(4, "-1", 10), d_tm.mkBitVector(4, "1111", 2));
ASSERT_EQ(d_tm.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
ASSERT_EQ(d_tm.mkBitVector(8, "F", 16).toString(), "#b00001111");
ASSERT_EQ(d_tm.mkBitVector(8, "-1", 10), d_tm.mkBitVector(8, "FF", 16));
}
TEST_F(TestApiBlackTermManager, mkFiniteFieldElem)
{
Sort f = d_tm.mkFiniteFieldSort("7");
Sort bv = d_tm.mkBitVectorSort(4);
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("0", f));
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("1", f));
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("6", f));
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("8", f));
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("-1", f));
ASSERT_THROW(d_tm.mkFiniteFieldElem("a", f), CVC5ApiException);
ASSERT_THROW(d_tm.mkFiniteFieldElem("-1", bv), CVC5ApiException);
ASSERT_EQ(d_tm.mkFiniteFieldElem("-1", f), d_tm.mkFiniteFieldElem("6", f));
ASSERT_EQ(d_tm.mkFiniteFieldElem("1", f), d_tm.mkFiniteFieldElem("8", f));
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("0", f, 2));
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("101", f, 3));
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("-10", f, 7));
ASSERT_NO_THROW(d_tm.mkFiniteFieldElem("abcde", f, 16));
ASSERT_EQ(d_tm.mkFiniteFieldElem("0", f, 2),
d_tm.mkFiniteFieldElem("0", f, 3));
ASSERT_EQ(d_tm.mkFiniteFieldElem("11", f, 2),
d_tm.mkFiniteFieldElem("10", f, 3));
ASSERT_EQ(d_tm.mkFiniteFieldElem("1010", f, 2),
d_tm.mkFiniteFieldElem("A", f, 16));
ASSERT_EQ(d_tm.mkFiniteFieldElem("-22", f, 3),
d_tm.mkFiniteFieldElem("10", f, 6));
}
TEST_F(TestApiBlackTermManager, mkConstArray)
{
Sort intSort = d_tm.getIntegerSort();
Sort arrSort = d_tm.mkArraySort(intSort, intSort);
Term zero = d_tm.mkInteger(0);
Term constArr = d_tm.mkConstArray(arrSort, zero);
ASSERT_THROW(d_tm.mkConstArray(Sort(), zero), CVC5ApiException);
ASSERT_THROW(d_tm.mkConstArray(arrSort, Term()), CVC5ApiException);
ASSERT_THROW(d_tm.mkConstArray(arrSort, d_tm.mkBitVector(1, 1)),
CVC5ApiException);
ASSERT_THROW(d_tm.mkConstArray(intSort, zero), CVC5ApiException);
Term zero2 = d_tm.mkInteger(0);
Sort arrSort2 =
d_tm.mkArraySort(d_tm.getIntegerSort(), d_tm.getIntegerSort());
ASSERT_NO_THROW(d_tm.mkConstArray(arrSort2, zero));
ASSERT_NO_THROW(d_tm.mkConstArray(arrSort, zero2));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkConstArray(arrSort, tm.mkInteger(0)));
ASSERT_NO_THROW(tm.mkConstArray(
tm.mkArraySort(tm.getIntegerSort(), tm.getIntegerSort()), zero));
}
TEST_F(TestApiBlackTermManager, mkVar)
{
Sort boolSort = d_tm.getBooleanSort();
Sort intSort = d_tm.getIntegerSort();
Sort funSort = d_tm.mkFunctionSort({intSort}, boolSort);
ASSERT_NO_THROW(d_tm.mkVar(boolSort));
ASSERT_NO_THROW(d_tm.mkVar(funSort));
ASSERT_NO_THROW(d_tm.mkVar(boolSort, std::string("b")));
ASSERT_NO_THROW(d_tm.mkVar(funSort, ""));
ASSERT_THROW(d_tm.mkVar(Sort()), CVC5ApiException);
ASSERT_THROW(d_tm.mkVar(Sort(), "a"), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkVar(boolSort, "x"));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkVar(boolSort, "c"));
}
TEST_F(TestApiBlackTermManager, mkBoolean)
{
ASSERT_NO_THROW(d_tm.mkBoolean(true));
ASSERT_NO_THROW(d_tm.mkBoolean(false));
}
TEST_F(TestApiBlackTermManager, mkRoundingMode)
{
ASSERT_EQ(
d_tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN).toString(),
"roundNearestTiesToEven");
ASSERT_EQ(d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE).toString(),
"roundTowardPositive");
ASSERT_EQ(d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE).toString(),
"roundTowardNegative");
ASSERT_EQ(d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO).toString(),
"roundTowardZero");
ASSERT_EQ(
d_tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY).toString(),
"roundNearestTiesToAway");
}
TEST_F(TestApiBlackTermManager, mkFloatingPoint)
{
Term t1 = d_tm.mkBitVector(8);
Term t2 = d_tm.mkBitVector(4);
ASSERT_NO_THROW(d_tm.mkFloatingPoint(3, 5, t1));
ASSERT_THROW(d_tm.mkFloatingPoint(0, 5, Term()), CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPoint(0, 5, t1), CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPoint(1, 5, t1), CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPoint(3, 0, t1), CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPoint(3, 1, t1), CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPoint(3, 5, t2), CVC5ApiException);
ASSERT_EQ(d_tm.mkFloatingPoint(
d_tm.mkBitVector(1), d_tm.mkBitVector(5), d_tm.mkBitVector(10)),
d_tm.mkFloatingPoint(5, 11, d_tm.mkBitVector(16)));
ASSERT_THROW(
d_tm.mkFloatingPoint(Term(), d_tm.mkBitVector(5), d_tm.mkBitVector(10)),
CVC5ApiException);
ASSERT_THROW(
d_tm.mkFloatingPoint(d_tm.mkBitVector(1), Term(), d_tm.mkBitVector(10)),
CVC5ApiException);
ASSERT_THROW(
d_tm.mkFloatingPoint(d_tm.mkBitVector(1), d_tm.mkBitVector(5), Term()),
CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPoint(d_tm.mkConst(d_tm.mkBitVectorSort(1)),
d_tm.mkBitVector(5),
d_tm.mkBitVector(10)),
CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPoint(d_tm.mkBitVector(1),
d_tm.mkConst(d_tm.mkBitVectorSort(5)),
d_tm.mkBitVector(10)),
CVC5ApiException);
ASSERT_THROW(d_tm.mkFloatingPoint(d_tm.mkBitVector(1),
d_tm.mkBitVector(5),
d_tm.mkConst(d_tm.mkBitVectorSort(5))),
CVC5ApiException);
ASSERT_THROW(
d_tm.mkFloatingPoint(
d_tm.mkBitVector(2), d_tm.mkBitVector(5), d_tm.mkBitVector(10)),
CVC5ApiException);
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkFloatingPoint(3, 5, t1));
ASSERT_NO_THROW(tm.mkFloatingPoint(
d_tm.mkBitVector(1), tm.mkBitVector(5), tm.mkBitVector(10)));
ASSERT_NO_THROW(tm.mkFloatingPoint(
tm.mkBitVector(1), d_tm.mkBitVector(5), tm.mkBitVector(10)));
ASSERT_NO_THROW(tm.mkFloatingPoint(
tm.mkBitVector(1), tm.mkBitVector(5), d_tm.mkBitVector(10)));
}
TEST_F(TestApiBlackTermManager, mkCardinalityConstraint)
{
Sort su = d_tm.mkUninterpretedSort("u");
Sort si = d_tm.getIntegerSort();
ASSERT_NO_THROW(d_tm.mkCardinalityConstraint(su, 3));
ASSERT_THROW(d_tm.mkCardinalityConstraint(si, 3), CVC5ApiException);
ASSERT_THROW(d_tm.mkCardinalityConstraint(su, 0), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkCardinalityConstraint(su, 3));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkCardinalityConstraint(su, 3));
}
TEST_F(TestApiBlackTermManager, mkEmptySet)
{
Sort s = d_tm.mkSetSort(d_tm.getBooleanSort());
ASSERT_THROW(d_tm.mkEmptySet(Sort()), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkEmptySet(s));
ASSERT_THROW(d_tm.mkEmptySet(d_tm.getBooleanSort()), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkEmptySet(s));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkEmptySet(s));
}
TEST_F(TestApiBlackTermManager, mkEmptyBag)
{
Sort s = d_tm.mkBagSort(d_tm.getBooleanSort());
ASSERT_THROW(d_tm.mkEmptyBag(Sort()), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkEmptyBag(s));
ASSERT_THROW(d_tm.mkEmptyBag(d_tm.getBooleanSort()), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkEmptyBag(s));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkEmptyBag(s));
}
TEST_F(TestApiBlackTermManager, mkEmptySequence)
{
Sort s = d_tm.mkSequenceSort(d_tm.getBooleanSort());
ASSERT_NO_THROW(d_tm.mkEmptySequence(s));
ASSERT_NO_THROW(d_tm.mkEmptySequence(d_tm.getBooleanSort()));
ASSERT_NO_THROW(d_tm.mkEmptySequence(s));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkEmptySequence(s));
}
TEST_F(TestApiBlackTermManager, mkFalse)
{
ASSERT_NO_THROW(d_tm.mkFalse());
ASSERT_NO_THROW(d_tm.mkFalse());
}
TEST_F(TestApiBlackTermManager, mkFloatingPointNaN)
{
ASSERT_NO_THROW(d_tm.mkFloatingPointNaN(3, 5));
}
TEST_F(TestApiBlackTermManager, mkFloatingPointNegZero)
{
ASSERT_NO_THROW(d_tm.mkFloatingPointNegZero(3, 5));
}
TEST_F(TestApiBlackTermManager, mkFloatingPointNegInf)
{
ASSERT_NO_THROW(d_tm.mkFloatingPointNegInf(3, 5));
}
TEST_F(TestApiBlackTermManager, mkFloatingPointPosInf)
{
ASSERT_NO_THROW(d_tm.mkFloatingPointPosInf(3, 5));
}
TEST_F(TestApiBlackTermManager, mkFloatingPointPosZero)
{
ASSERT_NO_THROW(d_tm.mkFloatingPointPosZero(3, 5));
}
TEST_F(TestApiBlackTermManager, mkOp)
{
// mkOp(Kind kind, const std::string& arg)
ASSERT_NO_THROW(d_tm.mkOp(Kind::DIVISIBLE, "2147483648"));
ASSERT_THROW(d_tm.mkOp(Kind::BITVECTOR_EXTRACT, "asdf"), CVC5ApiException);
// mkOp(Kind kind, std::vector<uint32_t> args)
ASSERT_NO_THROW(d_tm.mkOp(Kind::DIVISIBLE, {1}));
ASSERT_NO_THROW(d_tm.mkOp(Kind::BITVECTOR_ROTATE_LEFT, {1}));
ASSERT_NO_THROW(d_tm.mkOp(Kind::BITVECTOR_ROTATE_RIGHT, {1}));
ASSERT_THROW(d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {1}), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {1, 1}));
ASSERT_THROW(d_tm.mkOp(Kind::DIVISIBLE, {1, 2}), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkOp(Kind::TUPLE_PROJECT, {1, 2, 2}));
}
TEST_F(TestApiBlackTermManager, mkPi) { ASSERT_NO_THROW(d_tm.mkPi()); }
TEST_F(TestApiBlackTermManager, mkInteger)
{
ASSERT_NO_THROW(d_tm.mkInteger("123"));
ASSERT_THROW(d_tm.mkInteger("1.23"), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("1/23"), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("12/3"), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger(".2"), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("2."), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger(""), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("asdf"), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("1.2/3"), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("."), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("/"), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("2/"), CVC5ApiException);
ASSERT_THROW(d_tm.mkInteger("/2"), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkInteger(1));
ASSERT_NO_THROW(d_tm.mkInteger(-1));
}
TEST_F(TestApiBlackTermManager, mkReal)
{
ASSERT_NO_THROW(d_tm.mkReal("123"));
ASSERT_NO_THROW(d_tm.mkReal("1.23"));
ASSERT_NO_THROW(d_tm.mkReal("1/23"));
ASSERT_NO_THROW(d_tm.mkReal("12/3"));
ASSERT_NO_THROW(d_tm.mkReal(".2"));
ASSERT_NO_THROW(d_tm.mkReal("2."));
ASSERT_THROW(d_tm.mkReal(""), CVC5ApiException);
ASSERT_THROW(d_tm.mkReal("asdf"), CVC5ApiException);
ASSERT_THROW(d_tm.mkReal("1.2/3"), CVC5ApiException);
ASSERT_THROW(d_tm.mkReal("."), CVC5ApiException);
ASSERT_THROW(d_tm.mkReal("/"), CVC5ApiException);
ASSERT_THROW(d_tm.mkReal("2/"), CVC5ApiException);
ASSERT_THROW(d_tm.mkReal("/2"), CVC5ApiException);
int32_t val1 = 1;
int64_t val2 = -1;
uint32_t val3 = 1;
uint64_t val4 = -1;
ASSERT_NO_THROW(d_tm.mkReal(val1));
ASSERT_NO_THROW(d_tm.mkReal(val2));
ASSERT_NO_THROW(d_tm.mkReal(val3));
ASSERT_NO_THROW(d_tm.mkReal(val4));
ASSERT_NO_THROW(d_tm.mkReal(val4));
ASSERT_NO_THROW(d_tm.mkReal(val1, val1));
ASSERT_NO_THROW(d_tm.mkReal(val2, val2));
ASSERT_NO_THROW(d_tm.mkReal(val3, val3));
ASSERT_NO_THROW(d_tm.mkReal(val4, val4));
ASSERT_NO_THROW(d_tm.mkReal("-1/-1"));
ASSERT_NO_THROW(d_tm.mkReal("1/-1"));
ASSERT_NO_THROW(d_tm.mkReal("-1/1"));
ASSERT_NO_THROW(d_tm.mkReal("1/1"));
ASSERT_THROW(d_tm.mkReal("/-5"), CVC5ApiException);
ASSERT_THROW(d_tm.mkReal(1, 0), CVC5ApiException);
}
TEST_F(TestApiBlackTermManager, mkRegexpAll)
{
Sort strSort = d_tm.getStringSort();
Term s = d_tm.mkConst(strSort, "s");
ASSERT_NO_THROW(d_tm.mkTerm(Kind::STRING_IN_REGEXP, {s, d_tm.mkRegexpAll()}));
}
TEST_F(TestApiBlackTermManager, mkRegexpAllchar)
{
Sort strSort = d_tm.getStringSort();
Term s = d_tm.mkConst(strSort, "s");
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::STRING_IN_REGEXP, {s, d_tm.mkRegexpAllchar()}));
}
TEST_F(TestApiBlackTermManager, mkRegexpNone)
{
Sort strSort = d_tm.getStringSort();
Term s = d_tm.mkConst(strSort, "s");
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::STRING_IN_REGEXP, {s, d_tm.mkRegexpNone()}));
}
TEST_F(TestApiBlackTermManager, mkSepEmp) { ASSERT_NO_THROW(d_tm.mkSepEmp()); }
TEST_F(TestApiBlackTermManager, mkSepNil)
{
ASSERT_NO_THROW(d_tm.mkSepNil(d_tm.getBooleanSort()));
ASSERT_THROW(d_tm.mkSepNil(Sort()), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkSepNil(d_tm.getIntegerSort()));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkSepNil(d_tm.getBooleanSort()));
}
TEST_F(TestApiBlackTermManager, mkString)
{
ASSERT_NO_THROW(d_tm.mkString(""));
ASSERT_NO_THROW(d_tm.mkString("asdfasdf"));
ASSERT_EQ(d_tm.mkString("asdf\\nasdf").toString(), "\"asdf\\u{5c}nasdf\"");
ASSERT_EQ(d_tm.mkString("asdf\\u{005c}nasdf", true).toString(),
"\"asdf\\u{5c}nasdf\"");
std::wstring s;
ASSERT_EQ(d_tm.mkString(s).getStringValue(), s);
}
TEST_F(TestApiBlackTermManager, mkTerm)
{
Sort bv32 = d_tm.mkBitVectorSort(32);
Term a = d_tm.mkConst(bv32, "a");
Term b = d_tm.mkConst(bv32, "b");
std::vector<Term> v1 = {a, b};
std::vector<Term> v2 = {a, Term()};
std::vector<Term> v3 = {a, d_tm.mkTrue()};
std::vector<Term> v4 = {d_tm.mkInteger(1), d_tm.mkInteger(2)};
std::vector<Term> v5 = {d_tm.mkInteger(1), Term()};
std::vector<Term> v6 = {};
ASSERT_NO_THROW(d_tm.mkTerm(Kind::PI));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::PI, {v6}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::PI)));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::PI), {v6}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::REGEXP_NONE));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::REGEXP_NONE, {v6}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::REGEXP_NONE)));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::REGEXP_NONE), {v6}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::REGEXP_ALLCHAR));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::REGEXP_ALLCHAR, {v6}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::REGEXP_ALLCHAR)));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::REGEXP_ALLCHAR), {v6}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::SEP_EMP));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::SEP_EMP, {v6}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::SEP_EMP)));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::SEP_EMP), {v6}));
ASSERT_THROW(d_tm.mkTerm(Kind::CONST_BITVECTOR), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkTerm(Kind::NOT, {d_tm.mkTrue()}));
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::BAG_MAKE, {d_tm.mkTrue(), d_tm.mkInteger(1)}));
ASSERT_THROW(d_tm.mkTerm(Kind::NOT, {Term()}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::NOT, {a}), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkTerm(Kind::NOT, {d_tm.mkTrue()}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::EQUAL, {a, b}));
ASSERT_THROW(d_tm.mkTerm(Kind::EQUAL, {Term(), b}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::EQUAL, {a, Term()}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::EQUAL, {a, d_tm.mkTrue()}), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkTerm(Kind::EQUAL, {a, b}));
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::ITE, {d_tm.mkTrue(), d_tm.mkTrue(), d_tm.mkTrue()}));
ASSERT_THROW(d_tm.mkTerm(Kind::ITE, {Term(), d_tm.mkTrue(), d_tm.mkTrue()}),
CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::ITE, {d_tm.mkTrue(), Term(), d_tm.mkTrue()}),
CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::ITE, {d_tm.mkTrue(), d_tm.mkTrue(), Term()}),
CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::ITE, {d_tm.mkTrue(), d_tm.mkTrue(), b}),
CVC5ApiException);
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::ITE, {d_tm.mkTrue(), d_tm.mkTrue(), d_tm.mkTrue()}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::EQUAL, {v1}));
ASSERT_THROW(d_tm.mkTerm(Kind::EQUAL, {v2}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::EQUAL, {v3}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::DISTINCT, {v6}), CVC5ApiException);
// Test cases that are nary via the API but have arity = 2 internally
Sort s_bool = d_tm.getBooleanSort();
Term t_bool = d_tm.mkConst(s_bool, "t_bool");
ASSERT_NO_THROW(d_tm.mkTerm(Kind::IMPLIES, {t_bool, t_bool, t_bool}));
ASSERT_NO_THROW(
d_tm.mkTerm(d_tm.mkOp(Kind::IMPLIES), {t_bool, t_bool, t_bool}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::XOR, {t_bool, t_bool, t_bool}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::XOR), {t_bool, t_bool, t_bool}));
Term t_int = d_tm.mkConst(d_tm.getIntegerSort(), "t_int");
ASSERT_NO_THROW(d_tm.mkTerm(Kind::DIVISION, {t_int, t_int, t_int}));
ASSERT_NO_THROW(
d_tm.mkTerm(d_tm.mkOp(Kind::DIVISION), {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::INTS_DIVISION, {t_int, t_int, t_int}));
ASSERT_NO_THROW(
d_tm.mkTerm(d_tm.mkOp(Kind::INTS_DIVISION), {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::SUB, {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::SUB), {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::EQUAL, {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::EQUAL), {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::LT, {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::LT), {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::GT, {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::GT), {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::LEQ, {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::LEQ), {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::GEQ, {t_int, t_int, t_int}));
ASSERT_NO_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::GEQ), {t_int, t_int, t_int}));
Term t_reg = d_tm.mkConst(d_tm.getRegExpSort(), "t_reg");
ASSERT_NO_THROW(d_tm.mkTerm(Kind::REGEXP_DIFF, {t_reg, t_reg, t_reg}));
ASSERT_NO_THROW(
d_tm.mkTerm(d_tm.mkOp(Kind::REGEXP_DIFF), {t_reg, t_reg, t_reg}));
Term t_fun =
d_tm.mkConst(d_tm.mkFunctionSort({s_bool, s_bool, s_bool}, s_bool));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::HO_APPLY, {t_fun, t_bool, t_bool, t_bool}));
ASSERT_NO_THROW(
d_tm.mkTerm(d_tm.mkOp(Kind::HO_APPLY), {t_fun, t_bool, t_bool, t_bool}));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::ITE, {d_tm.mkTrue(), tm.mkTrue(), tm.mkTrue()}));
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::ITE, {tm.mkTrue(), d_tm.mkTrue(), tm.mkTrue()}));
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::ITE, {tm.mkTrue(), tm.mkTrue(), d_tm.mkTrue()}));
}
TEST_F(TestApiBlackTermManager, mkTermFromOp)
{
Sort bv32 = d_tm.mkBitVectorSort(32);
Term a = d_tm.mkConst(bv32, "a");
Term b = d_tm.mkConst(bv32, "b");
std::vector<Term> v1 = {d_tm.mkInteger(1), d_tm.mkInteger(2)};
std::vector<Term> v2 = {d_tm.mkInteger(1), Term()};
std::vector<Term> v3 = {};
std::vector<Term> v4 = {d_tm.mkInteger(5)};
// simple operator terms
Op opterm1 = d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {2, 1});
Op opterm2 = d_tm.mkOp(Kind::DIVISIBLE, {1});
// list datatype
Sort sort = d_tm.mkParamSort("T");
DatatypeDecl listDecl = d_tm.mkDatatypeDecl("paramlist", {sort});
DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil");
cons.addSelector("head", sort);
cons.addSelectorSelf("tail");
listDecl.addConstructor(cons);
listDecl.addConstructor(nil);
Sort listSort = d_tm.mkDatatypeSort(listDecl);
Sort intListSort =
listSort.instantiate(std::vector<Sort>{d_tm.getIntegerSort()});
Term c = d_tm.mkConst(intListSort, "c");
Datatype list = listSort.getDatatype();
// list datatype constructor and selector operator terms
Term consTerm = list.getConstructor("cons").getTerm();
Term nilTerm = list.getConstructor("nil").getTerm();
Term headTerm = list["cons"].getSelector("head").getTerm();
Term tailTerm = list["cons"]["tail"].getTerm();
// mkTerm(Op op, const std::vector<Term>& children) const
ASSERT_NO_THROW(d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {nilTerm}));
ASSERT_THROW(d_tm.mkTerm(Kind::APPLY_SELECTOR, {nilTerm}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::APPLY_SELECTOR, {consTerm}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {consTerm}),
CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(opterm1), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(Kind::APPLY_SELECTOR, {headTerm}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(opterm1), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {nilTerm}));
ASSERT_NO_THROW(d_tm.mkTerm(opterm1, {a}));
ASSERT_NO_THROW(d_tm.mkTerm(opterm2, {d_tm.mkInteger(1)}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::APPLY_SELECTOR, {headTerm, c}));
ASSERT_NO_THROW(d_tm.mkTerm(Kind::APPLY_SELECTOR, {tailTerm, c}));
ASSERT_THROW(d_tm.mkTerm(opterm2, {a}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(opterm1, {Term()}), CVC5ApiException);
ASSERT_THROW(
d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {consTerm, d_tm.mkInteger(0)}),
CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkTerm(opterm1, {a}));
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR,
{consTerm,
d_tm.mkInteger(0),
d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {nilTerm})}));
ASSERT_THROW(d_tm.mkTerm(opterm2, {d_tm.mkInteger(1), d_tm.mkInteger(2)}),
CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(opterm1, {a, b}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(opterm2, {d_tm.mkInteger(1), Term()}),
CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(opterm2, {Term(), d_tm.mkInteger(1)}),
CVC5ApiException);
ASSERT_NO_THROW(
d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR,
{consTerm,
d_tm.mkInteger(0),
d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {nilTerm})}));
ASSERT_THROW(d_tm.mkTerm(opterm1, {a, b, a}), CVC5ApiException);
ASSERT_THROW(
d_tm.mkTerm(opterm2, {d_tm.mkInteger(1), d_tm.mkInteger(1), Term()}),
CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkTerm(opterm2, {v4}));
ASSERT_THROW(d_tm.mkTerm(opterm2, {v1}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(opterm2, {v2}), CVC5ApiException);
ASSERT_THROW(d_tm.mkTerm(opterm2, {v3}), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkTerm(opterm2, {v4}));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkTerm(opterm2, {tm.mkInteger(1)}));
ASSERT_NO_THROW(
tm.mkTerm(tm.mkOp(Kind::DIVISIBLE, {1}), {d_tm.mkInteger(1)}));
}
TEST_F(TestApiBlackTermManager, mkTrue)
{
ASSERT_NO_THROW(d_tm.mkTrue());
ASSERT_NO_THROW(d_tm.mkTrue());
}
TEST_F(TestApiBlackTermManager, mkTuple)
{
ASSERT_NO_THROW(d_tm.mkTuple({d_tm.mkBitVector(3, "101", 2)}));
ASSERT_NO_THROW(d_tm.mkTuple({d_tm.mkInteger("5")}));
ASSERT_NO_THROW(d_tm.mkTuple({d_tm.mkReal("5.3")}));
ASSERT_NO_THROW(d_tm.mkTuple({d_tm.mkBitVector(3, "101", 2)}));
ASSERT_NO_THROW(d_tm.mkTuple({d_tm.mkBitVector(3, "101", 2)}));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkTuple({d_tm.mkBitVector(3, "101", 2)}));
}
TEST_F(TestApiBlackTermManager, mkNullableSome)
{
ASSERT_NO_THROW(d_tm.mkNullableSome(d_tm.mkBitVector(3, "101", 2)));
ASSERT_NO_THROW(d_tm.mkNullableSome(d_tm.mkInteger("5")));
ASSERT_NO_THROW(d_tm.mkNullableSome(d_tm.mkReal("5.3")));
ASSERT_NO_THROW(d_tm.mkNullableSome(d_tm.mkBitVector(3, "101", 2)));
ASSERT_NO_THROW(d_tm.mkNullableSome(d_tm.mkBitVector(3, "101", 2)));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkNullableSome(d_tm.mkBitVector(3, "101", 2)));
}
TEST_F(TestApiBlackTermManager, mkNullableVal)
{
Term value = d_tm.mkNullableVal(d_tm.mkNullableSome(d_tm.mkInteger(5)));
value = d_solver->simplify(value);
ASSERT_EQ(5, value.getInt32Value());
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(
tm.mkNullableVal(d_tm.mkNullableSome(d_tm.mkBitVector(3, "101", 2))));
}
TEST_F(TestApiBlackTermManager, mkNullableIsNull)
{
Term value = d_tm.mkNullableIsNull(d_tm.mkNullableSome(d_tm.mkInteger(5)));
value = d_solver->simplify(value);
ASSERT_EQ(false, value.getBooleanValue());
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkNullableIsNull(d_tm.mkNullableSome(d_tm.mkInteger(5))));
}
TEST_F(TestApiBlackTermManager, mkNullableIsSome)
{
Term value = d_tm.mkNullableIsSome(d_tm.mkNullableSome(d_tm.mkInteger(5)));
value = d_solver->simplify(value);
ASSERT_EQ(true, value.getBooleanValue());
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkNullableIsSome(d_tm.mkNullableSome(d_tm.mkInteger(5))));
}
TEST_F(TestApiBlackTermManager, mkNullableNull)
{
Sort nullableSort = d_tm.mkNullableSort(d_tm.getBooleanSort());
Term nullableNull = d_tm.mkNullableNull(nullableSort);
Term value = d_tm.mkNullableIsNull(nullableNull);
value = d_solver->simplify(value);
ASSERT_EQ(true, value.getBooleanValue());
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkNullableIsNull(
d_tm.mkNullableNull(d_tm.mkNullableSort(d_tm.getBooleanSort()))));
}
TEST_F(TestApiBlackTermManager, mkNullableLift)
{
Term some1 = d_tm.mkNullableSome(d_tm.mkInteger(1));
Term some2 = d_tm.mkNullableSome(d_tm.mkInteger(2));
Term some3 = d_tm.mkNullableLift(Kind::ADD, {some1, some2});
Term three = d_solver->simplify(d_tm.mkNullableVal(some3));
ASSERT_EQ(3, three.getInt32Value());
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkNullableLift(Kind::ADD,
{d_tm.mkNullableSome(d_tm.mkInteger(1)),
d_tm.mkNullableSome(d_tm.mkInteger(2))}));
}
TEST_F(TestApiBlackTermManager, mkUniverseSet)
{
ASSERT_NO_THROW(d_tm.mkUniverseSet(d_tm.getBooleanSort()));
ASSERT_THROW(d_tm.mkUniverseSet(Sort()), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkUniverseSet(d_tm.getBooleanSort()));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkUniverseSet(d_tm.getBooleanSort()));
}
TEST_F(TestApiBlackTermManager, mkConst)
{
Sort boolSort = d_tm.getBooleanSort();
Sort intSort = d_tm.getIntegerSort();
Sort funSort = d_tm.mkFunctionSort({intSort}, boolSort);
ASSERT_NO_THROW(d_tm.mkConst(boolSort));
ASSERT_NO_THROW(d_tm.mkConst(funSort));
ASSERT_NO_THROW(d_tm.mkConst(boolSort, std::string("b")));
ASSERT_NO_THROW(d_tm.mkConst(intSort, std::string("i")));
ASSERT_NO_THROW(d_tm.mkConst(funSort, "f"));
ASSERT_NO_THROW(d_tm.mkConst(funSort, ""));
ASSERT_THROW(d_tm.mkConst(Sort()), CVC5ApiException);
ASSERT_THROW(d_tm.mkConst(Sort(), "a"), CVC5ApiException);
ASSERT_NO_THROW(d_tm.mkConst(boolSort));
TermManager tm;
// this will throw when NodeManager is not a singleton anymore
ASSERT_NO_THROW(tm.mkConst(boolSort));
}
TEST_F(TestApiBlackTermManager, mkSkolem)
{
Sort integer = d_tm.getIntegerSort();
Sort arraySort = d_tm.mkArraySort(integer, integer);
Term a = d_tm.mkConst(arraySort, "a");
Term b = d_tm.mkConst(arraySort, "b");
Term sk = d_tm.mkSkolem(SkolemId::ARRAY_DEQ_DIFF, {a, b});
Term sk2 = d_tm.mkSkolem(SkolemId::ARRAY_DEQ_DIFF, {b, a});
ASSERT_THROW(d_tm.mkSkolem(SkolemId::ARRAY_DEQ_DIFF, {a}), CVC5ApiException);
ASSERT_TRUE(sk.isSkolem());
ASSERT_EQ(sk.getSkolemId(), SkolemId::ARRAY_DEQ_DIFF);
ASSERT_EQ(sk.getSkolemIndices(), std::vector<Term>({a, b}));
// ARRAY_DEQ_DIFF is commutative, so the order of the indices is sorted.
ASSERT_EQ(sk2.getSkolemIndices(), std::vector<Term>({a, b}));
}
TEST_F(TestApiBlackTermManager, getNumIndicesForSkolemId)
{
size_t numIndices = d_tm.getNumIndicesForSkolemId(SkolemId::BAGS_MAP_INDEX);
ASSERT_EQ(numIndices, 5);
}
TEST_F(TestApiBlackTermManager, uFIteration)
{
Sort intSort = d_tm.getIntegerSort();
Sort funSort = d_tm.mkFunctionSort({intSort, intSort}, intSort);
Term x = d_tm.mkConst(intSort, "x");
Term y = d_tm.mkConst(intSort, "y");
Term f = d_tm.mkConst(funSort, "f");
Term fxy = d_tm.mkTerm(Kind::APPLY_UF, {f, x, y});
// Expecting the uninterpreted function to be one of the children
Term expected_children[3] = {f, x, y};
uint32_t idx = 0;
for (auto c : fxy)
{
ASSERT_LT(idx, 3);
ASSERT_EQ(c, expected_children[idx]);
idx++;
}
}
TEST_F(TestApiBlackTermManager, getStatistics)
{
ASSERT_NO_THROW(cvc5::Stat());
// do some array reasoning to make sure we have statistics
{
Sort s1 = d_tm.getIntegerSort();
Sort s2 = d_tm.mkArraySort(s1, s1);
Term t1 = d_tm.mkConst(s1, "i");
Term t2 = d_tm.mkConst(s2, "a");
Term t3 = d_tm.mkTerm(Kind::SELECT, {t2, t1});
d_solver->assertFormula(t3.eqTerm(t1));
d_solver->checkSat();
}
cvc5::Statistics stats = d_tm.getStatistics();
{
std::stringstream ss;
ss << stats;
}
for (const auto& s : stats)
{
ASSERT_FALSE(s.first.empty());
}
for (auto it = stats.begin(true, true); it != stats.end(); ++it)
{
{
auto tmp1 = it, tmp2 = it;
++tmp1;
tmp2++;
ASSERT_EQ(tmp1, tmp2);
--tmp1;
tmp2--;
ASSERT_EQ(tmp1, tmp2);
ASSERT_EQ(tmp1, it);
ASSERT_EQ(it, tmp2);
}
const auto& s = *it;
// check some basic utility methods
ASSERT_TRUE(!(it == stats.end()));
ASSERT_EQ(s.first, it->first);
if (s.first == "cvc5::CONSTANT")
{
ASSERT_FALSE(s.second.isInternal());
ASSERT_FALSE(s.second.isDefault());
ASSERT_TRUE(s.second.isHistogram());
auto hist = s.second.getHistogram();
ASSERT_FALSE(hist.empty());
std::stringstream ss;
ss << s.second;
ASSERT_EQ(ss.str(), "{ UNKNOWN_TYPE_CONSTANT: 1, integer type: 1 }");
}
else if (s.first == "theory::arrays::avgIndexListLength")
{
ASSERT_TRUE(s.second.isInternal());
ASSERT_TRUE(s.second.isDouble());
ASSERT_TRUE(std::isnan(s.second.getDouble()));
}
}
}
TEST_F(TestApiBlackTermManager, printStatisticsSafe)
{
// do some array reasoning to make sure we have statistics
{
Sort s1 = d_tm.getIntegerSort();
Sort s2 = d_tm.mkArraySort(s1, s1);
Term t1 = d_tm.mkConst(s1, "i");
Term t2 = d_tm.mkConst(s2, "a");
Term t3 = d_tm.mkTerm(Kind::SELECT, {t2, t1});
d_solver->assertFormula(t3.eqTerm(t1));
d_solver->checkSat();
}
testing::internal::CaptureStdout();
d_tm.printStatisticsSafe(STDOUT_FILENO);
std::string out = testing::internal::GetCapturedStdout();
std::stringstream expected;
expected << "cvc5::CONSTANT = { integer type: 1, UNKNOWN_TYPE_CONSTANT: 1 }"
<< std::endl
<< "cvc5::TERM = { <unsupported>: 1 }" << std::endl;
ASSERT_EQ(out, expected.str());
}
} // namespace cvc5::internal::test
Reference in New Issue View Git Blame Copy Permalink