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                 :            :  * Utility functions for relations.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "rels_utils.h"
      14                 :            : 
      15                 :            : #include "expr/dtype.h"
      16                 :            : #include "expr/dtype_cons.h"
      17                 :            : #include "theory/datatypes/project_op.h"
      18                 :            : #include "theory/datatypes/tuple_utils.h"
      19                 :            : #include "theory/sets/normal_form.h"
      20                 :            : #include "theory/sets/set_reduction.h"
      21                 :            : 
      22                 :            : using namespace cvc5::internal::kind;
      23                 :            : using namespace cvc5::internal::theory::datatypes;
      24                 :            : using namespace cvc5::internal::theory::sets;
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace theory {
      28                 :            : namespace sets {
      29                 :            : 
      30                 :          9 : std::set<Node> RelsUtils::computeTC(const std::set<Node>& members, Node rel)
      31                 :            : {
      32                 :          9 :   std::set<Node>::iterator mem_it = members.begin();
      33                 :          9 :   std::map<Node, int> ele_num_map;
      34                 :          9 :   std::set<Node> tc_rel_mem;
      35                 :            : 
      36         [ +  + ]:         29 :   while (mem_it != members.end())
      37                 :            :   {
      38                 :         20 :     Node fst = TupleUtils::nthElementOfTuple(*mem_it, 0);
      39                 :         20 :     Node snd = TupleUtils::nthElementOfTuple(*mem_it, 1);
      40                 :         20 :     std::set<Node> traversed;
      41                 :         20 :     traversed.insert(fst);
      42                 :         20 :     computeTC(rel, members, fst, snd, traversed, tc_rel_mem);
      43                 :         20 :     mem_it++;
      44                 :         20 :   }
      45                 :         18 :   return tc_rel_mem;
      46                 :          9 : }
      47                 :            : 
      48                 :         37 : void RelsUtils::computeTC(Node rel,
      49                 :            :                           const std::set<Node>& members,
      50                 :            :                           Node a,
      51                 :            :                           Node b,
      52                 :            :                           std::set<Node>& traversed,
      53                 :            :                           std::set<Node>& transitiveClosureMembers)
      54                 :            : {
      55                 :         37 :   transitiveClosureMembers.insert(constructPair(rel, a, b));
      56         [ +  + ]:         37 :   if (traversed.find(b) != traversed.end())
      57                 :            :   {
      58                 :          3 :     return;
      59                 :            :   }
      60                 :         34 :   traversed.insert(b);
      61                 :         34 :   std::set<Node>::iterator mem_it = members.begin();
      62         [ +  + ]:        151 :   while (mem_it != members.end())
      63                 :            :   {
      64                 :        117 :     Node new_fst = TupleUtils::nthElementOfTuple(*mem_it, 0);
      65                 :        117 :     Node new_snd = TupleUtils::nthElementOfTuple(*mem_it, 1);
      66         [ +  + ]:        117 :     if (b == new_fst)
      67                 :            :     {
      68                 :         17 :       computeTC(rel, members, a, new_snd, traversed, transitiveClosureMembers);
      69                 :            :     }
      70                 :        117 :     mem_it++;
      71                 :        117 :   }
      72                 :            : }
      73                 :            : 
      74                 :       2400 : Node RelsUtils::constructPair(Node rel, Node a, Node b)
      75                 :            : {
      76                 :       2400 :   const DType& dt = rel.getType().getSetElementType().getDType();
      77                 :            :   return NodeManager::mkNode(
      78                 :       2400 :       Kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
      79                 :            : }
      80                 :            : 
      81                 :         17 : Node RelsUtils::evaluateGroup(TNode n)
      82                 :            : {
      83 [ -  + ][ -  + ]:         17 :   Assert(n.getKind() == Kind::RELATION_GROUP);
                 [ -  - ]
      84                 :            : 
      85                 :         17 :   Node A = n[0];
      86                 :         17 :   TypeNode setType = A.getType();
      87                 :         17 :   TypeNode partitionType = n.getType();
      88                 :            : 
      89         [ -  + ]:         17 :   if (A.getKind() == Kind::SET_EMPTY)
      90                 :            :   {
      91                 :            :     // return a nonempty partition
      92                 :          0 :     return NodeManager::mkNode(Kind::SET_SINGLETON, A);
      93                 :            :   }
      94                 :            : 
      95                 :            :   std::vector<uint32_t> indices =
      96                 :         17 :       n.getOperator().getConst<ProjectOp>().getIndices();
      97                 :            : 
      98                 :         17 :   std::set<Node> elements = NormalForm::getElementsFromNormalConstant(A);
      99         [ +  - ]:         17 :   Trace("sets-group") << "elements: " << elements << std::endl;
     100                 :            :   // a simple map from elements to equivalent classes with this invariant:
     101                 :            :   // each key element must appear exactly once in one of the values.
     102                 :         17 :   std::map<Node, std::set<Node>> sets;
     103                 :         17 :   std::set<Node> emptyClass;
     104         [ +  + ]:        127 :   for (const Node& element : elements)
     105                 :            :   {
     106                 :            :     // initially each singleton element is an equivalence class
     107                 :        220 :     sets[element] = {element};
     108                 :            :   }
     109         [ +  + ]:        127 :   for (std::set<Node>::iterator i = elements.begin(); i != elements.end(); ++i)
     110                 :            :   {
     111                 :        110 :     Node iElement = *i;
     112         [ +  + ]:        110 :     if (sets[iElement].empty())
     113                 :            :     {
     114                 :            :       // skip this element since its equivalent class has already been processed
     115                 :         63 :       continue;
     116                 :            :     }
     117                 :         47 :     std::set<Node>::iterator j = i;
     118                 :         47 :     ++j;
     119         [ +  + ]:        230 :     while (j != elements.end())
     120                 :            :     {
     121                 :        183 :       Node jElement = *j;
     122         [ +  + ]:        183 :       if (TupleUtils::sameProjection(indices, iElement, jElement))
     123                 :            :       {
     124                 :            :         // add element j to the equivalent class
     125                 :         63 :         sets[iElement].insert(jElement);
     126                 :            :         // mark the equivalent class of j as processed
     127                 :         63 :         sets[jElement] = emptyClass;
     128                 :            :       }
     129                 :        183 :       ++j;
     130                 :        183 :     }
     131         [ +  + ]:        110 :   }
     132                 :            : 
     133                 :            :   // construct the partition parts
     134                 :         17 :   std::set<Node> parts;
     135         [ +  + ]:        127 :   for (std::pair<Node, std::set<Node>> pair : sets)
     136                 :            :   {
     137                 :        110 :     const std::set<Node>& eqc = pair.second;
     138         [ +  + ]:        110 :     if (eqc.empty())
     139                 :            :     {
     140                 :         63 :       continue;
     141                 :            :     }
     142                 :         47 :     Node part = NormalForm::elementsToSet(eqc, setType);
     143                 :         47 :     parts.insert(part);
     144         [ +  + ]:        110 :   }
     145                 :         17 :   Node ret = NormalForm::elementsToSet(parts, partitionType);
     146         [ +  - ]:         17 :   Trace("sets-group") << "ret: " << ret << std::endl;
     147                 :         17 :   return ret;
     148                 :         17 : }
     149                 :            : 
     150                 :          2 : Node RelsUtils::evaluateRelationAggregate(TNode n)
     151                 :            : {
     152 [ -  + ][ -  + ]:          2 :   Assert(n.getKind() == Kind::RELATION_AGGREGATE);
                 [ -  - ]
     153                 :          2 :   if (!(n[1].isConst() && n[2].isConst()))
     154                 :            :   {
     155                 :            :     // we can't proceed further.
     156                 :          0 :     return n;
     157                 :            :   }
     158                 :            : 
     159                 :          2 :   Node reduction = SetReduction::reduceAggregateOperator(n);
     160                 :          2 :   return reduction;
     161                 :          2 : }
     162                 :            : 
     163                 :            : }  // namespace sets
     164                 :            : }  // namespace theory
     165                 :            : }  // namespace cvc5::internal