GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/inference_manager.cpp Lines: 43 86 50.0 %
Date: 2021-03-23 Branches: 92 378 24.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 Implementation of the inference manager for the theory of sets
13
 **/
14
15
#include "theory/sets/inference_manager.h"
16
17
#include "options/sets_options.h"
18
#include "theory/rewriter.h"
19
20
using namespace std;
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace sets {
26
27
8997
InferenceManager::InferenceManager(Theory& t,
28
                                   SolverState& s,
29
8997
                                   ProofNodeManager* pnm)
30
8997
    : InferenceManagerBuffered(t, s, pnm, "theory::sets"), d_state(s)
31
{
32
8997
  d_true = NodeManager::currentNM()->mkConst(true);
33
8997
  d_false = NodeManager::currentNM()->mkConst(false);
34
8997
}
35
36
106153
bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
37
{
38
  // should we send this fact out as a lemma?
39
212310
  if ((options::setsInferAsLemmas() && inferType != -1) || inferType == 1)
40
  {
41
106153
    if (d_state.isEntailed(fact, true))
42
    {
43
77955
      return false;
44
    }
45
56396
    Node lem = fact;
46
28198
    if (exp != d_true)
47
    {
48
22990
      lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
49
    }
50
28198
    addPendingLemma(lem, id);
51
28198
    return true;
52
  }
53
  Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
54
                     << std::endl;
55
  if (fact.isConst())
56
  {
57
    // either trivial or a conflict
58
    if (fact == d_false)
59
    {
60
      Trace("sets-lemma") << "Conflict : " << exp << std::endl;
61
      conflict(exp, id);
62
      return true;
63
    }
64
    return false;
65
  }
66
  else if (fact.getKind() == AND
67
           || (fact.getKind() == NOT && fact[0].getKind() == OR))
68
  {
69
    bool ret = false;
70
    Node f = fact.getKind() == NOT ? fact[0] : fact;
71
    for (unsigned i = 0; i < f.getNumChildren(); i++)
72
    {
73
      Node factc = fact.getKind() == NOT ? f[i].negate() : f[i];
74
      bool tret = assertFactRec(factc, id, exp, inferType);
75
      ret = ret || tret;
76
      if (d_state.isInConflict())
77
      {
78
        return true;
79
      }
80
    }
81
    return ret;
82
  }
83
  bool polarity = fact.getKind() != NOT;
84
  TNode atom = polarity ? fact : fact[0];
85
  if (d_state.isEntailed(atom, polarity))
86
  {
87
    return false;
88
  }
89
  // things we can assert to equality engine
90
  if (atom.getKind() == MEMBER
91
      || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
92
  {
93
    // send to equality engine
94
    if (assertInternalFact(atom, polarity, id, exp))
95
    {
96
      // return true if this wasn't redundant
97
      return true;
98
    }
99
  }
100
  else
101
  {
102
    // must send as lemma
103
    Node lem = fact;
104
    if (exp != d_true)
105
    {
106
      lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
107
    }
108
    addPendingLemma(lem, id);
109
    return true;
110
  }
111
  return false;
112
}
113
106153
void InferenceManager::assertInference(Node fact,
114
                                       InferenceId id,
115
                                       Node exp,
116
                                       int inferType)
117
{
118
106153
  if (assertFactRec(fact, id, exp, inferType))
119
  {
120
56396
    Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
121
28198
                        << id << std::endl;
122
56396
    Trace("sets-assertion") << "(assert (=> " << exp << " " << fact
123
28198
                            << ")) ; by " << id << std::endl;
124
  }
125
106153
}
126
127
60253
void InferenceManager::assertInference(Node fact,
128
                                       InferenceId id,
129
                                       std::vector<Node>& exp,
130
                                       int inferType)
131
{
132
60253
  Node exp_n = exp.empty() ? d_true
133
56996
                           : (exp.size() == 1
134
2366
                                  ? exp[0]
135
179868
                                  : NodeManager::currentNM()->mkNode(AND, exp));
136
60253
  assertInference(fact, id, exp_n, inferType);
137
60253
}
138
139
4797
void InferenceManager::assertInference(std::vector<Node>& conc,
140
                                       InferenceId id,
141
                                       Node exp,
142
                                       int inferType)
143
{
144
4797
  if (!conc.empty())
145
  {
146
738
    Node fact = conc.size() == 1 ? conc[0]
147
1132
                                 : NodeManager::currentNM()->mkNode(AND, conc);
148
394
    assertInference(fact, id, exp, inferType);
149
  }
150
4797
}
151
void InferenceManager::assertInference(std::vector<Node>& conc,
152
                                       InferenceId id,
153
                                       std::vector<Node>& exp,
154
                                       int inferType)
155
{
156
  Node exp_n = exp.empty() ? d_true
157
                           : (exp.size() == 1
158
                                  ? exp[0]
159
                                  : NodeManager::currentNM()->mkNode(AND, exp));
160
  assertInference(conc, id, exp_n, inferType);
161
}
162
163
362
void InferenceManager::split(Node n, InferenceId id, int reqPol)
164
{
165
362
  n = Rewriter::rewrite(n);
166
724
  Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
167
  // send the lemma
168
362
  lemma(lem, id);
169
362
  Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
170
362
  if (reqPol != 0)
171
  {
172
    Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
173
                        << std::endl;
174
    requirePhase(n, reqPol > 0);
175
  }
176
362
}
177
178
}  // namespace sets
179
}  // namespace theory
180
132842
}  // namespace CVC4