blob: 679a6216d4ff1b5a2c75117361efaa66dcc068be (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
/********************* */
/*! \file non_clausal_simp.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Aina Niemetz, Gereon Kremer
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Non-clausal simplification preprocessing pass.
**/
#include "cvc4_private.h"
#ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
#define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
#include "context/cdlist.h"
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
#include "theory/trust_node.h"
namespace cvc5 {
class LazyCDProof;
class ProofNodeManager;
namespace smt {
class PreprocessProofGenerator;
}
namespace theory {
class TrustSubstitutionMap;
}
namespace preprocessing {
namespace passes {
class NonClausalSimp : public PreprocessingPass
{
public:
NonClausalSimp(PreprocessingPassContext* preprocContext);
protected:
PreprocessingPassResult applyInternal(
AssertionPipeline* assertionsToPreprocess) override;
private:
struct Statistics
{
IntStat d_numConstantProps;
Statistics();
~Statistics();
};
Statistics d_statistics;
/**
* Transform learned literal lit. We apply substitutions in subs once and then
* apply constant propagations cp to fixed point. Return the rewritten
* form of lit.
*
* If proofs are enabled, then we require that the learned literal preprocess
* proof generator (d_llpg) has a proof of lit when this method is called,
* and ensure that the return literal also has a proof in d_llpg.
*/
Node processLearnedLit(Node lit,
theory::TrustSubstitutionMap* subs,
theory::TrustSubstitutionMap* cp);
/**
* Process rewritten learned literal. This is called when we have a
* learned literal lit that is rewritten to litr based on the proof generator
* contained in trn (if it exists). The trust node trn should be of kind
* REWRITE and proving (= lit litr).
*
* This tracks the proof in the learned literal preprocess proof generator
* d_llpg below and returns the rewritten learned literal.
*/
Node processRewrittenLearnedLit(theory::TrustNode trn);
/** Is proof enabled? */
bool isProofEnabled() const;
/** The proof node manager */
ProofNodeManager* d_pnm;
/** the learned literal preprocess proof generator */
std::unique_ptr<smt::PreprocessProofGenerator> d_llpg;
/**
* An lazy proof for learned literals that are reasserted into the assertions
* pipeline by this class.
*/
std::unique_ptr<LazyCDProof> d_llra;
/**
* A context-dependent list of trust substitution maps, which are required
* for storing proofs.
*/
context::CDList<std::shared_ptr<theory::TrustSubstitutionMap> > d_tsubsList;
};
} // namespace passes
} // namespace preprocessing
} // namespace cvc5
#endif
|
