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                 :            :  * Implementation of model builder class.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/fmf/model_builder.h"
      14                 :            : 
      15                 :            : #include "options/quantifiers_options.h"
      16                 :            : #include "options/strings_options.h"
      17                 :            : #include "theory/quantifiers/first_order_model.h"
      18                 :            : #include "theory/quantifiers/fmf/model_engine.h"
      19                 :            : #include "theory/quantifiers/instantiate.h"
      20                 :            : #include "theory/quantifiers/quant_rep_bound_ext.h"
      21                 :            : #include "theory/quantifiers/quantifiers_state.h"
      22                 :            : 
      23                 :            : using namespace std;
      24                 :            : using namespace cvc5::internal;
      25                 :            : using namespace cvc5::internal::kind;
      26                 :            : using namespace cvc5::context;
      27                 :            : using namespace cvc5::internal::theory;
      28                 :            : using namespace cvc5::internal::theory::quantifiers;
      29                 :            : 
      30                 :      28906 : QModelBuilder::QModelBuilder(Env& env,
      31                 :            :                              QuantifiersState& qs,
      32                 :            :                              QuantifiersInferenceManager& qim,
      33                 :            :                              QuantifiersRegistry& qr,
      34                 :      28906 :                              TermRegistry& tr)
      35                 :            :     : TheoryEngineModelBuilder(env),
      36                 :      28906 :       d_addedLemmas(0),
      37                 :      28906 :       d_triedLemmas(0),
      38                 :      28906 :       d_qstate(qs),
      39                 :      28906 :       d_qim(qim),
      40                 :      28906 :       d_qreg(qr),
      41                 :      28906 :       d_treg(tr),
      42                 :      28906 :       d_model(nullptr)
      43                 :            : {
      44                 :      28906 : }
      45                 :            : 
      46                 :      14596 : void QModelBuilder::finishInit()
      47                 :            : {
      48                 :            :   // allocate the default model
      49                 :      14596 :   d_modelAloc.reset(new FirstOrderModel(d_env, d_qstate, d_qreg, d_treg));
      50                 :      14596 :   d_model = d_modelAloc.get();
      51                 :      14596 : }
      52                 :            : 
      53                 :      15186 : bool QModelBuilder::optUseModel()
      54                 :            : {
      55                 :      15186 :   return options().quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE
      56 [ +  + ][ +  + ]:      15186 :          || options().quantifiers.fmfBound || options().strings.stringExp;
                 [ +  - ]
      57                 :            : }
      58                 :            : 
      59                 :      15764 : bool QModelBuilder::preProcessBuildModel(TheoryModel* m)
      60                 :            : {
      61                 :      15764 :   return preProcessBuildModelStd(m);
      62                 :            : }
      63                 :            : 
      64                 :      28169 : bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m)
      65                 :            : {
      66                 :      28169 :   d_addedLemmas = 0;
      67                 :      28169 :   d_triedLemmas = 0;
      68         [ +  + ]:      28169 :   if (options().quantifiers.fmfFunWellDefinedRelevant)
      69                 :            :   {
      70                 :            :     // traverse equality engine
      71                 :         52 :     std::map<TypeNode, bool> eqc_usort;
      72                 :            :     eq::EqClassesIterator eqcs_i =
      73                 :         52 :         eq::EqClassesIterator(m->getEqualityEngine());
      74         [ +  + ]:       1181 :     while (!eqcs_i.isFinished())
      75                 :            :     {
      76                 :       1129 :       TypeNode tr = (*eqcs_i).getType();
      77                 :       1129 :       eqc_usort[tr] = true;
      78                 :       1129 :       ++eqcs_i;
      79                 :       1129 :     }
      80                 :            :     // look at quantified formulas
      81                 :        349 :     for (size_t i = 0, nquant = d_model->getNumAssertedQuantifiers();
      82         [ +  + ]:        349 :          i < nquant;
      83                 :            :          i++)
      84                 :            :     {
      85                 :        297 :       Node q = d_model->getAssertedQuantifier(i, true);
      86         [ +  - ]:        297 :       if (d_model->isQuantifierActive(q))
      87                 :            :       {
      88                 :            :         // check if any of these quantified formulas can be set inactive
      89         [ +  - ]:        297 :         if (q[0].getNumChildren() == 1)
      90                 :            :         {
      91                 :        594 :           TypeNode tn = q[0][0].getType();
      92         [ +  + ]:        297 :           if (tn.getAttribute(AbsTypeFunDefAttribute()))
      93                 :            :           {
      94                 :            :             // we are allowed to assume the introduced type is empty
      95         [ +  + ]:        279 :             if (eqc_usort.find(tn) == eqc_usort.end())
      96                 :            :             {
      97         [ +  - ]:        318 :               Trace("model-engine-debug")
      98                 :        159 :                   << "Irrelevant function definition : " << q << std::endl;
      99                 :        159 :               d_model->setQuantifierActive(q, false);
     100                 :            :             }
     101                 :            :           }
     102                 :        297 :         }
     103                 :            :       }
     104                 :        297 :     }
     105                 :         52 :   }
     106                 :      28169 :   return true;
     107                 :            : }
     108                 :            : 
     109                 :        540 : void QModelBuilder::debugModel(TheoryModel* m)
     110                 :            : {
     111                 :            :   // debug the model: cycle through all instantiations for all quantifiers,
     112                 :            :   // report ones that are not true
     113         [ -  + ]:        540 :   if (TraceIsOn("quant-check-model"))
     114                 :            :   {
     115                 :          0 :     FirstOrderModel* fm = d_model;
     116         [ -  - ]:          0 :     Trace("quant-check-model")
     117                 :          0 :         << "Testing quantifier instantiations..." << std::endl;
     118                 :          0 :     int tests = 0;
     119                 :          0 :     int bad = 0;
     120                 :          0 :     QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
     121                 :          0 :     Instantiate* inst = d_qim.getInstantiate();
     122         [ -  - ]:          0 :     for (size_t i = 0, nquant = fm->getNumAssertedQuantifiers(); i < nquant;
     123                 :            :          i++)
     124                 :            :     {
     125                 :          0 :       Node q = fm->getAssertedQuantifier(i);
     126                 :          0 :       std::vector<Node> vars(q[0].begin(), q[0].end());
     127                 :          0 :       QRepBoundExt qrbe(d_env, qbi, d_qstate, d_treg, q);
     128                 :          0 :       RepSetIterator riter(m->getRepSet(), &qrbe);
     129         [ -  - ]:          0 :       if (riter.setQuantifier(q))
     130                 :            :       {
     131         [ -  - ]:          0 :         while (!riter.isFinished())
     132                 :            :         {
     133                 :          0 :           tests++;
     134                 :          0 :           std::vector<Node> terms;
     135         [ -  - ]:          0 :           for (unsigned k = 0; k < riter.getNumTerms(); k++)
     136                 :            :           {
     137                 :          0 :             terms.push_back(riter.getCurrentTerm(k));
     138                 :            :           }
     139                 :          0 :           Node n = inst->getInstantiation(q, vars, terms);
     140                 :          0 :           Node val = m->getValue(n);
     141                 :          0 :           if (!val.isConst() || !val.getConst<bool>())
     142                 :            :           {
     143         [ -  - ]:          0 :             Trace("quant-check-model")
     144                 :          0 :                 << "*******  Instantiation " << n << " for " << std::endl;
     145         [ -  - ]:          0 :             Trace("quant-check-model") << "         " << q << std::endl;
     146         [ -  - ]:          0 :             Trace("quant-check-model")
     147                 :          0 :                 << "         Evaluates to " << val << std::endl;
     148                 :          0 :             bad++;
     149                 :            :           }
     150                 :          0 :           riter.increment();
     151                 :          0 :         }
     152         [ -  - ]:          0 :         Trace("quant-check-model") << "Tested " << tests << " instantiations";
     153         [ -  - ]:          0 :         if (bad > 0)
     154                 :            :         {
     155         [ -  - ]:          0 :           Trace("quant-check-model") << ", " << bad << " failed" << std::endl;
     156                 :            :         }
     157         [ -  - ]:          0 :         Trace("quant-check-model") << "." << std::endl;
     158                 :            :       }
     159         [ -  - ]:          0 :       else if (riter.isIncomplete())
     160                 :            :       {
     161         [ -  - ]:          0 :         Trace("quant-check-model")
     162                 :          0 :             << "Warning: Could not test quantifier " << q << std::endl;
     163                 :            :       }
     164                 :          0 :     }
     165                 :            :   }
     166                 :        540 : }
     167                 :      28906 : FirstOrderModel* QModelBuilder::getModel() { return d_model; }