GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/preprocessor.cpp Lines: 58 61 95.1 %
Date: 2021-03-23 Branches: 62 156 39.7 %

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