1 /********************* */
2 /*! \file preprocessor.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Haniel Barbosa
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
,
45 context::UserContext
* u
,
47 SmtEngineStatistics
& stats
);
50 * Finish initialization
54 * Process the assertions that have been asserted in argument as. Returns
55 * true if no conflict was discovered while preprocessing them.
57 bool process(Assertions
& as
);
59 * Postprocess assertions, called after the SmtEngine has finished
60 * giving the assertions to the SMT solver and before the assertions are
63 void postprocess(Assertions
& as
);
65 * Clear learned literals from the Boolean propagator.
67 void clearLearnedLiterals();
69 * Cleanup, which deletes the processing passes owned by this module. This
70 * is required to be done explicitly so that passes are deleted before the
71 * objects they refer to in the SmtEngine destructor.
75 * Simplify a formula without doing "much" work. Does not involve
76 * the SAT Engine in the simplification, but uses the current
77 * definitions, assertions, and the current partial model, if one
78 * has been constructed. It also involves theory normalization.
80 * @param n The node to simplify
81 * @param removeItes Whether to remove ITE (and other terms with formulas in
82 * term positions) from the result.
83 * @return The simplified term.
85 Node
simplify(const Node
& n
, bool removeItes
= false);
87 * Expand the definitions in a term or formula n. No other
88 * simplification or normalization is done.
90 * @param n The node to expand
91 * @param expandOnly if true, then the expandDefinitions function of
92 * TheoryEngine is not called on subterms of n.
93 * @return The expanded term.
95 Node
expandDefinitions(const Node
& n
, bool expandOnly
= false);
96 /** Same as above, with a cache of previous results. */
97 Node
expandDefinitions(
99 std::unordered_map
<Node
, Node
, NodeHashFunction
>& cache
,
100 bool expandOnly
= false);
102 * Get the underlying term formula remover utility.
104 RemoveTermFormulas
& getTermFormulaRemover();
107 * Set proof node manager. Enables proofs in this preprocessor.
109 void setProofGenerator(PreprocessProofGenerator
* pppg
);
112 /** A copy of the current context */
113 context::Context
* d_context
;
114 /** Reference to the parent SmtEngine */
116 /** Reference to the abstract values utility */
117 AbstractValues
& d_absValues
;
119 * A circuit propagator for non-clausal propositional deduction.
121 theory::booleans::CircuitPropagator d_propagator
;
123 * User-context-dependent flag of whether any assertions have been processed.
125 context::CDO
<bool> d_assertionsProcessed
;
126 /** The preprocessing pass context */
127 std::unique_ptr
<preprocessing::PreprocessingPassContext
> d_ppContext
;
129 * Process assertions module, responsible for implementing the preprocessing
132 ProcessAssertions d_processor
;
134 * The term formula remover, responsible for eliminating formulas that occur
137 RemoveTermFormulas d_rtf
;
138 /** Proof node manager */
139 ProofNodeManager
* d_pnm
;