Branch data     Line data    Source code

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