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                 :            :  * [[ Add one-line brief description here ]]
      11                 :            :  *
      12                 :            :  * [[ Add lengthier description here ]]
      13                 :            :  * \todo document this file
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/atom_requests.h"
      17                 :            : 
      18                 :            : using namespace cvc5::internal;
      19                 :            : 
      20                 :      50915 : AtomRequests::AtomRequests(context::Context* context)
      21                 :      50915 :     : d_allRequests(context),
      22                 :      50915 :       d_requests(context),
      23                 :      50915 :       d_triggerToRequestMap(context)
      24                 :            : {
      25                 :      50915 : }
      26                 :            : 
      27                 :    9231085 : AtomRequests::element_index AtomRequests::getList(TNode trigger) const
      28                 :            : {
      29                 :            :   trigger_to_list_map::const_iterator find =
      30                 :    9231085 :       d_triggerToRequestMap.find(trigger);
      31         [ +  + ]:    9231085 :   if (find == d_triggerToRequestMap.end())
      32                 :            :   {
      33                 :    9194020 :     return null_index;
      34                 :            :   }
      35                 :            :   else
      36                 :            :   {
      37                 :      37065 :     return (*find).second;
      38                 :            :   }
      39                 :            : }
      40                 :            : 
      41                 :          0 : bool AtomRequests::isTrigger(TNode atom) const
      42                 :            : {
      43                 :          0 :   return getList(atom) != null_index;
      44                 :            : }
      45                 :            : 
      46                 :    9218439 : AtomRequests::atom_iterator AtomRequests::getAtomIterator(TNode trigger) const
      47                 :            : {
      48                 :    9218439 :   return atom_iterator(*this, getList(trigger));
      49                 :            : }
      50                 :            : 
      51                 :      12646 : void AtomRequests::add(TNode triggerAtom,
      52                 :            :                        TNode atomToSend,
      53                 :            :                        theory::TheoryId toTheory)
      54                 :            : {
      55         [ +  - ]:      25292 :   Trace("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", "
      56                 :      12646 :                          << atomToSend << ", " << toTheory << ")" << std::endl;
      57                 :            : 
      58                 :      12646 :   Request request(atomToSend, toTheory);
      59                 :            : 
      60         [ -  + ]:      12646 :   if (d_allRequests.find(request) != d_allRequests.end())
      61                 :            :   {
      62                 :            :     // Have it already
      63         [ -  - ]:          0 :     Trace("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", "
      64                 :          0 :                            << atomToSend << ", " << toTheory
      65                 :          0 :                            << "): already there" << std::endl;
      66                 :          0 :     return;
      67                 :            :   }
      68         [ +  - ]:      25292 :   Trace("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", "
      69                 :          0 :                          << atomToSend << ", " << toTheory << "): adding"
      70                 :      12646 :                          << std::endl;
      71                 :            : 
      72                 :            :   /// Mark the new request
      73                 :      12646 :   d_allRequests.insert(request);
      74                 :            : 
      75                 :            :   // Index of the new request in the list of trigger
      76                 :      12646 :   element_index index = d_requests.size();
      77                 :      12646 :   element_index previous = getList(triggerAtom);
      78                 :      12646 :   d_requests.push_back(Element(request, previous));
      79                 :      12646 :   d_triggerToRequestMap[triggerAtom] = index;
      80         [ +  - ]:      12646 : }
      81                 :            : 
      82                 :    9260656 : bool AtomRequests::atom_iterator::done() const { return d_index == null_index; }
      83                 :            : 
      84                 :      42217 : void AtomRequests::atom_iterator::next()
      85                 :            : {
      86                 :      42217 :   d_index = d_requests.d_requests[d_index].d_previous;
      87                 :      42217 : }
      88                 :            : 
      89                 :      42217 : const AtomRequests::Request& AtomRequests::atom_iterator::get() const
      90                 :            : {
      91                 :      42217 :   return d_requests.d_requests[d_index].d_request;
      92                 :            : }