1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Haniel Barbosa, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* [[ Add one-line brief description here ]] |
14 |
|
* |
15 |
|
* [[ Add lengthier description here ]] |
16 |
|
* \todo document this file |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "theory/builtin/theory_builtin_rewriter.h" |
20 |
|
|
21 |
|
#include "expr/attribute.h" |
22 |
|
#include "expr/node_algorithm.h" |
23 |
|
#include "theory/rewriter.h" |
24 |
|
|
25 |
|
using namespace std; |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace builtin { |
30 |
|
|
31 |
11026 |
Node TheoryBuiltinRewriter::blastDistinct(TNode in) { |
32 |
11026 |
Assert(in.getKind() == kind::DISTINCT); |
33 |
|
|
34 |
11026 |
if(in.getNumChildren() == 2) { |
35 |
|
// if this is the case exactly 1 != pair will be generated so the |
36 |
|
// AND is not required |
37 |
20174 |
Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, in[0], in[1]); |
38 |
20174 |
Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); |
39 |
10087 |
return neq; |
40 |
|
} |
41 |
|
|
42 |
|
// assume that in.getNumChildren() > 2 => diseqs.size() > 1 |
43 |
1878 |
vector<Node> diseqs; |
44 |
6640 |
for(TNode::iterator i = in.begin(); i != in.end(); ++i) { |
45 |
5701 |
TNode::iterator j = i; |
46 |
118939 |
while(++j != in.end()) { |
47 |
113238 |
Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, *i, *j); |
48 |
113238 |
Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); |
49 |
56619 |
diseqs.push_back(neq); |
50 |
|
} |
51 |
|
} |
52 |
1878 |
Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs); |
53 |
939 |
return out; |
54 |
|
} |
55 |
|
|
56 |
533842 |
RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) { |
57 |
|
// otherwise, do the default call |
58 |
533842 |
return doRewrite(node); |
59 |
|
} |
60 |
|
|
61 |
829987 |
RewriteResponse TheoryBuiltinRewriter::doRewrite(TNode node) |
62 |
|
{ |
63 |
829987 |
switch (node.getKind()) |
64 |
|
{ |
65 |
2469 |
case kind::WITNESS: |
66 |
|
{ |
67 |
|
// it is important to run this rewriting at prerewrite and postrewrite, |
68 |
|
// since e.g. arithmetic rewrites equalities in ways that may make an |
69 |
|
// equality not in solved form syntactically, e.g. (= x (+ 1 a)) rewrites |
70 |
|
// to (= a (- x 1)), where x no longer is in solved form. |
71 |
4938 |
Node rnode = rewriteWitness(node); |
72 |
2469 |
return RewriteResponse(REWRITE_DONE, rnode); |
73 |
|
} |
74 |
11026 |
case kind::DISTINCT: |
75 |
11026 |
return RewriteResponse(REWRITE_DONE, blastDistinct(node)); |
76 |
816492 |
default: return RewriteResponse(REWRITE_DONE, node); |
77 |
|
} |
78 |
|
} |
79 |
|
|
80 |
2469 |
Node TheoryBuiltinRewriter::rewriteWitness(TNode node) |
81 |
|
{ |
82 |
2469 |
Assert(node.getKind() == kind::WITNESS); |
83 |
2469 |
if (node[1].getKind() == kind::EQUAL) |
84 |
|
{ |
85 |
63 |
for (size_t i = 0; i < 2; i++) |
86 |
|
{ |
87 |
|
// (witness ((x T)) (= x t)) ---> t |
88 |
42 |
if (node[1][i] == node[0][0]) |
89 |
|
{ |
90 |
|
Trace("builtin-rewrite") << "Witness rewrite: " << node << " --> " |
91 |
|
<< node[1][1 - i] << std::endl; |
92 |
|
// also must be a legal elimination: the other side of the equality |
93 |
|
// cannot contain the variable, and it must be a subtype of the |
94 |
|
// variable |
95 |
|
if (!expr::hasSubterm(node[1][1 - i], node[0][0]) |
96 |
|
&& node[1][i].getType().isSubtypeOf(node[0][0].getType())) |
97 |
|
{ |
98 |
|
return node[1][1 - i]; |
99 |
|
} |
100 |
|
} |
101 |
|
} |
102 |
|
} |
103 |
2448 |
else if (node[1] == node[0][0]) |
104 |
|
{ |
105 |
|
// (witness ((x Bool)) x) ---> true |
106 |
|
return NodeManager::currentNM()->mkConst(true); |
107 |
|
} |
108 |
2448 |
else if (node[1].getKind() == kind::NOT && node[1][0] == node[0][0]) |
109 |
|
{ |
110 |
|
// (witness ((x Bool)) (not x)) ---> false |
111 |
|
return NodeManager::currentNM()->mkConst(false); |
112 |
|
} |
113 |
2469 |
return node; |
114 |
|
} |
115 |
|
|
116 |
|
} // namespace builtin |
117 |
|
} // namespace theory |
118 |
31137 |
} // namespace cvc5 |