1 /********************* */
2 /*! \file preprocessing_pass_context.cpp
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Andrew Reynolds, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief The preprocessing pass context for passes
14 ** The preprocessing pass context for passes.
17 #include "preprocessing/preprocessing_pass_context.h"
19 #include "expr/node_algorithm.h"
22 namespace preprocessing
{
24 PreprocessingPassContext::PreprocessingPassContext(
26 theory::booleans::CircuitPropagator
* circuitPropagator
,
27 ProofNodeManager
* pnm
)
29 d_resourceManager(smt
->getResourceManager()),
30 d_topLevelSubstitutions(smt
->getUserContext(), pnm
),
31 d_circuitPropagator(circuitPropagator
),
33 d_symsInAssertions(smt
->getUserContext())
37 void PreprocessingPassContext::widenLogic(theory::TheoryId id
)
39 LogicRequest
req(*d_smt
);
43 theory::TrustSubstitutionMap
&
44 PreprocessingPassContext::getTopLevelSubstitutions()
46 return d_topLevelSubstitutions
;
49 void PreprocessingPassContext::enableIntegers()
51 LogicRequest
req(*d_smt
);
55 void PreprocessingPassContext::recordSymbolsInAssertions(
56 const std::vector
<Node
>& assertions
)
58 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
59 std::unordered_set
<Node
, NodeHashFunction
> syms
;
60 for (TNode cn
: assertions
)
62 expr::getSymbols(cn
, syms
, visited
);
64 for (const Node
& s
: syms
)
66 d_symsInAssertions
.insert(s
);
70 ProofNodeManager
* PreprocessingPassContext::getProofNodeManager()
75 } // namespace preprocessing