GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets.cpp Lines: 100 108 92.6 %
Date: 2021-03-22 Branches: 150 316 47.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Kshitij Bansal, Andres Noetzli
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 Sets theory.
13
 **
14
 ** Sets theory.
15
 **/
16
17
#include "theory/sets/theory_sets.h"
18
19
#include "options/sets_options.h"
20
#include "theory/sets/theory_sets_private.h"
21
#include "theory/sets/theory_sets_rewriter.h"
22
#include "theory/theory_model.h"
23
#include "theory/trust_substitutions.h"
24
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace sets {
30
31
8995
TheorySets::TheorySets(context::Context* c,
32
                       context::UserContext* u,
33
                       OutputChannel& out,
34
                       Valuation valuation,
35
                       const LogicInfo& logicInfo,
36
8995
                       ProofNodeManager* pnm)
37
    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
38
      d_skCache(),
39
      d_state(c, u, valuation, d_skCache),
40
      d_im(*this, d_state, nullptr),
41
8995
      d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)),
42
17990
      d_notify(*d_internal.get(), d_im)
43
{
44
  // use the official theory state and inference manager objects
45
8995
  d_theoryState = &d_state;
46
8995
  d_inferManager = &d_im;
47
8995
}
48
49
17984
TheorySets::~TheorySets()
50
{
51
17984
}
52
53
8995
TheoryRewriter* TheorySets::getTheoryRewriter()
54
{
55
8995
  return d_internal->getTheoryRewriter();
56
}
57
58
8995
bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
59
{
60
8995
  esi.d_notify = &d_notify;
61
8995
  esi.d_name = "theory::sets::ee";
62
8995
  return true;
63
}
64
65
8995
void TheorySets::finishInit()
66
{
67
8995
  Assert(d_equalityEngine != nullptr);
68
69
8995
  d_valuation.setUnevaluatedKind(COMPREHENSION);
70
  // choice is used to eliminate witness
71
8995
  d_valuation.setUnevaluatedKind(WITNESS);
72
  // Universe set is not evaluated. This is moreover important for ensuring that
73
  // we do not eliminate terms whose value involves the universe set.
74
8995
  d_valuation.setUnevaluatedKind(UNIVERSE_SET);
75
76
  // functions we are doing congruence over
77
8995
  d_equalityEngine->addFunctionKind(SINGLETON);
78
8995
  d_equalityEngine->addFunctionKind(UNION);
79
8995
  d_equalityEngine->addFunctionKind(INTERSECTION);
80
8995
  d_equalityEngine->addFunctionKind(SETMINUS);
81
8995
  d_equalityEngine->addFunctionKind(MEMBER);
82
8995
  d_equalityEngine->addFunctionKind(SUBSET);
83
  // relation operators
84
8995
  d_equalityEngine->addFunctionKind(PRODUCT);
85
8995
  d_equalityEngine->addFunctionKind(JOIN);
86
8995
  d_equalityEngine->addFunctionKind(TRANSPOSE);
87
8995
  d_equalityEngine->addFunctionKind(TCLOSURE);
88
8995
  d_equalityEngine->addFunctionKind(JOIN_IMAGE);
89
8995
  d_equalityEngine->addFunctionKind(IDEN);
90
8995
  d_equalityEngine->addFunctionKind(APPLY_CONSTRUCTOR);
91
  // we do congruence over cardinality
92
8995
  d_equalityEngine->addFunctionKind(CARD);
93
94
  // finish initialization internally
95
8995
  d_internal->finishInit();
96
8995
}
97
98
67774
void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
99
100
107382
void TheorySets::notifyFact(TNode atom,
101
                            bool polarity,
102
                            TNode fact,
103
                            bool isInternal)
104
{
105
107382
  d_internal->notifyFact(atom, polarity, fact);
106
107382
}
107
108
4576
bool TheorySets::collectModelValues(TheoryModel* m,
109
                                    const std::set<Node>& termSet)
