src/theory/model_manager_distributed.cpp

   1 /*********************                                                        */
   2 /*! \file model_manager_distributed.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 Management of a distributed approach for model generation.
  13  **/
  14
  15 #include "theory/model_manager_distributed.h"
  16
  17 #include "theory/theory_engine.h"
  18 #include "theory/theory_model.h"
  19
  20 namespace CVC4 {
  21 namespace theory {
  22
  23 ModelManagerDistributed::ModelManagerDistributed(TheoryEngine& te,
  24                                                  EqEngineManager& eem)
  25     : ModelManager(te, eem)
  26 {
  27 }
  28
  29 ModelManagerDistributed::~ModelManagerDistributed()
  30 {
  31   // pop the model context which we pushed on initialization
  32   d_modelEeContext.pop();
  33 }
  34
  35 void ModelManagerDistributed::initializeModelEqEngine(
  36     eq::EqualityEngineNotify* notify)
  37 {
  38   // initialize the model equality engine, use the provided notification object,
  39   // which belongs e.g. to CombinationModelBased
  40   EeSetupInfo esim;
  41   esim.d_notify = notify;
  42   esim.d_name = d_model->getName() + "::ee";
  43   esim.d_constantsAreTriggers = false;
  44   d_modelEqualityEngineAlloc.reset(
  45       d_eem.allocateEqualityEngine(esim, &d_modelEeContext));
  46   d_modelEqualityEngine = d_modelEqualityEngineAlloc.get();
  47   // finish initializing the model
  48   d_model->finishInit(d_modelEqualityEngine);
  49   // We push a context during initialization since the model is cleared during
  50   // collectModelInfo using pop/push.
  51   d_modelEeContext.push();
  52 }
  53
  54 bool ModelManagerDistributed::prepareModel()
  55 {
  56   Trace("model-builder") << "ModelManagerDistributed: reset model..."
  57                          << std::endl;
  58
  59   // push/pop to clear the equality engine of the model
  60   d_modelEeContext.pop();
  61   d_modelEeContext.push();
  62
  63   // Collect model info from the theories
  64   Trace("model-builder") << "ModelManagerDistributed: Collect model info..."
  65                          << std::endl;
  66   // Consult each active theory to get all relevant information concerning the
  67   // model, which includes both dump their equality information and assigning
  68   // values. Notice the order of theories here is important and is the same
  69   // as the list in CVC4_FOR_EACH_THEORY in theory_engine.cpp.
  70   for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
  71        ++theoryId)
  72   {
  73     if (!d_logicInfo.isTheoryEnabled(theoryId))
  74     {
  75       // theory not active, skip
  76       continue;
  77     }
  78     Theory* t = d_te.theoryOf(theoryId);
  79     Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId
  80                            << std::endl;
  81     if (!t->collectModelInfo(d_model))
  82     {
  83       Trace("model-builder")
  84           << "ModelManagerDistributed: fail collect model info" << std::endl;
  85       return false;
  86     }
  87   }
  88
  89   if (!collectModelBooleanVariables())
  90   {
  91     Trace("model-builder") << "ModelManagerDistributed: fail Boolean variables"
  92                            << std::endl;
  93     return false;
  94   }
  95
  96   return true;
  97 }
  98
  99 bool ModelManagerDistributed::finishBuildModel() const
 100 {
 101   // do not use relevant terms
 102   if (!d_modelBuilder->buildModel(d_model))
 103   {
 104     Trace("model-builder") << "ModelManager: fail build model" << std::endl;
 105     return false;
 106   }
 107   return true;
 108 }
 109
 110 }  // namespace theory
 111 }  // namespace CVC4