Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * White box testing of the Term class.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "test_api.h"
      14                 :            : 
      15                 :            : namespace cvc5::internal {
      16                 :            : 
      17                 :            : namespace test {
      18                 :            : 
      19                 :            : class TestApiWhiteTerm : public TestApi
      20                 :            : {
      21                 :            : };
      22                 :            : 
      23                 :          4 : TEST_F(TestApiWhiteTerm, getOp)
      24                 :            : {
      25                 :          1 :   Sort intsort = d_tm.getIntegerSort();
      26                 :          1 :   Sort bvsort = d_tm.mkBitVectorSort(8);
      27                 :          1 :   Sort arrsort = d_tm.mkArraySort(bvsort, intsort);
      28                 :          3 :   Sort funsort = d_tm.mkFunctionSort({intsort}, bvsort);
      29                 :            : 
      30                 :          1 :   Term x = d_tm.mkConst(intsort, "x");
      31                 :          1 :   Term a = d_tm.mkConst(arrsort, "a");
      32                 :          1 :   Term b = d_tm.mkConst(bvsort, "b");
      33                 :            : 
      34                 :          4 :   Term ab = d_tm.mkTerm(Kind::SELECT, {a, b});
      35                 :          1 :   Op ext = d_tm.mkOp(Kind::BITVECTOR_EXTRACT, {4, 0});
      36                 :          3 :   Term extb = d_tm.mkTerm(ext, {b});
      37                 :            : 
      38 [ -  + ][ +  - ]:          2 :   ASSERT_EQ(ab.getOp(), Op(d_solver->getTermManager().d_nm, Kind::SELECT));
      39                 :            :   // can compare directly to a Kind (will invoke Op constructor)
      40 [ -  + ][ +  - ]:          2 :   ASSERT_EQ(ab.getOp(), Op(d_solver->getTermManager().d_nm, Kind::SELECT));
      41                 :            : 
      42                 :          1 :   Term f = d_tm.mkConst(funsort, "f");
      43                 :          4 :   Term fx = d_tm.mkTerm(Kind::APPLY_UF, {f, x});
      44                 :            : 
      45 [ -  + ][ +  - ]:          2 :   ASSERT_EQ(fx.getOp(), Op(d_solver->getTermManager().d_nm, Kind::APPLY_UF));
      46                 :            :   // testing rebuild from op and children
      47                 :            : 
      48                 :            :   // Test Datatypes Ops
      49                 :          1 :   Sort sort = d_tm.mkParamSort("T");
      50                 :          3 :   DatatypeDecl listDecl = d_tm.mkDatatypeDecl("paramlist", {sort});
      51                 :          2 :   DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons");
      52                 :          2 :   DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil");
      53                 :          1 :   cons.addSelector("head", sort);
      54                 :          1 :   cons.addSelectorSelf("tail");
      55                 :          1 :   listDecl.addConstructor(cons);
      56                 :          1 :   listDecl.addConstructor(nil);
      57                 :          1 :   Sort listSort = d_tm.mkDatatypeSort(listDecl);
      58                 :            :   Sort intListSort =
      59                 :          3 :       listSort.instantiate(std::vector<Sort>{d_tm.getIntegerSort()});
      60                 :          1 :   Term c = d_tm.mkConst(intListSort, "c");
      61                 :          1 :   Datatype list = listSort.getDatatype();
      62                 :            :   // list datatype constructor and selector operator terms
      63                 :          2 :   Term consOpTerm = list.getConstructor("cons").getTerm();
      64                 :          2 :   Term nilOpTerm = list.getConstructor("nil").getTerm();
      65                 :          2 :   Term headOpTerm = list["cons"].getSelector("head").getTerm();
      66                 :          2 :   Term tailOpTerm = list["cons"].getSelector("tail").getTerm();
      67                 :            : 
      68                 :          3 :   Term nilTerm = d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {nilOpTerm});
      69                 :          3 :   Term consTerm = d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR,
      70                 :          2 :                               {consOpTerm, d_tm.mkInteger(0), nilTerm});
      71                 :          4 :   Term headTerm = d_tm.mkTerm(Kind::APPLY_SELECTOR, {headOpTerm, consTerm});
      72                 :          4 :   Term tailTerm = d_tm.mkTerm(Kind::APPLY_SELECTOR, {tailOpTerm, consTerm});
      73                 :            : 
      74         [ -  + ]:          2 :   ASSERT_EQ(nilTerm.getOp(),
      75         [ +  - ]:          1 :             Op(d_solver->getTermManager().d_nm, Kind::APPLY_CONSTRUCTOR));
      76         [ -  + ]:          2 :   ASSERT_EQ(consTerm.getOp(),
      77         [ +  - ]:          1 :             Op(d_solver->getTermManager().d_nm, Kind::APPLY_CONSTRUCTOR));
      78         [ -  + ]:          2 :   ASSERT_EQ(headTerm.getOp(),
      79         [ +  - ]:          1 :             Op(d_solver->getTermManager().d_nm, Kind::APPLY_SELECTOR));
      80         [ -  + ]:          2 :   ASSERT_EQ(tailTerm.getOp(),
      81         [ +  - ]:          1 :             Op(d_solver->getTermManager().d_nm, Kind::APPLY_SELECTOR));
      82 [ +  - ][ +  - ]:          1 : }
         [ +  - ][ +  - ]
         [ +  - ][ +  - ]
         [ +  - ][ +  - ]
         [ +  - ][ +  - ]
      83                 :            : }  // namespace test
      84                 :            : }  // namespace cvc5::internal