GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_white.cpp Lines: 46 46 100.0 %
Date: 2021-03-22 Branches: 66 228 28.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Tim King, Dejan Jovanovic
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Black box testing of CVC4::theory::Theory.
13
 **
14
 ** Black box testing of CVC4::theory::Theory.
15
 **/
16
17
#include <memory>
18
#include <vector>
19
20
#include "context/context.h"
21
#include "expr/node.h"
22
#include "test_smt.h"
23
#include "theory/theory.h"
24
#include "theory/theory_engine.h"
25
#include "util/resource_manager.h"
26
27
namespace CVC4 {
28
29
using namespace theory;
30
using namespace expr;
31
using namespace context;
32
33
namespace test {
34
35
12
class TestTheoryWhite : public TestSmtNoFinishInit
36
{
37
 protected:
38
6
  void SetUp() override
39
  {
40
6
    TestSmtNoFinishInit::SetUp();
41
6
    d_context = d_smtEngine->getContext();
42
6
    d_user_context = d_smtEngine->getUserContext();
43
6
    d_logicInfo.reset(new LogicInfo());
44
6
    d_logicInfo->lock();
45
6
    d_smtEngine->finishInit();
46
6
    delete d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN];
47
6
    delete d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN];
48
6
    d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = nullptr;
49
6
    d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = nullptr;
50
51
18
    d_dummy_theory.reset(new DummyTheory<THEORY_BUILTIN>(d_context,
52
                                                         d_user_context,
53
                                                         d_outputChannel,
54
12
                                                         Valuation(nullptr),
55
6
                                                         *d_logicInfo,
56
6
                                                         nullptr));
57
6
    d_outputChannel.clear();
58
6
    d_atom0 = d_nodeManager->mkConst(true);
59
6
    d_atom1 = d_nodeManager->mkConst(false);
60
6
  }
61
62
  Context* d_context;
63
  UserContext* d_user_context;
64
  std::unique_ptr<LogicInfo> d_logicInfo;
65
  DummyOutputChannel d_outputChannel;
66
  std::unique_ptr<DummyTheory<THEORY_BUILTIN>> d_dummy_theory;
67
  Node d_atom0;
68
  Node d_atom1;
69
};
70
71
12
TEST_F(TestTheoryWhite, effort)
72
{
73
2
  Theory::Effort s = Theory::EFFORT_STANDARD;
74
2
  Theory::Effort f = Theory::EFFORT_FULL;
75
76
2
  ASSERT_TRUE(Theory::standardEffortOnly(s));
77
2
  ASSERT_FALSE(Theory::standardEffortOnly(f));
78
79
2
  ASSERT_FALSE(Theory::fullEffort(s));
80
2
  ASSERT_TRUE(Theory::fullEffort(f));
81
82
2
  ASSERT_TRUE(Theory::standardEffortOrMore(s));
83
2
  ASSERT_TRUE(Theory::standardEffortOrMore(f));
84
}
85
86
12
TEST_F(TestTheoryWhite, done)
87
{
88
2
  ASSERT_TRUE(d_dummy_theory->done());
89
90
2
  d_dummy_theory->assertFact(d_atom0, true);
91
2
  d_dummy_theory->assertFact(d_atom1, true);
92
93
2
  ASSERT_FALSE(d_dummy_theory->done());
94
95
2
  d_dummy_theory->check(Theory::EFFORT_FULL);
96
97
2
  ASSERT_TRUE(d_dummy_theory->done());
98
}
99
100
12
TEST_F(TestTheoryWhite, outputChannel)
101
{
102
4
  Node n = d_atom0.orNode(d_atom1);
103
2
  d_outputChannel.lemma(n);
104
2
  d_outputChannel.split(d_atom0);
105
4
  Node s = d_atom0.orNode(d_atom0.notNode());
106
2
  ASSERT_EQ(d_outputChannel.d_callHistory.size(), 2u);
107
2
  ASSERT_EQ(d_outputChannel.d_callHistory[0], std::make_pair(LEMMA, n));
108
2
  ASSERT_EQ(d_outputChannel.d_callHistory[1], std::make_pair(LEMMA, s));
109
2
  d_outputChannel.d_callHistory.clear();
110
}
111
}  // namespace test
112
39790
}  // namespace CVC4