1 /*********************                                                        */
2 /*! \file preprocessing_pass_context.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Aina Niemetz, Mathias Preiner, Justin Xu
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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.\endverbatim
11  **
12  ** \brief The preprocessing pass context for passes
13  **
14  ** Implementation of the preprocessing pass context for passes. This context
15  ** allows preprocessing passes to retrieve information besides the assertions
16  ** from the solver and interact with it without getting full access.
17  **/
18 
19 #include "cvc4_private.h"
20 
21 #ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
22 #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
23 
24 #include "context/cdo.h"
25 #include "context/context.h"
26 #include "decision/decision_engine.h"
27 #include "preprocessing/util/ite_utilities.h"
28 #include "smt/smt_engine.h"
29 #include "smt/term_formula_removal.h"
30 #include "theory/booleans/circuit_propagator.h"
31 #include "theory/theory_engine.h"
32 #include "util/resource_manager.h"
33 
34 namespace CVC4 {
35 namespace preprocessing {
36 
37 class PreprocessingPassContext
38 {
39  public:
40   PreprocessingPassContext(
41       SmtEngine* smt,
42       ResourceManager* resourceManager,
43       RemoveTermFormulas* iteRemover,
44       theory::booleans::CircuitPropagator* circuitPropagator);
45 
getSmt()46   SmtEngine* getSmt() { return d_smt; }
getTheoryEngine()47   TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
getDecisionEngine()48   DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
getPropEngine()49   prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
getUserContext()50   context::Context* getUserContext() { return d_smt->d_userContext; }
getDecisionContext()51   context::Context* getDecisionContext() { return d_smt->d_context; }
getIteRemover()52   RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
53 
getCircuitPropagator()54   theory::booleans::CircuitPropagator* getCircuitPropagator()
55   {
56     return d_circuitPropagator;
57   }
58 
getSymsInAssertions()59   context::CDHashSet<Node, NodeHashFunction>& getSymsInAssertions()
60   {
61     return d_symsInAssertions;
62   }
63 
spendResource(unsigned amount)64   void spendResource(unsigned amount)
65   {
66     d_resourceManager->spendResource(amount);
67   }
68 
getLogicInfo()69   const LogicInfo& getLogicInfo() { return d_smt->d_logic; }
70 
71   /* Widen the logic to include the given theory. */
72   void widenLogic(theory::TheoryId id);
73 
getSubstitutionsIndex()74   unsigned getSubstitutionsIndex() const { return d_substitutionsIndex.get(); }
75 
setSubstitutionsIndex(unsigned i)76   void setSubstitutionsIndex(unsigned i) { d_substitutionsIndex = i; }
77 
78   /** Gets a reference to the top-level substitution map */
getTopLevelSubstitutions()79   theory::SubstitutionMap& getTopLevelSubstitutions()
80   {
81     return d_topLevelSubstitutions;
82   }
83 
84   /* Enable Integers. */
85   void enableIntegers();
86 
87   /** Record symbols in assertions
88    *
89    * This method is called when a set of assertions is finalized. It adds
90    * the symbols to d_symsInAssertions that occur in assertions.
91    */
92   void recordSymbolsInAssertions(const std::vector<Node>& assertions);
93 
94  private:
95   /** Pointer to the SmtEngine that this context was created in. */
96   SmtEngine* d_smt;
97 
98   /** Pointer to the ResourceManager for this context. */
99   ResourceManager* d_resourceManager;
100 
101   /** Instance of the ITE remover */
102   RemoveTermFormulas* d_iteRemover;
103 
104   /* Index for where to store substitutions */
105   context::CDO<unsigned> d_substitutionsIndex;
106 
107   /* The top level substitutions */
108   theory::SubstitutionMap d_topLevelSubstitutions;
109 
110   /** Instance of the circuit propagator */
111   theory::booleans::CircuitPropagator* d_circuitPropagator;
112 
113   /**
114    * The (user-context-dependent) set of symbols that occur in at least one
115    * assertion in the current user context.
116    */
117   context::CDHashSet<Node, NodeHashFunction> d_symsInAssertions;
118 
119 };  // class PreprocessingPassContext
120 
121 }  // namespace preprocessing
122 }  // namespace CVC4
123 
124 #endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
125