1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* The preprocessor of the SMT engine. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "smt/preprocessor.h" |
17 |
|
|
18 |
|
#include "options/base_options.h" |
19 |
|
#include "options/expr_options.h" |
20 |
|
#include "options/smt_options.h" |
21 |
|
#include "preprocessing/preprocessing_pass_context.h" |
22 |
|
#include "printer/printer.h" |
23 |
|
#include "smt/abstract_values.h" |
24 |
|
#include "smt/assertions.h" |
25 |
|
#include "smt/dump.h" |
26 |
|
#include "smt/env.h" |
27 |
|
#include "smt/preprocess_proof_generator.h" |
28 |
|
#include "smt/smt_engine.h" |
29 |
|
#include "theory/rewriter.h" |
30 |
|
|
31 |
|
using namespace std; |
32 |
|
using namespace cvc5::theory; |
33 |
|
using namespace cvc5::kind; |
34 |
|
|
35 |
|
namespace cvc5 { |
36 |
|
namespace smt { |
37 |
|
|
38 |
10501 |
Preprocessor::Preprocessor(SmtEngine& smt, |
39 |
|
Env& env, |
40 |
|
AbstractValues& abs, |
41 |
10501 |
SmtEngineStatistics& stats) |
42 |
|
: d_smt(smt), |
43 |
|
d_env(env), |
44 |
|
d_absValues(abs), |
45 |
|
d_propagator(true, true), |
46 |
10501 |
d_assertionsProcessed(env.getUserContext(), false), |
47 |
|
d_exDefs(env, stats), |
48 |
10501 |
d_processor(smt, *env.getResourceManager(), stats), |
49 |
31503 |
d_pnm(nullptr) |
50 |
|
{ |
51 |
10501 |
} |
52 |
|
|
53 |
21002 |
Preprocessor::~Preprocessor() |
54 |
|
{ |
55 |
10501 |
if (d_propagator.getNeedsFinish()) |
56 |
|
{ |
57 |
6817 |
d_propagator.finish(); |
58 |
6817 |
d_propagator.setNeedsFinish(false); |
59 |
|
} |
60 |
10501 |
} |
61 |
|
|
62 |
9856 |
void Preprocessor::finishInit() |
63 |
|
{ |
64 |
19712 |
d_ppContext.reset(new preprocessing::PreprocessingPassContext( |
65 |
9856 |
&d_smt, d_env, &d_propagator)); |
66 |
|
|
67 |
|
// initialize the preprocessing passes |
68 |
9856 |
d_processor.finishInit(d_ppContext.get()); |
69 |
9856 |
} |
70 |
|
|
71 |
13753 |
bool Preprocessor::process(Assertions& as) |
72 |
|
{ |
73 |
13753 |
preprocessing::AssertionPipeline& ap = as.getAssertionPipeline(); |
74 |
|
|
75 |
|
// should not be called if empty |
76 |
13753 |
Assert(ap.size() != 0) |
77 |
|
<< "Can only preprocess a non-empty list of assertions"; |
78 |
|
|
79 |
13753 |
if (d_assertionsProcessed && options::incrementalSolving()) |
80 |
|
{ |
81 |
|
// TODO(b/1255): Substitutions in incremental mode should be managed with a |
82 |
|
// proper data structure. |
83 |
3754 |
ap.enableStoreSubstsInAsserts(); |
84 |
|
} |
85 |
|
else |
86 |
|
{ |
87 |
9999 |
ap.disableStoreSubstsInAsserts(); |
88 |
|
} |
89 |
|
|
90 |
|
// process the assertions, return true if no conflict is discovered |
91 |
13753 |
bool noConflict = d_processor.apply(as); |
92 |
|
|
93 |
|
// now, post-process the assertions |
94 |
|
|
95 |
|
// if incremental, compute which variables are assigned |
96 |
13743 |
if (options::incrementalSolving()) |
97 |
|
{ |
98 |
6147 |
d_ppContext->recordSymbolsInAssertions(ap.ref()); |
99 |
|
} |
100 |
|
|
101 |
|
// mark that we've processed assertions |
102 |
13743 |
d_assertionsProcessed = true; |
103 |
|
|
104 |
13743 |
return noConflict; |
105 |
|
} |
106 |
|
|
107 |
3497 |
void Preprocessor::clearLearnedLiterals() |
108 |
|
{ |
109 |
3497 |
d_propagator.getLearnedLiterals().clear(); |
110 |
3497 |
} |
111 |
|
|
112 |
10501 |
void Preprocessor::cleanup() { d_processor.cleanup(); } |
113 |
|
|
114 |
4975 |
Node Preprocessor::expandDefinitions(const Node& n) |
115 |
|
{ |
116 |
9950 |
std::unordered_map<Node, Node> cache; |
117 |
9950 |
return expandDefinitions(n, cache); |
118 |
|
} |
119 |
|
|
120 |
5708 |
Node Preprocessor::expandDefinitions(const Node& node, |
121 |
|
std::unordered_map<Node, Node>& cache) |
122 |
|
{ |
123 |
5708 |
Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl; |
124 |
|
// Substitute out any abstract values in node. |
125 |
5708 |
Node n = d_absValues.substituteAbstractValues(node); |
126 |
5708 |
if (options::typeChecking()) |
127 |
|
{ |
128 |
|
// Ensure node is type-checked at this point. |
129 |
5708 |
n.getType(true); |
130 |
|
} |
131 |
|
// we apply substitutions here, before expanding definitions |
132 |
5708 |
n = d_env.getTopLevelSubstitutions().apply(n, false); |
133 |
|
// now call expand definitions |
134 |
5708 |
n = d_exDefs.expandDefinitions(n, cache); |
135 |
5708 |
return n; |
136 |
|
} |
137 |
|
|
138 |
68 |
Node Preprocessor::simplify(const Node& node) |
139 |
|
{ |
140 |
68 |
Trace("smt") << "SMT simplify(" << node << ")" << endl; |
141 |
68 |
if (Dump.isOn("benchmark")) |
142 |
|
{ |
143 |
|
d_smt.getOutputManager().getPrinter().toStreamCmdSimplify( |
144 |
|
d_smt.getOutputManager().getDumpOut(), node); |
145 |
|
} |
146 |
68 |
Node ret = expandDefinitions(node); |
147 |
68 |
ret = theory::Rewriter::rewrite(ret); |
148 |
68 |
return ret; |
149 |
|
} |
150 |
|
|
151 |
3771 |
void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) |
152 |
|
{ |
153 |
3771 |
Assert(pppg != nullptr); |
154 |
3771 |
d_pnm = pppg->getManager(); |
155 |
3771 |
d_exDefs.setProofNodeManager(d_pnm); |
156 |
3771 |
d_propagator.setProof(d_pnm, d_env.getUserContext(), pppg); |
157 |
3771 |
} |
158 |
|
|
159 |
|
} // namespace smt |
160 |
29358 |
} // namespace cvc5 |