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 preprocessing pass context for passes
      11                 :            :  *
      12                 :            :  * Implementation of the preprocessing pass context for passes. This context
      13                 :            :  * allows preprocessing passes to retrieve information besides the assertions
      14                 :            :  * from the solver and interact with it without getting full access.
      15                 :            :  */
      16                 :            : 
      17                 :            : #include "cvc5_private.h"
      18                 :            : 
      19                 :            : #ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
      20                 :            : #define CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
      21                 :            : 
      22                 :            : #include "context/cdhashset.h"
      23                 :            : #include "preprocessing/learned_literal_manager.h"
      24                 :            : #include "smt/env_obj.h"
      25                 :            : #include "theory/logic_info.h"
      26                 :            : #include "theory/trust_substitutions.h"
      27                 :            : #include "util/resource_manager.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : 
      31                 :            : class Env;
      32                 :            : class TheoryEngine;
      33                 :            : 
      34                 :            : namespace theory::booleans {
      35                 :            : class CircuitPropagator;
      36                 :            : }
      37                 :            : 
      38                 :            : namespace prop {
      39                 :            : class PropEngine;
      40                 :            : }
      41                 :            : 
      42                 :            : namespace preprocessing {
      43                 :            : 
      44                 :            : class PreprocessingPassContext : protected EnvObj
      45                 :            : {
      46                 :            :  public:
      47                 :            :   /** Constructor. */
      48                 :            :   PreprocessingPassContext(
      49                 :            :       Env& env,
      50                 :            :       TheoryEngine* te,
      51                 :            :       prop::PropEngine* pe,
      52                 :            :       theory::booleans::CircuitPropagator* circuitPropagator);
      53                 :            : 
      54                 :            :   /** Get the associated Environment. */
      55                 :    1966046 :   Env& getEnv() { return d_env; }
      56                 :            :   /** Get the associated TheoryEngine. */
      57                 :            :   TheoryEngine* getTheoryEngine() const;
      58                 :            :   /** Get the associated Propengine. */
      59                 :            :   prop::PropEngine* getPropEngine() const;
      60                 :            : 
      61                 :            :   /** Get the associated circuit propagator. */
      62                 :      41078 :   theory::booleans::CircuitPropagator* getCircuitPropagator() const
      63                 :            :   {
      64                 :      41078 :     return d_circuitPropagator;
      65                 :            :   }
      66                 :            : 
      67                 :            :   /**
      68                 :            :    * Get the (user-context-dependent) set of symbols that occur in at least one
      69                 :            :    * assertion in the current user context.
      70                 :            :    */
      71                 :       3033 :   const context::CDHashSet<Node>& getSymsInAssertions() const
      72                 :            :   {
      73                 :       3033 :     return d_symsInAssertions;
      74                 :            :   }
      75                 :            : 
      76                 :            :   /** Spend resource in the resource manager of the associated Env. */
      77                 :            :   void spendResource(Resource r);
      78                 :            : 
      79                 :            :   /**
      80                 :            :    * Get a reference to the top-level substitution map. Note that all
      81                 :            :    * substitutions added to this map should use the addSubstitution methods
      82                 :            :    * below for the purposes of proper debugging information.
      83                 :            :    */
      84                 :            :   theory::TrustSubstitutionMap& getTopLevelSubstitutions() const;
      85                 :            : 
      86                 :            :   /** Record symbols in assertions
      87                 :            :    *
      88                 :            :    * This method is called when a set of assertions is finalized. It adds
      89                 :            :    * the symbols to d_symsInAssertions that occur in assertions.
      90                 :            :    */
      91                 :            :   void recordSymbolsInAssertions(const std::vector<Node>& assertions);
      92                 :            : 
      93                 :            :   /**
      94                 :            :    * Notify learned literal. This method is called when a literal is
      95                 :            :    * entailed by the current set of assertions.
      96                 :            :    *
      97                 :            :    * It should be rewritten, and such that top level substitutions have
      98                 :            :    * been applied to it.
      99                 :            :    */
     100                 :            :   void notifyLearnedLiteral(TNode lit);
     101                 :            :   /**
     102                 :            :    * Get the learned literals
     103                 :            :    */
     104                 :            :   std::vector<Node> getLearnedLiterals() const;
     105                 :            :   /**
     106                 :            :    * Add substitution to the top-level substitutions, which also as a
     107                 :            :    * consequence is used by the theory model.
     108                 :            :    * @param lhs The node replaced by node 'rhs'
     109                 :            :    * @param rhs The node to substitute node 'lhs'
     110                 :            :    * @param pg The proof generator that can provide a proof of lhs == rhs.
     111                 :            :    */
     112                 :            :   void addSubstitution(const Node& lhs,
     113                 :            :                        const Node& rhs,
     114                 :            :                        ProofGenerator* pg = nullptr);
     115                 :            :   /** Same as above, with proof id */
     116                 :            :   void addSubstitution(const Node& lhs,
     117                 :            :                        const Node& rhs,
     118                 :            :                        ProofRule id,
     119                 :            :                        const std::vector<Node>& args);
     120                 :            :   /** Add top level substitutions for a substitution map */
     121                 :            :   void addSubstitutions(theory::TrustSubstitutionMap& tm);
     122                 :            : 
     123                 :            :  private:
     124                 :            :   /** Helper method for printing substitutions */
     125                 :            :   void printSubstitution(const Node& lhs, const Node& rhs) const;
     126                 :            : 
     127                 :            :   /** Pointer to the theory engine associated with this context. */
     128                 :            :   TheoryEngine* d_theoryEngine;
     129                 :            :   /** Pointer to the prop engine associated with this context. */
     130                 :            :   prop::PropEngine* d_propEngine;
     131                 :            :   /** Instance of the circuit propagator */
     132                 :            :   theory::booleans::CircuitPropagator* d_circuitPropagator;
     133                 :            :   /**
     134                 :            :    * The learned literal manager
     135                 :            :    */
     136                 :            :   LearnedLiteralManager d_llm;
     137                 :            : 
     138                 :            :   /**
     139                 :            :    * The (user-context-dependent) set of symbols that occur in at least one
     140                 :            :    * assertion in the current user context.
     141                 :            :    */
     142                 :            :   context::CDHashSet<Node> d_symsInAssertions;
     143                 :            : 
     144                 :            : };  // class PreprocessingPassContext
     145                 :            : 
     146                 :            : }  // namespace preprocessing
     147                 :            : }  // namespace cvc5::internal
     148                 :            : 
     149                 :            : #endif /* CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */