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