GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_module.cpp Lines: 23 23 100.0 %
Date: 2021-09-29 Branches: 7 14 50.0 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Andrew Reynolds, Aina Niemetz
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Implementation of quantifier module.
14
 */
15
16
#include "theory/quantifiers/quant_module.h"
17
18
using namespace cvc5::kind;
19
20
namespace cvc5 {
21
namespace theory {
22
23
24030
QuantifiersModule::QuantifiersModule(
24
    Env& env,
25
    quantifiers::QuantifiersState& qs,
26
    quantifiers::QuantifiersInferenceManager& qim,
27
    quantifiers::QuantifiersRegistry& qr,
28
24030
    quantifiers::TermRegistry& tr)
29
24030
    : EnvObj(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
30
{
31
24030
}
32
33
18066
QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
34
{
35
18066
  return QEFFORT_NONE;
36
}
37
38
14907
eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
39
{
40
14907
  return d_qstate.getEqualityEngine();
41
}
42
43
497205
bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
44
{
45
497205
  return d_qstate.areEqual(n1, n2);
46
}
47
48
17814
bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
49
{
50
17814
  return d_qstate.areDisequal(n1, n2);
51
}
52
53
965528
TNode QuantifiersModule::getRepresentative(TNode n) const
54
{
55
965528
  return d_qstate.getRepresentative(n);
56
}
57
58
1880216
quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
59
{
60
1880216
  return d_treg.getTermDatabase();
61
}
62
63
63883
quantifiers::QuantifiersState& QuantifiersModule::getState()
64
{
65
63883
  return d_qstate;
66
}
67
68
quantifiers::QuantifiersInferenceManager&
69
31408
QuantifiersModule::getInferenceManager()
70
{
71
31408
  return d_qim;
72
}
73
74
4
quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry()
75
{
76
4
  return d_qreg;
77
}
78
79
}  // namespace theory
80
22746
}  // namespace cvc5