mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
100 lines
2.9 KiB
C++
100 lines
2.9 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Hans-Jörg Schurr
|
|
*
|
|
* 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 guards of the C++ API functions.
|
|
*/
|
|
|
|
#include <gtest/gtest.h>
|
|
|
|
#include "test_api.h"
|
|
|
|
namespace cvc5::internal {
|
|
|
|
namespace test {
|
|
|
|
class TestApiBlackProof : public TestApi
|
|
{
|
|
protected:
|
|
Proof create_proof()
|
|
{
|
|
d_solver.setOption("produce-proofs", "true");
|
|
|
|
Sort uSort = d_solver.mkUninterpretedSort("u");
|
|
Sort intSort = d_solver.getIntegerSort();
|
|
Sort boolSort = d_solver.getBooleanSort();
|
|
Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
|
|
Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
|
|
std::vector<Proof> proof;
|
|
|
|
Term x = d_solver.mkConst(uSort, "x");
|
|
Term y = d_solver.mkConst(uSort, "y");
|
|
Term f = d_solver.mkConst(uToIntSort, "f");
|
|
Term p = d_solver.mkConst(intPredSort, "p");
|
|
Term zero = d_solver.mkInteger(0);
|
|
Term one = d_solver.mkInteger(1);
|
|
Term f_x = d_solver.mkTerm(Kind::APPLY_UF, {f, x});
|
|
Term f_y = d_solver.mkTerm(Kind::APPLY_UF, {f, y});
|
|
Term sum = d_solver.mkTerm(Kind::ADD, {f_x, f_y});
|
|
Term p_0 = d_solver.mkTerm(Kind::APPLY_UF, {p, zero});
|
|
Term p_f_y = d_solver.mkTerm(Kind::APPLY_UF, {p, f_y});
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind::GT, {zero, f_x}));
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind::GT, {zero, f_y}));
|
|
d_solver.assertFormula(d_solver.mkTerm(Kind::GT, {sum, one}));
|
|
d_solver.assertFormula(p_0);
|
|
d_solver.assertFormula(p_f_y.notTerm());
|
|
d_solver.checkSat();
|
|
|
|
return d_solver.getProof().front();
|
|
}
|
|
};
|
|
|
|
TEST_F(TestApiBlackProof, nullProof)
|
|
{
|
|
Proof proof;
|
|
ASSERT_EQ(proof.getRule(), ProofRule::UNKNOWN);
|
|
|
|
ASSERT_EQ(std::hash<cvc5::ProofRule>()(ProofRule::UNKNOWN),
|
|
static_cast<size_t>(ProofRule::UNKNOWN));
|
|
ASSERT_TRUE(proof.getResult().isNull());
|
|
ASSERT_TRUE(proof.getChildren().empty());
|
|
ASSERT_TRUE(proof.getArguments().empty());
|
|
}
|
|
|
|
TEST_F(TestApiBlackProof, getRule)
|
|
{
|
|
Proof proof = create_proof();
|
|
ASSERT_EQ(proof.getRule(), ProofRule::SCOPE);
|
|
}
|
|
|
|
TEST_F(TestApiBlackProof, getResult)
|
|
{
|
|
Proof proof = create_proof();
|
|
ASSERT_NO_THROW(proof.getResult());
|
|
}
|
|
|
|
TEST_F(TestApiBlackProof, getChildren)
|
|
{
|
|
Proof proof = create_proof();
|
|
std::vector<Proof> children;
|
|
ASSERT_NO_THROW(children = proof.getChildren());
|
|
ASSERT_FALSE(children.empty());
|
|
}
|
|
|
|
TEST_F(TestApiBlackProof, getArguments)
|
|
{
|
|
Proof proof = create_proof();
|
|
ASSERT_NO_THROW(proof.getArguments());
|
|
}
|
|
|
|
} // namespace test
|
|
} // namespace cvc5::internal
|