GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/assertions.cpp Lines: 85 95 89.5 %
Date: 2021-03-23 Branches: 99 228 43.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file assertions.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
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 module for storing assertions for an SMT engine.
13
 **/
14
15
#include "smt/assertions.h"
16
17
#include <sstream>
18
19
#include "expr/node_algorithm.h"
20
#include "options/base_options.h"
21
#include "options/language.h"
22
#include "options/smt_options.h"
23
#include "proof/proof_manager.h"
24
#include "smt/abstract_values.h"
25
#include "smt/smt_engine.h"
26
27
using namespace CVC4::theory;
28
using namespace CVC4::kind;
29
30
namespace CVC4 {
31
namespace smt {
32
33
9622
Assertions::Assertions(context::UserContext* u, AbstractValues& absv)
34
    : d_userContext(u),
35
      d_absValues(absv),
36
      d_assertionList(nullptr),
37
      d_globalNegation(false),
38
9622
      d_assertions()
39
{
40
9622
}
41
42
19202
Assertions::~Assertions()
43
{
44
9601
  if (d_assertionList != nullptr)
45
  {
46
4670
    d_assertionList->deleteSelf();
47
  }
48
9601
}
49
50
8997
void Assertions::finishInit()
51
{
52
  // [MGD 10/20/2011] keep around in incremental mode, due to a
53
  // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
54
  // first, some user-context-dependent TNodes might still exist
55
  // with rc == 0.
56
23594
  if (options::produceAssertions() || options::incrementalSolving())
57
  {
58
    // In the case of incremental solving, we appear to need these to
59
    // ensure the relevant Nodes remain live.
60
4671
    d_assertionList = new (true) AssertionList(d_userContext);
61
4671
    d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
62
  }
63
8997
}
64
65
13478
void Assertions::clearCurrent()
66
{
67
13478
  d_assertions.clear();
68
13478
  d_assertions.getIteSkolemMap().clear();
69
13478
}
70
71
12435
void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
72
                                    bool inUnsatCore,
73
                                    bool isEntailmentCheck)
74
{
75
12435
  NodeManager* nm = NodeManager::currentNM();
76
  // reset global negation
77
12435
  d_globalNegation = false;
78
  // clear the assumptions
79
12435
  d_assumptions.clear();
80
12435
  if (isEntailmentCheck)
81
  {
82
275
    size_t size = assumptions.size();
83
275
    if (size > 1)
84
    {
85
      /* Assume: not (BIGAND assumptions)  */
86
2
      d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode());
87
    }
88
273
    else if (size == 1)
89
    {
90
      /* Assume: not expr  */
91
273
      d_assumptions.push_back(assumptions[0].notNode());
92
    }
93
  }
94
  else
95
  {
96
    /* Assume: BIGAND assumptions  */
97
12160
    d_assumptions = assumptions;
98
  }
99
100
24870
  Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
101
14646
  for (const Node& e : d_assumptions)
102
  {
103
    // Substitute out any abstract values in ex.
104
4422
    Node n = d_absValues.substituteAbstractValues(e);
105
    // Ensure expr is type-checked at this point.
106
2211
    ensureBoolean(n);
107
2211
    addFormula(n, inUnsatCore, true, true, false);
108
  }
109
12435
  if (d_globalDefineFunRecLemmas != nullptr)
110
  {
111
    // Global definitions are asserted at check-sat-time because we have to
112
    // make sure that they are always present (they are essentially level
113
    // zero assertions)
114
8152
    for (const Node& lemma : *d_globalDefineFunRecLemmas)
115
    {
116
30
      addFormula(lemma, false, true, false, false);
117
    }
118
  }
119
12435
}
120
121
79466
void Assertions::assertFormula(const Node& n, bool inUnsatCore)
122
{
123
79466
  ensureBoolean(n);
124
79466
  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
125
79466
  addFormula(n, inUnsatCore, true, false, maybeHasFv);
126
79466
}
127
128
8
std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
129
12401
bool Assertions::isGlobalNegated() const { return d_globalNegation; }
130
4
void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; }
131
132
40889
preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
133
{
134
40889
  return d_assertions;
135
}
136
137
3329
context::CDList<Node>* Assertions::getAssertionList()
138
{
139
3329
  return d_assertionList;
140
}
141
142
81887
void Assertions::addFormula(
143
    TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
144
{
145
  // add to assertion list if it exists
146
81887
  if (d_assertionList != nullptr)
147
  {
148
37076
    d_assertionList->push_back(n);
149
  }
150
81887
  if (n.isConst() && n.getConst<bool>())
151
  {
152
    // true, nothing to do
153
216
    return;
154
  }
155
156
163342
  Trace("smt") << "SmtEnginePrivate::addFormula(" << n
157
81671
               << "), inUnsatCore = " << inUnsatCore
158
81671
               << ", inInput = " << inInput
159
81671
               << ", isAssumption = " << isAssumption << std::endl;
160
161
  // Ensure that it does not contain free variables
162
81671
  if (maybeHasFv)
163
  {
164
1055
    if (expr::hasFreeVar(n))
165
    {
166
      std::stringstream se;
167
      se << "Cannot process assertion with free variable.";
168
      if (language::isInputLangSygus(options::inputLanguage()))
169
      {
170
        // Common misuse of SyGuS is to use top-level assert instead of
171
        // constraint when defining the synthesis conjecture.
172
        se << " Perhaps you meant `constraint` instead of `assert`?";
173
      }
174
      throw ModalException(se.str().c_str());
175
    }
176
  }
177
178
  // Give it to the old proof manager
179
81671
  if (options::unsatCores() && !isProofEnabled())
180
  {
181
15512
    if (inInput)
182
    {  // n is an input assertion
183
316455
      if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores()
184
39218
          || options::checkUnsatCores())
185
      {
186
15512
        ProofManager::currentPM()->addCoreAssertion(n);
187
      }
188
    }
189
    else
190
    {
191
      // n is the result of an unknown preprocessing step, add it to dependency
192
      // map to null
193
      ProofManager::currentPM()->addDependence(n, Node::null());
194
    }
195
  }
196
197
  // Add the normalized formula to the queue
198
81671
  d_assertions.push_back(n, isAssumption, true);
199
}
200
201
196
void Assertions::addDefineFunRecDefinition(Node n, bool global)
202
{
203
196
  n = d_absValues.substituteAbstractValues(n);
204
196
  if (d_assertionList != nullptr)
205
  {
206
103
    d_assertionList->push_back(n);
207
  }
208
196
  if (global && d_globalDefineFunRecLemmas != nullptr)
209
  {
210
    // Global definitions are asserted at check-sat-time because we have to
211
    // make sure that they are always present
212
16
    Assert(!language::isInputLangSygus(options::inputLanguage()));
213
16
    d_globalDefineFunRecLemmas->emplace_back(n);
214
  }
215
  else
216
  {
217
180
    bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
218
180
    addFormula(n, false, true, false, maybeHasFv);
219
  }
220
196
}
221
222
81677
void Assertions::ensureBoolean(const Node& n)
223
{
224
268958
  TypeNode type = n.getType(options::typeChecking());
225
81677
  if (!type.isBoolean())
226
  {
227
    std::stringstream ss;
228
    ss << "Expected Boolean type\n"
229
       << "The assertion : " << n << "\n"
230
       << "Its type      : " << type;
231
    throw TypeCheckingExceptionPrivate(n, ss.str());
232
  }
233
81677
}
234
235
962
void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
236
{
237
962
  d_assertions.setProofGenerator(pppg);
238
962
}
239
240
15512
bool Assertions::isProofEnabled() const
241
{
242
15512
  return d_assertions.isProofEnabled();
243
}
244
245
}  // namespace smt
246
461884
}  // namespace CVC4