Line data Source code
1 : // Author(s): Jeroen Keiren 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : /// \file int_test.cpp 10 : /// \brief Basic regression test for data expressions. 11 : 12 : #define BOOST_TEST_MODULE int_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/data/standard_numbers_utility.h" 16 : 17 : using namespace mcrl2; 18 : using namespace mcrl2::data; 19 : 20 1 : void recogniser_test() 21 : { 22 2 : variable i("i", sort_int::int_()); 23 2 : application minus(sort_int::minus(i, sort_int::int_("5"))); 24 1 : application negate(sort_int::negate(i)); 25 : 26 1 : BOOST_CHECK(sort_int::is_minus_application(minus)); 27 1 : BOOST_CHECK(!sort_int::is_negate_application(minus)); 28 1 : BOOST_CHECK(sort_int::is_negate_application(negate)); 29 1 : BOOST_CHECK(!sort_int::is_minus_application(negate)); 30 1 : } 31 : 32 2 : BOOST_AUTO_TEST_CASE(test_main) 33 : { 34 1 : recogniser_test(); 35 1 : }