1 /********************* */
2 /*! \file preprocessing_pass_context.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Mathias Preiner, Andres Noetzli
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 ** The preprocessing pass context for passes.
15 **/
16
17 #include "preprocessing_pass_context.h"
18
19 #include "expr/node_algorithm.h"
20
21 namespace CVC4 {
22 namespace preprocessing {
23
PreprocessingPassContext(SmtEngine * smt,ResourceManager * resourceManager,RemoveTermFormulas * iteRemover,theory::booleans::CircuitPropagator * circuitPropagator)24 PreprocessingPassContext::PreprocessingPassContext(
25 SmtEngine* smt,
26 ResourceManager* resourceManager,
27 RemoveTermFormulas* iteRemover,
28 theory::booleans::CircuitPropagator* circuitPropagator)
29 : d_smt(smt),
30 d_resourceManager(resourceManager),
31 d_iteRemover(iteRemover),
32 d_substitutionsIndex(smt->d_userContext, 0),
33 d_topLevelSubstitutions(smt->d_userContext),
34 d_circuitPropagator(circuitPropagator),
35 d_symsInAssertions(smt->d_userContext)
36 {
37 }
38
widenLogic(theory::TheoryId id)39 void PreprocessingPassContext::widenLogic(theory::TheoryId id)
40 {
41 LogicRequest req(*d_smt);
42 req.widenLogic(id);
43 }
44
enableIntegers()45 void PreprocessingPassContext::enableIntegers()
46 {
47 LogicRequest req(*d_smt);
48 req.enableIntegers();
49 }
50
recordSymbolsInAssertions(const std::vector<Node> & assertions)51 void PreprocessingPassContext::recordSymbolsInAssertions(
52 const std::vector<Node>& assertions)
53 {
54 std::unordered_set<TNode, TNodeHashFunction> visited;
55 std::unordered_set<Node, NodeHashFunction> syms;
56 for (TNode cn : assertions)
57 {
58 expr::getSymbols(cn, syms, visited);
59 }
60 for (const Node& s : syms)
61 {
62 d_symsInAssertions.insert(s);
63 }
64 }
65
66 } // namespace preprocessing
67 } // namespace CVC4
68