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