Branch data     Line data    Source code

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