GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/model_blocker.cpp Lines: 122 144 84.7 %
Date: 2021-03-22 Branches: 279 766 36.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file model_blocker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 utility for blocking models.
13
 **
14
 **/
15
16
#include "smt/model_blocker.h"
17
18
#include "expr/node.h"
19
#include "expr/node_algorithm.h"
20
#include "theory/quantifiers/term_util.h"
21
#include "theory/rewriter.h"
22
#include "theory/theory_model.h"
23
24
using namespace CVC4::kind;
25
26
namespace CVC4 {
27
28
20
Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
29
                                   theory::TheoryModel* m,
30
                                   options::BlockModelsMode mode,
31
                                   const std::vector<Node>& exprToBlock)
32
{
33
20
  NodeManager* nm = NodeManager::currentNM();
34
  // convert to nodes
35
40
  std::vector<Node> tlAsserts = assertions;
36
40
  std::vector<Node> nodesToBlock = exprToBlock;
37
20
  Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
38
40
  Node blocker;
39
20
  if (mode == options::BlockModelsMode::LITERALS)
40
  {
41
8
    Assert(nodesToBlock.empty());
42
    // optimization: filter out top-level unit assertions, as they cannot
43
    // contribute to model blocking.
44
8
    unsigned counter = 0;
45
16
    std::vector<Node> asserts;
46
48
    while (counter < tlAsserts.size())
47
    {
48
40
      Node cur = tlAsserts[counter];
49
20
      counter++;
50
40
      Node catom = cur.getKind() == NOT ? cur[0] : cur;
51
20
      bool cpol = cur.getKind() != NOT;
52
20
      if (catom.getKind() == NOT)
53
      {
54
        tlAsserts.push_back(catom[0]);
55
      }
56
20
      else if (catom.getKind() == AND && cpol)
57
      {
58
        tlAsserts.insert(tlAsserts.end(), catom.begin(), catom.end());
59
      }
60
20
      else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
61
      {
62
8
        asserts.push_back(cur);
63
8
        Trace("model-blocker") << "  " << cur << std::endl;
64
      }
65
    }
66
8
    if (asserts.empty())
67
    {
68
      Node blockTriv = nm->mkConst(false);
69
      Trace("model-blocker")
70
          << "...model blocker is (trivially) " << blockTriv << std::endl;
71
      return blockTriv;
72
    }
73
74
16
    Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0];
75
16
    std::unordered_map<TNode, Node, TNodeHashFunction> visited;
76
16
    std::unordered_map<TNode, Node, TNodeHashFunction> implicant;
77
8
    std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
78
16
    std::vector<TNode> visit;
79
16
    TNode cur;
80
8
    visit.push_back(formula);
81
22
    do
82
    {
83
30
      cur = visit.back();
84
30
      visit.pop_back();
85
30
      it = visited.find(cur);
86
87
30
      Trace("model-blocker-debug") << "Visit : " << cur << std::endl;
88
89
30
      if (it == visited.end())
90
      {
91
18
        visited[cur] = Node::null();
92
36
        Node catom = cur.getKind() == NOT ? cur[0] : cur;
93
18
        bool cpol = cur.getKind() != NOT;
94
        // compute the implicant
95
        // impl is a formula that implies cur that is also satisfied by m
96
36
        Node impl;
97
18
        if (catom.getKind() == NOT)
98
        {
99
          // double negation
100
          impl = catom[0];
101
        }
102
18
        else if (catom.getKind() == OR || catom.getKind() == AND)
103
        {
104
          // if disjunctive
105
8
          if ((catom.getKind() == OR) == cpol)
106
          {
107
            // take the first literal that is satisfied
108
18
            for (Node n : catom)
109
            {
110
              // rewrite, this ensures that e.g. the propositional value of
111
              // quantified formulas can be queried
112
18
              n = theory::Rewriter::rewrite(n);
113
30
              Node vn = m->getValue(n);
114
18
              Assert(vn.isConst());
115
18
              if (vn.getConst<bool>() == cpol)
116
              {
117
6
                impl = cpol ? n : n.negate();
118
6
                break;
119
              }
120
            }
121
          }
122
2
          else if (catom.getKind() == OR)
123
          {
124
            // one step NNF
125
            std::vector<Node> children;
126
            for (const Node& cn : catom)
127
            {
128
              children.push_back(cn.negate());
129
            }
130
            impl = nm->mkNode(AND, children);
131
          }
132
        }
133
10
        else if (catom.getKind() == ITE)
134
        {
135
          Node vcond = m->getValue(cur[0]);
136
          Assert(vcond.isConst());
137
          Node cond = cur[0];
138
          Node branch;
139
          if (vcond.getConst<bool>())
140
          {
141
            branch = cur[1];
142
          }
143
          else
144
          {
145
            cond = cond.negate();
146
            branch = cur[2];
147
          }
148
          impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate());
149
        }
150
28
        else if ((catom.getKind() == EQUAL && catom[0].getType().isBoolean())
151
28
                 || catom.getKind() == XOR)
152
        {
153
          // based on how the children evaluate in the model
154
4
          std::vector<Node> children;
155
6
          for (const Node& cn : catom)
156
          {
157
8
            Node vn = m->getValue(cn);
158
4
            Assert(vn.isConst());
159
4
            children.push_back(vn.getConst<bool>() ? cn : cn.negate());
160
          }
161
2
          impl = nm->mkNode(AND, children);
162
        }
163
        else
164
        {
165
          // literals justified by themselves
166
8
          visited[cur] = cur;
167
8
          Trace("model-blocker-debug") << "...self justified" << std::endl;
168
        }
169
18
        if (visited[cur].isNull())
170
        {
171
10
          visit.push_back(cur);
172
10
          if (impl.isNull())
173
          {
174
2
            Assert(cur.getKind() == AND);
175
2
            Trace("model-blocker-debug") << "...recurse" << std::endl;
176
2
            visit.insert(visit.end(), cur.begin(), cur.end());
177
          }
178
          else
179
          {
180
16
            Trace("model-blocker-debug")
181
8
                << "...implicant : " << impl << std::endl;
182
8
            implicant[cur] = impl;
183
8
            visit.push_back(impl);
184
          }
185
        }
186
      }
187
12
      else if (it->second.isNull())
188
      {
189
20
        Node ret = cur;
190
10
        it = implicant.find(cur);
191
10
        if (it != implicant.end())
192
        {
193
16
          Node impl = it->second;
194
8
          it = visited.find(impl);
195
8
          Assert(it != visited.end());
196
8
          Assert(!it->second.isNull());
197
8
          ret = it->second;
198
16
          Trace("model-blocker-debug")
199
8
              << "...implicant res: " << ret << std::endl;
200
        }
201
        else
202
        {
203
2
          bool childChanged = false;
204
4
          std::vector<Node> children;
205
          // we never recurse to parameterized nodes
206
2
          Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
207
6
          for (const Node& cn : cur)
208
          {
209
4
            it = visited.find(cn);
210
4
            Assert(it != visited.end());
211
4
            Assert(!it->second.isNull());
212
4
            childChanged = childChanged || cn != it->second;
213
4
            children.push_back(it->second);
214
          }
215
2
          if (childChanged)
216
          {
217
            ret = nm->mkNode(cur.getKind(), children);
218
          }
219
2
          Trace("model-blocker-debug") << "...recons res: " << ret << std::endl;
220
        }
221
10
        visited[cur] = ret;
222
      }
223
30
    } while (!visit.empty());
