Branch data     Line data    Source code

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