Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Mathias Preiner, Yoni Zohar, Andrew Reynolds
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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                 :      51607 : StaticLearning::StaticLearning(PreprocessingPassContext* preprocContext)
      31                 :            :     : PreprocessingPass(preprocContext, "static-learning"),
      32                 :      51607 :       d_cache(userContext()){};
      33                 :            : 
      34                 :      37224 : PreprocessingPassResult StaticLearning::applyInternal(
      35                 :            :     AssertionPipeline* assertionsToPreprocess)
      36                 :            : {
      37                 :      37224 :   d_preprocContext->spendResource(Resource::PreprocessStep);
      38                 :            : 
      39                 :      37224 :   std::vector<TNode> toProcess;
      40                 :            : 
      41         [ +  + ]:     594955 :   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
      42                 :            :   {
      43                 :     557731 :     const Node& n = (*assertionsToPreprocess)[i];
      44                 :            : 
      45                 :            :     /* Already processed in this context. */
      46         [ +  + ]:     557731 :     if (d_cache.find(n) != d_cache.end())
      47                 :            :     {
      48                 :     169445 :       continue;
      49                 :            :     }
      50                 :            : 
      51                 :            :     /* Process all assertions in nested AND terms. */
      52                 :     776572 :     std::vector<TNode> assertions;
      53                 :     388286 :     flattenAnd(n, assertions);
      54                 :     776572 :     std::vector<TrustNode> tlems;
      55         [ +  + ]:     844115 :     for (TNode a : assertions)
      56                 :            :     {
      57                 :     455829 :       d_preprocContext->getTheoryEngine()->ppStaticLearn(a, tlems);
      58                 :            :     }
      59                 :            : 
      60                 :            :     // add the lemmas to the end
      61         [ +  + ]:     394892 :     for (const TrustNode& trn : tlems)
      62                 :            :     {
      63                 :            :       // ensure all learned lemmas are rewritten
      64                 :       6606 :       assertionsToPreprocess->pushBackTrusted(
      65                 :            :           trn, TrustId::PREPROCESS_STATIC_LEARNING_LEMMA, true);
      66                 :            :     }
      67                 :            :   }
      68                 :      74448 :   return PreprocessingPassResult::NO_CONFLICT;
      69                 :            : }
      70                 :            : 
      71                 :     388286 : void StaticLearning::flattenAnd(TNode node, std::vector<TNode>& children)
      72                 :            : {
      73                 :    1941430 :   std::vector<TNode> visit = {node};
      74                 :      69403 :   do
      75                 :            :   {
      76                 :     457689 :     TNode cur = visit.back();
      77                 :     457689 :     visit.pop_back();
      78                 :            : 
      79         [ +  + ]:     457689 :     if (d_cache.find(cur) != d_cache.end())
      80                 :            :     {
      81                 :         86 :       continue;
      82                 :            :     }
      83                 :     457603 :     d_cache.insert(cur);
      84                 :            : 
      85         [ +  + ]:     457603 :     if (cur.getKind() == Kind::AND)
      86                 :            :     {
      87                 :       1774 :       visit.insert(visit.end(), cur.begin(), cur.end());
      88                 :            :     }
      89                 :            :     else
      90                 :            :     {
      91                 :     455829 :       children.push_back(cur);
      92                 :            :     }
      93         [ +  + ]:     457689 :   } while (!visit.empty());
      94                 :     388286 : }
      95                 :            : 
      96                 :            : }  // namespace passes
      97                 :            : }  // namespace preprocessing
      98                 :            : }  // namespace cvc5::internal