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 quantifiers bound inference.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/quantifiers/quant_bound_inference.h"
      17                 :            : 
      18                 :            : #include "theory/quantifiers/fmf/bounded_integers.h"
      19                 :            : #include "util/rational.h"
      20                 :            : 
      21                 :            : using namespace cvc5::internal::kind;
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : namespace theory {
      25                 :            : namespace quantifiers {
      26                 :            : 
      27                 :      49208 : QuantifiersBoundInference::QuantifiersBoundInference(unsigned cardMax,
      28                 :      49208 :                                                      bool isFmf)
      29                 :      49208 :     : d_cardMax(cardMax), d_isFmf(isFmf), d_bint(nullptr)
      30                 :            : {
      31                 :      49208 : }
      32                 :            : 
      33                 :      42087 : void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; }
      34                 :            : 
      35                 :      16263 : bool QuantifiersBoundInference::mayComplete(TypeNode tn)
      36                 :            : {
      37                 :      16263 :   std::unordered_map<TypeNode, bool>::iterator it = d_may_complete.find(tn);
      38         [ +  + ]:      16263 :   if (it == d_may_complete.end())
      39                 :            :   {
      40                 :            :     // cache
      41                 :       1029 :     bool mc = mayComplete(tn, d_cardMax);
      42                 :       1029 :     d_may_complete[tn] = mc;
      43                 :       1029 :     return mc;
      44                 :            :   }
      45                 :      15234 :   return it->second;
      46                 :            : }
      47                 :            : 
      48                 :       1029 : bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
      49                 :            : {
      50         [ +  + ]:       1029 :   if (!tn.isClosedEnumerable())
      51                 :            :   {
      52                 :        443 :     return false;
      53                 :            :   }
      54                 :        586 :   bool mc = false;
      55                 :            :   // we cannot use FMF to complete interpreted types, thus we pass
      56                 :            :   // false for fmfEnabled here
      57         [ +  + ]:        586 :   if (isCardinalityClassFinite(tn.getCardinalityClass(), false))
      58                 :            :   {
      59                 :        194 :     Cardinality c = tn.getCardinality();
      60         [ +  + ]:         97 :     if (!c.isLargeFinite())
      61                 :            :     {
      62                 :            :       // check if less than fixed upper bound
      63                 :         91 :       mc = (c.getFiniteCardinality() < Integer(maxCard));
      64                 :            :     }
      65                 :            :   }
      66                 :        586 :   return mc;
      67                 :            : }
      68                 :            : 
      69                 :      11935 : bool QuantifiersBoundInference::isFiniteBound(Node q, Node v)
      70                 :            : {
      71                 :      11935 :   if (d_bint && d_bint->isBound(q, v))
      72                 :            :   {
      73                 :        100 :     return true;
      74                 :            :   }
      75                 :      23670 :   TypeNode tn = v.getType();
      76 [ +  + ][ +  + ]:      11835 :   if (tn.isUninterpretedSort() && d_isFmf)
                 [ +  + ]
      77                 :            :   {
      78                 :       1957 :     return true;
      79                 :            :   }
      80         [ +  + ]:       9878 :   else if (mayComplete(tn))
      81                 :            :   {
      82                 :        117 :     return true;
      83                 :            :   }
      84                 :       9761 :   return false;
      85                 :            : }
      86                 :            : 
      87                 :       6699 : BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v)
      88                 :            : {
      89         [ +  + ]:       6699 :   if (d_bint)
      90                 :            :   {
      91                 :       5926 :     BoundVarType bvt = d_bint->getBoundVarType(q, v);
      92                 :            :     // If the bounded integer module has a bound, use it. Otherwise, we fall
      93                 :            :     // through.
      94         [ +  + ]:       5926 :     if (bvt != BOUND_NONE)
      95                 :            :     {
      96                 :       4654 :       return bvt;
      97                 :            :     }
      98                 :            :   }
      99         [ +  + ]:       2045 :   return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
     100                 :            : }
     101                 :            : 
     102                 :       8377 : void QuantifiersBoundInference::getBoundVarIndices(
     103                 :            :     Node q, std::vector<size_t>& indices) const
     104                 :            : {
     105 [ -  + ][ -  + ]:       8377 :   Assert(indices.empty());
                 [ -  - ]
     106                 :            :   // we take the bounded variables first
     107         [ +  + ]:       8377 :   if (d_bint)
     108                 :            :   {
     109                 :       7908 :     d_bint->getBoundVarIndices(q, indices);
     110                 :            :   }
     111                 :            :   // then get the remaining ones
     112         [ +  + ]:      19659 :   for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
     113                 :            :   {
     114         [ +  + ]:      11282 :     if (std::find(indices.begin(), indices.end(), i) == indices.end())
     115                 :            :     {
     116                 :       4994 :       indices.push_back(i);
     117                 :            :     }
     118                 :            :   }
     119                 :       8377 : }
     120                 :            : 
     121                 :       3117 : bool QuantifiersBoundInference::getBoundElements(
     122                 :            :     RepSetIterator* rsi,
     123                 :            :     bool initial,
     124                 :            :     Node q,
     125                 :            :     Node v,
     126                 :            :     std::vector<Node>& elements) const
     127                 :            : {
     128         [ +  + ]:       3117 :   if (d_bint)
     129                 :            :   {
     130                 :       3109 :     return d_bint->getBoundElements(rsi, initial, q, v, elements);
     131                 :            :   }
     132                 :          8 :   return false;
     133                 :            : }
     134                 :            : 
     135                 :            : }  // namespace quantifiers
     136                 :            : }  // namespace theory
     137                 :            : }  // namespace cvc5::internal