1 /********************* */
2 /*! \file preprocessor.h
4 ** Top contributors (to current version):
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 preprocessor of the SmtEngine.
15 #include "cvc4_private.h"
17 #ifndef CVC4__SMT__PREPROCESSOR_H
18 #define CVC4__SMT__PREPROCESSOR_H
22 #include "preprocessing/preprocessing_pass_context.h"
23 #include "smt/process_assertions.h"
24 #include "smt/term_formula_removal.h"
25 #include "theory/booleans/circuit_propagator.h"
33 * The preprocessor module of an SMT engine.
35 * This class is responsible for:
36 * (1) preprocessing the set of assertions from input before they are sent to
38 * (2) implementing methods for expanding and simplifying formulas. The latter
39 * takes into account the substitutions inferred by this class.
44 Preprocessor(SmtEngine
& smt
, context::UserContext
* u
, AbstractValues
& abs
);
47 * Finish initialization
51 * Process the assertions that have been asserted in argument as. Returns
52 * true if no conflict was discovered while preprocessing them.
54 bool process(Assertions
& as
);
56 * Postprocess assertions, called after the SmtEngine has finished
57 * giving the assertions to the SMT solver and before the assertions are
60 void postprocess(Assertions
& as
);
62 * Clear learned literals from the Boolean propagator.
64 void clearLearnedLiterals();
66 * Cleanup, which deletes the processing passes owned by this module. This
67 * is required to be done explicitly so that passes are deleted before the
68 * objects they refer to in the SmtEngine destructor.
72 * Simplify a formula without doing "much" work. Does not involve
73 * the SAT Engine in the simplification, but uses the current
74 * definitions, assertions, and the current partial model, if one
75 * has been constructed. It also involves theory normalization.
77 * @param n The node to simplify
78 * @param removeItes Whether to remove ITE (and other terms with formulas in
79 * term positions) from the result.
80 * @return The simplified term.
82 Node
simplify(const Node
& n
, bool removeItes
= false);
84 * Expand the definitions in a term or formula n. No other
85 * simplification or normalization is done.
87 * @param n The node to expand
88 * @param expandOnly if true, then the expandDefinitions function of
89 * TheoryEngine is not called on subterms of n.
90 * @return The expanded term.
92 Node
expandDefinitions(const Node
& n
, bool expandOnly
= false);
93 /** Same as above, with a cache of previous results. */
94 Node
expandDefinitions(
96 std::unordered_map
<Node
, Node
, NodeHashFunction
>& cache
,
97 bool expandOnly
= false);
99 * Get the underlying term formula remover utility.
101 RemoveTermFormulas
& getTermFormulaRemover();
105 * Apply substitutions that have been inferred by preprocessing, return the
106 * substituted form of node.
108 Node
applySubstitutions(TNode node
);
109 /** Reference to the parent SmtEngine */
111 /** Reference to the abstract values utility */
112 AbstractValues
& d_absValues
;
114 * A circuit propagator for non-clausal propositional deduction.
116 theory::booleans::CircuitPropagator d_propagator
;
118 * User-context-dependent flag of whether any assertions have been processed.
120 context::CDO
<bool> d_assertionsProcessed
;
121 /** The preprocessing pass context */
122 std::unique_ptr
<preprocessing::PreprocessingPassContext
> d_ppContext
;
124 * Process assertions module, responsible for implementing the preprocessing
127 ProcessAssertions d_processor
;
129 * The term formula remover, responsible for eliminating formulas that occur
132 RemoveTermFormulas d_rtf
;