From: Aina Niemetz Date: Wed, 24 Feb 2021 10:39:00 +0000 (-0800) Subject: google test: theory: Migrate logic_info_white. (#5973) X-Git-Tag: cvc5-1.0.0~2224 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f642cb7bc300b42c6e6b930ce02ee6bbe356c86;p=cvc5.git google test: theory: Migrate logic_info_white. (#5973) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 37ae06bdf..4ee9b2fc9 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -11,7 +11,7 @@ cvc4_add_unit_test_black(regexp_operation_black theory) cvc4_add_cxx_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) -cvc4_add_cxx_unit_test_white(logic_info_white theory) +cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory) cvc4_add_unit_test_white(strings_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp new file mode 100644 index 000000000..7ffbd6d2a --- /dev/null +++ b/test/unit/theory/logic_info_white.cpp @@ -0,0 +1,1374 @@ +/********************* */ +/*! \file logic_info_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Unit testing for CVC4::LogicInfo class + ** + ** Unit testing for CVC4::LogicInfo class. + **/ + +#include "base/configuration.h" +#include "expr/kind.h" +#include "test.h" +#include "theory/logic_info.h" + +namespace CVC4 { + +using namespace theory; + +namespace test { + +class TestTheoryWhiteLogicInfo : public TestInternal +{ +#warning \ + "This test is of questionable compatiblity with contrib/new-theory. Is the new theory id handled correctly by the Logic info." + protected: + void eq(const LogicInfo& logic1, const LogicInfo& logic2) const + { + std::cout << "asserting that " << logic1 << " == " << logic2 << std::endl; + + ASSERT_TRUE(logic1 == logic2); + ASSERT_FALSE((logic1 != logic2)); + ASSERT_FALSE((logic1 < logic2)); + ASSERT_FALSE((logic1 > logic2)); + ASSERT_TRUE(logic1 <= logic2); + ASSERT_TRUE(logic1 >= logic2); + ASSERT_TRUE(logic1.isComparableTo(logic2)); + + ASSERT_TRUE(logic2 == logic1); + ASSERT_FALSE((logic2 != logic1)); + ASSERT_FALSE((logic2 < logic1)); + ASSERT_FALSE((logic2 > logic1)); + ASSERT_TRUE(logic2 <= logic1); + ASSERT_TRUE(logic2 >= logic1); + ASSERT_TRUE(logic2.isComparableTo(logic1)); + } + + void nc(const LogicInfo& logic1, const LogicInfo& logic2) const + { + std::cout << "asserting that " << logic1 << " is-not-comparable-to " + << logic2 << std::endl; + ASSERT_FALSE((logic1 == logic2)); + ASSERT_TRUE(logic1 != logic2); + ASSERT_FALSE((logic1 < logic2)); + ASSERT_FALSE((logic1 > logic2)); + ASSERT_FALSE((logic1 <= logic2)); + ASSERT_FALSE((logic1 >= logic2)); + ASSERT_FALSE(logic1.isComparableTo(logic2)); + + ASSERT_FALSE((logic2 == logic1)); + ASSERT_TRUE(logic2 != logic1); + ASSERT_FALSE((logic2 < logic1)); + ASSERT_FALSE((logic2 > logic1)); + ASSERT_FALSE((logic2 <= logic1)); + ASSERT_FALSE((logic2 >= logic1)); + ASSERT_FALSE(logic2.isComparableTo(logic1)); + } + + void lt(const LogicInfo& logic1, const LogicInfo& logic2) const + { + std::cout << "asserting that " << logic1 << " < " << logic2 << std::endl; + + ASSERT_FALSE((logic1 == logic2)); + ASSERT_TRUE(logic1 != logic2); + ASSERT_TRUE(logic1 < logic2); + ASSERT_FALSE((logic1 > logic2)); + ASSERT_TRUE(logic1 <= logic2); + ASSERT_FALSE((logic1 >= logic2)); + ASSERT_TRUE(logic1.isComparableTo(logic2)); + + ASSERT_FALSE((logic2 == logic1)); + ASSERT_TRUE(logic2 != logic1); + ASSERT_FALSE((logic2 < logic1)); + ASSERT_TRUE(logic2 > logic1); + ASSERT_FALSE((logic2 <= logic1)); + ASSERT_TRUE(logic2 >= logic1); + ASSERT_TRUE(logic2.isComparableTo(logic1)); + } + + void gt(const LogicInfo& logic1, const LogicInfo& logic2) const + { + std::cout << "asserting that " << logic1 << " > " << logic2 << std::endl; + + ASSERT_FALSE((logic1 == logic2)); + ASSERT_TRUE(logic1 != logic2); + ASSERT_FALSE((logic1 < logic2)); + ASSERT_TRUE(logic1 > logic2); + ASSERT_FALSE((logic1 <= logic2)); + ASSERT_TRUE(logic1 >= logic2); + ASSERT_TRUE(logic1.isComparableTo(logic2)); + + ASSERT_FALSE((logic2 == logic1)); + ASSERT_TRUE(logic2 != logic1); + ASSERT_TRUE(logic2 < logic1); + ASSERT_FALSE((logic2 > logic1)); + ASSERT_TRUE(logic2 <= logic1); + ASSERT_FALSE((logic2 >= logic1)); + ASSERT_TRUE(logic2.isComparableTo(logic1)); + } +}; + +TEST_F(TestTheoryWhiteLogicInfo, smtlib_logics) +{ + LogicInfo info("QF_SAT"); + ASSERT_TRUE(info.isLocked()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_TRUE(info.isPure(THEORY_BOOL)); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_TRUE(info.hasNothing()); + + info = LogicInfo("AUFLIA"); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_FALSE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("AUFLIRA"); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("AUFNIRA"); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isLinear()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("LRA"); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_TRUE(info.isQuantified()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_FALSE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_ABV"); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_AUFBV"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_AUFLIA"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_FALSE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_AX"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_BV"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_IDL"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_TRUE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_LIA"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_LRA"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_FALSE(info.areIntegersUsed()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_NIA"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_FALSE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_NRA"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_FALSE(info.areIntegersUsed()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_RDL"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_TRUE(info.isDifferenceLogic()); + ASSERT_FALSE(info.areIntegersUsed()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_UF"); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_FALSE(info.isQuantified()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_TRUE(info.isPure(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_UFBV"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_UFIDL"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_TRUE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.areRealsUsed()); + ASSERT_FALSE(info.areTranscendentalsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_UFLIA"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.areRealsUsed()); + ASSERT_FALSE(info.areTranscendentalsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_UFLRA"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_FALSE(info.areIntegersUsed()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.areTranscendentalsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_UFNRA"); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_FALSE(info.areIntegersUsed()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.areTranscendentalsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("UFLRA"); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_FALSE(info.areIntegersUsed()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_FALSE(info.areTranscendentalsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("UFNIA"); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isLinear()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.areRealsUsed()); + ASSERT_FALSE(info.areTranscendentalsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("QF_ALL_SUPPORTED"); + ASSERT_TRUE(info.isLocked()); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isLinear()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_TRUE(info.areTranscendentalsUsed()); + ASSERT_FALSE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); + + info = LogicInfo("ALL_SUPPORTED"); + ASSERT_TRUE(info.isLocked()); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isLinear()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_TRUE(info.hasEverything()); + ASSERT_FALSE(info.hasNothing()); +} + +TEST_F(TestTheoryWhiteLogicInfo, default_logic) +{ + LogicInfo info; + ASSERT_FALSE(info.isLocked()); + + ASSERT_THROW(info.getLogicString(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_BUILTIN), + CVC4::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_BOOL), + CVC4::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_UF), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_ARITH), + CVC4::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_ARRAYS), + CVC4::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_BV), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_DATATYPES), + CVC4::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_QUANTIFIERS), + CVC4::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BUILTIN), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BOOL), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_UF), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_ARITH), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_ARRAYS), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BV), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_DATATYPES), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_QUANTIFIERS), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isQuantified(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.areIntegersUsed(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.areRealsUsed(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.isLinear(), CVC4::IllegalArgumentException); + + info.lock(); + ASSERT_TRUE(info.isLocked()); + ASSERT_EQ(info.getLogicString(), "ALL"); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BUILTIN)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_QUANTIFIERS)); + ASSERT_FALSE(info.isPure(THEORY_BUILTIN)); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_FALSE(info.isPure(THEORY_UF)); + ASSERT_FALSE(info.isPure(THEORY_ARITH)); + ASSERT_FALSE(info.isPure(THEORY_ARRAYS)); + ASSERT_FALSE(info.isPure(THEORY_BV)); + ASSERT_FALSE(info.isPure(THEORY_DATATYPES)); + ASSERT_FALSE(info.isPure(THEORY_QUANTIFIERS)); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_TRUE(info.areTranscendentalsUsed()); + ASSERT_FALSE(info.isLinear()); + + ASSERT_THROW(info.arithOnlyLinear(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.disableIntegers(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.disableQuantifiers(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException); + ASSERT_THROW(info.disableTheory(THEORY_DATATYPES), + CVC4::IllegalArgumentException); + ASSERT_THROW(info.enableIntegers(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.disableReals(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.disableTheory(THEORY_ARITH), + CVC4::IllegalArgumentException); + ASSERT_THROW(info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException); + info = info.getUnlockedCopy(); + ASSERT_FALSE(info.isLocked()); + info.disableTheory(THEORY_STRINGS); + info.disableTheory(THEORY_SETS); + info.disableTheory(THEORY_BAGS); + info.arithOnlyLinear(); + info.disableIntegers(); + info.lock(); + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA"); + } + else + { + ASSERT_EQ(info.getLogicString(), "SEP_AUFBVDTLRA"); + } + + info = info.getUnlockedCopy(); + ASSERT_FALSE(info.isLocked()); + info.disableQuantifiers(); + info.disableTheory(THEORY_BAGS); + info.lock(); + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); + } + else + { + ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVDTLRA"); + } + + info = info.getUnlockedCopy(); + ASSERT_FALSE(info.isLocked()); + info.disableTheory(THEORY_BV); + info.disableTheory(THEORY_DATATYPES); + info.disableTheory(THEORY_BAGS); + info.enableIntegers(); + info.disableReals(); + info.lock(); + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA"); + } + else + { + ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFLIA"); + } + + info = info.getUnlockedCopy(); + ASSERT_FALSE(info.isLocked()); + info.disableTheory(THEORY_ARITH); + info.disableTheory(THEORY_UF); + info.disableTheory(THEORY_FP); + info.disableTheory(THEORY_SEP); + info.disableTheory(THEORY_BAGS); + info.lock(); + ASSERT_EQ(info.getLogicString(), "QF_AX"); + ASSERT_TRUE(info.isPure(THEORY_ARRAYS)); + ASSERT_FALSE(info.isQuantified()); + // check all-excluded logic + info = info.getUnlockedCopy(); + ASSERT_FALSE(info.isLocked()); + info.disableEverything(); + info.lock(); + ASSERT_TRUE(info.isLocked()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isPure(THEORY_BOOL)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_THROW(info.isLinear(), IllegalArgumentException); + ASSERT_THROW(info.areIntegersUsed(), IllegalArgumentException); + ASSERT_THROW(info.isDifferenceLogic(), IllegalArgumentException); + ASSERT_THROW(info.areRealsUsed(), IllegalArgumentException); + ASSERT_THROW(info.areTranscendentalsUsed(), IllegalArgumentException); + + // check copy is unchanged + info = info.getUnlockedCopy(); + ASSERT_FALSE(info.isLocked()); + info.lock(); + ASSERT_TRUE(info.isLocked()); + ASSERT_FALSE(info.isSharingEnabled()); + ASSERT_FALSE(info.isQuantified()); + ASSERT_TRUE(info.isPure(THEORY_BOOL)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_FALSE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_THROW(info.isLinear(), IllegalArgumentException); + ASSERT_THROW(info.areIntegersUsed(), IllegalArgumentException); + ASSERT_THROW(info.isDifferenceLogic(), IllegalArgumentException); + ASSERT_THROW(info.areRealsUsed(), IllegalArgumentException); + ASSERT_THROW(info.areTranscendentalsUsed(), IllegalArgumentException); + + // check all-included logic + info = info.getUnlockedCopy(); + ASSERT_FALSE(info.isLocked()); + info.enableEverything(); + info.lock(); + ASSERT_TRUE(info.isLocked()); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isLinear()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_TRUE(info.areTranscendentalsUsed()); + + // check copy is unchanged + info = info.getUnlockedCopy(); + ASSERT_FALSE(info.isLocked()); + info.lock(); + ASSERT_TRUE(info.isLocked()); + ASSERT_FALSE(info.isPure(THEORY_BOOL)); + ASSERT_TRUE(info.isSharingEnabled()); + ASSERT_TRUE(info.isQuantified()); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARRAYS)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_UF)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_ARITH)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BV)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_DATATYPES)); + ASSERT_TRUE(info.isTheoryEnabled(THEORY_BOOL)); + ASSERT_FALSE(info.isLinear()); + ASSERT_TRUE(info.areIntegersUsed()); + ASSERT_FALSE(info.isDifferenceLogic()); + ASSERT_TRUE(info.areRealsUsed()); + ASSERT_TRUE(info.areTranscendentalsUsed()); +} + +TEST_F(TestTheoryWhiteLogicInfo, comparison) +{ + LogicInfo ufHo = LogicInfo("QF_UF").getUnlockedCopy(); + ufHo.enableHigherOrder(); + ufHo.lock(); + + eq("QF_UF", "QF_UF"); + nc("QF_UF", "QF_LRA"); + nc("QF_UF", "QF_LIA"); + lt("QF_UF", "QF_UFLRA"); + lt("QF_UF", "QF_UFLIA"); + lt("QF_UF", "QF_AUFLIA"); + lt("QF_UF", "QF_AUFLIRA"); + nc("QF_UF", "QF_BV"); + nc("QF_UF", "QF_ABV"); + lt("QF_UF", "QF_AUFBV"); + nc("QF_UF", "QF_IDL"); + nc("QF_UF", "QF_RDL"); + lt("QF_UF", "QF_UFIDL"); + nc("QF_UF", "QF_NIA"); + nc("QF_UF", "QF_NRA"); + lt("QF_UF", "QF_AUFNIRA"); + nc("QF_UF", "LRA"); + nc("QF_UF", "NRA"); + nc("QF_UF", "NIA"); + lt("QF_UF", "UFLRA"); + lt("QF_UF", "UFNIA"); + lt("QF_UF", "AUFLIA"); + lt("QF_UF", "AUFLIRA"); + lt("QF_UF", "AUFNIRA"); + lt("QF_UF", "QF_UFC"); + lt("QF_UF", ufHo); + nc("QF_UFC", ufHo); + + nc("QF_LRA", "QF_UF"); + eq("QF_LRA", "QF_LRA"); + nc("QF_LRA", "QF_LIA"); + lt("QF_LRA", "QF_UFLRA"); + nc("QF_LRA", "QF_UFLIA"); + nc("QF_LRA", "QF_AUFLIA"); + lt("QF_LRA", "QF_AUFLIRA"); + nc("QF_LRA", "QF_BV"); + nc("QF_LRA", "QF_ABV"); + nc("QF_LRA", "QF_AUFBV"); + nc("QF_LRA", "QF_IDL"); + gt("QF_LRA", "QF_RDL"); + nc("QF_LRA", "QF_UFIDL"); + nc("QF_LRA", "QF_NIA"); + lt("QF_LRA", "QF_NRA"); + lt("QF_LRA", "QF_AUFNIRA"); + lt("QF_LRA", "LRA"); + lt("QF_LRA", "NRA"); + nc("QF_LRA", "NIA"); + lt("QF_LRA", "UFLRA"); + nc("QF_LRA", "UFNIA"); + nc("QF_LRA", "AUFLIA"); + lt("QF_LRA", "AUFLIRA"); + lt("QF_LRA", "AUFNIRA"); + lt("QF_LRA", "QF_UFCLRA"); + + nc("QF_LIA", "QF_UF"); + nc("QF_LIA", "QF_LRA"); + eq("QF_LIA", "QF_LIA"); + nc("QF_LIA", "QF_UFLRA"); + lt("QF_LIA", "QF_UFLIA"); + lt("QF_LIA", "QF_AUFLIA"); + lt("QF_LIA", "QF_AUFLIRA"); + nc("QF_LIA", "QF_BV"); + nc("QF_LIA", "QF_ABV"); + nc("QF_LIA", "QF_AUFBV"); + gt("QF_LIA", "QF_IDL"); + nc("QF_LIA", "QF_RDL"); + nc("QF_LIA", "QF_UFIDL"); + lt("QF_LIA", "QF_NIA"); + nc("QF_LIA", "QF_NRA"); + lt("QF_LIA", "QF_AUFNIRA"); + nc("QF_LIA", "LRA"); + nc("QF_LIA", "NRA"); + lt("QF_LIA", "NIA"); + nc("QF_LIA", "UFLRA"); + lt("QF_LIA", "UFNIA"); + lt("QF_LIA", "AUFLIA"); + lt("QF_LIA", "AUFLIRA"); + lt("QF_LIA", "AUFNIRA"); + + gt("QF_UFLRA", "QF_UF"); + gt("QF_UFLRA", "QF_LRA"); + nc("QF_UFLRA", "QF_LIA"); + eq("QF_UFLRA", "QF_UFLRA"); + nc("QF_UFLRA", "QF_UFLIA"); + nc("QF_UFLRA", "QF_AUFLIA"); + lt("QF_UFLRA", "QF_AUFLIRA"); + nc("QF_UFLRA", "QF_BV"); + nc("QF_UFLRA", "QF_ABV"); + nc("QF_UFLRA", "QF_AUFBV"); + nc("QF_UFLRA", "QF_IDL"); + gt("QF_UFLRA", "QF_RDL"); + nc("QF_UFLRA", "QF_UFIDL"); + nc("QF_UFLRA", "QF_NIA"); + nc("QF_UFLRA", "QF_NRA"); + lt("QF_UFLRA", "QF_AUFNIRA"); + nc("QF_UFLRA", "LRA"); + nc("QF_UFLRA", "NRA"); + nc("QF_UFLRA", "NIA"); + lt("QF_UFLRA", "UFLRA"); + nc("QF_UFLRA", "UFNIA"); + nc("QF_UFLRA", "AUFLIA"); + lt("QF_UFLRA", "AUFLIRA"); + lt("QF_UFLRA", "AUFNIRA"); + + gt("QF_UFLIA", "QF_UF"); + nc("QF_UFLIA", "QF_LRA"); + gt("QF_UFLIA", "QF_LIA"); + nc("QF_UFLIA", "QF_UFLRA"); + eq("QF_UFLIA", "QF_UFLIA"); + lt("QF_UFLIA", "QF_AUFLIA"); + lt("QF_UFLIA", "QF_AUFLIRA"); + nc("QF_UFLIA", "QF_BV"); + nc("QF_UFLIA", "QF_ABV"); + nc("QF_UFLIA", "QF_AUFBV"); + gt("QF_UFLIA", "QF_IDL"); + nc("QF_UFLIA", "QF_RDL"); + gt("QF_UFLIA", "QF_UFIDL"); + nc("QF_UFLIA", "QF_NIA"); + nc("QF_UFLIA", "QF_NRA"); + lt("QF_UFLIA", "QF_AUFNIRA"); + nc("QF_UFLIA", "LRA"); + nc("QF_UFLIA", "NRA"); + nc("QF_UFLIA", "NIA"); + nc("QF_UFLIA", "UFLRA"); + lt("QF_UFLIA", "UFNIA"); + lt("QF_UFLIA", "AUFLIA"); + lt("QF_UFLIA", "AUFLIRA"); + lt("QF_UFLIA", "AUFNIRA"); + + gt("QF_AUFLIA", "QF_UF"); + nc("QF_AUFLIA", "QF_LRA"); + gt("QF_AUFLIA", "QF_LIA"); + nc("QF_AUFLIA", "QF_UFLRA"); + gt("QF_AUFLIA", "QF_UFLIA"); + eq("QF_AUFLIA", "QF_AUFLIA"); + lt("QF_AUFLIA", "QF_AUFLIRA"); + nc("QF_AUFLIA", "QF_BV"); + nc("QF_AUFLIA", "QF_ABV"); + nc("QF_AUFLIA", "QF_AUFBV"); + gt("QF_AUFLIA", "QF_IDL"); + nc("QF_AUFLIA", "QF_RDL"); + gt("QF_AUFLIA", "QF_UFIDL"); + nc("QF_AUFLIA", "QF_NIA"); + nc("QF_AUFLIA", "QF_NRA"); + lt("QF_AUFLIA", "QF_AUFNIRA"); + nc("QF_AUFLIA", "LRA"); + nc("QF_AUFLIA", "NRA"); + nc("QF_AUFLIA", "NIA"); + nc("QF_AUFLIA", "UFLRA"); + nc("QF_AUFLIA", "UFNIA"); + lt("QF_AUFLIA", "AUFLIA"); + lt("QF_AUFLIA", "AUFLIRA"); + lt("QF_AUFLIA", "AUFNIRA"); + + gt("QF_AUFLIRA", "QF_UF"); + gt("QF_AUFLIRA", "QF_LRA"); + gt("QF_AUFLIRA", "QF_LIA"); + gt("QF_AUFLIRA", "QF_UFLRA"); + gt("QF_AUFLIRA", "QF_UFLIA"); + gt("QF_AUFLIRA", "QF_AUFLIA"); + eq("QF_AUFLIRA", "QF_AUFLIRA"); + nc("QF_AUFLIRA", "QF_BV"); + nc("QF_AUFLIRA", "QF_ABV"); + nc("QF_AUFLIRA", "QF_AUFBV"); + gt("QF_AUFLIRA", "QF_IDL"); + gt("QF_AUFLIRA", "QF_RDL"); + gt("QF_AUFLIRA", "QF_UFIDL"); + nc("QF_AUFLIRA", "QF_NIA"); + nc("QF_AUFLIRA", "QF_NRA"); + lt("QF_AUFLIRA", "QF_AUFNIRA"); + nc("QF_AUFLIRA", "LRA"); + nc("QF_AUFLIRA", "NRA"); + nc("QF_AUFLIRA", "NIA"); + nc("QF_AUFLIRA", "UFLRA"); + nc("QF_AUFLIRA", "UFNIA"); + nc("QF_AUFLIRA", "AUFLIA"); + lt("QF_AUFLIRA", "AUFLIRA"); + lt("QF_AUFLIRA", "AUFNIRA"); + + nc("QF_BV", "QF_UF"); + nc("QF_BV", "QF_LRA"); + nc("QF_BV", "QF_LIA"); + nc("QF_BV", "QF_UFLRA"); + nc("QF_BV", "QF_UFLIA"); + nc("QF_BV", "QF_AUFLIA"); + nc("QF_BV", "QF_AUFLIRA"); + eq("QF_BV", "QF_BV"); + lt("QF_BV", "QF_ABV"); + lt("QF_BV", "QF_AUFBV"); + nc("QF_BV", "QF_IDL"); + nc("QF_BV", "QF_RDL"); + nc("QF_BV", "QF_UFIDL"); + nc("QF_BV", "QF_NIA"); + nc("QF_BV", "QF_NRA"); + nc("QF_BV", "QF_AUFNIRA"); + nc("QF_BV", "LRA"); + nc("QF_BV", "NRA"); + nc("QF_BV", "NIA"); + nc("QF_BV", "UFLRA"); + nc("QF_BV", "UFNIA"); + nc("QF_BV", "AUFLIA"); + nc("QF_BV", "AUFLIRA"); + nc("QF_BV", "AUFNIRA"); + + nc("QF_ABV", "QF_UF"); + nc("QF_ABV", "QF_LRA"); + nc("QF_ABV", "QF_LIA"); + nc("QF_ABV", "QF_UFLRA"); + nc("QF_ABV", "QF_UFLIA"); + nc("QF_ABV", "QF_AUFLIA"); + nc("QF_ABV", "QF_AUFLIRA"); + gt("QF_ABV", "QF_BV"); + eq("QF_ABV", "QF_ABV"); + lt("QF_ABV", "QF_AUFBV"); + nc("QF_ABV", "QF_IDL"); + nc("QF_ABV", "QF_RDL"); + nc("QF_ABV", "QF_UFIDL"); + nc("QF_ABV", "QF_NIA"); + nc("QF_ABV", "QF_NRA"); + nc("QF_ABV", "QF_AUFNIRA"); + nc("QF_ABV", "LRA"); + nc("QF_ABV", "NRA"); + nc("QF_ABV", "NIA"); + nc("QF_ABV", "UFLRA"); + nc("QF_ABV", "UFNIA"); + nc("QF_ABV", "AUFLIA"); + nc("QF_ABV", "AUFLIRA"); + nc("QF_ABV", "AUFNIRA"); + + gt("QF_AUFBV", "QF_UF"); + nc("QF_AUFBV", "QF_LRA"); + nc("QF_AUFBV", "QF_LIA"); + nc("QF_AUFBV", "QF_UFLRA"); + nc("QF_AUFBV", "QF_UFLIA"); + nc("QF_AUFBV", "QF_AUFLIA"); + nc("QF_AUFBV", "QF_AUFLIRA"); + gt("QF_AUFBV", "QF_BV"); + gt("QF_AUFBV", "QF_ABV"); + eq("QF_AUFBV", "QF_AUFBV"); + nc("QF_AUFBV", "QF_IDL"); + nc("QF_AUFBV", "QF_RDL"); + nc("QF_AUFBV", "QF_UFIDL"); + nc("QF_AUFBV", "QF_NIA"); + nc("QF_AUFBV", "QF_NRA"); + nc("QF_AUFBV", "QF_AUFNIRA"); + nc("QF_AUFBV", "LRA"); + nc("QF_AUFBV", "NRA"); + nc("QF_AUFBV", "NIA"); + nc("QF_AUFBV", "UFLRA"); + nc("QF_AUFBV", "UFNIA"); + nc("QF_AUFBV", "AUFLIA"); + nc("QF_AUFBV", "AUFLIRA"); + nc("QF_AUFBV", "AUFNIRA"); + + nc("QF_IDL", "QF_UF"); + nc("QF_IDL", "QF_LRA"); + lt("QF_IDL", "QF_LIA"); + nc("QF_IDL", "QF_UFLRA"); + lt("QF_IDL", "QF_UFLIA"); + lt("QF_IDL", "QF_AUFLIA"); + lt("QF_IDL", "QF_AUFLIRA"); + nc("QF_IDL", "QF_BV"); + nc("QF_IDL", "QF_ABV"); + nc("QF_IDL", "QF_AUFBV"); + eq("QF_IDL", "QF_IDL"); + nc("QF_IDL", "QF_RDL"); + lt("QF_IDL", "QF_UFIDL"); + lt("QF_IDL", "QF_NIA"); + nc("QF_IDL", "QF_NRA"); + nc("QF_IDL", "QF_NRAT"); + lt("QF_IDL", "QF_AUFNIRA"); + nc("QF_IDL", "LRA"); + nc("QF_IDL", "NRA"); + lt("QF_IDL", "NIA"); + nc("QF_IDL", "UFLRA"); + lt("QF_IDL", "UFNIA"); + lt("QF_IDL", "AUFLIA"); + lt("QF_IDL", "AUFLIRA"); + lt("QF_IDL", "AUFNIRA"); + + nc("QF_RDL", "QF_UF"); + lt("QF_RDL", "QF_LRA"); + nc("QF_RDL", "QF_LIA"); + lt("QF_RDL", "QF_UFLRA"); + nc("QF_RDL", "QF_UFLIA"); + nc("QF_RDL", "QF_AUFLIA"); + lt("QF_RDL", "QF_AUFLIRA"); + nc("QF_RDL", "QF_BV"); + nc("QF_RDL", "QF_ABV"); + nc("QF_RDL", "QF_AUFBV"); + nc("QF_RDL", "QF_IDL"); + eq("QF_RDL", "QF_RDL"); + nc("QF_RDL", "QF_UFIDL"); + nc("QF_RDL", "QF_NIA"); + lt("QF_RDL", "QF_NRA"); + lt("QF_RDL", "QF_AUFNIRA"); + lt("QF_RDL", "LRA"); + lt("QF_RDL", "NRA"); + nc("QF_RDL", "NIA"); + lt("QF_RDL", "UFLRA"); + nc("QF_RDL", "UFNIA"); + nc("QF_RDL", "AUFLIA"); + lt("QF_RDL", "AUFLIRA"); + lt("QF_RDL", "AUFNIRA"); + + gt("QF_UFIDL", "QF_UF"); + nc("QF_UFIDL", "QF_LRA"); + nc("QF_UFIDL", "QF_LIA"); + nc("QF_UFIDL", "QF_UFLRA"); + lt("QF_UFIDL", "QF_UFLIA"); + lt("QF_UFIDL", "QF_AUFLIA"); + lt("QF_UFIDL", "QF_AUFLIRA"); + nc("QF_UFIDL", "QF_BV"); + nc("QF_UFIDL", "QF_ABV"); + nc("QF_UFIDL", "QF_AUFBV"); + gt("QF_UFIDL", "QF_IDL"); + nc("QF_UFIDL", "QF_RDL"); + eq("QF_UFIDL", "QF_UFIDL"); + nc("QF_UFIDL", "QF_NIA"); + nc("QF_UFIDL", "QF_NRA"); + lt("QF_UFIDL", "QF_AUFNIRA"); + nc("QF_UFIDL", "LRA"); + nc("QF_UFIDL", "NRA"); + nc("QF_UFIDL", "NIA"); + nc("QF_UFIDL", "UFLRA"); + lt("QF_UFIDL", "UFNIA"); + lt("QF_UFIDL", "AUFLIA"); + lt("QF_UFIDL", "AUFLIRA"); + lt("QF_UFIDL", "AUFNIRA"); + + nc("QF_NIA", "QF_UF"); + nc("QF_NIA", "QF_LRA"); + gt("QF_NIA", "QF_LIA"); + nc("QF_NIA", "QF_UFLRA"); + nc("QF_NIA", "QF_UFLIA"); + nc("QF_NIA", "QF_AUFLIA"); + nc("QF_NIA", "QF_AUFLIRA"); + nc("QF_NIA", "QF_BV"); + nc("QF_NIA", "QF_ABV"); + nc("QF_NIA", "QF_AUFBV"); + gt("QF_NIA", "QF_IDL"); + nc("QF_NIA", "QF_RDL"); + nc("QF_NIA", "QF_UFIDL"); + eq("QF_NIA", "QF_NIA"); + nc("QF_NIA", "QF_NRA"); + lt("QF_NIA", "QF_AUFNIRA"); + nc("QF_NIA", "LRA"); + nc("QF_NIA", "NRA"); + lt("QF_NIA", "NIA"); + nc("QF_NIA", "UFLRA"); + lt("QF_NIA", "UFNIA"); + nc("QF_NIA", "AUFLIA"); + nc("QF_NIA", "AUFLIRA"); + lt("QF_NIA", "AUFNIRA"); + + nc("QF_NRA", "QF_UF"); + gt("QF_NRA", "QF_LRA"); + nc("QF_NRA", "QF_LIA"); + nc("QF_NRA", "QF_UFLRA"); + nc("QF_NRA", "QF_UFLIA"); + nc("QF_NRA", "QF_AUFLIA"); + nc("QF_NRA", "QF_AUFLIRA"); + nc("QF_NRA", "QF_BV"); + nc("QF_NRA", "QF_ABV"); + nc("QF_NRA", "QF_AUFBV"); + nc("QF_NRA", "QF_IDL"); + gt("QF_NRA", "QF_RDL"); + nc("QF_NRA", "QF_UFIDL"); + nc("QF_NRA", "QF_NIA"); + eq("QF_NRA", "QF_NRA"); + lt("QF_NRA", "QF_AUFNIRA"); + nc("QF_NRA", "LRA"); + lt("QF_NRA", "NRA"); + nc("QF_NRA", "NIA"); + nc("QF_NRA", "UFLRA"); + nc("QF_NRA", "UFNIA"); + nc("QF_NRA", "AUFLIA"); + nc("QF_NRA", "AUFLIRA"); + lt("QF_NRA", "AUFNIRA"); + lt("QF_NRA", "QF_NRAT"); + + gt("QF_AUFNIRA", "QF_UF"); + gt("QF_AUFNIRA", "QF_LRA"); + gt("QF_AUFNIRA", "QF_LIA"); + gt("QF_AUFNIRA", "QF_UFLRA"); + gt("QF_AUFNIRA", "QF_UFLIA"); + gt("QF_AUFNIRA", "QF_AUFLIA"); + gt("QF_AUFNIRA", "QF_AUFLIRA"); + nc("QF_AUFNIRA", "QF_BV"); + nc("QF_AUFNIRA", "QF_ABV"); + nc("QF_AUFNIRA", "QF_AUFBV"); + gt("QF_AUFNIRA", "QF_IDL"); + gt("QF_AUFNIRA", "QF_RDL"); + gt("QF_AUFNIRA", "QF_UFIDL"); + gt("QF_AUFNIRA", "QF_NIA"); + gt("QF_AUFNIRA", "QF_NRA"); + eq("QF_AUFNIRA", "QF_AUFNIRA"); + nc("QF_AUFNIRA", "LRA"); + nc("QF_AUFNIRA", "NRA"); + nc("QF_AUFNIRA", "NIA"); + nc("QF_AUFNIRA", "UFLRA"); + nc("QF_AUFNIRA", "UFNIA"); + nc("QF_AUFNIRA", "AUFLIA"); + nc("QF_AUFNIRA", "AUFLIRA"); + lt("QF_AUFNIRA", "AUFNIRA"); + lt("QF_AUFNIRA", "QF_AUFNIRAT"); + + nc("LRA", "QF_UF"); + gt("LRA", "QF_LRA"); + nc("LRA", "QF_LIA"); + nc("LRA", "QF_UFLRA"); + nc("LRA", "QF_UFLIA"); + nc("LRA", "QF_AUFLIA"); + nc("LRA", "QF_AUFLIRA"); + nc("LRA", "QF_BV"); + nc("LRA", "QF_ABV"); + nc("LRA", "QF_AUFBV"); + nc("LRA", "QF_IDL"); + gt("LRA", "QF_RDL"); + nc("LRA", "QF_UFIDL"); + nc("LRA", "QF_NIA"); + nc("LRA", "QF_NRA"); + nc("LRA", "QF_AUFNIRA"); + eq("LRA", "LRA"); + lt("LRA", "NRA"); + nc("LRA", "NIA"); + lt("LRA", "UFLRA"); + nc("LRA", "UFNIA"); + nc("LRA", "AUFLIA"); + lt("LRA", "AUFLIRA"); + lt("LRA", "AUFNIRA"); + + nc("NRA", "QF_UF"); + gt("NRA", "QF_LRA"); + nc("NRA", "QF_LIA"); + nc("NRA", "QF_UFLRA"); + nc("NRA", "QF_UFLIA"); + nc("NRA", "QF_AUFLIA"); + nc("NRA", "QF_AUFLIRA"); + nc("NRA", "QF_BV"); + nc("NRA", "QF_ABV"); + nc("NRA", "QF_AUFBV"); + nc("NRA", "QF_IDL"); + gt("NRA", "QF_RDL"); + nc("NRA", "QF_UFIDL"); + nc("NRA", "QF_NIA"); + gt("NRA", "QF_NRA"); + nc("NRA", "QF_AUFNIRA"); + gt("NRA", "LRA"); + eq("NRA", "NRA"); + nc("NRA", "NIA"); + nc("NRA", "UFLRA"); + nc("NRA", "UFNIA"); + nc("NRA", "AUFLIA"); + nc("NRA", "AUFLIRA"); + lt("NRA", "AUFNIRA"); + + nc("NIA", "QF_UF"); + nc("NIA", "QF_LRA"); + gt("NIA", "QF_LIA"); + nc("NIA", "QF_UFLRA"); + nc("NIA", "QF_UFLIA"); + nc("NIA", "QF_AUFLIA"); + nc("NIA", "QF_AUFLIRA"); + nc("NIA", "QF_BV"); + nc("NIA", "QF_ABV"); + nc("NIA", "QF_AUFBV"); + gt("NIA", "QF_IDL"); + nc("NIA", "QF_RDL"); + nc("NIA", "QF_UFIDL"); + gt("NIA", "QF_NIA"); + nc("NIA", "QF_NRA"); + nc("NIA", "QF_AUFNIRA"); + nc("NIA", "LRA"); + nc("NIA", "NRA"); + eq("NIA", "NIA"); + nc("NIA", "UFLRA"); + lt("NIA", "UFNIA"); + nc("NIA", "AUFLIA"); + nc("NIA", "AUFLIRA"); + lt("NIA", "AUFNIRA"); + + gt("UFLRA", "QF_UF"); + gt("UFLRA", "QF_LRA"); + nc("UFLRA", "QF_LIA"); + gt("UFLRA", "QF_UFLRA"); + nc("UFLRA", "QF_UFLIA"); + nc("UFLRA", "QF_AUFLIA"); + nc("UFLRA", "QF_AUFLIRA"); + nc("UFLRA", "QF_BV"); + nc("UFLRA", "QF_ABV"); + nc("UFLRA", "QF_AUFBV"); + nc("UFLRA", "QF_IDL"); + gt("UFLRA", "QF_RDL"); + nc("UFLRA", "QF_UFIDL"); + nc("UFLRA", "QF_NIA"); + nc("UFLRA", "QF_NRA"); + nc("UFLRA", "QF_AUFNIRA"); + gt("UFLRA", "LRA"); + nc("UFLRA", "NRA"); + nc("UFLRA", "NIA"); + eq("UFLRA", "UFLRA"); + nc("UFLRA", "UFNIA"); + nc("UFLRA", "AUFLIA"); + lt("UFLRA", "AUFLIRA"); + lt("UFLRA", "AUFNIRA"); + + gt("UFNIA", "QF_UF"); + nc("UFNIA", "QF_LRA"); + gt("UFNIA", "QF_LIA"); + nc("UFNIA", "QF_UFLRA"); + gt("UFNIA", "QF_UFLIA"); + nc("UFNIA", "QF_AUFLIA"); + nc("UFNIA", "QF_AUFLIRA"); + nc("UFNIA", "QF_BV"); + nc("UFNIA", "QF_ABV"); + nc("UFNIA", "QF_AUFBV"); + gt("UFNIA", "QF_IDL"); + nc("UFNIA", "QF_RDL"); + gt("UFNIA", "QF_UFIDL"); + gt("UFNIA", "QF_NIA"); + nc("UFNIA", "QF_NRA"); + nc("UFNIA", "QF_AUFNIRA"); + nc("UFNIA", "LRA"); + nc("UFNIA", "NRA"); + gt("UFNIA", "NIA"); + nc("UFNIA", "UFLRA"); + eq("UFNIA", "UFNIA"); + nc("UFNIA", "AUFLIA"); + nc("UFNIA", "AUFLIRA"); + lt("UFNIA", "AUFNIRA"); + + gt("AUFLIA", "QF_UF"); + nc("AUFLIA", "QF_LRA"); + gt("AUFLIA", "QF_LIA"); + nc("AUFLIA", "QF_UFLRA"); + gt("AUFLIA", "QF_UFLIA"); + gt("AUFLIA", "QF_AUFLIA"); + nc("AUFLIA", "QF_AUFLIRA"); + nc("AUFLIA", "QF_BV"); + nc("AUFLIA", "QF_ABV"); + nc("AUFLIA", "QF_AUFBV"); + gt("AUFLIA", "QF_IDL"); + nc("AUFLIA", "QF_RDL"); + gt("AUFLIA", "QF_UFIDL"); + nc("AUFLIA", "QF_NIA"); + nc("AUFLIA", "QF_NRA"); + nc("AUFLIA", "QF_AUFNIRA"); + nc("AUFLIA", "LRA"); + nc("AUFLIA", "NRA"); + nc("AUFLIA", "NIA"); + nc("AUFLIA", "UFLRA"); + nc("AUFLIA", "UFNIA"); + eq("AUFLIA", "AUFLIA"); + lt("AUFLIA", "AUFLIRA"); + lt("AUFLIA", "AUFNIRA"); + + gt("AUFLIRA", "QF_UF"); + gt("AUFLIRA", "QF_LRA"); + gt("AUFLIRA", "QF_LIA"); + gt("AUFLIRA", "QF_UFLRA"); + gt("AUFLIRA", "QF_UFLIA"); + gt("AUFLIRA", "QF_AUFLIA"); + gt("AUFLIRA", "QF_AUFLIRA"); + nc("AUFLIRA", "QF_BV"); + nc("AUFLIRA", "QF_ABV"); + nc("AUFLIRA", "QF_AUFBV"); + gt("AUFLIRA", "QF_IDL"); + gt("AUFLIRA", "QF_RDL"); + gt("AUFLIRA", "QF_UFIDL"); + nc("AUFLIRA", "QF_NIA"); + nc("AUFLIRA", "QF_NRA"); + nc("AUFLIRA", "QF_AUFNIRA"); + gt("AUFLIRA", "LRA"); + nc("AUFLIRA", "NRA"); + nc("AUFLIRA", "NIA"); + gt("AUFLIRA", "UFLRA"); + nc("AUFLIRA", "UFNIA"); + gt("AUFLIRA", "AUFLIA"); + eq("AUFLIRA", "AUFLIRA"); + lt("AUFLIRA", "AUFNIRA"); + + gt("AUFNIRA", "QF_UF"); + gt("AUFNIRA", "QF_LRA"); + gt("AUFNIRA", "QF_LIA"); + gt("AUFNIRA", "QF_UFLRA"); + gt("AUFNIRA", "QF_UFLIA"); + gt("AUFNIRA", "QF_AUFLIA"); + gt("AUFNIRA", "QF_AUFLIRA"); + nc("AUFNIRA", "QF_BV"); + nc("AUFNIRA", "QF_ABV"); + nc("AUFNIRA", "QF_AUFBV"); + gt("AUFNIRA", "QF_IDL"); + gt("AUFNIRA", "QF_RDL"); + gt("AUFNIRA", "QF_UFIDL"); + gt("AUFNIRA", "QF_NIA"); + gt("AUFNIRA", "QF_NRA"); + gt("AUFNIRA", "QF_AUFNIRA"); + gt("AUFNIRA", "LRA"); + gt("AUFNIRA", "NRA"); + gt("AUFNIRA", "NIA"); + gt("AUFNIRA", "UFLRA"); + gt("AUFNIRA", "UFNIA"); + gt("AUFNIRA", "AUFLIA"); + gt("AUFNIRA", "AUFLIRA"); + eq("AUFNIRA", "AUFNIRA"); + lt("AUFNIRA", "AUFNIRAT"); + + gt("QF_UFC", "QF_UF"); + gt("QF_UFCLRA", "QF_UFLRA"); + + gt(ufHo, "QF_UF"); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h deleted file mode 100644 index 055ff41cc..000000000 --- a/test/unit/theory/logic_info_white.h +++ /dev/null @@ -1,1376 +0,0 @@ -/********************* */ -/*! \file logic_info_white.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Unit testing for CVC4::LogicInfo class - ** - ** Unit testing for CVC4::LogicInfo class. - **/ - -#include - -#include "base/configuration.h" -#include "expr/kind.h" -#include "theory/logic_info.h" -using namespace CVC4; -using namespace CVC4::theory; - -using namespace std; - -class LogicInfoWhite : public CxxTest::TestSuite { - -public: - -#warning "This test is of questionable compatiblity with contrib/new-theory. Is the new theory id handled correctly by the Logic info." - - void testSmtlibLogics() { - LogicInfo info("QF_SAT"); - TS_ASSERT( info.isLocked() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( info.isPure( THEORY_BOOL ) ); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( info.hasNothing() ); - - info = LogicInfo("AUFLIA"); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("AUFLIRA"); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("AUFNIRA"); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("LRA"); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_ABV"); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_AUFBV"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_AUFLIA"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_AX"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_BV"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_IDL"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( info.isDifferenceLogic() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_LIA"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_LRA"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_NIA"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_NRA"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_RDL"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( info.isDifferenceLogic() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_UF"); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARITH ) ); - TS_ASSERT( info.isPure( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_UFBV"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_UFIDL"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( info.isDifferenceLogic() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.areRealsUsed() ); - TS_ASSERT(!info.areTranscendentalsUsed()); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_UFLIA"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.areRealsUsed() ); - TS_ASSERT(!info.areTranscendentalsUsed()); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_UFLRA"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT(!info.areTranscendentalsUsed()); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_UFNRA"); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT(!info.areTranscendentalsUsed()); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("UFLRA"); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( !info.areIntegersUsed() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT(!info.areTranscendentalsUsed()); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("UFNIA"); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isPure( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.areRealsUsed() ); - TS_ASSERT(!info.areTranscendentalsUsed()); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("QF_ALL_SUPPORTED"); - TS_ASSERT( info.isLocked() ); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT(info.areTranscendentalsUsed()); - TS_ASSERT( !info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - - info = LogicInfo("ALL_SUPPORTED"); - TS_ASSERT( info.isLocked() ); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT( info.hasEverything() ); - TS_ASSERT( !info.hasNothing() ); - } - - void testDefaultLogic() { - LogicInfo info; - TS_ASSERT( !info.isLocked() ); - - TS_ASSERT_THROWS(info.getLogicString(), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BUILTIN), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BOOL), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_UF), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_ARITH), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_ARRAYS), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BV), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_DATATYPES), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_QUANTIFIERS), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isPure(THEORY_BUILTIN), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isPure(THEORY_BOOL), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isPure(THEORY_UF), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isPure(THEORY_ARITH), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isPure(THEORY_ARRAYS), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isPure(THEORY_BV), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isPure(THEORY_DATATYPES), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isPure(THEORY_QUANTIFIERS), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.isQuantified(), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.areIntegersUsed(), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.areRealsUsed(), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(!info.isLinear(), CVC4::IllegalArgumentException&); - - info.lock(); - TS_ASSERT( info.isLocked() ); - TS_ASSERT_EQUALS( info.getLogicString(), "ALL" ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BUILTIN ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_QUANTIFIERS ) ); - TS_ASSERT( ! info.isPure( THEORY_BUILTIN ) ); - TS_ASSERT( ! info.isPure( THEORY_BOOL ) ); - TS_ASSERT( ! info.isPure( THEORY_UF ) ); - TS_ASSERT( ! info.isPure( THEORY_ARITH ) ); - TS_ASSERT( ! info.isPure( THEORY_ARRAYS ) ); - TS_ASSERT( ! info.isPure( THEORY_BV ) ); - TS_ASSERT( ! info.isPure( THEORY_DATATYPES ) ); - TS_ASSERT( ! info.isPure( THEORY_QUANTIFIERS ) ); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT(info.areTranscendentalsUsed()); - TS_ASSERT( !info.isLinear() ); - - TS_ASSERT_THROWS(info.arithOnlyLinear(), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.disableIntegers(), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.disableQuantifiers(), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.disableTheory(THEORY_BV), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.disableTheory(THEORY_DATATYPES), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.enableIntegers(), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.disableReals(), CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.disableTheory(THEORY_ARITH), - CVC4::IllegalArgumentException&); - TS_ASSERT_THROWS(info.disableTheory(THEORY_UF), - CVC4::IllegalArgumentException&); - info = info.getUnlockedCopy(); - TS_ASSERT(!info.isLocked()); - info.disableTheory(THEORY_STRINGS); - info.disableTheory(THEORY_SETS); - info.disableTheory(THEORY_BAGS); - info.arithOnlyLinear(); - info.disableIntegers(); - info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) - { - TS_ASSERT_EQUALS(info.getLogicString(), "SEP_AUFBVFPDTLRA"); - } - else - { - TS_ASSERT_EQUALS(info.getLogicString(), "SEP_AUFBVDTLRA"); - } - - info = info.getUnlockedCopy(); - TS_ASSERT(!info.isLocked()); - info.disableQuantifiers(); - info.disableTheory(THEORY_BAGS); - info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) - { - TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); - } - else - { - TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVDTLRA"); - } - - info = info.getUnlockedCopy(); - TS_ASSERT(!info.isLocked()); - info.disableTheory(THEORY_BV); - info.disableTheory(THEORY_DATATYPES); - info.disableTheory(THEORY_BAGS); - info.enableIntegers(); - info.disableReals(); - info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) - { - TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFFPLIA"); - } - else - { - TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFLIA"); - } - - info = info.getUnlockedCopy(); - TS_ASSERT(!info.isLocked()); - info.disableTheory(THEORY_ARITH); - info.disableTheory(THEORY_UF); - info.disableTheory(THEORY_FP); - info.disableTheory(THEORY_SEP); - info.disableTheory(THEORY_BAGS); - info.lock(); - TS_ASSERT_EQUALS(info.getLogicString(), "QF_AX"); - TS_ASSERT(info.isPure(THEORY_ARRAYS)); - TS_ASSERT(!info.isQuantified()); - // check all-excluded logic - info = info.getUnlockedCopy(); - TS_ASSERT( !info.isLocked() ); - info.disableEverything(); - info.lock(); - TS_ASSERT( info.isLocked() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isPure( THEORY_BOOL ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT_THROWS(info.isLinear(), IllegalArgumentException&); - TS_ASSERT_THROWS(info.areIntegersUsed(), IllegalArgumentException&); - TS_ASSERT_THROWS(info.isDifferenceLogic(), IllegalArgumentException&); - TS_ASSERT_THROWS(info.areRealsUsed(), IllegalArgumentException&); - TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException&); - - // check copy is unchanged - info = info.getUnlockedCopy(); - TS_ASSERT( !info.isLocked() ); - info.lock(); - TS_ASSERT( info.isLocked() ); - TS_ASSERT( !info.isSharingEnabled() ); - TS_ASSERT( !info.isQuantified() ); - TS_ASSERT( info.isPure( THEORY_BOOL ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT_THROWS(info.isLinear(), IllegalArgumentException&); - TS_ASSERT_THROWS(info.areIntegersUsed(), IllegalArgumentException&); - TS_ASSERT_THROWS(info.isDifferenceLogic(), IllegalArgumentException&); - TS_ASSERT_THROWS(info.areRealsUsed(), IllegalArgumentException&); - TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException&); - - // check all-included logic - info = info.getUnlockedCopy(); - TS_ASSERT( !info.isLocked() ); - info.enableEverything(); - info.lock(); - TS_ASSERT( info.isLocked() ); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT(info.areTranscendentalsUsed()); - - // check copy is unchanged - info = info.getUnlockedCopy(); - TS_ASSERT( !info.isLocked() ); - info.lock(); - TS_ASSERT( info.isLocked() ); - TS_ASSERT( !info.isPure( THEORY_BOOL ) ); - TS_ASSERT( info.isSharingEnabled() ); - TS_ASSERT( info.isQuantified() ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); - TS_ASSERT( !info.isLinear() ); - TS_ASSERT( info.areIntegersUsed() ); - TS_ASSERT( !info.isDifferenceLogic() ); - TS_ASSERT( info.areRealsUsed() ); - TS_ASSERT(info.areTranscendentalsUsed()); - } - - void eq(const LogicInfo& logic1, const LogicInfo& logic2) const { - cout << "asserting that " << logic1 << " == " << logic2 << endl; - - TS_ASSERT( logic1 == logic2 ); - TS_ASSERT( !(logic1 != logic2) ); - TS_ASSERT( !(logic1 < logic2) ); - TS_ASSERT( !(logic1 > logic2) ); - TS_ASSERT( logic1 <= logic2 ); - TS_ASSERT( logic1 >= logic2 ); - TS_ASSERT( logic1.isComparableTo(logic2) ); - - TS_ASSERT( logic2 == logic1 ); - TS_ASSERT( !(logic2 != logic1) ); - TS_ASSERT( !(logic2 < logic1) ); - TS_ASSERT( !(logic2 > logic1) ); - TS_ASSERT( logic2 <= logic1 ); - TS_ASSERT( logic2 >= logic1 ); - TS_ASSERT( logic2.isComparableTo(logic1) ); - } - - void nc(const LogicInfo& logic1, const LogicInfo& logic2) const { - cout << "asserting that " << logic1 << " is-not-comparable-to " << logic2 << endl; - TS_ASSERT( !(logic1 == logic2) ); - TS_ASSERT( logic1 != logic2 ); - TS_ASSERT( !(logic1 < logic2) ); - TS_ASSERT( !(logic1 > logic2) ); - TS_ASSERT( !(logic1 <= logic2) ); - TS_ASSERT( !(logic1 >= logic2) ); - TS_ASSERT( !logic1.isComparableTo(logic2) ); - - TS_ASSERT( !(logic2 == logic1) ); - TS_ASSERT( logic2 != logic1 ); - TS_ASSERT( !(logic2 < logic1) ); - TS_ASSERT( !(logic2 > logic1) ); - TS_ASSERT( !(logic2 <= logic1) ); - TS_ASSERT( !(logic2 >= logic1) ); - TS_ASSERT( !logic2.isComparableTo(logic1) ); - } - - void lt(const LogicInfo& logic1, const LogicInfo& logic2) const { - cout << "asserting that " << logic1 << " < " << logic2 << endl; - - TS_ASSERT( !(logic1 == logic2) ); - TS_ASSERT( logic1 != logic2 ); - TS_ASSERT( logic1 < logic2 ); - TS_ASSERT( !(logic1 > logic2) ); - TS_ASSERT( logic1 <= logic2 ); - TS_ASSERT( !(logic1 >= logic2) ); - TS_ASSERT( logic1.isComparableTo(logic2) ); - - TS_ASSERT( !(logic2 == logic1) ); - TS_ASSERT( logic2 != logic1 ); - TS_ASSERT( !(logic2 < logic1) ); - TS_ASSERT( logic2 > logic1 ); - TS_ASSERT( !(logic2 <= logic1) ); - TS_ASSERT( logic2 >= logic1 ); - TS_ASSERT( logic2.isComparableTo(logic1) ); - } - - void gt(const LogicInfo& logic1, const LogicInfo& logic2) const { - cout << "asserting that " << logic1 << " > " << logic2 << endl; - - TS_ASSERT( !(logic1 == logic2) ); - TS_ASSERT( logic1 != logic2 ); - TS_ASSERT( !(logic1 < logic2) ); - TS_ASSERT( logic1 > logic2 ); - TS_ASSERT( !(logic1 <= logic2) ); - TS_ASSERT( logic1 >= logic2 ); - TS_ASSERT( logic1.isComparableTo(logic2) ); - - TS_ASSERT( !(logic2 == logic1) ); - TS_ASSERT( logic2 != logic1 ); - TS_ASSERT( logic2 < logic1 ); - TS_ASSERT( !(logic2 > logic1) ); - TS_ASSERT( logic2 <= logic1 ); - TS_ASSERT( !(logic2 >= logic1) ); - TS_ASSERT( logic2.isComparableTo(logic1) ); - } - - void testComparison() { - LogicInfo ufHo = LogicInfo("QF_UF").getUnlockedCopy(); - ufHo.enableHigherOrder(); - ufHo.lock(); - - eq("QF_UF", "QF_UF"); - nc("QF_UF", "QF_LRA"); - nc("QF_UF", "QF_LIA"); - lt("QF_UF", "QF_UFLRA"); - lt("QF_UF", "QF_UFLIA"); - lt("QF_UF", "QF_AUFLIA"); - lt("QF_UF", "QF_AUFLIRA"); - nc("QF_UF", "QF_BV"); - nc("QF_UF", "QF_ABV"); - lt("QF_UF", "QF_AUFBV"); - nc("QF_UF", "QF_IDL"); - nc("QF_UF", "QF_RDL"); - lt("QF_UF", "QF_UFIDL"); - nc("QF_UF", "QF_NIA"); - nc("QF_UF", "QF_NRA"); - lt("QF_UF", "QF_AUFNIRA"); - nc("QF_UF", "LRA"); - nc("QF_UF", "NRA"); - nc("QF_UF", "NIA"); - lt("QF_UF", "UFLRA"); - lt("QF_UF", "UFNIA"); - lt("QF_UF", "AUFLIA"); - lt("QF_UF", "AUFLIRA"); - lt("QF_UF", "AUFNIRA"); - lt("QF_UF", "QF_UFC"); - lt("QF_UF", ufHo); - nc("QF_UFC", ufHo); - - nc("QF_LRA", "QF_UF"); - eq("QF_LRA", "QF_LRA"); - nc("QF_LRA", "QF_LIA"); - lt("QF_LRA", "QF_UFLRA"); - nc("QF_LRA", "QF_UFLIA"); - nc("QF_LRA", "QF_AUFLIA"); - lt("QF_LRA", "QF_AUFLIRA"); - nc("QF_LRA", "QF_BV"); - nc("QF_LRA", "QF_ABV"); - nc("QF_LRA", "QF_AUFBV"); - nc("QF_LRA", "QF_IDL"); - gt("QF_LRA", "QF_RDL"); - nc("QF_LRA", "QF_UFIDL"); - nc("QF_LRA", "QF_NIA"); - lt("QF_LRA", "QF_NRA"); - lt("QF_LRA", "QF_AUFNIRA"); - lt("QF_LRA", "LRA"); - lt("QF_LRA", "NRA"); - nc("QF_LRA", "NIA"); - lt("QF_LRA", "UFLRA"); - nc("QF_LRA", "UFNIA"); - nc("QF_LRA", "AUFLIA"); - lt("QF_LRA", "AUFLIRA"); - lt("QF_LRA", "AUFNIRA"); - lt("QF_LRA", "QF_UFCLRA"); - - nc("QF_LIA", "QF_UF"); - nc("QF_LIA", "QF_LRA"); - eq("QF_LIA", "QF_LIA"); - nc("QF_LIA", "QF_UFLRA"); - lt("QF_LIA", "QF_UFLIA"); - lt("QF_LIA", "QF_AUFLIA"); - lt("QF_LIA", "QF_AUFLIRA"); - nc("QF_LIA", "QF_BV"); - nc("QF_LIA", "QF_ABV"); - nc("QF_LIA", "QF_AUFBV"); - gt("QF_LIA", "QF_IDL"); - nc("QF_LIA", "QF_RDL"); - nc("QF_LIA", "QF_UFIDL"); - lt("QF_LIA", "QF_NIA"); - nc("QF_LIA", "QF_NRA"); - lt("QF_LIA", "QF_AUFNIRA"); - nc("QF_LIA", "LRA"); - nc("QF_LIA", "NRA"); - lt("QF_LIA", "NIA"); - nc("QF_LIA", "UFLRA"); - lt("QF_LIA", "UFNIA"); - lt("QF_LIA", "AUFLIA"); - lt("QF_LIA", "AUFLIRA"); - lt("QF_LIA", "AUFNIRA"); - - gt("QF_UFLRA", "QF_UF"); - gt("QF_UFLRA", "QF_LRA"); - nc("QF_UFLRA", "QF_LIA"); - eq("QF_UFLRA", "QF_UFLRA"); - nc("QF_UFLRA", "QF_UFLIA"); - nc("QF_UFLRA", "QF_AUFLIA"); - lt("QF_UFLRA", "QF_AUFLIRA"); - nc("QF_UFLRA", "QF_BV"); - nc("QF_UFLRA", "QF_ABV"); - nc("QF_UFLRA", "QF_AUFBV"); - nc("QF_UFLRA", "QF_IDL"); - gt("QF_UFLRA", "QF_RDL"); - nc("QF_UFLRA", "QF_UFIDL"); - nc("QF_UFLRA", "QF_NIA"); - nc("QF_UFLRA", "QF_NRA"); - lt("QF_UFLRA", "QF_AUFNIRA"); - nc("QF_UFLRA", "LRA"); - nc("QF_UFLRA", "NRA"); - nc("QF_UFLRA", "NIA"); - lt("QF_UFLRA", "UFLRA"); - nc("QF_UFLRA", "UFNIA"); - nc("QF_UFLRA", "AUFLIA"); - lt("QF_UFLRA", "AUFLIRA"); - lt("QF_UFLRA", "AUFNIRA"); - - gt("QF_UFLIA", "QF_UF"); - nc("QF_UFLIA", "QF_LRA"); - gt("QF_UFLIA", "QF_LIA"); - nc("QF_UFLIA", "QF_UFLRA"); - eq("QF_UFLIA", "QF_UFLIA"); - lt("QF_UFLIA", "QF_AUFLIA"); - lt("QF_UFLIA", "QF_AUFLIRA"); - nc("QF_UFLIA", "QF_BV"); - nc("QF_UFLIA", "QF_ABV"); - nc("QF_UFLIA", "QF_AUFBV"); - gt("QF_UFLIA", "QF_IDL"); - nc("QF_UFLIA", "QF_RDL"); - gt("QF_UFLIA", "QF_UFIDL"); - nc("QF_UFLIA", "QF_NIA"); - nc("QF_UFLIA", "QF_NRA"); - lt("QF_UFLIA", "QF_AUFNIRA"); - nc("QF_UFLIA", "LRA"); - nc("QF_UFLIA", "NRA"); - nc("QF_UFLIA", "NIA"); - nc("QF_UFLIA", "UFLRA"); - lt("QF_UFLIA", "UFNIA"); - lt("QF_UFLIA", "AUFLIA"); - lt("QF_UFLIA", "AUFLIRA"); - lt("QF_UFLIA", "AUFNIRA"); - - gt("QF_AUFLIA", "QF_UF"); - nc("QF_AUFLIA", "QF_LRA"); - gt("QF_AUFLIA", "QF_LIA"); - nc("QF_AUFLIA", "QF_UFLRA"); - gt("QF_AUFLIA", "QF_UFLIA"); - eq("QF_AUFLIA", "QF_AUFLIA"); - lt("QF_AUFLIA", "QF_AUFLIRA"); - nc("QF_AUFLIA", "QF_BV"); - nc("QF_AUFLIA", "QF_ABV"); - nc("QF_AUFLIA", "QF_AUFBV"); - gt("QF_AUFLIA", "QF_IDL"); - nc("QF_AUFLIA", "QF_RDL"); - gt("QF_AUFLIA", "QF_UFIDL"); - nc("QF_AUFLIA", "QF_NIA"); - nc("QF_AUFLIA", "QF_NRA"); - lt("QF_AUFLIA", "QF_AUFNIRA"); - nc("QF_AUFLIA", "LRA"); - nc("QF_AUFLIA", "NRA"); - nc("QF_AUFLIA", "NIA"); - nc("QF_AUFLIA", "UFLRA"); - nc("QF_AUFLIA", "UFNIA"); - lt("QF_AUFLIA", "AUFLIA"); - lt("QF_AUFLIA", "AUFLIRA"); - lt("QF_AUFLIA", "AUFNIRA"); - - gt("QF_AUFLIRA", "QF_UF"); - gt("QF_AUFLIRA", "QF_LRA"); - gt("QF_AUFLIRA", "QF_LIA"); - gt("QF_AUFLIRA", "QF_UFLRA"); - gt("QF_AUFLIRA", "QF_UFLIA"); - gt("QF_AUFLIRA", "QF_AUFLIA"); - eq("QF_AUFLIRA", "QF_AUFLIRA"); - nc("QF_AUFLIRA", "QF_BV"); - nc("QF_AUFLIRA", "QF_ABV"); - nc("QF_AUFLIRA", "QF_AUFBV"); - gt("QF_AUFLIRA", "QF_IDL"); - gt("QF_AUFLIRA", "QF_RDL"); - gt("QF_AUFLIRA", "QF_UFIDL"); - nc("QF_AUFLIRA", "QF_NIA"); - nc("QF_AUFLIRA", "QF_NRA"); - lt("QF_AUFLIRA", "QF_AUFNIRA"); - nc("QF_AUFLIRA", "LRA"); - nc("QF_AUFLIRA", "NRA"); - nc("QF_AUFLIRA", "NIA"); - nc("QF_AUFLIRA", "UFLRA"); - nc("QF_AUFLIRA", "UFNIA"); - nc("QF_AUFLIRA", "AUFLIA"); - lt("QF_AUFLIRA", "AUFLIRA"); - lt("QF_AUFLIRA", "AUFNIRA"); - - nc("QF_BV", "QF_UF"); - nc("QF_BV", "QF_LRA"); - nc("QF_BV", "QF_LIA"); - nc("QF_BV", "QF_UFLRA"); - nc("QF_BV", "QF_UFLIA"); - nc("QF_BV", "QF_AUFLIA"); - nc("QF_BV", "QF_AUFLIRA"); - eq("QF_BV", "QF_BV"); - lt("QF_BV", "QF_ABV"); - lt("QF_BV", "QF_AUFBV"); - nc("QF_BV", "QF_IDL"); - nc("QF_BV", "QF_RDL"); - nc("QF_BV", "QF_UFIDL"); - nc("QF_BV", "QF_NIA"); - nc("QF_BV", "QF_NRA"); - nc("QF_BV", "QF_AUFNIRA"); - nc("QF_BV", "LRA"); - nc("QF_BV", "NRA"); - nc("QF_BV", "NIA"); - nc("QF_BV", "UFLRA"); - nc("QF_BV", "UFNIA"); - nc("QF_BV", "AUFLIA"); - nc("QF_BV", "AUFLIRA"); - nc("QF_BV", "AUFNIRA"); - - nc("QF_ABV", "QF_UF"); - nc("QF_ABV", "QF_LRA"); - nc("QF_ABV", "QF_LIA"); - nc("QF_ABV", "QF_UFLRA"); - nc("QF_ABV", "QF_UFLIA"); - nc("QF_ABV", "QF_AUFLIA"); - nc("QF_ABV", "QF_AUFLIRA"); - gt("QF_ABV", "QF_BV"); - eq("QF_ABV", "QF_ABV"); - lt("QF_ABV", "QF_AUFBV"); - nc("QF_ABV", "QF_IDL"); - nc("QF_ABV", "QF_RDL"); - nc("QF_ABV", "QF_UFIDL"); - nc("QF_ABV", "QF_NIA"); - nc("QF_ABV", "QF_NRA"); - nc("QF_ABV", "QF_AUFNIRA"); - nc("QF_ABV", "LRA"); - nc("QF_ABV", "NRA"); - nc("QF_ABV", "NIA"); - nc("QF_ABV", "UFLRA"); - nc("QF_ABV", "UFNIA"); - nc("QF_ABV", "AUFLIA"); - nc("QF_ABV", "AUFLIRA"); - nc("QF_ABV", "AUFNIRA"); - - gt("QF_AUFBV", "QF_UF"); - nc("QF_AUFBV", "QF_LRA"); - nc("QF_AUFBV", "QF_LIA"); - nc("QF_AUFBV", "QF_UFLRA"); - nc("QF_AUFBV", "QF_UFLIA"); - nc("QF_AUFBV", "QF_AUFLIA"); - nc("QF_AUFBV", "QF_AUFLIRA"); - gt("QF_AUFBV", "QF_BV"); - gt("QF_AUFBV", "QF_ABV"); - eq("QF_AUFBV", "QF_AUFBV"); - nc("QF_AUFBV", "QF_IDL"); - nc("QF_AUFBV", "QF_RDL"); - nc("QF_AUFBV", "QF_UFIDL"); - nc("QF_AUFBV", "QF_NIA"); - nc("QF_AUFBV", "QF_NRA"); - nc("QF_AUFBV", "QF_AUFNIRA"); - nc("QF_AUFBV", "LRA"); - nc("QF_AUFBV", "NRA"); - nc("QF_AUFBV", "NIA"); - nc("QF_AUFBV", "UFLRA"); - nc("QF_AUFBV", "UFNIA"); - nc("QF_AUFBV", "AUFLIA"); - nc("QF_AUFBV", "AUFLIRA"); - nc("QF_AUFBV", "AUFNIRA"); - - nc("QF_IDL", "QF_UF"); - nc("QF_IDL", "QF_LRA"); - lt("QF_IDL", "QF_LIA"); - nc("QF_IDL", "QF_UFLRA"); - lt("QF_IDL", "QF_UFLIA"); - lt("QF_IDL", "QF_AUFLIA"); - lt("QF_IDL", "QF_AUFLIRA"); - nc("QF_IDL", "QF_BV"); - nc("QF_IDL", "QF_ABV"); - nc("QF_IDL", "QF_AUFBV"); - eq("QF_IDL", "QF_IDL"); - nc("QF_IDL", "QF_RDL"); - lt("QF_IDL", "QF_UFIDL"); - lt("QF_IDL", "QF_NIA"); - nc("QF_IDL", "QF_NRA"); - nc("QF_IDL", "QF_NRAT"); - lt("QF_IDL", "QF_AUFNIRA"); - nc("QF_IDL", "LRA"); - nc("QF_IDL", "NRA"); - lt("QF_IDL", "NIA"); - nc("QF_IDL", "UFLRA"); - lt("QF_IDL", "UFNIA"); - lt("QF_IDL", "AUFLIA"); - lt("QF_IDL", "AUFLIRA"); - lt("QF_IDL", "AUFNIRA"); - - nc("QF_RDL", "QF_UF"); - lt("QF_RDL", "QF_LRA"); - nc("QF_RDL", "QF_LIA"); - lt("QF_RDL", "QF_UFLRA"); - nc("QF_RDL", "QF_UFLIA"); - nc("QF_RDL", "QF_AUFLIA"); - lt("QF_RDL", "QF_AUFLIRA"); - nc("QF_RDL", "QF_BV"); - nc("QF_RDL", "QF_ABV"); - nc("QF_RDL", "QF_AUFBV"); - nc("QF_RDL", "QF_IDL"); - eq("QF_RDL", "QF_RDL"); - nc("QF_RDL", "QF_UFIDL"); - nc("QF_RDL", "QF_NIA"); - lt("QF_RDL", "QF_NRA"); - lt("QF_RDL", "QF_AUFNIRA"); - lt("QF_RDL", "LRA"); - lt("QF_RDL", "NRA"); - nc("QF_RDL", "NIA"); - lt("QF_RDL", "UFLRA"); - nc("QF_RDL", "UFNIA"); - nc("QF_RDL", "AUFLIA"); - lt("QF_RDL", "AUFLIRA"); - lt("QF_RDL", "AUFNIRA"); - - gt("QF_UFIDL", "QF_UF"); - nc("QF_UFIDL", "QF_LRA"); - nc("QF_UFIDL", "QF_LIA"); - nc("QF_UFIDL", "QF_UFLRA"); - lt("QF_UFIDL", "QF_UFLIA"); - lt("QF_UFIDL", "QF_AUFLIA"); - lt("QF_UFIDL", "QF_AUFLIRA"); - nc("QF_UFIDL", "QF_BV"); - nc("QF_UFIDL", "QF_ABV"); - nc("QF_UFIDL", "QF_AUFBV"); - gt("QF_UFIDL", "QF_IDL"); - nc("QF_UFIDL", "QF_RDL"); - eq("QF_UFIDL", "QF_UFIDL"); - nc("QF_UFIDL", "QF_NIA"); - nc("QF_UFIDL", "QF_NRA"); - lt("QF_UFIDL", "QF_AUFNIRA"); - nc("QF_UFIDL", "LRA"); - nc("QF_UFIDL", "NRA"); - nc("QF_UFIDL", "NIA"); - nc("QF_UFIDL", "UFLRA"); - lt("QF_UFIDL", "UFNIA"); - lt("QF_UFIDL", "AUFLIA"); - lt("QF_UFIDL", "AUFLIRA"); - lt("QF_UFIDL", "AUFNIRA"); - - nc("QF_NIA", "QF_UF"); - nc("QF_NIA", "QF_LRA"); - gt("QF_NIA", "QF_LIA"); - nc("QF_NIA", "QF_UFLRA"); - nc("QF_NIA", "QF_UFLIA"); - nc("QF_NIA", "QF_AUFLIA"); - nc("QF_NIA", "QF_AUFLIRA"); - nc("QF_NIA", "QF_BV"); - nc("QF_NIA", "QF_ABV"); - nc("QF_NIA", "QF_AUFBV"); - gt("QF_NIA", "QF_IDL"); - nc("QF_NIA", "QF_RDL"); - nc("QF_NIA", "QF_UFIDL"); - eq("QF_NIA", "QF_NIA"); - nc("QF_NIA", "QF_NRA"); - lt("QF_NIA", "QF_AUFNIRA"); - nc("QF_NIA", "LRA"); - nc("QF_NIA", "NRA"); - lt("QF_NIA", "NIA"); - nc("QF_NIA", "UFLRA"); - lt("QF_NIA", "UFNIA"); - nc("QF_NIA", "AUFLIA"); - nc("QF_NIA", "AUFLIRA"); - lt("QF_NIA", "AUFNIRA"); - - nc("QF_NRA", "QF_UF"); - gt("QF_NRA", "QF_LRA"); - nc("QF_NRA", "QF_LIA"); - nc("QF_NRA", "QF_UFLRA"); - nc("QF_NRA", "QF_UFLIA"); - nc("QF_NRA", "QF_AUFLIA"); - nc("QF_NRA", "QF_AUFLIRA"); - nc("QF_NRA", "QF_BV"); - nc("QF_NRA", "QF_ABV"); - nc("QF_NRA", "QF_AUFBV"); - nc("QF_NRA", "QF_IDL"); - gt("QF_NRA", "QF_RDL"); - nc("QF_NRA", "QF_UFIDL"); - nc("QF_NRA", "QF_NIA"); - eq("QF_NRA", "QF_NRA"); - lt("QF_NRA", "QF_AUFNIRA"); - nc("QF_NRA", "LRA"); - lt("QF_NRA", "NRA"); - nc("QF_NRA", "NIA"); - nc("QF_NRA", "UFLRA"); - nc("QF_NRA", "UFNIA"); - nc("QF_NRA", "AUFLIA"); - nc("QF_NRA", "AUFLIRA"); - lt("QF_NRA", "AUFNIRA"); - lt("QF_NRA", "QF_NRAT"); - - gt("QF_AUFNIRA", "QF_UF"); - gt("QF_AUFNIRA", "QF_LRA"); - gt("QF_AUFNIRA", "QF_LIA"); - gt("QF_AUFNIRA", "QF_UFLRA"); - gt("QF_AUFNIRA", "QF_UFLIA"); - gt("QF_AUFNIRA", "QF_AUFLIA"); - gt("QF_AUFNIRA", "QF_AUFLIRA"); - nc("QF_AUFNIRA", "QF_BV"); - nc("QF_AUFNIRA", "QF_ABV"); - nc("QF_AUFNIRA", "QF_AUFBV"); - gt("QF_AUFNIRA", "QF_IDL"); - gt("QF_AUFNIRA", "QF_RDL"); - gt("QF_AUFNIRA", "QF_UFIDL"); - gt("QF_AUFNIRA", "QF_NIA"); - gt("QF_AUFNIRA", "QF_NRA"); - eq("QF_AUFNIRA", "QF_AUFNIRA"); - nc("QF_AUFNIRA", "LRA"); - nc("QF_AUFNIRA", "NRA"); - nc("QF_AUFNIRA", "NIA"); - nc("QF_AUFNIRA", "UFLRA"); - nc("QF_AUFNIRA", "UFNIA"); - nc("QF_AUFNIRA", "AUFLIA"); - nc("QF_AUFNIRA", "AUFLIRA"); - lt("QF_AUFNIRA", "AUFNIRA"); - lt("QF_AUFNIRA", "QF_AUFNIRAT"); - - nc("LRA", "QF_UF"); - gt("LRA", "QF_LRA"); - nc("LRA", "QF_LIA"); - nc("LRA", "QF_UFLRA"); - nc("LRA", "QF_UFLIA"); - nc("LRA", "QF_AUFLIA"); - nc("LRA", "QF_AUFLIRA"); - nc("LRA", "QF_BV"); - nc("LRA", "QF_ABV"); - nc("LRA", "QF_AUFBV"); - nc("LRA", "QF_IDL"); - gt("LRA", "QF_RDL"); - nc("LRA", "QF_UFIDL"); - nc("LRA", "QF_NIA"); - nc("LRA", "QF_NRA"); - nc("LRA", "QF_AUFNIRA"); - eq("LRA", "LRA"); - lt("LRA", "NRA"); - nc("LRA", "NIA"); - lt("LRA", "UFLRA"); - nc("LRA", "UFNIA"); - nc("LRA", "AUFLIA"); - lt("LRA", "AUFLIRA"); - lt("LRA", "AUFNIRA"); - - nc("NRA", "QF_UF"); - gt("NRA", "QF_LRA"); - nc("NRA", "QF_LIA"); - nc("NRA", "QF_UFLRA"); - nc("NRA", "QF_UFLIA"); - nc("NRA", "QF_AUFLIA"); - nc("NRA", "QF_AUFLIRA"); - nc("NRA", "QF_BV"); - nc("NRA", "QF_ABV"); - nc("NRA", "QF_AUFBV"); - nc("NRA", "QF_IDL"); - gt("NRA", "QF_RDL"); - nc("NRA", "QF_UFIDL"); - nc("NRA", "QF_NIA"); - gt("NRA", "QF_NRA"); - nc("NRA", "QF_AUFNIRA"); - gt("NRA", "LRA"); - eq("NRA", "NRA"); - nc("NRA", "NIA"); - nc("NRA", "UFLRA"); - nc("NRA", "UFNIA"); - nc("NRA", "AUFLIA"); - nc("NRA", "AUFLIRA"); - lt("NRA", "AUFNIRA"); - - nc("NIA", "QF_UF"); - nc("NIA", "QF_LRA"); - gt("NIA", "QF_LIA"); - nc("NIA", "QF_UFLRA"); - nc("NIA", "QF_UFLIA"); - nc("NIA", "QF_AUFLIA"); - nc("NIA", "QF_AUFLIRA"); - nc("NIA", "QF_BV"); - nc("NIA", "QF_ABV"); - nc("NIA", "QF_AUFBV"); - gt("NIA", "QF_IDL"); - nc("NIA", "QF_RDL"); - nc("NIA", "QF_UFIDL"); - gt("NIA", "QF_NIA"); - nc("NIA", "QF_NRA"); - nc("NIA", "QF_AUFNIRA"); - nc("NIA", "LRA"); - nc("NIA", "NRA"); - eq("NIA", "NIA"); - nc("NIA", "UFLRA"); - lt("NIA", "UFNIA"); - nc("NIA", "AUFLIA"); - nc("NIA", "AUFLIRA"); - lt("NIA", "AUFNIRA"); - - gt("UFLRA", "QF_UF"); - gt("UFLRA", "QF_LRA"); - nc("UFLRA", "QF_LIA"); - gt("UFLRA", "QF_UFLRA"); - nc("UFLRA", "QF_UFLIA"); - nc("UFLRA", "QF_AUFLIA"); - nc("UFLRA", "QF_AUFLIRA"); - nc("UFLRA", "QF_BV"); - nc("UFLRA", "QF_ABV"); - nc("UFLRA", "QF_AUFBV"); - nc("UFLRA", "QF_IDL"); - gt("UFLRA", "QF_RDL"); - nc("UFLRA", "QF_UFIDL"); - nc("UFLRA", "QF_NIA"); - nc("UFLRA", "QF_NRA"); - nc("UFLRA", "QF_AUFNIRA"); - gt("UFLRA", "LRA"); - nc("UFLRA", "NRA"); - nc("UFLRA", "NIA"); - eq("UFLRA", "UFLRA"); - nc("UFLRA", "UFNIA"); - nc("UFLRA", "AUFLIA"); - lt("UFLRA", "AUFLIRA"); - lt("UFLRA", "AUFNIRA"); - - gt("UFNIA", "QF_UF"); - nc("UFNIA", "QF_LRA"); - gt("UFNIA", "QF_LIA"); - nc("UFNIA", "QF_UFLRA"); - gt("UFNIA", "QF_UFLIA"); - nc("UFNIA", "QF_AUFLIA"); - nc("UFNIA", "QF_AUFLIRA"); - nc("UFNIA", "QF_BV"); - nc("UFNIA", "QF_ABV"); - nc("UFNIA", "QF_AUFBV"); - gt("UFNIA", "QF_IDL"); - nc("UFNIA", "QF_RDL"); - gt("UFNIA", "QF_UFIDL"); - gt("UFNIA", "QF_NIA"); - nc("UFNIA", "QF_NRA"); - nc("UFNIA", "QF_AUFNIRA"); - nc("UFNIA", "LRA"); - nc("UFNIA", "NRA"); - gt("UFNIA", "NIA"); - nc("UFNIA", "UFLRA"); - eq("UFNIA", "UFNIA"); - nc("UFNIA", "AUFLIA"); - nc("UFNIA", "AUFLIRA"); - lt("UFNIA", "AUFNIRA"); - - gt("AUFLIA", "QF_UF"); - nc("AUFLIA", "QF_LRA"); - gt("AUFLIA", "QF_LIA"); - nc("AUFLIA", "QF_UFLRA"); - gt("AUFLIA", "QF_UFLIA"); - gt("AUFLIA", "QF_AUFLIA"); - nc("AUFLIA", "QF_AUFLIRA"); - nc("AUFLIA", "QF_BV"); - nc("AUFLIA", "QF_ABV"); - nc("AUFLIA", "QF_AUFBV"); - gt("AUFLIA", "QF_IDL"); - nc("AUFLIA", "QF_RDL"); - gt("AUFLIA", "QF_UFIDL"); - nc("AUFLIA", "QF_NIA"); - nc("AUFLIA", "QF_NRA"); - nc("AUFLIA", "QF_AUFNIRA"); - nc("AUFLIA", "LRA"); - nc("AUFLIA", "NRA"); - nc("AUFLIA", "NIA"); - nc("AUFLIA", "UFLRA"); - nc("AUFLIA", "UFNIA"); - eq("AUFLIA", "AUFLIA"); - lt("AUFLIA", "AUFLIRA"); - lt("AUFLIA", "AUFNIRA"); - - gt("AUFLIRA", "QF_UF"); - gt("AUFLIRA", "QF_LRA"); - gt("AUFLIRA", "QF_LIA"); - gt("AUFLIRA", "QF_UFLRA"); - gt("AUFLIRA", "QF_UFLIA"); - gt("AUFLIRA", "QF_AUFLIA"); - gt("AUFLIRA", "QF_AUFLIRA"); - nc("AUFLIRA", "QF_BV"); - nc("AUFLIRA", "QF_ABV"); - nc("AUFLIRA", "QF_AUFBV"); - gt("AUFLIRA", "QF_IDL"); - gt("AUFLIRA", "QF_RDL"); - gt("AUFLIRA", "QF_UFIDL"); - nc("AUFLIRA", "QF_NIA"); - nc("AUFLIRA", "QF_NRA"); - nc("AUFLIRA", "QF_AUFNIRA"); - gt("AUFLIRA", "LRA"); - nc("AUFLIRA", "NRA"); - nc("AUFLIRA", "NIA"); - gt("AUFLIRA", "UFLRA"); - nc("AUFLIRA", "UFNIA"); - gt("AUFLIRA", "AUFLIA"); - eq("AUFLIRA", "AUFLIRA"); - lt("AUFLIRA", "AUFNIRA"); - - gt("AUFNIRA", "QF_UF"); - gt("AUFNIRA", "QF_LRA"); - gt("AUFNIRA", "QF_LIA"); - gt("AUFNIRA", "QF_UFLRA"); - gt("AUFNIRA", "QF_UFLIA"); - gt("AUFNIRA", "QF_AUFLIA"); - gt("AUFNIRA", "QF_AUFLIRA"); - nc("AUFNIRA", "QF_BV"); - nc("AUFNIRA", "QF_ABV"); - nc("AUFNIRA", "QF_AUFBV"); - gt("AUFNIRA", "QF_IDL"); - gt("AUFNIRA", "QF_RDL"); - gt("AUFNIRA", "QF_UFIDL"); - gt("AUFNIRA", "QF_NIA"); - gt("AUFNIRA", "QF_NRA"); - gt("AUFNIRA", "QF_AUFNIRA"); - gt("AUFNIRA", "LRA"); - gt("AUFNIRA", "NRA"); - gt("AUFNIRA", "NIA"); - gt("AUFNIRA", "UFLRA"); - gt("AUFNIRA", "UFNIA"); - gt("AUFNIRA", "AUFLIA"); - gt("AUFNIRA", "AUFLIRA"); - eq("AUFNIRA", "AUFNIRA"); - lt("AUFNIRA", "AUFNIRAT"); - - gt("QF_UFC", "QF_UF"); - gt("QF_UFCLRA", "QF_UFLRA"); - - gt(ufHo, "QF_UF"); - } - -};/* class LogicInfoWhite */