1 /********************* */
2 /*! \file preprocessing_pass_context.cpp
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Mathias Preiner, Andrew Reynolds
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_pass_context.h"
19 #include "expr/node_algorithm.h"
22 namespace preprocessing
{
24 PreprocessingPassContext::PreprocessingPassContext(
26 RemoveTermFormulas
* iteRemover
,
27 theory::booleans::CircuitPropagator
* circuitPropagator
)
29 d_resourceManager(smt
->getResourceManager()),
30 d_iteRemover(iteRemover
),
31 d_topLevelSubstitutions(smt
->getUserContext()),
32 d_circuitPropagator(circuitPropagator
),
33 d_symsInAssertions(smt
->getUserContext())
37 void PreprocessingPassContext::widenLogic(theory::TheoryId id
)
39 LogicRequest
req(*d_smt
);
43 void PreprocessingPassContext::enableIntegers()
45 LogicRequest
req(*d_smt
);
49 void PreprocessingPassContext::recordSymbolsInAssertions(
50 const std::vector
<Node
>& assertions
)
52 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
53 std::unordered_set
<Node
, NodeHashFunction
> syms
;
54 for (TNode cn
: assertions
)
56 expr::getSymbols(cn
, syms
, visited
);
58 for (const Node
& s
: syms
)
60 d_symsInAssertions
.insert(s
);
64 } // namespace preprocessing