GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quantifiers_modules.cpp Lines: 55 55 100.0 %
Date: 2021-03-23 Branches: 84 136 61.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_modules.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 Class for initializing the modules of quantifiers engine
13
 **/
14
15
#include "theory/quantifiers/quantifiers_modules.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers_engine.h"
19
#include "theory/quantifiers/relevant_domain.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace quantifiers {
24
25
6054
QuantifiersModules::QuantifiersModules()
26
    : d_rel_dom(nullptr),
27
      d_alpha_equiv(nullptr),
28
      d_inst_engine(nullptr),
29
      d_model_engine(nullptr),
30
      d_builder(nullptr),
31
      d_bint(nullptr),
32
      d_qcf(nullptr),
33
      d_sg_gen(nullptr),
34
      d_synth_e(nullptr),
35
      d_fs(nullptr),
36
      d_i_cbqi(nullptr),
37
      d_qsplit(nullptr),
38
6054
      d_sygus_inst(nullptr)
39
{
40
6054
}
41
6051
QuantifiersModules::~QuantifiersModules() {}
42
6054
void QuantifiersModules::initialize(QuantifiersEngine* qe,
43
                                    QuantifiersState& qs,
44
                                    QuantifiersInferenceManager& qim,
45
                                    QuantifiersRegistry& qr,
46
                                    DecisionManager* dm,
47
                                    std::vector<QuantifiersModule*>& modules)
48
{
49
  // add quantifiers modules
50
6054
  if (options::quantConflictFind())
51
  {
52
3605
    d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr));
53
3605
    modules.push_back(d_qcf.get());
54
  }
55
6054
  if (options::conjectureGen())
56
  {
57
12
    d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr));
58
12
    modules.push_back(d_sg_gen.get());
59
  }
60
6054
  if (!options::finiteModelFind() || options::fmfInstEngine())
61
  {
62
5828
    d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr));
63
5828
    modules.push_back(d_inst_engine.get());
64
  }
65
6054
  if (options::cegqi())
66
  {
67
5977
    d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr));
68
5977
    modules.push_back(d_i_cbqi.get());
69
5977
    qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
70
  }
71
6054
  if (options::sygus())
72
  {
73
2190
    d_synth_e.reset(new SynthEngine(qe, qs, qim, qr));
74
2190
    modules.push_back(d_synth_e.get());
75
  }
76
  // finite model finding
77
6054
  if (options::fmfBound())
78
  {
79
611
    d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, dm));
80
611
    modules.push_back(d_bint.get());
81
  }
82
6054
  if (options::finiteModelFind() || options::fmfBound())
83
  {
84
824
    d_model_engine.reset(new ModelEngine(qe, qs, qim, qr));
85
824
    modules.push_back(d_model_engine.get());
86
1648
    Trace("quant-init-debug")
87
1648
        << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
88
824
        << options::fmfBound() << std::endl;
89
824
    if (useFmcModel())
90
    {
91
810
      Trace("quant-init-debug") << "...make fmc builder." << std::endl;
92
810
      d_builder.reset(new fmcheck::FullModelChecker(qs, qr));
93
    }
94
    else
95
    {
96
28
      Trace("quant-init-debug")
97
14
          << "...make default model builder." << std::endl;
98
14
      d_builder.reset(new QModelBuilder(qs, qr));
99
    }
100
    // !!!!!!!!!!!!! temporary (project #15)
101
824
    d_builder->finishInit(qe);
102
  }
103
6054
  if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
104
  {
105
5008
    d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr));
106
5008
    modules.push_back(d_qsplit.get());
107
  }
108
12108
  if (options::quantAlphaEquiv())
109
  {
110
6054
    d_alpha_equiv.reset(new AlphaEquivalence(qe));
111
  }
112
  // full saturation : instantiate from relevant domain, then arbitrary terms
113
6054
  if (options::fullSaturateQuant() || options::fullSaturateInterleave())
114
  {
115
79
    d_rel_dom.reset(new RelevantDomain(qe, qr));
116
79
    d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get()));
117
79
    modules.push_back(d_fs.get());
118
  }
119
6054
  if (options::sygusInst())
120
  {
121
19
    d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr));
122
19
    modules.push_back(d_sygus_inst.get());
123
  }
124
6054
}
125
126
1664
bool QuantifiersModules::useFmcModel()
127
{
128
1664
  return options::mbqiMode() == options::MbqiMode::FMC
129
1250
         || options::mbqiMode() == options::MbqiMode::TRUST
130
2914
         || options::fmfBound();
131
}
132
133
}  // namespace quantifiers
134
}  // namespace theory
135
26685
}  // namespace CVC4