GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/theory_bags.cpp Lines: 108 122 88.5 %
Date: 2021-03-23 Branches: 161 398 40.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bags.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed, Andrew Reynolds
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 Bags theory.
13
 **/
14
15
#include "theory/bags/theory_bags.h"
16
17
#include "smt/logic_exception.h"
18
#include "theory/bags/normal_form.h"
19
#include "theory/rewriter.h"
20
#include "theory/theory_model.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace bags {
27
28
8997
TheoryBags::TheoryBags(context::Context* c,
29
                       context::UserContext* u,
30
                       OutputChannel& out,
31
                       Valuation valuation,
32
                       const LogicInfo& logicInfo,
33
8997
                       ProofNodeManager* pnm)
34
    : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm),
35
      d_state(c, u, valuation),
36
      d_im(*this, d_state, nullptr),
37
      d_ig(&d_state, &d_im),
38
      d_notify(*this, d_im),
39
      d_statistics(),
40
      d_rewriter(&d_statistics.d_rewrites),
41
      d_termReg(d_state, d_im),
42
8997
      d_solver(d_state, d_im, d_termReg)
43
{
44
  // use the official theory state and inference manager objects
45
8997
  d_theoryState = &d_state;
46
8997
  d_inferManager = &d_im;
47
8997
}
48
49
17988
TheoryBags::~TheoryBags() {}
50
51
8997
TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
52
53
8997
bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
54
{
55
8997
  esi.d_notify = &d_notify;
56
8997
  esi.d_name = "theory::bags::ee";
57
8997
  return true;
58
}
59
60
8997
void TheoryBags::finishInit()
61
{
62
8997
  Assert(d_equalityEngine != nullptr);
63
64
  // choice is used to eliminate witness
65
8997
  d_valuation.setUnevaluatedKind(WITNESS);
66
67
  // functions we are doing congruence over
68
8997
  d_equalityEngine->addFunctionKind(UNION_MAX);
69
8997
  d_equalityEngine->addFunctionKind(UNION_DISJOINT);
70
8997
  d_equalityEngine->addFunctionKind(INTERSECTION_MIN);
71
8997
  d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT);
72
8997
  d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE);
73
8997
  d_equalityEngine->addFunctionKind(BAG_COUNT);
74
8997
  d_equalityEngine->addFunctionKind(DUPLICATE_REMOVAL);
75
8997
  d_equalityEngine->addFunctionKind(MK_BAG);
76
8997
  d_equalityEngine->addFunctionKind(BAG_CARD);
77
8997
  d_equalityEngine->addFunctionKind(BAG_FROM_SET);
78
8997
  d_equalityEngine->addFunctionKind(BAG_TO_SET);
79
8997
}
80
81
19583
void TheoryBags::postCheck(Effort effort)
82
{
83
19583
  d_im.doPendingFacts();
84
  // TODO issue #78: add Assert(d_strat.isStrategyInit());
85
19583
  if (!d_state.isInConflict() && !d_valuation.needCheck())
86
  // TODO issue #78:  add && d_strat.hasStrategyEffort(e))
87
  {
88
11257
    Trace("bags::TheoryBags::postCheck") << "effort: " << std::endl;
89
90
    // TODO issue #78: add ++(d_statistics.d_checkRuns);
91
11257
    bool sentLemma = false;
92
11257
    bool hadPending = false;
93
11257
    Trace("bags-check") << "Full effort check..." << std::endl;
94
    do
95
    {
96
11257
      d_im.reset();
97
      // TODO issue #78: add ++(d_statistics.d_strategyRuns);
98
11257
      Trace("bags-check") << "  * Run strategy..." << std::endl;
99
      // TODO issue #78: add runStrategy(e);
100
101
11257
      d_solver.postCheck();
102
103
      // remember if we had pending facts or lemmas
104
11257
      hadPending = d_im.hasPending();
105
      // Send the facts *and* the lemmas. We send lemmas regardless of whether
106
      // we send facts since some lemmas cannot be dropped. Other lemmas are
107
      // otherwise avoided by aborting the strategy when a fact is ready.
108
11257
      d_im.doPending();
109
      // Did we successfully send a lemma? Notice that if hasPending = true
110
      // and sentLemma = false, then the above call may have:
111
      // (1) had no pending lemmas, but successfully processed pending facts,
112
      // (2) unsuccessfully processed pending lemmas.
113
      // In either case, we repeat the strategy if we are not in conflict.
114
11257
      sentLemma = d_im.hasSentLemma();
115
11257
      if (Trace.isOn("bags-check"))
116
      {
117
        // TODO: clean this Trace("bags-check") << "  ...finish run strategy: ";
118
        Trace("bags-check") << (hadPending ? "hadPending " : "");
119
        Trace("bags-check") << (sentLemma ? "sentLemma " : "");
120
        Trace("bags-check") << (d_state.isInConflict() ? "conflict " : "");
121
        if (!hadPending && !sentLemma && !d_state.isInConflict())
122
        {
123
          Trace("bags-check") << "(none)";
124
        }
125
        Trace("bags-check") << std::endl;
126
      }
127
      // repeat if we did not add a lemma or conflict, and we had pending
128
      // facts or lemmas.
129
11257
    } while (!d_state.isInConflict() && !sentLemma && hadPending);
130
  }
131
19583
  Trace("bags-check") << "Theory of bags, done check : " << effort << std::endl;
132
19583
  Assert(!d_im.hasPendingFact());
133
19583
  Assert(!d_im.hasPendingLemma());
134
19583
}
135
136
2204
void TheoryBags::notifyFact(TNode atom,
137
                            bool polarity,
138
                            TNode fact,
139
                            bool isInternal)
