1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
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 |
|
* Alpha equivalence checking. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/alpha_equivalence.h" |
17 |
|
|
18 |
|
using namespace cvc5::kind; |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
namespace theory { |
22 |
|
namespace quantifiers { |
23 |
|
|
24 |
|
struct sortTypeOrder { |
25 |
|
expr::TermCanonize* d_tu; |
26 |
22014 |
bool operator() (TypeNode i, TypeNode j) { |
27 |
22014 |
return d_tu->getIdForType( i )<d_tu->getIdForType( j ); |
28 |
|
} |
29 |
|
}; |
30 |
|
|
31 |
26930 |
Node AlphaEquivalenceTypeNode::registerNode( |
32 |
|
Node q, |
33 |
|
Node t, |
34 |
|
std::vector<TypeNode>& typs, |
35 |
|
std::map<TypeNode, size_t>& typCount) |
36 |
|
{ |
37 |
26930 |
AlphaEquivalenceTypeNode* aetn = this; |
38 |
26930 |
size_t index = 0; |
39 |
107458 |
while (index < typs.size()) |
40 |
|
{ |
41 |
80528 |
TypeNode curr = typs[index]; |
42 |
40264 |
Assert(typCount.find(curr) != typCount.end()); |
43 |
40264 |
Trace("aeq-debug") << "[" << curr << " " << typCount[curr] << "] "; |
44 |
80528 |
std::pair<TypeNode, size_t> key(curr, typCount[curr]); |
45 |
40264 |
aetn = &(aetn->d_children[key]); |
46 |
40264 |
index = index + 1; |
47 |
|
} |
48 |
26930 |
Trace("aeq-debug") << " : "; |
49 |
26930 |
std::map<Node, Node>::iterator it = aetn->d_quant.find(t); |
50 |
26930 |
if (it != aetn->d_quant.end()) |
51 |
|
{ |
52 |
1882 |
return it->second; |
53 |
|
} |
54 |
25048 |
aetn->d_quant[t] = q; |
55 |
25048 |
return q; |
56 |
|
} |
57 |
|
|
58 |
26930 |
Node AlphaEquivalenceDb::addTerm(Node q) |
59 |
|
{ |
60 |
26930 |
Assert(q.getKind() == FORALL); |
61 |
26930 |
Trace("aeq") << "Alpha equivalence : register " << q << std::endl; |
62 |
|
//construct canonical quantified formula |
63 |
53860 |
Node t = d_tc->getCanonicalTerm(q[1], true); |
64 |
26930 |
Trace("aeq") << " canonical form: " << t << std::endl; |
65 |
|
//compute variable type counts |
66 |
53860 |
std::map<TypeNode, size_t> typCount; |
67 |
53860 |
std::vector< TypeNode > typs; |
68 |
89439 |
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ |
69 |
125018 |
TypeNode tn = q[0][i].getType(); |
70 |
62509 |
typCount[tn]++; |
71 |
62509 |
if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){ |
72 |
40264 |
typs.push_back( tn ); |
73 |
|
} |
74 |
|
} |
75 |
|
sortTypeOrder sto; |
76 |
26930 |
sto.d_tu = d_tc; |
77 |
26930 |
std::sort( typs.begin(), typs.end(), sto ); |
78 |
26930 |
Trace("aeq-debug") << " "; |
79 |
26930 |
Node ret = d_ae_typ_trie.registerNode(q, t, typs, typCount); |
80 |
26930 |
Trace("aeq") << " ...result : " << ret << std::endl; |
81 |
53860 |
return ret; |
82 |
|
} |
83 |
|
|
84 |
6413 |
AlphaEquivalence::AlphaEquivalence() : d_termCanon(), d_aedb(&d_termCanon) {} |
85 |
|
|
86 |
26930 |
Node AlphaEquivalence::reduceQuantifier(Node q) |
87 |
|
{ |
88 |
26930 |
Assert(q.getKind() == FORALL); |
89 |
26930 |
Trace("aeq") << "Alpha equivalence : register " << q << std::endl; |
90 |
53860 |
Node ret = d_aedb.addTerm(q); |
91 |
26930 |
Node lem; |
92 |
26930 |
if (ret != q) |
93 |
|
{ |
94 |
|
// lemma ( q <=> d_quant ) |
95 |
|
// Notice that we infer this equivalence regardless of whether q or ret |
96 |
|
// have annotations (e.g. user patterns, names, etc.). |
97 |
1882 |
Trace("alpha-eq") << "Alpha equivalent : " << std::endl; |
98 |
1882 |
Trace("alpha-eq") << " " << q << std::endl; |
99 |
1882 |
Trace("alpha-eq") << " " << ret << std::endl; |
100 |
1882 |
lem = q.eqNode(ret); |
101 |
1882 |
if (q.getNumChildren() == 3) |
102 |
|
{ |
103 |
128 |
Notice() << "Ignoring annotated quantified formula based on alpha " |
104 |
|
"equivalence: " |
105 |
|
<< q << std::endl; |
106 |
|
} |
107 |
|
} |
108 |
53860 |
return lem; |
109 |
|
} |
110 |
|
|
111 |
|
} // namespace quantifiers |
112 |
|
} // namespace theory |
113 |
28191 |
} // namespace cvc5 |