blob: 97fa32d1759129cdc701c60d12a8b2c763cf0c78 (
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
|
/********************* */
/*! \file preprocessing_pass.h
** \verbatim
** Top contributors (to current version):
** Justin Xu, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 The preprocessing pass super class
**
** Implementation of the preprocessing pass super class. Preprocessing passes
** that inherit from this class, need to pass their name to the constructor to
** register the pass appropriately. The core of a preprocessing pass lives
** in applyInternal(), which operates on a list of assertions and is called
** from apply() in the super class. The apply() method automatically takes
** care of the following:
**
** - Dumping assertions before and after the pass
** - Initializing the timer
** - Tracing and chatting
**
** Optionally, preprocessing passes can overwrite the initInteral() method to
** do work that only needs to be done once.
**/
#include "cvc4_private.h"
#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
#include <string>
#include <vector>
#include "context/cdo.h"
#include "expr/node.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/smt_engine_scope.h"
#include "smt/term_formula_removal.h"
#include "theory/substitutions.h"
namespace CVC4 {
namespace preprocessing {
/**
* Assertion Pipeline stores a list of assertions modified by preprocessing
* passes.
*/
class AssertionPipeline
{
public:
AssertionPipeline(context::Context* context);
size_t size() const { return d_nodes.size(); }
void resize(size_t n) { d_nodes.resize(n); }
void clear()
{
d_nodes.clear();
d_realAssertionsEnd = 0;
}
Node& operator[](size_t i) { return d_nodes[i]; }
const Node& operator[](size_t i) const { return d_nodes[i]; }
void push_back(Node n) { d_nodes.push_back(n); }
std::vector<Node>& ref() { return d_nodes; }
const std::vector<Node>& ref() const { return d_nodes; }
std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
/*
* Replaces assertion i with node n and records the dependency between the
* original assertion and its replacement.
*/
void replace(size_t i, Node n);
/*
* Replaces assertion i with node n and records that this replacement depends
* on assertion i and the nodes listed in addnDeps. The dependency
* information is used for unsat cores and proofs.
*/
void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
/*
* Replaces an assertion with a vector of assertions and records the
* dependencies.
*/
void replace(size_t i, const std::vector<Node>& ns);
IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
context::CDO<unsigned>& getSubstitutionsIndex()
{
return d_substitutionsIndex;
}
theory::SubstitutionMap& getTopLevelSubstitutions()
{
return d_topLevelSubstitutions;
}
size_t getRealAssertionsEnd() { return d_realAssertionsEnd; }
void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
private:
std::vector<Node> d_nodes;
/**
* Map from skolem variables to index in d_assertions containing
* corresponding introduced Boolean ite
*/
IteSkolemMap d_iteSkolemMap;
/* Index for where to store substitutions */
context::CDO<unsigned> d_substitutionsIndex;
/* The top level substitutions */
theory::SubstitutionMap d_topLevelSubstitutions;
/** Size of d_nodes when preprocessing starts */
size_t d_realAssertionsEnd;
}; /* class AssertionPipeline */
/**
* Preprocessing passes return a result which indicates whether a conflict has
* been detected during preprocessing.
*/
enum PreprocessingPassResult { CONFLICT, NO_CONFLICT };
class PreprocessingPass {
public:
/* Preprocesses a list of assertions assertionsToPreprocess */
PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
PreprocessingPass(PreprocessingPassContext* preprocContext,
const std::string& name);
virtual ~PreprocessingPass();
protected:
/*
* Method for dumping assertions within a pass. Also called before and after
* applying the pass.
*/
void dumpAssertions(const char* key, const AssertionPipeline& assertionList);
/*
* Abstract method that each pass implements to do the actual preprocessing.
*/
virtual PreprocessingPassResult applyInternal(
AssertionPipeline* assertionsToPreprocess) = 0;
/* Context for Preprocessing Passes that initializes necessary variables */
PreprocessingPassContext* d_preprocContext;
private:
/* Name of pass */
std::string d_name;
/* Timer for registering the preprocessing time of this pass */
TimerStat d_timer;
};
} // namespace preprocessing
} // namespace CVC4
#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_H */
|
