GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/global_negate.cpp Lines: 48 49 98.0 %
Date: 2021-03-23 Branches: 86 166 51.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file global_negate.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Yoni Zohar
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 global_negate
13
 **/
14
15
#include "preprocessing/passes/global_negate.h"
16
17
#include <vector>
18
19
#include "expr/node.h"
20
#include "preprocessing/assertion_pipeline.h"
21
#include "theory/rewriter.h"
22
23
using namespace std;
24
using namespace CVC4::kind;
25
using namespace CVC4::theory;
26
27
namespace CVC4 {
28
namespace preprocessing {
29
namespace passes {
30
31
4
Node GlobalNegate::simplify(const std::vector<Node>& assertions,
32
                            NodeManager* nm)
33
{
34
4
  Assert(!assertions.empty());
35
4
  Trace("cegqi-gn") << "Global negate : " << std::endl;
36
  // collect free variables in all assertions
37
8
  std::vector<Node> free_vars;
38
8
  std::vector<TNode> visit;
39
8
  std::unordered_set<TNode, TNodeHashFunction> visited;
40
12
  for (const Node& as : assertions)
41
  {
42
8
    Trace("cegqi-gn") << "  " << as << std::endl;
43
16
    TNode cur = as;
44
    // compute free variables
45
8
    visit.push_back(cur);
46
167
    do
47
    {
48
175
      cur = visit.back();
49
175
      visit.pop_back();
50
175
      if (visited.find(cur) == visited.end())
51
      {
52
115
        visited.insert(cur);
53
115
        if (cur.isVar() && cur.getKind() != BOUND_VARIABLE)
54
        {
55
11
          free_vars.push_back(cur);
56
        }
57
282
        for (const TNode& cn : cur)
58
        {
59
167
          visit.push_back(cn);
60
        }
61
      }
62
175
    } while (!visit.empty());
63
  }
64
65
4
  Node body;
66
4
  if (assertions.size() == 1)
67
  {
68
    body = assertions[0];
69
  }
70
  else
71
  {
72
4
    body = nm->mkNode(AND, assertions);
73
  }
74
75
  // do the negation
76
4
  body = body.negate();
77
78
4
  if (!free_vars.empty())
79
  {
80
4
    std::vector<Node> bvs;
81
13
    for (const Node& v : free_vars)
82
    {
83
22
      Node bv = nm->mkBoundVar(v.getType());
84
11
      bvs.push_back(bv);
85
    }
86
87
2
    body = body.substitute(
88
        free_vars.begin(), free_vars.end(), bvs.begin(), bvs.end());
89
90
4
    Node bvl = nm->mkNode(BOUND_VAR_LIST, bvs);
91
92
2
    body = nm->mkNode(FORALL, bvl, body);
93
  }
94
95
4
  Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
96
4
  body = Rewriter::rewrite(body);
97
4
  Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl;
98
8
  return body;
99
}
100
101
8997
GlobalNegate::GlobalNegate(PreprocessingPassContext* preprocContext)
102
8997
    : PreprocessingPass(preprocContext, "global-negate"){};
103
104
4
PreprocessingPassResult GlobalNegate::applyInternal(
105
    AssertionPipeline* assertionsToPreprocess)
106
{
107
4
  NodeManager* nm = NodeManager::currentNM();
108
8
  Node simplifiedNode = simplify(assertionsToPreprocess->ref(), nm);
109
8
  Node trueNode = nm->mkConst(true);
110
12
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
111
  {
112
8
    if (i == 0)
113
    {
114
4
      assertionsToPreprocess->replace(i, simplifiedNode);
115
    }
116
    else
117
    {
118
4
      assertionsToPreprocess->replace(i, trueNode);
119
    }
120
  }
121
8
  return PreprocessingPassResult::NO_CONFLICT;
122
}
123
124
125
}  // namespace passes
126
}  // namespace preprocessing
127
26685
}  // namespace CVC4