src/theory/model_manager.cpp

   1 /*********************                                                        */
   2 /*! \file model_manager.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 Abstract management of models for TheoryEngine.
  13  **/
  14
  15 #include "theory/model_manager.h"
  16
  17 #include "options/theory_options.h"
  18 #include "theory/quantifiers_engine.h"
  19 #include "theory/theory_engine.h"
  20
  21 namespace CVC4 {
  22 namespace theory {
  23
  24 ModelManager::ModelManager(TheoryEngine& te, EqEngineManager& eem)
  25     : d_te(te),
  26       d_logicInfo(te.getLogicInfo()),
  27       d_eem(eem),
  28       d_modelEqualityEngine(nullptr),
  29       d_modelEqualityEngineAlloc(nullptr),
  30       d_model(nullptr),
  31       d_modelBuilder(nullptr),
  32       d_modelBuilt(false),
  33       d_modelBuiltSuccess(false)
  34 {
  35 }
  36
  37 ModelManager::~ModelManager() {}
  38
  39 void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
  40 {
  41   // construct the model
  42   const LogicInfo& logicInfo = d_te.getLogicInfo();
  43   // Initialize the model and model builder.
  44   if (logicInfo.isQuantified())
  45   {
  46     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
  47     Assert(qe != nullptr);
  48     d_modelBuilder = qe->getModelBuilder();
  49     d_model = qe->getModel();
  50   }
  51   else
  52   {
  53     context::Context* u = d_te.getUserContext();
  54     d_alocModel.reset(
  55         new TheoryModel(u, "DefaultModel", options::assignFunctionValues()));
  56     d_model = d_alocModel.get();
  57   }
  58
  59   // make the default builder, e.g. in the case that the quantifiers engine does
  60   // not have a model builder
  61   if (d_modelBuilder == nullptr)
  62   {
  63     d_alocModelBuilder.reset(new TheoryEngineModelBuilder(&d_te));
  64     d_modelBuilder = d_alocModelBuilder.get();
  65   }
  66   // notice that the equality engine of the model has yet to be assigned.
  67   initializeModelEqEngine(notify);
  68 }
  69
  70 void ModelManager::resetModel()
  71 {
  72   d_modelBuilt = false;
  73   d_modelBuiltSuccess = false;
  74   // Reset basic information on the model object
  75   d_model->reset();
  76 }
  77
  78 bool ModelManager::buildModel()
  79 {
  80   if (d_modelBuilt)
  81   {
  82     // already computed
  83     return d_modelBuiltSuccess;
  84   }
  85   // reset the flags now
  86   d_modelBuilt = true;
  87   d_modelBuiltSuccess = false;
  88
  89   // prepare the model, which is specific to the manager
  90   if (!prepareModel())
  91   {
  92     Trace("model-builder") << "ModelManager: fail prepare model" << std::endl;
  93     return false;
  94   }
  95
  96   // now, finish building the model
  97   d_modelBuiltSuccess = finishBuildModel();
  98   return d_modelBuiltSuccess;
  99 }
 100
 101 bool ModelManager::isModelBuilt() const { return d_modelBuilt; }
 102
 103 void ModelManager::postProcessModel(bool incomplete)
 104 {
 105   if (!d_modelBuilt)
 106   {
 107     // model not built, nothing to do
 108     return;
 109   }
 110   Trace("model-builder") << "ModelManager: post-process model..." << std::endl;
 111   // model construction should always succeed unless lemmas were added
 112   AlwaysAssert(d_modelBuiltSuccess);
 113   if (!options::produceModels())
 114   {
 115     return;
 116   }
 117   // Do post-processing of model from the theories (used for THEORY_SEP
 118   // to construct heap model)
 119   for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
 120        ++theoryId)
 121   {
 122     Theory* t = d_te.theoryOf(theoryId);
 123     if (t == nullptr)
 124     {
 125       // theory not active, skip
 126       continue;
 127     }
 128     Trace("model-builder-debug")
 129         << "  PostProcessModel on theory: " << theoryId << std::endl;
 130     t->postProcessModel(d_model);
 131   }
 132   // also call the model builder's post-process model
 133   d_modelBuilder->postProcessModel(incomplete, d_model);
 134 }
 135
 136 theory::TheoryModel* ModelManager::getModel() { return d_model; }
 137
 138 bool ModelManager::collectModelBooleanVariables()
 139 {
 140   Trace("model-builder") << "  CollectModelInfo boolean variables" << std::endl;
 141   // Get value of the Boolean variables
 142   prop::PropEngine* propEngine = d_te.getPropEngine();
 143   std::vector<TNode> boolVars;
 144   propEngine->getBooleanVariables(boolVars);
 145   std::vector<TNode>::iterator it, iend = boolVars.end();
 146   bool hasValue, value;
 147   for (it = boolVars.begin(); it != iend; ++it)
 148   {
 149     TNode var = *it;
 150     hasValue = propEngine->hasValue(var, value);
 151     // Should we assert that hasValue is true?
 152     if (!hasValue)
 153     {
 154       Trace("model-builder-assertions")
 155           << "    has no value : " << var << std::endl;
 156       value = false;
 157     }
 158     Trace("model-builder-assertions")
 159         << "(assert" << (value ? " " : " (not ") << var
 160         << (value ? ");" : "));") << std::endl;
 161     if (!d_model->assertPredicate(var, value))
 162     {
 163       return false;
 164     }
 165   }
 166   return true;
 167 }
 168
 169 void ModelManager::collectAssertedTerms(TheoryId tid,
 170                                         std::set<Node>& termSet,
 171                                         bool includeShared) const
 172 {
 173   Theory* t = d_te.theoryOf(tid);
 174   // Collect all terms appearing in assertions
 175   context::CDList<Assertion>::const_iterator assert_it = t->facts_begin(),
 176                                              assert_it_end = t->facts_end();
 177   for (; assert_it != assert_it_end; ++assert_it)
 178   {
 179     collectTerms(tid, *assert_it, termSet);
 180   }
 181
 182   if (includeShared)
 183   {
 184     // Add terms that are shared terms
 185     context::CDList<TNode>::const_iterator shared_it = t->shared_terms_begin(),
 186                                            shared_it_end =
 187                                                t->shared_terms_end();
 188     for (; shared_it != shared_it_end; ++shared_it)
 189     {
 190       collectTerms(tid, *shared_it, termSet);
 191     }
 192   }
 193 }
 194
 195 void ModelManager::collectTerms(TheoryId tid,
 196                                 TNode n,
 197                                 std::set<Node>& termSet) const
 198 {
 199   const std::set<Kind>& irrKinds = d_model->getIrrelevantKinds();
 200   std::vector<TNode> visit;
 201   TNode cur;
 202   visit.push_back(n);
 203   do
 204   {
 205     cur = visit.back();
 206     visit.pop_back();
 207     if (termSet.find(cur) != termSet.end())
 208     {
 209       // already visited
 210       continue;
 211     }
 212     Kind k = cur.getKind();
 213     // only add to term set if a relevant kind
 214     if (irrKinds.find(k) == irrKinds.end())
 215     {
 216       termSet.insert(cur);
 217     }
 218     // traverse owned terms, don't go under quantifiers
 219     if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == tid)
 220         && !cur.isClosure())
 221     {
 222       visit.insert(visit.end(), cur.begin(), cur.end());
 223     }
 224   } while (!visit.empty());
 225 }
 226
 227 }  // namespace theory
 228 }  // namespace CVC4