diff options
Diffstat (limited to 'test/unit/api/term_white.cpp')
-rw-r--r-- | test/unit/api/term_white.cpp | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/test/unit/api/term_white.cpp b/test/unit/api/term_white.cpp new file mode 100644 index 000000000..da1557024 --- /dev/null +++ b/test/unit/api/term_white.cpp @@ -0,0 +1,84 @@ +/********************* */ +/*! \file term_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 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.\endverbatim + ** + ** \brief White box testing of the Term class. + **/ + +#include "test_api.h" + +namespace CVC4 { + +using namespace api; + +namespace test { + +class TestApiWhiteTerm : public TestApi +{ +}; + +TEST_F(TestApiWhiteTerm, getOp) +{ + Sort intsort = d_solver.getIntegerSort(); + Sort bvsort = d_solver.mkBitVectorSort(8); + Sort arrsort = d_solver.mkArraySort(bvsort, intsort); + Sort funsort = d_solver.mkFunctionSort(intsort, bvsort); + + Term x = d_solver.mkConst(intsort, "x"); + Term a = d_solver.mkConst(arrsort, "a"); + Term b = d_solver.mkConst(bvsort, "b"); + + Term ab = d_solver.mkTerm(SELECT, a, b); + Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + Term extb = d_solver.mkTerm(ext, b); + + ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT)); + // can compare directly to a Kind (will invoke Op constructor) + ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT)); + + Term f = d_solver.mkConst(funsort, "f"); + Term fx = d_solver.mkTerm(APPLY_UF, f, x); + + ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF)); + // testing rebuild from op and children + + // Test Datatypes Ops + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + cons.addSelector("head", sort); + cons.addSelectorSelf("tail"); + listDecl.addConstructor(cons); + listDecl.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(listDecl); + Sort intListSort = + listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}); + Term c = d_solver.mkConst(intListSort, "c"); + Datatype list = listSort.getDatatype(); + // list datatype constructor and selector operator terms + Term consOpTerm = list.getConstructorTerm("cons"); + Term nilOpTerm = list.getConstructorTerm("nil"); + Term headOpTerm = list["cons"].getSelectorTerm("head"); + Term tailOpTerm = list["cons"].getSelectorTerm("tail"); + + Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm); + Term consTerm = d_solver.mkTerm( + APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm); + Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm); + Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm); + + ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); + ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); + ASSERT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); + ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); +} +} // namespace test +} // namespace CVC4 |