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                 :            :  * Apply substitutions preprocessing pass.
      11                 :            :  *
      12                 :            :  * Apply top level substitutions to assertions, rewrite, and store back into
      13                 :            :  * assertions.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "preprocessing/passes/apply_substs.h"
      17                 :            : 
      18                 :            : #include "context/cdo.h"
      19                 :            : #include "preprocessing/assertion_pipeline.h"
      20                 :            : #include "preprocessing/preprocessing_pass_context.h"
      21                 :            : #include "smt/env.h"
      22                 :            : #include "theory/substitutions.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace preprocessing {
      26                 :            : namespace passes {
      27                 :            : 
      28                 :      28895 : ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext)
      29                 :      28895 :     : PreprocessingPass(preprocContext, "apply-substs")
      30                 :            : {
      31                 :      28895 : }
      32                 :            : 
      33                 :      31310 : PreprocessingPassResult ApplySubsts::applyInternal(
      34                 :            :     AssertionPipeline* assertionsToPreprocess)
      35                 :            : {
      36                 :      31310 :   verbose(2) << "applying substitutions..." << std::endl;
      37         [ +  - ]:      62620 :   Trace("apply-substs") << "ApplySubsts::processAssertions(): "
      38                 :      31310 :                         << "applying substitutions" << std::endl;
      39                 :            :   // TODO(#1255): Substitutions in incremental mode should be managed with a
      40                 :            :   // proper data structure.
      41                 :            : 
      42                 :            :   theory::TrustSubstitutionMap& tlsm =
      43                 :      31310 :       d_preprocContext->getTopLevelSubstitutions();
      44                 :      31310 :   unsigned size = assertionsToPreprocess->size();
      45         [ +  + ]:     514473 :   for (unsigned i = 0; i < size; ++i)
      46                 :            :   {
      47         [ -  + ]:     486159 :     if (assertionsToPreprocess->isSubstsIndex(i))
      48                 :            :     {
      49                 :          0 :       continue;
      50                 :            :     }
      51         [ +  - ]:     972318 :     Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
      52                 :     486159 :                           << std::endl;
      53                 :     486159 :     d_preprocContext->spendResource(Resource::PreprocessStep);
      54                 :     486159 :     assertionsToPreprocess->replaceTrusted(
      55                 :            :         i,
      56                 :     972318 :         tlsm.applyTrusted((*assertionsToPreprocess)[i], d_env.getRewriter()));
      57         [ +  - ]:     972318 :     Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
      58                 :     486159 :                           << std::endl;
      59                 :            :     // if rewritten to false, we are done
      60         [ +  + ]:     486159 :     if (assertionsToPreprocess->isInConflict())
      61                 :            :     {
      62                 :       2996 :       return PreprocessingPassResult::CONFLICT;
      63                 :            :     }
      64                 :            :   }
      65                 :      28314 :   return PreprocessingPassResult::NO_CONFLICT;
      66                 :            : }
      67                 :            : 
      68                 :            : }  // namespace passes
      69                 :            : }  // namespace preprocessing
      70                 :            : }  // namespace cvc5::internal