110
{
111
4576
  return d_internal->collectModelValues(m, termSet);
112
}
113
114
5913
void TheorySets::computeCareGraph() {
115
5913
  d_internal->computeCareGraph();
116
5913
}
117
118
1896
TrustNode TheorySets::explain(TNode node)
119
{
120
3792
  Node exp = d_internal->explain(node);
121
3792
  return TrustNode::mkTrustPropExp(node, exp, nullptr);
122
}
123
124
Node TheorySets::getModelValue(TNode node) {
125
  return Node::null();
126
}
127
128
58456
void TheorySets::preRegisterTerm(TNode node)
129
{
130
58456
  d_internal->preRegisterTerm(node);
131
58456
}
132
133
20
TrustNode TheorySets::expandDefinition(Node n)
134
{
135
  // we currently do not expand any set operators
136
20
  return TrustNode::null();
137
}
138
139
44544
TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
140
{
141
44544
  Kind nk = n.getKind();
142
44544
  if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
143
44003
      || nk == COMPREHENSION)
144
  {
145
564
    if (!options::setsExt())
146
    {
147
4
      std::stringstream ss;
148
2
      ss << "Extended set operators are not supported in default mode, try "
149
            "--sets-ext.";
150
2
      throw LogicException(ss.str());
151
    }
152
  }
153
44542
  if (nk == COMPREHENSION)
154
  {
155
    // set comprehension is an implicit quantifier, require it in the logic
156
23
    if (!getLogicInfo().isQuantified())
157
    {
158
2
      std::stringstream ss;
159
1
      ss << "Set comprehensions require quantifiers in the background logic.";
160
1
      throw LogicException(ss.str());
161
    }
162
  }
163
44541
  return d_internal->ppRewrite(n, lems);
164
}
165
166
2832
Theory::PPAssertStatus TheorySets::ppAssert(
167
    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
168
{
169
5664
  TNode in = tin.getNode();
170
2832
  Debug("sets-proc") << "ppAssert : " << in << std::endl;
171
2832
  Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
172
173
  // this is based off of Theory::ppAssert
174
2832
  if (in.getKind() == EQUAL)
175
  {
176
1064
    if (in[0].isVar() && isLegalElimination(in[0], in[1]))
177
    {
178
      // We cannot solve for sets if setsExt is enabled, since universe set
179
      // may appear when this option is enabled, and solving for such a set
180
      // impacts the semantics of universe set, see
181
      // regress0/sets/pre-proc-univ.smt2
182
333
      if (!in[0].getType().isSet() || !options::setsExt())
183
      {
184
273
        outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
185
273
        status = Theory::PP_ASSERT_STATUS_SOLVED;
186
      }
187
    }
188
731
    else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
189
    {
190
14
      if (!in[0].getType().isSet() || !options::setsExt())
191
      {
192
        outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
193
        status = Theory::PP_ASSERT_STATUS_SOLVED;
194
      }
195
    }
196
717
    else if (in[0].isConst() && in[1].isConst())
197
    {
198
      if (in[0] != in[1])
199
      {
200
        status = Theory::PP_ASSERT_STATUS_CONFLICT;
201
      }
202
    }
203
  }
204
5664
  return status;
205
}
206
207
12416
void TheorySets::presolve() {
208
12416
  d_internal->presolve();
209
12416
}
210
211
bool TheorySets::isEntailed( Node n, bool pol ) {
212
  return d_internal->isEntailed( n, pol );
213
}
214
215
/**************************** eq::NotifyClass *****************************/
216
217
49866
void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
218
{
219
99732
  Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:"
220
49866
                   << " t = " << t << std::endl;
221
49866
  d_theory.eqNotifyNewClass(t);
222
49866
}
223
224
114752
void TheorySets::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
225
{
226
229504
  Debug("sets-eq") << "[sets-eq] eqNotifyMerge:"
227
114752
                   << " t1 = " << t1 << " t2 = " << t2 << std::endl;
228
114752
  d_theory.eqNotifyMerge(t1, t2);
229
114752
}
230
231
26889
void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
232
{
233
53778
  Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:"
234
26889
                   << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
235
26889
                   << std::endl;
236
26889
  d_theory.eqNotifyDisequal(t1, t2, reason);
237
26889
}
238
239
}/* CVC4::theory::sets namespace */
240
}/* CVC4::theory namespace */
241
26676
}/* CVC4 namespace */