224
8
    Assert(visited.find(formula) != visited.end());
225
8
    Assert(!visited.find(formula)->second.isNull());
226
8
    blocker = visited[formula].negate();
227
  }
228
  else
229
  {
230
12
    Assert(mode == options::BlockModelsMode::VALUES);
231
24
    std::vector<Node> blockers;
232
    // if specific terms were not specified, block all variables of
233
    // the model
234
12
    if (nodesToBlock.empty())
235
    {
236
8
      Trace("model-blocker")
237
4
          << "no specific terms to block recognized" << std::endl;
238
8
      std::unordered_set<Node, NodeHashFunction> symbols;
239
22
      for (Node n : tlAsserts)
240
      {
241
18
        expr::getSymbols(n, symbols);
242
      }
243
20
      for (Node s : symbols)
244
      {
245
16
        if (s.getType().getKind() != kind::FUNCTION_TYPE)
246
        {
247
24
          Node v = m->getValue(s);
248
24
          Node a = nm->mkNode(DISTINCT, s, v);
249
12
          blockers.push_back(a);
250
        }
251
      }
252
    }
253
    // otherwise, block all terms that were specified in get-value
254
    else
255
    {
256
16
      std::unordered_set<Node, NodeHashFunction> terms;
257
16
      for (Node n : nodesToBlock)
258
      {
259
16
        Node v = m->getValue(n);
260
16
        Node a = nm->mkNode(DISTINCT, n, v);
261
8
        blockers.push_back(a);
262
      }
263
    }
264
12
    if (blockers.size() == 0)
265
    {
266
      blocker = nm->mkConst<bool>(true);
267
    }
268
12
    else if (blockers.size() == 1)
269
    {
270
8
      blocker = blockers[0];
271
    }
272
    else
273
    {
274
4
      blocker = nm->mkNode(OR, blockers);
275
    }
276
  }
277
20
  Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
278
20
  return blocker;
279
}
280
281
26676
} /* namespace CVC4 */