GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/preprocessor.cpp Lines: 60 63 95.2 %
Date: 2021-09-17 Branches: 54 130 41.5 %

Line Exec Source
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
13209
Preprocessor::Preprocessor(SmtEngine& smt,
39
                           Env& env,
40
                           AbstractValues& abs,
41
13209
                           SmtEngineStatistics& stats)
42
    : d_smt(smt),
43
      d_env(env),
44
      d_absValues(abs),
45
      d_propagator(true, true),
46
13209
      d_assertionsProcessed(env.getUserContext(), false),
47
      d_exDefs(env, stats),
48
13209
      d_processor(smt, *env.getResourceManager(), stats),
49
39627
      d_pnm(nullptr)
50
{
51
13209
}
52
53
21124
Preprocessor::~Preprocessor()
54
{
55
10562
  if (d_propagator.getNeedsFinish())
56
  {
57
6842
    d_propagator.finish();
58
6842
    d_propagator.setNeedsFinish(false);
59
  }
60
10562
}
61
62
9942
void Preprocessor::finishInit()
63
{
64
19884
  d_ppContext.reset(new preprocessing::PreprocessingPassContext(
65
9942
      &d_smt, d_env, &d_propagator));
66
67
  // initialize the preprocessing passes
68
9942
  d_processor.finishInit(d_ppContext.get());
69
9942
}
70
71
13802
bool Preprocessor::process(Assertions& as)
72
{
73
13802
  preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
74
75
  // should not be called if empty
76
13802
  Assert(ap.size() != 0)
77
      << "Can only preprocess a non-empty list of assertions";
78
79
13802
  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
10048
    ap.disableStoreSubstsInAsserts();
88
  }
89
90
  // process the assertions, return true if no conflict is discovered
91
13802
  bool noConflict = d_processor.apply(as);
92
93
  // now, post-process the assertions
94
95
  // if incremental, compute which variables are assigned
96
13792
  if (options::incrementalSolving())
97
  {
98
6155
    d_ppContext->recordSymbolsInAssertions(ap.ref());
99
  }
100
101
  // mark that we've processed assertions
102
13792
  d_assertionsProcessed = true;
103
104
13792
  return noConflict;
105
}
106
107
3497
void Preprocessor::clearLearnedLiterals()
108
{
109
3497
  d_propagator.getLearnedLiterals().clear();
110
3497
}
111
112
10562
void Preprocessor::cleanup() { d_processor.cleanup(); }
113
114
4252
Node Preprocessor::expandDefinitions(const Node& n)
115
{
116
8504
  std::unordered_map<Node, Node> cache;
117
8504
  return expandDefinitions(n, cache);
118
}
119
120
4922
Node Preprocessor::expandDefinitions(const Node& node,
121
                                     std::unordered_map<Node, Node>& cache)
122
{
123
4922
  Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl;
124
  // Substitute out any abstract values in node.
125
4922
  Node n = d_absValues.substituteAbstractValues(node);
126
4922
  if (options::typeChecking())
127
  {
128
    // Ensure node is type-checked at this point.
129
4922
    n.getType(true);
130
  }
131
  // we apply substitutions here, before expanding definitions
132
4922
  n = d_env.getTopLevelSubstitutions().apply(n, false);
133
  // now call expand definitions
134
4922
  n = d_exDefs.expandDefinitions(n, cache);
135
4922
  return n;
136
}
137
138
84
void Preprocessor::expandDefinitions(std::vector<Node>& ns)
139
{
140
168
  std::unordered_map<Node, Node> cache;
141
312
  for (size_t i = 0, nasserts = ns.size(); i < nasserts; i++)
142
  {
143
228
    ns[i] = expandDefinitions(ns[i], cache);
144
  }
145
84
}
146
147
68
Node Preprocessor::simplify(const Node& node)
148
{
149
68
  Trace("smt") << "SMT simplify(" << node << ")" << endl;
150
68
  if (Dump.isOn("benchmark"))
151
  {
152
    d_smt.getOutputManager().getPrinter().toStreamCmdSimplify(
153
        d_smt.getOutputManager().getDumpOut(), node);
154
  }
155
68
  Node ret = expandDefinitions(node);
156
68
  ret = theory::Rewriter::rewrite(ret);
157
68
  return ret;
158
}
159
160
3796
void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
161
{
162
3796
  Assert(pppg != nullptr);
163
3796
  d_pnm = pppg->getManager();
164
3796
  d_exDefs.setProofNodeManager(d_pnm);
165
3796
  d_propagator.setProof(d_pnm, d_env.getUserContext(), pppg);
166
3796
}
167
168
}  // namespace smt
169
29577
}  // namespace cvc5