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                 :            :  * Implementation of assertion list
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "decision/assertion_list.h"
      14                 :            : 
      15                 :            : namespace cvc5::internal {
      16                 :            : namespace decision {
      17                 :            : 
      18                 :          0 : const char* toString(DecisionStatus s)
      19                 :            : {
      20 [ -  - ][ -  - ]:          0 :   switch (s)
                    [ - ]
      21                 :            :   {
      22                 :          0 :     case DecisionStatus::INACTIVE: return "INACTIVE";
      23                 :          0 :     case DecisionStatus::NO_DECISION: return "NO_DECISION";
      24                 :          0 :     case DecisionStatus::DECISION: return "DECISION";
      25                 :          0 :     case DecisionStatus::BACKTRACK: return "BACKTRACK";
      26                 :          0 :     default: return "?";
      27                 :            :   }
      28                 :            : }
      29                 :            : 
      30                 :          0 : std::ostream& operator<<(std::ostream& out, DecisionStatus s)
      31                 :            : {
      32                 :          0 :   out << toString(s);
      33                 :          0 :   return out;
      34                 :            : }
      35                 :            : 
      36                 :      41696 : AssertionList::AssertionList(context::Context* ac,
      37                 :            :                              context::Context* ic,
      38                 :      41696 :                              bool useDyn)
      39                 :          0 :     : d_assertions(ac),
      40                 :      41696 :       d_assertionIndex(ic),
      41                 :      41696 :       d_usingDynamic(useDyn),
      42                 :      83392 :       d_dindex(ic)
      43                 :            : {
      44                 :      41696 : }
      45                 :            : 
      46                 :      43726 : void AssertionList::presolve()
      47                 :            : {
      48         [ +  - ]:      43726 :   Trace("jh-status") << "AssertionList::presolve" << std::endl;
      49                 :      43726 :   d_assertionIndex = 0;
      50                 :      43726 :   d_dlist.clear();
      51                 :      43726 :   d_dindex = 0;
      52                 :      43726 : }
      53                 :            : 
      54                 :    1482421 : void AssertionList::addAssertion(TNode n) { d_assertions.push_back(n); }
      55                 :            : 
      56                 :   56700196 : TNode AssertionList::getNextAssertion()
      57                 :            : {
      58                 :            :   size_t fromIndex;
      59         [ +  + ]:   56700196 :   if (d_usingDynamic)
      60                 :            :   {
      61                 :            :     // is a dynamic assertion ready?
      62                 :      26256 :     fromIndex = d_dindex.get();
      63         [ +  + ]:      26256 :     if (fromIndex < d_dlist.size())
      64                 :            :     {
      65                 :       8792 :       d_dindex = d_dindex.get() + 1;
      66         [ +  - ]:      17584 :       Trace("jh-status") << "Assertion " << d_dlist[fromIndex].getId()
      67                 :       8792 :                          << " from dynamic list" << std::endl;
      68                 :       8792 :       return d_dlist[fromIndex];
      69                 :            :     }
      70                 :            :   }
      71                 :            :   // check if dynamic assertions
      72                 :   56691404 :   fromIndex = d_assertionIndex.get();
      73 [ -  + ][ -  + ]:   56691404 :   Assert(fromIndex <= d_assertions.size());
                 [ -  - ]
      74         [ +  + ]:   56691404 :   if (fromIndex == d_assertions.size())
      75                 :            :   {
      76                 :   54806676 :     return Node::null();
      77                 :            :   }
      78                 :            :   // increment for the next iteration
      79                 :   29288066 :   d_assertionIndex = d_assertionIndex + 1;
      80         [ +  - ]:   58576132 :   Trace("jh-status") << "Assertion " << d_assertions[fromIndex].getId()
      81                 :   29288066 :                      << std::endl;
      82                 :   29288066 :   return d_assertions[fromIndex];
      83                 :            : }
      84                 :    1482421 : size_t AssertionList::size() const { return d_assertions.size(); }
      85                 :            : 
      86                 :   27427662 : void AssertionList::notifyStatus(TNode n, DecisionStatus s)
      87                 :            : {
      88         [ +  - ]:   54855324 :   Trace("jh-status") << "Assertion status " << s << " for " << n.getId()
      89                 :   27427662 :                      << ", current " << d_dindex.get() << "/" << d_dlist.size()
      90                 :   27427662 :                      << std::endl;
      91         [ +  + ]:   27427662 :   if (!d_usingDynamic)
      92                 :            :   {
      93                 :            :     // not using dynamic ordering, return
      94                 :   27426947 :     return;
      95                 :            :   }
      96         [ +  + ]:      26095 :   if (s == DecisionStatus::NO_DECISION)
      97                 :            :   {
      98                 :            :     // no decision does not impact the decision order
      99                 :      23626 :     return;
     100                 :            :   }
     101                 :       2469 :   std::unordered_set<TNode>::iterator it = d_dlistSet.find(n);
     102         [ +  + ]:       2469 :   if (s == DecisionStatus::DECISION)
     103                 :            :   {
     104         [ +  + ]:       1754 :     if (it == d_dlistSet.end())
     105                 :            :     {
     106                 :            :       // if we just had a status on an assertion and it didn't occur in dlist,
     107                 :            :       // then our index should have exhausted dlist
     108 [ -  + ][ -  + ]:        192 :       Assert(d_dindex.get() == d_dlist.size());
                 [ -  - ]
     109         [ +  - ]:        192 :       if (d_dindex.get() == d_dlist.size())
     110                 :            :       {
     111                 :        192 :         d_dindex = d_dindex.get() + 1;
     112                 :            :       }
     113                 :            :       // add to back of the decision list if not already there
     114                 :        192 :       d_dlist.push_back(n);
     115                 :        192 :       d_dlistSet.insert(n);
     116         [ +  - ]:        192 :       Trace("jh-status") << "...push due to decision" << std::endl;
     117                 :            :     }
     118                 :       1754 :     return;
     119                 :            :   }
     120         [ +  - ]:        715 :   if (s == DecisionStatus::BACKTRACK)
     121                 :            :   {
     122                 :            :     // backtrack inserts at the current position
     123         [ +  + ]:        715 :     if (it == d_dlistSet.end())
     124                 :            :     {
     125                 :         89 :       d_dlist.insert(d_dlist.begin(), n);
     126                 :         89 :       d_dlistSet.insert(n);
     127                 :            :     }
     128                 :            :   }
     129                 :            : }
     130                 :            : 
     131                 :            : }  // namespace decision
     132                 :            : }  // namespace cvc5::internal