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                 :            :  * Utilities for term enumeration.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/term_pools.h"
      14                 :            : 
      15                 :            : #include "theory/quantifiers/quantifiers_state.h"
      16                 :            : 
      17                 :            : namespace cvc5::internal {
      18                 :            : namespace theory {
      19                 :            : namespace quantifiers {
      20                 :            : 
      21                 :        263 : void TermPoolDomain::initialize() { d_terms.clear(); }
      22                 :            : 
      23                 :        124 : std::vector<Node>& TermPoolDomain::getTerms() { return d_terms; }
      24                 :            : 
      25                 :        481 : void TermPoolDomain::add(Node n)
      26                 :            : {
      27         [ +  + ]:        481 :   if (std::find(d_terms.begin(), d_terms.end(), n) == d_terms.end())
      28                 :            :   {
      29                 :        451 :     d_terms.push_back(n);
      30                 :            :   }
      31                 :        481 : }
      32                 :            : 
      33                 :      10919 : void TermPoolQuantInfo::initialize()
      34                 :            : {
      35                 :      10919 :   d_instAddToPool.clear();
      36                 :      10919 :   d_skolemAddToPool.clear();
      37                 :      10919 : }
      38                 :            : 
      39                 :      49952 : TermPools::TermPools(Env& env, QuantifiersState& qs)
      40                 :      49952 :     : QuantifiersUtil(env), d_qs(qs)
      41                 :            : {
      42                 :      49952 : }
      43                 :            : 
      44                 :      66665 : bool TermPools::reset(CVC5_UNUSED Theory::Effort e)
      45                 :            : {
      46         [ +  + ]:      66733 :   for (std::pair<const Node, TermPoolDomain>& p : d_pools)
      47                 :            :   {
      48                 :         68 :     p.second.d_currTerms.clear();
      49                 :            :   }
      50                 :      66665 :   return true;
      51                 :            : }
      52                 :            : 
      53                 :      53188 : void TermPools::registerQuantifier(Node q)
      54                 :            : {
      55         [ +  + ]:      53188 :   if (q.getNumChildren() < 3)
      56                 :            :   {
      57                 :      42269 :     return;
      58                 :            :   }
      59                 :      10919 :   TermPoolQuantInfo& qi = d_qinfo[q];
      60                 :      10919 :   qi.initialize();
      61         [ +  + ]:      22696 :   for (const Node& p : q[2])
      62                 :            :   {
      63                 :      11777 :     Kind pk = p.getKind();
      64         [ +  + ]:      11777 :     if (pk == Kind::INST_ADD_TO_POOL)
      65                 :            :     {
      66                 :         20 :       qi.d_instAddToPool.push_back(p);
      67                 :            :     }
      68         [ +  + ]:      11757 :     else if (pk == Kind::SKOLEM_ADD_TO_POOL)
      69                 :            :     {
      70                 :         14 :       qi.d_skolemAddToPool.push_back(p);
      71                 :            :     }
      72                 :      22696 :   }
      73 [ +  + ][ +  + ]:      10919 :   if (qi.d_instAddToPool.empty() && qi.d_skolemAddToPool.empty())
                 [ +  + ]
      74                 :            :   {
      75                 :      10895 :     d_qinfo.erase(q);
      76                 :            :   }
      77                 :            : }
      78                 :            : 
      79                 :          0 : std::string TermPools::identify() const { return "TermPools"; }
      80                 :            : 
      81                 :        263 : void TermPools::registerPool(Node p, const std::vector<Node>& initValue)
      82                 :            : {
      83                 :        263 :   TermPoolDomain& d = d_pools[p];
      84                 :        263 :   d.initialize();
      85         [ +  + ]:        655 :   for (const Node& i : initValue)
      86                 :            :   {
      87 [ -  + ][ -  + ]:        392 :     Assert(i.getType() == p.getType().getSetElementType());
                 [ -  - ]
      88                 :        392 :     d.add(i);
      89                 :            :   }
      90                 :        263 : }
      91                 :            : 
      92                 :        124 : void TermPools::getTermsForPool(Node p, std::vector<Node>& terms)
      93                 :            : {
      94                 :            :   // for now, we assume p is a variable
      95 [ -  + ][ -  + ]:        124 :   Assert(p.isVar());
                 [ -  - ]
      96                 :        124 :   TermPoolDomain& dom = d_pools[p];
      97                 :        124 :   std::vector<Node>& dterms = dom.getTerms();
      98         [ -  + ]:        124 :   if (dterms.empty())
      99                 :            :   {
     100                 :          0 :     return;
     101                 :            :   }
     102                 :            :   // if we have yet to compute terms on this round
     103         [ +  + ]:        124 :   if (dom.d_currTerms.empty())
     104                 :            :   {
     105                 :         39 :     std::unordered_set<Node> reps;
     106                 :            :     // eliminate modulo equality
     107         [ +  + ]:        150 :     for (const Node& t : dterms)
     108                 :            :     {
     109                 :        222 :       Node r = d_qs.getRepresentative(t);
     110                 :        111 :       const auto i = reps.insert(r);
     111         [ +  - ]:        111 :       if (i.second)
     112                 :            :       {
     113                 :        111 :         dom.d_currTerms.push_back(t);
     114                 :            :       }
     115                 :        111 :     }
     116         [ +  - ]:         78 :     Trace("pool-terms") << "* Domain for pool " << p << " is "
     117                 :         39 :                         << dom.d_currTerms << std::endl;
     118                 :         39 :   }
     119                 :        124 :   terms.insert(terms.end(), dom.d_currTerms.begin(), dom.d_currTerms.end());
     120                 :            : }
     121                 :            : 
     122                 :     180960 : void TermPools::processInstantiation(Node q, const std::vector<Node>& terms)
     123                 :            : {
     124                 :            :   // success is ignored, meaning that inst-add-to-pool annotates
     125                 :     180960 :   processInternal(q, terms, true);
     126                 :     180960 : }
     127                 :            : 
     128                 :       5788 : void TermPools::processSkolemization(Node q, const std::vector<Node>& skolems)
     129                 :            : {
     130                 :       5788 :   processInternal(q, skolems, false);
     131                 :       5788 : }
     132                 :            : 
     133                 :     186748 : void TermPools::processInternal(Node q,
     134                 :            :                                 const std::vector<Node>& ts,
     135                 :            :                                 bool isInst)
     136                 :            : {
     137 [ -  + ][ -  + ]:     186748 :   Assert(q.getKind() == Kind::FORALL);
                 [ -  - ]
     138                 :     186748 :   std::map<Node, TermPoolQuantInfo>::iterator it = d_qinfo.find(q);
     139         [ +  + ]:     186748 :   if (it == d_qinfo.end())
     140                 :            :   {
     141                 :            :     // does not impact
     142                 :     186678 :     return;
     143                 :            :   }
     144                 :        140 :   std::vector<Node> vars(q[0].begin(), q[0].end());
     145 [ -  + ][ -  + ]:         70 :   Assert(vars.size() == ts.size());
                 [ -  - ]
     146                 :            :   std::vector<Node>& cmds =
     147         [ +  + ]:         70 :       isInst ? it->second.d_instAddToPool : it->second.d_skolemAddToPool;
     148         [ +  + ]:        159 :   for (const Node& c : cmds)
     149                 :            :   {
     150 [ -  + ][ -  + ]:         89 :     Assert(c.getNumChildren() == 2);
                 [ -  - ]
     151                 :         89 :     Node t = c[0];
     152                 :            :     // substitute the term
     153                 :         89 :     Node st = t.substitute(vars.begin(), vars.end(), ts.begin(), ts.end());
     154                 :            :     // add to pool
     155         [ +  - ]:        178 :     Trace("pool-terms") << "Due to "
     156         [ -  - ]:          0 :                         << (isInst ? "instantiation" : "skolemization")
     157 [ -  + ][ -  - ]:         89 :                         << ", add " << st << " to pool " << c[1] << std::endl;
     158                 :         89 :     TermPoolDomain& dom = d_pools[c[1]];
     159                 :         89 :     dom.add(st);
     160                 :         89 :   }
     161                 :         70 : }
     162                 :            : 
     163                 :            : }  // namespace quantifiers
     164                 :            : }  // namespace theory
     165                 :            : }  // namespace cvc5::internal