Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Abstract management of models for TheoryEngine.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/model_manager.h"
      14                 :            : 
      15                 :            : #include "options/smt_options.h"
      16                 :            : #include "options/theory_options.h"
      17                 :            : #include "prop/prop_engine.h"
      18                 :            : #include "smt/env.h"
      19                 :            : #include "theory/quantifiers/first_order_model.h"
      20                 :            : #include "theory/quantifiers/fmf/model_builder.h"
      21                 :            : #include "theory/quantifiers_engine.h"
      22                 :            : #include "theory/theory_engine.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace theory {
      26                 :            : 
      27                 :      28664 : ModelManager::ModelManager(Env& env, TheoryEngine& te, EqEngineManager& eem)
      28                 :            :     : EnvObj(env),
      29                 :      28664 :       d_te(te),
      30                 :      28664 :       d_eem(eem),
      31                 :      28664 :       d_modelEqualityEngine(nullptr),
      32                 :      28664 :       d_modelEqualityEngineAlloc(nullptr),
      33                 :      57328 :       d_model(new TheoryModel(
      34                 :      28664 :           env, "DefaultModel", options().theory.assignFunctionValues)),
      35                 :      28664 :       d_modelBuilder(nullptr),
      36                 :      28664 :       d_modelBuilt(false),
      37                 :      57328 :       d_modelBuiltSuccess(false)
      38                 :            : {
      39                 :      28664 : }
      40                 :            : 
      41                 :      28651 : ModelManager::~ModelManager() {}
      42                 :            : 
      43                 :      28664 : void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
      44                 :            : {
      45                 :            :   // construct the model
      46                 :            :   // Initialize the model and model builder.
      47         [ +  + ]:      28664 :   if (logicInfo().isQuantified())
      48                 :            :   {
      49                 :      22259 :     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
      50 [ -  + ][ -  + ]:      22259 :     Assert(qe != nullptr);
                 [ -  - ]
      51                 :      22259 :     d_modelBuilder = qe->getModelBuilder();
      52                 :            :   }
      53                 :            : 
      54                 :            :   // make the default builder, e.g. in the case that the quantifiers engine does
      55                 :            :   // not have a model builder
      56         [ +  + ]:      28664 :   if (d_modelBuilder == nullptr)
      57                 :            :   {
      58                 :       6405 :     d_alocModelBuilder.reset(new TheoryEngineModelBuilder(d_env));
      59                 :       6405 :     d_modelBuilder = d_alocModelBuilder.get();
      60                 :            :   }
      61                 :            :   // notice that the equality engine of the model has yet to be assigned.
      62                 :      28664 :   initializeModelEqEngine(notify);
      63                 :      28664 : }
      64                 :            : 
      65                 :      45916 : void ModelManager::resetModel()
      66                 :            : {
      67                 :      45916 :   d_modelBuilt = false;
      68                 :      45916 :   d_modelBuiltSuccess = false;
      69                 :            :   // Reset basic information on the model object
      70                 :      45916 :   d_model->reset();
      71                 :      45916 : }
      72                 :            : 
      73                 :      56618 : bool ModelManager::buildModel()
      74                 :            : {
      75         [ +  + ]:      56618 :   if (d_modelBuilt)
      76                 :            :   {
      77                 :            :     // already computed
      78                 :      27401 :     return d_modelBuiltSuccess;
      79                 :            :   }
      80                 :            : 
      81                 :      29217 :   ResourceManager* rm = d_env.getResourceManager();
      82                 :            : 
      83                 :            :   // Disable resource manager limit while building the model. This ensures
      84                 :            :   // that building the model is not interrupted (and shouldn't take too
      85                 :            :   // long).
      86                 :      29217 :   rm->setEnabled(false);
      87                 :            : 
      88                 :            :   // reset the flags now
      89                 :      29217 :   d_modelBuilt = true;
      90                 :      29217 :   d_modelBuiltSuccess = false;
      91                 :            : 
      92                 :            :   // prepare the model, which is specific to the manager
      93         [ +  + ]:      29217 :   if (!prepareModel())
      94                 :            :   {
      95         [ +  - ]:        263 :     Trace("model-builder") << "ModelManager: fail prepare model" << std::endl;
      96                 :            :   }
      97                 :            :   else
      98                 :            :   {
      99                 :            :     // now, finish building the model
     100                 :      28954 :     d_modelBuiltSuccess = finishBuildModel();
     101                 :            : 
     102         [ -  + ]:      28954 :     if (TraceIsOn("model-final"))
     103                 :            :     {
     104         [ -  - ]:          0 :       Trace("model-final") << "Final model:" << std::endl;
     105                 :          0 :       Trace("model-final") << d_model->debugPrintModelEqc() << std::endl;
     106                 :            :     }
     107                 :            : 
     108         [ +  - ]:      57908 :     Trace("model-builder") << "ModelManager: model built success is "
     109                 :      28954 :                            << d_modelBuiltSuccess << std::endl;
     110                 :            :   }
     111                 :            : 
     112                 :            :   // Enable resource management again.
     113                 :      29217 :   rm->setEnabled(true);
     114                 :            : 
     115                 :      29217 :   return d_modelBuiltSuccess;
     116                 :            : }
     117                 :            : 
     118                 :          0 : bool ModelManager::isModelBuilt() const { return d_modelBuilt; }
     119                 :            : 
     120                 :      13723 : void ModelManager::postProcessModel(bool incomplete)
     121                 :            : {
     122         [ +  + ]:      13723 :   if (!d_modelBuilt)
     123                 :            :   {
     124                 :            :     // model not built, nothing to do
     125                 :      10033 :     return;
     126                 :            :   }
     127         [ +  - ]:       3690 :   Trace("model-builder") << "ModelManager: post-process model..." << std::endl;
     128                 :            :   // model construction should always succeed unless lemmas were added
     129 [ -  + ][ -  + ]:       3690 :   AlwaysAssert(d_modelBuiltSuccess);
                 [ -  - ]
     130         [ +  + ]:       3690 :   if (!options().smt.produceModels)
     131                 :            :   {
     132                 :       1122 :     return;
     133                 :            :   }
     134                 :            :   // Do post-processing of model from the theories (used for THEORY_SEP
     135                 :            :   // to construct heap model)
     136         [ +  + ]:      38520 :   for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
     137                 :      35952 :        ++theoryId)
     138                 :            :   {
     139                 :      35952 :     Theory* t = d_te.theoryOf(theoryId);
     140         [ -  + ]:      35952 :     if (t == nullptr)
     141                 :            :     {
     142                 :            :       // theory not active, skip
     143                 :          0 :       continue;
     144                 :            :     }
     145         [ +  - ]:      71904 :     Trace("model-builder-debug")
     146                 :      35952 :         << "  PostProcessModel on theory: " << theoryId << std::endl;
     147                 :      35952 :     t->postProcessModel(d_model.get());
     148                 :            :   }
     149                 :            :   // also call the model builder's post-process model
     150                 :       2568 :   d_modelBuilder->postProcessModel(incomplete, d_model.get());
     151                 :            : }
     152                 :            : 
     153                 :    1308450 : theory::TheoryModel* ModelManager::getModel() { return d_model.get(); }
     154                 :            : 
     155                 :      28954 : bool ModelManager::collectModelBooleanVariables()
     156                 :            : {
     157         [ +  - ]:      28954 :   Trace("model-builder") << "  CollectModelInfo boolean variables" << std::endl;
     158                 :            :   // Get value of the Boolean variables
     159                 :      28954 :   prop::PropEngine* propEngine = d_te.getPropEngine();
     160                 :      28954 :   std::vector<TNode> boolVars;
     161                 :      28954 :   propEngine->getBooleanVariables(boolVars);
     162                 :      28954 :   std::vector<TNode>::iterator it, iend = boolVars.end();
     163                 :            :   bool hasValue, value;
     164         [ +  + ]:     107234 :   for (it = boolVars.begin(); it != iend; ++it)
     165                 :            :   {
     166                 :      78280 :     TNode var = *it;
     167                 :      78280 :     hasValue = propEngine->hasValue(var, value);
     168                 :            :     // Should we assert that hasValue is true?
     169         [ +  + ]:      78280 :     if (!hasValue)
     170                 :            :     {
     171         [ +  - ]:      31724 :       Trace("model-builder-assertions")
     172                 :      15862 :           << "    has no value : " << var << std::endl;
     173                 :      15862 :       value = false;
     174                 :            :     }
     175         [ +  - ]:     156560 :     Trace("model-builder-assertions")
     176         [ -  - ]:          0 :         << "(assert" << (value ? " " : " (not ") << var
     177         [ -  - ]:      78280 :         << (value ? ");" : "));") << std::endl;
     178         [ -  + ]:      78280 :     if (!d_model->assertPredicate(var, value))
     179                 :            :     {
     180                 :          0 :       return false;
     181                 :            :     }
     182         [ +  - ]:      78280 :   }
     183                 :      28954 :   return true;
     184                 :      28954 : }
     185                 :            : 
     186                 :            : }  // namespace theory
     187                 :            : }  // namespace cvc5::internal