Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Mathias Preiner, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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                 :            :  * Implementation of quantifier relevance.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/quantifiers/quant_relevance.h"
      17                 :            : 
      18                 :            : using namespace std;
      19                 :            : using namespace cvc5::internal::kind;
      20                 :            : using namespace cvc5::context;
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : namespace quantifiers {
      25                 :            : 
      26                 :          5 : QuantRelevance::QuantRelevance(Env& env) : QuantifiersUtil(env) {}
      27                 :            : 
      28                 :        458 : void QuantRelevance::registerQuantifier(Node f)
      29                 :            : {
      30                 :            :   // compute symbols in f
      31                 :        458 :   std::vector<Node> syms;
      32                 :        458 :   computeSymbols(f[1], syms);
      33                 :        458 :   d_syms[f].insert(d_syms[f].begin(), syms.begin(), syms.end());
      34                 :        458 : }
      35                 :            : 
      36                 :            : /** compute symbols */
      37                 :      63331 : void QuantRelevance::computeSymbols(Node n, std::vector<Node>& syms)
      38                 :            : {
      39         [ +  + ]:      63331 :   if (n.getKind() == Kind::APPLY_UF)
      40                 :            :   {
      41                 :      69204 :     Node op = n.getOperator();
      42         [ +  + ]:      34602 :     if (std::find(syms.begin(), syms.end(), op) == syms.end())
      43                 :            :     {
      44                 :       2101 :       syms.push_back(op);
      45                 :            :     }
      46                 :            :   }
      47         [ +  + ]:      63331 :   if (n.getKind() != Kind::FORALL)
      48                 :            :   {
      49         [ +  + ]:     126120 :     for (int i = 0; i < (int)n.getNumChildren(); i++)
      50                 :            :     {
      51                 :      62873 :       computeSymbols(n[i], syms);
      52                 :            :     }
      53                 :            :   }
      54                 :      63331 : }
      55                 :            : 
      56                 :       1934 : size_t QuantRelevance::getNumQuantifiersForSymbol(Node s) const
      57                 :            : {
      58                 :       1934 :   std::map<Node, std::vector<Node> >::const_iterator it = d_syms_quants.find(s);
      59         [ +  - ]:       1934 :   if (it == d_syms_quants.end())
      60                 :            :   {
      61                 :       1934 :     return 0;
      62                 :            :   }
      63                 :          0 :   return it->second.size();
      64                 :            : }
      65                 :            : 
      66                 :            : }  // namespace quantifiers
      67                 :            : }  // namespace theory
      68                 :            : }  // namespace cvc5::internal