Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Mathias Preiner, Yoni Zohar, Aina Niemetz
       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                 :            :  * The static learning preprocessing pass.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "preprocessing/passes/static_learning.h"
      17                 :            : 
      18                 :            : #include <string>
      19                 :            : 
      20                 :            : #include "expr/node.h"
      21                 :            : #include "preprocessing/assertion_pipeline.h"
      22                 :            : #include "preprocessing/preprocessing_pass_context.h"
      23                 :            : #include "theory/rewriter.h"
      24                 :            : #include "theory/theory_engine.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace preprocessing {
      28                 :            : namespace passes {
      29                 :            : 
      30                 :      48144 : StaticLearning::StaticLearning(PreprocessingPassContext* preprocContext)
      31                 :            :     : PreprocessingPass(preprocContext, "static-learning"),
      32                 :      48144 :       d_cache(userContext()){};
      33                 :            : 
      34                 :      34459 : PreprocessingPassResult StaticLearning::applyInternal(
      35                 :            :     AssertionPipeline* assertionsToPreprocess)
      36                 :            : {
      37                 :      34459 :   d_preprocContext->spendResource(Resource::PreprocessStep);
      38                 :            : 
      39                 :      34459 :   std::vector<TNode> toProcess;
      40                 :            : 
      41         [ +  + ]:     538626 :   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
      42                 :            :   {
      43                 :     504167 :     const Node& n = (*assertionsToPreprocess)[i];
      44                 :            : 
      45                 :            :     /* Already processed in this context. */
      46         [ +  + ]:     504167 :     if (d_cache.find(n) != d_cache.end())
      47                 :            :     {
      48                 :     153151 :       continue;
      49                 :            :     }
      50                 :            : 
      51                 :     702032 :     NodeBuilder learned(Kind::AND);
      52                 :     351016 :     learned << n;
      53                 :            : 
      54                 :            :     /* Process all assertions in nested AND terms. */
      55                 :     702032 :     std::vector<TNode> assertions;
      56                 :     351016 :     flattenAnd(n, assertions);
      57         [ +  + ]:     760980 :     for (TNode a : assertions)
      58                 :            :     {
      59                 :     409964 :       d_preprocContext->getTheoryEngine()->ppStaticLearn(a, learned);
      60                 :            :     }
      61                 :            : 
      62         [ +  + ]:     351016 :     if (learned.getNumChildren() == 1)
      63                 :            :     {
      64                 :     349483 :       learned.clear();
      65                 :            :     }
      66                 :            :     else
      67                 :            :     {
      68                 :       1533 :       assertionsToPreprocess->replace(i, rewrite(learned.constructNode()));
      69                 :            :     }
      70                 :            :   }
      71                 :      68918 :   return PreprocessingPassResult::NO_CONFLICT;
      72                 :            : }
      73                 :            : 
      74                 :     351016 : void StaticLearning::flattenAnd(TNode node, std::vector<TNode>& children)
      75                 :            : {
      76                 :    1755080 :   std::vector<TNode> visit = {node};
      77                 :      60577 :   do
      78                 :            :   {
      79                 :     411593 :     TNode cur = visit.back();
      80                 :     411593 :     visit.pop_back();
      81                 :            : 
      82         [ +  + ]:     411593 :     if (d_cache.find(cur) != d_cache.end())
      83                 :            :     {
      84                 :         75 :       continue;
      85                 :            :     }
      86                 :     411518 :     d_cache.insert(cur);
      87                 :            : 
      88         [ +  + ]:     411518 :     if (cur.getKind() == Kind::AND)
      89                 :            :     {
      90                 :       1554 :       visit.insert(visit.end(), cur.begin(), cur.end());
      91                 :            :     }
      92                 :            :     else
      93                 :            :     {
      94                 :     409964 :       children.push_back(cur);
      95                 :            :     }
      96         [ +  + ]:     411593 :   } while (!visit.empty());
      97                 :     351016 : }
      98                 :            : 
      99                 :            : }  // namespace passes
     100                 :            : }  // namespace preprocessing
     101                 :            : }  // namespace cvc5::internal