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                 :            :  * The preprocessor of the SMT engine.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "smt/preprocessor.h"
      14                 :            : 
      15                 :            : #include "options/base_options.h"
      16                 :            : #include "options/expr_options.h"
      17                 :            : #include "options/smt_options.h"
      18                 :            : #include "preprocessing/assertion_pipeline.h"
      19                 :            : #include "preprocessing/preprocessing_pass_context.h"
      20                 :            : #include "printer/printer.h"
      21                 :            : #include "smt/assertions.h"
      22                 :            : #include "smt/env.h"
      23                 :            : #include "smt/preprocess_proof_generator.h"
      24                 :            : #include "theory/rewriter.h"
      25                 :            : 
      26                 :            : using namespace std;
      27                 :            : using namespace cvc5::internal::theory;
      28                 :            : using namespace cvc5::internal::kind;
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : namespace smt {
      32                 :            : 
      33                 :      41728 : Preprocessor::Preprocessor(Env& env, SolverEngineStatistics& stats)
      34                 :            :     : EnvObj(env),
      35                 :      41728 :       d_pppg(nullptr),
      36                 :      41728 :       d_propagator(env, true, true),
      37                 :      41728 :       d_assertionsProcessed(env.getUserContext(), false),
      38                 :      83456 :       d_processor(env, stats)
      39                 :            : {
      40                 :      41728 : }
      41                 :            : 
      42                 :      37237 : Preprocessor::~Preprocessor() {}
      43                 :            : 
      44                 :      28895 : void Preprocessor::finishInit(TheoryEngine* te,
      45                 :            :                               prop::PropEngine* pe,
      46                 :            :                               PreprocessProofGenerator* pppg)
      47                 :            : {
      48                 :            :   // set up the preprocess proof generator, if necessary
      49 [ +  + ][ +  + ]:      28895 :   if (d_pppg == nullptr && pppg != nullptr)
      50                 :            :   {
      51                 :      15359 :     d_pppg = pppg;
      52         [ +  - ]:      15359 :     d_propagator.enableProofs(userContext(), d_pppg);
      53                 :            :   }
      54                 :            : 
      55                 :      28895 :   d_ppContext.reset(new preprocessing::PreprocessingPassContext(
      56                 :      28895 :       d_env, te, pe, &d_propagator));
      57                 :            : 
      58                 :            :   // initialize the preprocessing passes
      59                 :      28895 :   d_processor.finishInit(d_ppContext.get());
      60                 :      28895 : }
      61                 :            : 
      62                 :      41454 : bool Preprocessor::process(preprocessing::AssertionPipeline& ap)
      63                 :            : {
      64         [ +  + ]:      41454 :   if (ap.size() == 0)
      65                 :            :   {
      66                 :            :     // nothing to do
      67                 :       9913 :     return true;
      68                 :            :   }
      69 [ +  + ][ +  + ]:      31541 :   if (d_assertionsProcessed && options().base.incrementalSolving)
                 [ +  + ]
      70                 :            :   {
      71                 :            :     // TODO(b/1255): Substitutions in incremental mode should be managed with a
      72                 :            :     // proper data structure.
      73                 :       3217 :     ap.enableStoreSubstsInAsserts();
      74                 :            :   }
      75                 :            :   else
      76                 :            :   {
      77                 :      28324 :     ap.disableStoreSubstsInAsserts();
      78                 :            :   }
      79                 :            : 
      80                 :            :   // process the assertions, return true if no conflict is discovered
      81                 :      31541 :   bool noConflict = d_processor.apply(ap);
      82                 :            : 
      83                 :            :   // now, post-process the assertions
      84                 :            : 
      85                 :            :   // if incremental, compute which variables are assigned
      86         [ +  + ]:      31520 :   if (options().base.incrementalSolving)
      87                 :            :   {
      88                 :       6771 :     d_ppContext->recordSymbolsInAssertions(ap.ref());
      89                 :            :   }
      90                 :            : 
      91                 :            :   // mark that we've processed assertions
      92                 :      31520 :   d_assertionsProcessed = true;
      93                 :            : 
      94                 :      31520 :   return noConflict;
      95                 :            : }
      96                 :            : 
      97                 :       3081 : void Preprocessor::clearLearnedLiterals()
      98                 :            : {
      99                 :       3081 :   d_propagator.getLearnedLiterals().clear();
     100                 :       3081 : }
     101                 :            : 
     102                 :          0 : std::vector<Node> Preprocessor::getLearnedLiterals() const
     103                 :            : {
     104         [ -  - ]:          0 :   if (d_ppContext == nullptr)
     105                 :            :   {
     106                 :          0 :     return {};
     107                 :            :   }
     108                 :          0 :   return d_ppContext->getLearnedLiterals();
     109                 :            : }
     110                 :            : 
     111                 :      37237 : void Preprocessor::cleanup() { d_processor.cleanup(); }
     112                 :            : 
     113                 :      15182 : Node Preprocessor::applySubstitutions(const Node& node)
     114                 :            : {
     115                 :      15182 :   return d_env.getTopLevelSubstitutions().apply(node);
     116                 :            : }
     117                 :            : 
     118                 :         61 : void Preprocessor::applySubstitutions(std::vector<Node>& ns)
     119                 :            : {
     120         [ +  + ]:        186 :   for (size_t i = 0, nasserts = ns.size(); i < nasserts; i++)
     121                 :            :   {
     122                 :        125 :     ns[i] = applySubstitutions(ns[i]);
     123                 :            :   }
     124                 :         61 : }
     125                 :            : 
     126                 :      29380 : PreprocessProofGenerator* Preprocessor::getPreprocessProofGenerator()
     127                 :            : {
     128                 :      29380 :   return d_pppg;
     129                 :            : }
     130                 :            : 
     131                 :            : }  // namespace smt
     132                 :            : }  // namespace cvc5::internal