Branch data     Line data    Source code

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