1 /********************* */
2 /*! \file theory_preprocessor.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic
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 theory preprocessor.
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__THEORY_PREPROCESSOR_H
18 #define CVC4__THEORY__THEORY_PREPROCESSOR_H
20 #include <unordered_map>
22 #include "expr/lazy_proof.h"
23 #include "expr/node.h"
24 #include "expr/term_conversion_proof_generator.h"
25 #include "theory/trust_node.h"
31 class RemoveTermFormulas
;
36 * The preprocessor used in TheoryEngine.
38 class TheoryPreprocessor
40 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
43 /** Constructs a theory preprocessor */
44 TheoryPreprocessor(TheoryEngine
& engine
,
45 RemoveTermFormulas
& tfr
,
46 ProofNodeManager
* pnm
= nullptr);
47 /** Destroys a theory preprocessor */
48 ~TheoryPreprocessor();
49 /** Clear the cache of this class */
52 * Preprocesses the given assertion node. It returns a TrustNode of kind
53 * TrustNodeKind::REWRITE indicating the preprocessed form of node. It stores
54 * additional lemmas in newLemmas, which are trust nodes of kind
55 * TrustNodeKind::LEMMA. These correspond to e.g. lemmas corresponding to ITE
56 * removal. For each lemma in newLemmas, we add the corresponding skolem that
57 * the lemma defines. The flag doTheoryPreprocess is whether we should run
58 * theory-specific preprocessing.
60 * @param node The assertion to preprocess,
61 * @param newLemmas The lemmas to add to the set of assertions,
62 * @param newSkolems The skolems that newLemmas correspond to,
63 * @param doTheoryPreprocess whether to run theory-specific preprocessing.
64 * @return The trust node corresponding to rewriting node via preprocessing.
66 TrustNode
preprocess(TNode node
,
67 std::vector
<TrustNode
>& newLemmas
,
68 std::vector
<Node
>& newSkolems
,
69 bool doTheoryPreprocess
);
71 * Runs theory specific preprocessing on the non-Boolean parts of
72 * the formula. This is only called on input assertions, after ITEs
75 TrustNode
theoryPreprocess(TNode node
);
78 /** Reference to owning theory engine */
79 TheoryEngine
& d_engine
;
80 /** Logic info of theory engine */
81 const LogicInfo
& d_logicInfo
;
82 /** Cache for theory-preprocessing of assertions */
84 /** The term formula remover */
85 RemoveTermFormulas
& d_tfr
;
86 /** The context for the proof generator below */
87 context::Context d_pfContext
;
88 /** A term conversion proof generator */
89 std::unique_ptr
<TConvProofGenerator
> d_tpg
;
90 /** A lazy proof, for additional lemmas. */
91 std::unique_ptr
<LazyCDProof
> d_lp
;
92 /** Helper for theoryPreprocess */
93 Node
ppTheoryRewrite(TNode term
);
95 * Rewrite with proof, which stores a REWRITE step in d_tpg if necessary
96 * and returns the rewritten form of term.
98 Node
rewriteWithProof(Node term
);
100 * Preprocess with proof, which calls the appropriate ppRewrite method,
101 * stores the corresponding rewrite step in d_tpg if necessary and returns
102 * the preprocessed and rewritten form of term. It should be the case that
103 * term is already in rewritten form.
105 Node
preprocessWithProof(Node term
);
106 /** Proofs enabled */
107 bool isProofEnabled() const;
110 } // namespace theory
113 #endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */