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