140
{
141
2204
}
142
143
4553
bool TheoryBags::collectModelValues(TheoryModel* m,
144
                                    const std::set<Node>& termSet)
145
{
146
4553
  Trace("bags-model") << "TheoryBags : Collect model values" << std::endl;
147
148
4553
  Trace("bags-model") << "Term set: " << termSet << std::endl;
149
150
9106
  std::set<Node> processedBags;
151
152
  // get the relevant bag equivalence classes
153
4760
  for (const Node& n : termSet)
154
  {
155
237
    TypeNode tn = n.getType();
156
207
    if (!tn.isBag())
157
    {
158
      // we are only concerned here about bag terms
159
151
      continue;
160
    }
161
86
    Node r = d_state.getRepresentative(n);
162
56
    if (processedBags.find(r) != processedBags.end())
163
    {
164
      // skip bags whose representatives are already processed
165
26
      continue;
166
    }
167
168
30
    processedBags.insert(r);
169
170
60
    std::set<Node> solverElements = d_state.getElements(r);
171
60
    std::set<Node> elements;
172
    // only consider terms in termSet and ignore other elements in the solver
173
30
    std::set_intersection(termSet.begin(),
174
                          termSet.end(),
175
                          solverElements.begin(),
176
                          solverElements.end(),
177
30
                          std::inserter(elements, elements.begin()));
178
60
    Trace("bags-model") << "Elements of bag " << n << " are: " << std::endl
179
30
                        << elements << std::endl;
180
60
    std::map<Node, Node> elementReps;
181
72
    for (const Node& e : elements)
182
    {
183
84
      Node key = d_state.getRepresentative(e);
184
84
      Node countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, r);
185
84
      Node value = d_state.getRepresentative(countTerm);
186
42
      elementReps[key] = value;
187
    }
188
60
    Node rep = NormalForm::constructBagFromElements(tn, elementReps);
189
30
    rep = Rewriter::rewrite(rep);
190
191
30
    Trace("bags-model") << "rep of " << n << " is: " << rep << std::endl;
192
72
    for (std::pair<Node, Node> pair : elementReps)
193
    {
194
42
      m->assertSkeleton(pair.first);
195
42
      m->assertSkeleton(pair.second);
196
    }
197
30
    m->assertEquality(rep, n, true);
198
30
    m->assertSkeleton(rep);
199
  }
200
9106
  return true;
201
}
202
203
873
TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); }
204
205
Node TheoryBags::getModelValue(TNode node) { return Node::null(); }
206
207
1224
void TheoryBags::preRegisterTerm(TNode n)
208
{
209
1224
  Trace("bags::TheoryBags::preRegisterTerm") << n << std::endl;
210
1224
  switch (n.getKind())
211
  {
212
    case BAG_CARD:
213
    case BAG_FROM_SET:
214
    case BAG_TO_SET:
215
    case BAG_IS_SINGLETON:
216
    {
217
      std::stringstream ss;
218
      ss << "Term of kind " << n.getKind() << " is not supported yet";
219
      throw LogicException(ss.str());
220
    }
221
1224
    default: break;
222
  }
223
1224
}
224
225
TrustNode TheoryBags::expandDefinition(Node n)
226
{
227
  // TODO(projects#224): add choose and is_singleton here
228
  return TrustNode::null();
229
}
230
231
12418
void TheoryBags::presolve() {}
232
233
/**************************** eq::NotifyClass *****************************/
234
235
935
void TheoryBags::eqNotifyNewClass(TNode n) {}
236
237
1781
void TheoryBags::eqNotifyMerge(TNode n1, TNode n2) {}
238
239
197
void TheoryBags::eqNotifyDisequal(TNode n1, TNode n2, TNode reason) {}
240
241
935
void TheoryBags::NotifyClass::eqNotifyNewClass(TNode n)
242
{
243
1870
  Debug("bags-eq") << "[bags-eq] eqNotifyNewClass:"
244
935
                   << " n = " << n << std::endl;
245
935
  d_theory.eqNotifyNewClass(n);
246
935
}
247
248
1781
void TheoryBags::NotifyClass::eqNotifyMerge(TNode n1, TNode n2)
249
{
250
3562
  Debug("bags-eq") << "[bags-eq] eqNotifyMerge:"
251
1781
                   << " n1 = " << n1 << " n2 = " << n2 << std::endl;
252
1781
  d_theory.eqNotifyMerge(n1, n2);
253
1781
}
254
255
197
void TheoryBags::NotifyClass::eqNotifyDisequal(TNode n1, TNode n2, TNode reason)
256
{
257
394
  Debug("bags-eq") << "[bags-eq] eqNotifyDisequal:"
258
197
                   << " n1 = " << n1 << " n2 = " << n2 << " reason = " << reason
259
197
                   << std::endl;
260
197
  d_theory.eqNotifyDisequal(n1, n2, reason);
261
197
}
262
263
}  // namespace bags
264
}  // namespace theory
265
26685
}  // namespace CVC4