test/unit/test_node.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Aina Niemetz, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Common header for Node unit tests.
  14  */
  15
  16 #ifndef CVC5__TEST__UNIT__TEST_NODE_H
  17 #define CVC5__TEST__UNIT__TEST_NODE_H
  18
  19 #include "expr/node_manager.h"
  20 #include "expr/skolem_manager.h"
  21 #include "smt/solver_engine.h"
  22 #include "smt/solver_engine_scope.h"
  23 #include "test.h"
  24
  25 namespace cvc5 {
  26 namespace test {
  27
  28 class TestNode : public TestInternal
  29 {
  30  protected:
  31   void SetUp() override
  32   {
  33     d_nodeManager = NodeManager::currentNM();
  34     d_nodeManager->init();
  35     d_skolemManager = d_nodeManager->getSkolemManager();
  36     d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType()));
  37     d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2)));
  38     d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType()));
  39     d_realTypeNode.reset(new TypeNode(d_nodeManager->realType()));
  40   }
  41
  42   NodeManager* d_nodeManager;
  43   SkolemManager* d_skolemManager;
  44   std::unique_ptr<TypeNode> d_boolTypeNode;
  45   std::unique_ptr<TypeNode> d_bvTypeNode;
  46   std::unique_ptr<TypeNode> d_intTypeNode;
  47   std::unique_ptr<TypeNode> d_realTypeNode;
  48 };
  49
  50 }  // namespace test
  51 }  // namespace cvc5
  52 #endif