mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
0a35879fc1
This pull requests makes the enum that lists all proof rules a part of the API. It also renames the enum from PfRule to ProofRule. It also renames some unrelated types and function names that share the PfRule name (such as DslPfRule). This rename unfortunately touches many files since PfRule is not an uncommon type. (second to last commit)
54 lines
1.3 KiB
C++
54 lines
1.3 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Mathias Preiner
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2023 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.
|
|
* ****************************************************************************
|
|
*
|
|
* Black box testing of the Kind enum of the C++ API.
|
|
*/
|
|
|
|
#include <cvc5/cvc5_proof_rule.h>
|
|
|
|
#include <algorithm>
|
|
|
|
#include "base/output.h"
|
|
#include "gtest/gtest.h"
|
|
|
|
namespace cvc5::internal {
|
|
|
|
namespace test {
|
|
|
|
class TestApiProofRule : public ::testing::Test
|
|
{
|
|
};
|
|
|
|
TEST_F(TestApiProofRule, proofRuleToString)
|
|
{
|
|
for (int32_t r = static_cast<int32_t>(ProofRule::ASSUME);
|
|
r < static_cast<int32_t>(ProofRule::UNKNOWN);
|
|
++r)
|
|
{
|
|
auto rulestr = toString(static_cast<ProofRule>(r));
|
|
if (r == static_cast<int32_t>(ProofRule::UNKNOWN))
|
|
{
|
|
ASSERT_EQ(rulestr, "UNKNONW");
|
|
}
|
|
else
|
|
{
|
|
// If this assertion fails, the switch in cvc5_proof_rule.cpp is missing
|
|
// rule r.
|
|
ASSERT_NE(rulestr, "UNKNOWN");
|
|
ASSERT_NE(rulestr, "?");
|
|
}
|
|
}
|
|
}
|
|
|
|
} // namespace test
|
|
} // namespace cvc5::internal
|