GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/ackermann.cpp Lines: 106 109 97.2 %
Date: 2021-03-23 Branches: 217 526 41.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ackermann.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Ying Sheng, Yoni Zohar, Aina Niemetz
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 Ackermannization preprocessing pass.
13
 **
14
 ** This implements the Ackermannization preprocessing pass, which enables
15
 ** very limited theory combination support for eager bit-blasting via
16
 ** Ackermannization. It reduces constraints over the combination of the
17
 ** theories of fixed-size bit-vectors and uninterpreted functions as
18
 ** described in
19
 **   Liana Hadarean, An Efficient and Trustworthy Theory Solver for
20
 **   Bit-vectors in Satisfiability Modulo Theories.
21
 **   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
22
 **/
23
24
#include "preprocessing/passes/ackermann.h"
25
26
#include <cmath>
27
28
#include "base/check.h"
29
#include "expr/node_algorithm.h"
30
#include "options/options.h"
31
#include "options/smt_options.h"
32
#include "preprocessing/assertion_pipeline.h"
33
#include "preprocessing/preprocessing_pass_context.h"
34
35
using namespace CVC4;
36
using namespace CVC4::theory;
37
38
namespace CVC4 {
39
namespace preprocessing {
40
namespace passes {
41
42
/* -------------------------------------------------------------------------- */
43
44
namespace {
45
46
292
void addLemmaForPair(TNode args1,
47
                     TNode args2,
48
                     const TNode func,
49
                     AssertionPipeline* assertionsToPreprocess,
50
                     NodeManager* nm)
51
{
52
584
  Node args_eq;
53
54
292
  if (args1.getKind() == kind::APPLY_UF)
55
  {
56
230
    Assert(args1.getOperator() == func);
57
230
    Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func);
58
230
    Assert(args1.getNumChildren() == args2.getNumChildren());
59
230
    Assert(args1.getNumChildren() >= 1);
60
61
460
    std::vector<Node> eqs(args1.getNumChildren());
62
63
460
    for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
64
    {
65
230
      eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
66
    }
67
230
    if (eqs.size() >= 2)
68
    {
69
      args_eq = nm->mkNode(kind::AND, eqs);
70
    }
71
    else
72
    {
73
230
      args_eq = eqs[0];
74
    }
75
  }
76
  else
77
  {
78
62
    Assert(args1.getKind() == kind::SELECT && args1.getOperator() == func);
79
62
    Assert(args2.getKind() == kind::SELECT && args2.getOperator() == func);
80
62
    Assert(args1.getNumChildren() == 2);
81
62
    Assert(args2.getNumChildren() == 2);
82
186
    args_eq = nm->mkNode(Kind::AND,
83
124
      nm->mkNode(kind::EQUAL, args1[0], args2[0]),
84
124
      nm->mkNode(kind::EQUAL, args1[1], args2[1])
85
    );
86
  }
87
584
  Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
88
584
  Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
89
292
  assertionsToPreprocess->push_back(lemma);
90
292
}
91
92
188
void storeFunctionAndAddLemmas(TNode func,
93
                               TNode term,
94
                               FunctionToArgsMap& fun_to_args,
95
                               SubstitutionMap& fun_to_skolem,
96
                               AssertionPipeline* assertions,
97
                               NodeManager* nm,
98
                               std::vector<TNode>* vec)
99
{
100
188
  if (fun_to_args.find(func) == fun_to_args.end())
101
  {
102
60
    fun_to_args.insert(make_pair(func, TNodeSet()));
103
  }
104
188
  TNodeSet& set = fun_to_args[func];
105
188
  if (set.find(term) == set.end())
106
  {
107
376
    TypeNode tn = term.getType();
108
    Node skolem = nm->mkSkolem("SKOLEM$$",
109
                               tn,
110
                               "is a variable created by the ackermannization "
111
376
                               "preprocessing pass");
112
480
    for (const auto& t : set)
113
    {
114
292
      addLemmaForPair(t, term, func, assertions, nm);
115
    }
116
188
    fun_to_skolem.addSubstitution(term, skolem);
117
188
    set.insert(term);
118
    /* Add the arguments of term (newest element in set) to the vector, so that
119
     * collectFunctionsAndLemmas will process them as well.
120
     * This is only needed if the set has at least two elements
121
     * (otherwise, no lemma is generated).
122
     * Therefore, we defer this for term in case it is the first element in the
123
     * set*/
124
188
    if (set.size() == 2)
125
    {
126
156
      for (TNode elem : set)
127
      {
128
104
        vec->insert(vec->end(), elem.begin(), elem.end());
129
      }
130
    }
131
136
    else if (set.size() > 2)
132
    {
133
76
      vec->insert(vec->end(), term.begin(), term.end());
134
    }
135
  }
136
188
}
137
138
/* We only add top-level applications of functions.
139
 * For example: when we see "f(g(x))", we do not add g as a function and x as a
140
 * parameter.
141
 * Instead, we only include f as a function and g(x) as a parameter.
142
 * However, if we see g(x) later on as a top-level application, we will add it
143
 * as well.
144
 * Another example: for the formula f(g(x))=f(g(y)),
145
 * we first only add f as a function and g(x),g(y) as arguments.
146
 * storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) ->
147
 * f(g(x))=f(g(y)).
148
 * Now that we see g(x) and g(y), we explicitly add them as well. */
149
43
void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
150
                               SubstitutionMap& fun_to_skolem,
151
                               std::vector<TNode>* vec,
152
                               AssertionPipeline* assertions)
153
{
154
86
  TNodeSet seen;
155
43
  NodeManager* nm = NodeManager::currentNM();
156
86
  TNode term;
157
5921
  while (!vec->empty())
158
  {
159
2939
    term = vec->back();
160
2939
    vec->pop_back();
161
2939
    if (seen.find(term) == seen.end())
162
    {
163
3348
      TNode func;
164
1674
      if (term.getKind() == kind::APPLY_UF || term.getKind() == kind::SELECT)
165
      {
166
188
        storeFunctionAndAddLemmas(term.getOperator(),
167
                                  term,
168
                                  fun_to_args,
169
                                  fun_to_skolem,
170
                                  assertions,
171
                                  nm,
172
                                  vec);
173
      }
174
      else
175
      {
176
1486
        AlwaysAssert(term.getKind() != kind::STORE)
177
            << "Cannot use Ackermannization on formula with stores to arrays";
178
        /* add children to the vector, so that they are processed later */
179
4026
        for (TNode n : term)
180
        {
181
2540
          vec->push_back(n);
182
        }
183
      }
184
1674
      seen.insert(term);
185
    }
186
  }
187
43
}
188
189
}  // namespace
190
191
/* -------------------------------------------------------------------------- */
192
193
/* Given a minimum capacity for an uninterpreted sort, return the size of the
194
 * new BV type */
195
42
size_t getBVSkolemSize(size_t capacity)
196
{
197
42
  return static_cast<size_t>(log2(capacity)) + 1;
198
}
199
200
/* Given the lowest capacity requirements for each uninterpreted sort, assign
201
 * a sufficient bit-vector size.
202
 * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
203
 * the fresh skolem BV variables. variables */
204
6
void collectUSortsToBV(const std::unordered_set<TNode, TNodeHashFunction>& vars,
205
                       const USortToBVSizeMap& usortCardinality,
206
                       SubstitutionMap& usVarsToBVVars)
207
{
208
6
  NodeManager* nm = NodeManager::currentNM();
209
210
48
  for (TNode var : vars)
211
  {
212
84
    TypeNode type = var.getType();
213
42
    size_t size = getBVSkolemSize(usortCardinality.at(type));
214
    Node skolem = nm->mkSkolem(
215
        "BVSKOLEM$$",
216
84
        nm->mkBitVectorType(size),
217
        "a variable created by the ackermannization "
218
        "preprocessing pass, representing a variable with uninterpreted sort "
219
168
            + type.toString() + ".");
220
42
    usVarsToBVVars.addSubstitution(var, skolem);
221
  }
222
6
}
223
224
/* This function returns the list of terms with uninterpreted sort in the
225
 * formula represented by assertions. */
226
43
std::unordered_set<TNode, TNodeHashFunction> getVarsWithUSorts(
227
    AssertionPipeline* assertions)
228
{
229
43
  std::unordered_set<TNode, TNodeHashFunction> res;
230
231
526
  for (const Node& assertion : assertions->ref())
232
  {
233
966
    std::unordered_set<TNode, TNodeHashFunction> vars;
234
483
    expr::getVariables(assertion, vars);
235
236
2016
    for (const TNode& var : vars)
237
    {
238
1533
      if (var.getType().isSort())
239
      {
240
162
        res.insert(var);
241
      }
242
    }
243
  }
244
245
43
  return res;
246
}
247
248
/* This is the top level of converting uninterpreted sorts to bit-vectors.
249
 * We count the number of different variables for each uninterpreted sort.
250
 * Then for each sort, we will assign a new bit-vector type with a sufficient
251
 * size. The size is calculated to have enough capacity, that can accommodate
252
 * the variables occured in the original formula. At the end, all variables of
253
 * uninterpreted sorts will be converted into Skolem variables of BV */
254
43
void usortsToBitVectors(const LogicInfo& d_logic,
255
                        AssertionPipeline* assertions,
256
                        USortToBVSizeMap& usortCardinality,
257
                        SubstitutionMap& usVarsToBVVars)
258
{
259
  std::unordered_set<TNode, TNodeHashFunction> toProcess =
260
86
      getVarsWithUSorts(assertions);
261
262
43
  if (toProcess.size() > 0)
263
  {
264
    /* the current version only supports BV for removing uninterpreted sorts */
265
6
    if (not d_logic.isTheoryEnabled(theory::THEORY_BV))
266
    {
267
      return;
268
    }
269
270
48
    for (TNode term : toProcess)
271
    {
272
84
      TypeNode type = term.getType();
273
      /* Update the counts for each uninterpreted sort.
274
       * For non-existing keys, C++ will create a new element for it, which has
275
       * a default 0 value, before incrementing by 1. */
276
42
      usortCardinality[type] = usortCardinality[type] + 1;
277
    }
278
279
6
    collectUSortsToBV(toProcess, usortCardinality, usVarsToBVVars);
280
281
102
    for (size_t i = 0, size = assertions->size(); i < size; ++i)
282
    {
283
192
      Node old = (*assertions)[i];
284
192
      Node newA = usVarsToBVVars.apply((*assertions)[i]);
285
96
      if (newA != old)
286
      {
287
72
        assertions->replace(i, newA);
288
144
        Trace("uninterpretedSorts-to-bv")
289
72
            << "  " << old << " => " << (*assertions)[i] << "\n";
290
      }
291
    }
292
  }
293
}
294
295
/* -------------------------------------------------------------------------- */
296
297
8997
Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
298
    : PreprocessingPass(preprocContext, "ackermann"),
299
      d_funcToSkolem(preprocContext->getUserContext()),
300
      d_usVarsToBVVars(preprocContext->getUserContext()),
301
8997
      d_logic(preprocContext->getLogicInfo())
302
{
303
8997
}
304
305
43
PreprocessingPassResult Ackermann::applyInternal(
306
    AssertionPipeline* assertionsToPreprocess)
307
{
308
43
  AlwaysAssert(!options::incrementalSolving());
309
310
  /* collect all function applications and generate consistency lemmas
311
   * accordingly */
312
86
  std::vector<TNode> to_process;
313
234
  for (const Node& a : assertionsToPreprocess->ref())
314
  {
315
191
    to_process.push_back(a);
316
  }
317
43
  collectFunctionsAndLemmas(
318
      d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess);
319
320
  /* replace applications of UF by skolems */
321
  // FIXME for model building, github issue #1901
322
526
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
323
  {
324
483
    assertionsToPreprocess->replace(
325
966
        i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
326
  }
327
328
  /* replace uninterpreted sorts with bit-vectors */
329
43
  usortsToBitVectors(
330
      d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars);
331
332
86
  return PreprocessingPassResult::NO_CONFLICT;
333
}
334
335
/* -------------------------------------------------------------------------- */
336
337
}  // namespace passes
338
}  // namespace preprocessing
339
26685
}  // namespace CVC4