GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/sort_infer.cpp Lines: 36 36 100.0 %
Date: 2021-03-22 Branches: 54 100 54.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sort_infer.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 Sort inference preprocessing pass
13
 **/
14
15
#include "preprocessing/passes/sort_infer.h"
16
17
#include "options/smt_options.h"
18
#include "options/uf_options.h"
19
#include "preprocessing/assertion_pipeline.h"
20
#include "preprocessing/preprocessing_pass_context.h"
21
#include "smt/dump_manager.h"
22
#include "smt/smt_engine_scope.h"
23
#include "theory/rewriter.h"
24
#include "theory/sort_inference.h"
25
#include "theory/theory_engine.h"
26
27
using namespace std;
28
29
namespace CVC4 {
30
namespace preprocessing {
31
namespace passes {
32
33
8995
SortInferencePass::SortInferencePass(PreprocessingPassContext* preprocContext)
34
8995
    : PreprocessingPass(preprocContext, "sort-inference")
35
{
36
8995
}
37
38
16
PreprocessingPassResult SortInferencePass::applyInternal(
39
    AssertionPipeline* assertionsToPreprocess)
40
{
41
  theory::SortInference* si =
42
16
      d_preprocContext->getTheoryEngine()->getSortInference();
43
44
32654
  if (options::sortInference())
45
  {
46
12
    si->initialize(assertionsToPreprocess->ref());
47
24
    std::map<Node, Node> model_replace_f;
48
24
    std::map<Node, std::map<TypeNode, Node> > visited;
49
61
    for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; i++)
50
    {
51
98
      Node prev = (*assertionsToPreprocess)[i];
52
98
      Node next = si->simplify(prev, model_replace_f, visited);
53
49
      if (next != prev)
54
      {
55
15
        next = theory::Rewriter::rewrite(next);
56
15
        assertionsToPreprocess->replace(i, next);
57
30
        Trace("sort-infer-preprocess")
58
15
            << "*** Preprocess SortInferencePass " << prev << endl;
59
30
        Trace("sort-infer-preprocess")
60
15
            << "   ...got " << (*assertionsToPreprocess)[i] << endl;
61
      }
62
    }
63
24
    std::vector<Node> newAsserts;
64
12
    si->getNewAssertions(newAsserts);
65
13
    for (const Node& na : newAsserts)
66
    {
67
2
      Node nar = theory::Rewriter::rewrite(na);
68
2
      Trace("sort-infer-preprocess")
69
1
          << "*** Preprocess SortInferencePass : new constraint " << nar
70
1
          << endl;
71
1
      assertionsToPreprocess->push_back(nar);
72
    }
73
    // indicate correspondence between the functions
74
12
    SmtEngine* smt = smt::currentSmtEngine();
75
12
    smt::DumpManager* dm = smt->getDumpManager();
76
17
    for (const std::pair<const Node, Node>& mrf : model_replace_f)
77
    {
78
5
      dm->setPrintFuncInModel(mrf.first, false);
79
5
      dm->setPrintFuncInModel(mrf.second, true);
80
    }
81
  }
82
  // only need to compute monotonicity on the resulting formula if we are
83
  // using this option
84
100407
  if (options::ufssFairnessMonotone())
85
  {
86
4
    si->computeMonotonicity(assertionsToPreprocess->ref());
87
  }
88
16
  return PreprocessingPassResult::NO_CONFLICT;
89
}
90
91
92
}  // namespace passes
93
}  // namespace preprocessing
94
159705
}  // namespace CVC4