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/env.h" |
26 |
|
#include "smt/preprocess_proof_generator.h" |
27 |
|
#include "smt/solver_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 |
18633 |
Preprocessor::Preprocessor(Env& env, |
38 |
|
AbstractValues& abs, |
39 |
18633 |
SolverEngineStatistics& stats) |
40 |
|
: EnvObj(env), |
41 |
|
d_absValues(abs), |
42 |
|
d_propagator(env, true, true), |
43 |
18633 |
d_assertionsProcessed(env.getUserContext(), false), |
44 |
|
d_exDefs(env), |
45 |
|
d_processor(env, stats), |
46 |
37266 |
d_pnm(nullptr) |
47 |
|
{ |
48 |
18633 |
} |
49 |
|
|
50 |
31768 |
Preprocessor::~Preprocessor() |
51 |
|
{ |
52 |
15884 |
if (d_propagator.getNeedsFinish()) |
53 |
|
{ |
54 |
12072 |
d_propagator.finish(); |
55 |
12072 |
d_propagator.setNeedsFinish(false); |
56 |
|
} |
57 |
15884 |
} |
58 |
|
|
59 |
15340 |
void Preprocessor::finishInit(TheoryEngine* te, prop::PropEngine* pe) |
60 |
|
{ |
61 |
30680 |
d_ppContext.reset(new preprocessing::PreprocessingPassContext( |
62 |
15340 |
d_env, te, pe, &d_propagator)); |
63 |
|
|
64 |
|
// initialize the preprocessing passes |
65 |
15340 |
d_processor.finishInit(d_ppContext.get()); |
66 |
15340 |
} |
67 |
|
|
68 |
19110 |
bool Preprocessor::process(Assertions& as) |
69 |
|
{ |
70 |
19110 |
preprocessing::AssertionPipeline& ap = as.getAssertionPipeline(); |
71 |
|
|
72 |
|
// should not be called if empty |
73 |
19110 |
Assert(ap.size() != 0) |
74 |
|
<< "Can only preprocess a non-empty list of assertions"; |
75 |
|
|
76 |
19110 |
if (d_assertionsProcessed && options().base.incrementalSolving) |
77 |
|
{ |
78 |
|
// TODO(b/1255): Substitutions in incremental mode should be managed with a |
79 |
|
// proper data structure. |
80 |
3764 |
ap.enableStoreSubstsInAsserts(); |
81 |
|
} |
82 |
|
else |
83 |
|
{ |
84 |
15346 |
ap.disableStoreSubstsInAsserts(); |
85 |
|
} |
86 |
|
|
87 |
|
// process the assertions, return true if no conflict is discovered |
88 |
19110 |
bool noConflict = d_processor.apply(as); |
89 |
|
|
90 |
|
// now, post-process the assertions |
91 |
|
|
92 |
|
// if incremental, compute which variables are assigned |
93 |
19095 |
if (options().base.incrementalSolving) |
94 |
|
{ |
95 |
10256 |
d_ppContext->recordSymbolsInAssertions(ap.ref()); |
96 |
|
} |
97 |
|
|
98 |
|
// mark that we've processed assertions |
99 |
19095 |
d_assertionsProcessed = true; |
100 |
|
|
101 |
19095 |
return noConflict; |
102 |
|
} |
103 |
|
|
104 |
3558 |
void Preprocessor::clearLearnedLiterals() |
105 |
|
{ |
106 |
3558 |
d_propagator.getLearnedLiterals().clear(); |
107 |
3558 |
} |
108 |
|
|
109 |
15884 |
void Preprocessor::cleanup() { d_processor.cleanup(); } |
110 |
|
|
111 |
11844 |
Node Preprocessor::expandDefinitions(const Node& n) |
112 |
|
{ |
113 |
23688 |
std::unordered_map<Node, Node> cache; |
114 |
23688 |
return expandDefinitions(n, cache); |
115 |
|
} |
116 |
|
|
117 |
12607 |
Node Preprocessor::expandDefinitions(const Node& node, |
118 |
|
std::unordered_map<Node, Node>& cache) |
119 |
|
{ |
120 |
12607 |
Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl; |
121 |
|
// Substitute out any abstract values in node. |
122 |
12607 |
Node n = d_absValues.substituteAbstractValues(node); |
123 |
12607 |
if (options().expr.typeChecking) |
124 |
|
{ |
125 |
|
// Ensure node is type-checked at this point. |
126 |
12607 |
n.getType(true); |
127 |
|
} |
128 |
|
// we apply substitutions here, before expanding definitions |
129 |
12607 |
n = d_env.getTopLevelSubstitutions().apply(n, false); |
130 |
|
// now call expand definitions |
131 |
12607 |
n = d_exDefs.expandDefinitions(n, cache); |
132 |
12607 |
return n; |
133 |
|
} |
134 |
|
|
135 |
110 |
void Preprocessor::expandDefinitions(std::vector<Node>& ns) |
136 |
|
{ |
137 |
220 |
std::unordered_map<Node, Node> cache; |
138 |
420 |
for (size_t i = 0, nasserts = ns.size(); i < nasserts; i++) |
139 |
|
{ |
140 |
310 |
ns[i] = expandDefinitions(ns[i], cache); |
141 |
|
} |
142 |
110 |
} |
143 |
|
|
144 |
70 |
Node Preprocessor::simplify(const Node& node) |
145 |
|
{ |
146 |
70 |
Trace("smt") << "SMT simplify(" << node << ")" << endl; |
147 |
70 |
Node ret = expandDefinitions(node); |
148 |
70 |
ret = rewrite(ret); |
149 |
70 |
return ret; |
150 |
|
} |
151 |
|
|
152 |
7989 |
void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) |
153 |
|
{ |
154 |
7989 |
Assert(pppg != nullptr); |
155 |
7989 |
d_pnm = pppg->getManager(); |
156 |
7989 |
d_exDefs.setProofNodeManager(d_pnm); |
157 |
7989 |
d_propagator.setProof(d_pnm, userContext(), pppg); |
158 |
7989 |
} |
159 |
|
|
160 |
|
} // namespace smt |
161 |
31137 |
} // namespace cvc5 |