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