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 : : * Black box testing of cvc5::KindMap. 11 : : */ 12 : : 13 : : #include <iostream> 14 : : #include <sstream> 15 : : #include <string> 16 : : 17 : : #include "expr/kind_map.h" 18 : : #include "test.h" 19 : : 20 : : namespace cvc5::internal { 21 : : 22 : : using namespace internal; 23 : : using namespace internal::kind; 24 : : 25 : : namespace test { 26 : : 27 : : class TestNodeBlackKindMap : public TestInternal 28 : : { 29 : : }; 30 : : 31 : 4 : TEST_F(TestNodeBlackKindMap, simple) 32 : : { 33 [ + + ]: 5 : KindMap map; 34 [ - + ][ + - ]: 1 : ASSERT_FALSE(map.test(Kind::AND)); 35 : 1 : map.set(Kind::AND); 36 [ - + ][ + - ]: 1 : ASSERT_TRUE(map.test(Kind::AND)); 37 : 1 : map.reset(Kind::AND); 38 [ - + ][ + - ]: 1 : ASSERT_FALSE(map.test(Kind::AND)); 39 : : #ifdef CVC5_ASSERTIONS 40 : 1 : ASSERT_THROW(map.set(Kind::LAST_KIND), AssertArgumentException); 41 : : #endif 42 : : } 43 : : 44 : : } // namespace test 45 : : } // namespace cvc5::internal