src/theory/quantifiers/quantifiers_modules.cpp

   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/relevant_domain.h"
  19 #include "theory/quantifiers/term_registry.h"
  20 #include "theory/quantifiers_engine.h"
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace quantifiers {
  25
  26 QuantifiersModules::QuantifiersModules()
  27     : d_rel_dom(nullptr),
  28       d_alpha_equiv(nullptr),
  29       d_inst_engine(nullptr),
  30       d_model_engine(nullptr),
  31       d_builder(nullptr),
  32       d_bint(nullptr),
  33       d_qcf(nullptr),
  34       d_sg_gen(nullptr),
  35       d_synth_e(nullptr),
  36       d_fs(nullptr),
  37       d_i_cbqi(nullptr),
  38       d_qsplit(nullptr),
  39       d_sygus_inst(nullptr)
  40 {
  41 }
  42 QuantifiersModules::~QuantifiersModules() {}
  43 void QuantifiersModules::initialize(QuantifiersEngine* qe,
  44                                     QuantifiersState& qs,
  45                                     QuantifiersInferenceManager& qim,
  46                                     QuantifiersRegistry& qr,
  47                                     TermRegistry& tr,
  48                                     DecisionManager* dm,
  49                                     std::vector<QuantifiersModule*>& modules)
  50 {
  51   // add quantifiers modules
  52   if (options::quantConflictFind())
  53   {
  54     d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr));
  55     modules.push_back(d_qcf.get());
  56   }
  57   if (options::conjectureGen())
  58   {
  59     d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr));
  60     modules.push_back(d_sg_gen.get());
  61   }
  62   if (!options::finiteModelFind() || options::fmfInstEngine())
  63   {
  64     d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr, tr));
  65     modules.push_back(d_inst_engine.get());
  66   }
  67   if (options::cegqi())
  68   {
  69     d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr));
  70     modules.push_back(d_i_cbqi.get());
  71     qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
  72   }
  73   if (options::sygus())
  74   {
  75     d_synth_e.reset(new SynthEngine(qe, qs, qim, qr));
  76     modules.push_back(d_synth_e.get());
  77   }
  78   // finite model finding
  79   if (options::fmfBound())
  80   {
  81     d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, dm));
  82     modules.push_back(d_bint.get());
  83   }
  84   if (options::finiteModelFind() || options::fmfBound())
  85   {
  86     d_model_engine.reset(new ModelEngine(qe, qs, qim, qr));
  87     modules.push_back(d_model_engine.get());
  88     Trace("quant-init-debug")
  89         << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
  90         << options::fmfBound() << std::endl;
  91     if (tr.useFmcModel())
  92     {
  93       Trace("quant-init-debug") << "...make fmc builder." << std::endl;
  94       d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim));
  95     }
  96     else
  97     {
  98       Trace("quant-init-debug")
  99           << "...make default model builder." << std::endl;
 100       d_builder.reset(new QModelBuilder(qs, qr, qim));
 101     }
 102   }
 103   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
 104   {
 105     d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr));
 106     modules.push_back(d_qsplit.get());
 107   }
 108   if (options::quantAlphaEquiv())
 109   {
 110     d_alpha_equiv.reset(new AlphaEquivalence(qe));
 111   }
 112   // full saturation : instantiate from relevant domain, then arbitrary terms
 113   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
 114   {
 115     d_rel_dom.reset(new RelevantDomain(qe, qr));
 116     d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get()));
 117     modules.push_back(d_fs.get());
 118   }
 119   if (options::sygusInst())
 120   {
 121     d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr));
 122     modules.push_back(d_sygus_inst.get());
 123   }
 124 }
 125
 126 }  // namespace quantifiers
 127 }  // namespace theory
 128 }  // namespace CVC4