GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quantifiers_inference_manager.cpp Lines: 15 15 100.0 %
Date: 2021-03-23 Branches: 8 18 44.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_inference_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 Utility for quantifiers inference manager
13
 **/
14
15
#include "theory/quantifiers/quantifiers_inference_manager.h"
16
17
#include "theory/quantifiers/instantiate.h"
18
#include "theory/quantifiers/skolemize.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace quantifiers {
23
24
8997
QuantifiersInferenceManager::QuantifiersInferenceManager(
25
    Theory& t,
26
    QuantifiersState& state,
27
    QuantifiersRegistry& qr,
28
    TermRegistry& tr,
29
    FirstOrderModel* m,
30
8997
    ProofNodeManager* pnm)
31
    : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"),
32
8997
      d_instantiate(new Instantiate(state, *this, qr, tr, m, pnm)),
33
17994
      d_skolemize(new Skolemize(state, pnm))
34
{
35
8997
}
36
37
17988
QuantifiersInferenceManager::~QuantifiersInferenceManager() {}
38
39
546072
Instantiate* QuantifiersInferenceManager::getInstantiate()
40
{
41
546072
  return d_instantiate.get();
42
}
43
44
22232
Skolemize* QuantifiersInferenceManager::getSkolemize()
45
{
46
22232
  return d_skolemize.get();
47
}
48
49
173024
void QuantifiersInferenceManager::doPending()
50
{
51
173024
  doPendingLemmas();
52
173023
  doPendingPhaseRequirements();
53
173023
}
54
55
}  // namespace quantifiers
56
}  // namespace theory
57
26685
}  // namespace CVC4