1 /********************* */
2 /*! \file alpha_equivalence.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 Alpha equivalence checking
13 **
14 **/
15
16 #include "theory/quantifiers/alpha_equivalence.h"
17 #include "theory/quantifiers/term_canonize.h"
18
19 using namespace CVC4;
20 using namespace std;
21 using namespace CVC4::theory;
22 using namespace CVC4::theory::quantifiers;
23 using namespace CVC4::kind;
24
25 struct sortTypeOrder {
26 TermCanonize* d_tu;
operator ()sortTypeOrder27 bool operator() (TypeNode i, TypeNode j) {
28 return d_tu->getIdForType( i )<d_tu->getIdForType( j );
29 }
30 };
31
registerNode(Node q,Node t)32 Node AlphaEquivalenceNode::registerNode(Node q, Node t)
33 {
34 AlphaEquivalenceNode* aen = this;
35 std::vector<Node> tt;
36 std::vector<int> arg_index;
37 tt.push_back(t);
38 std::map< Node, bool > visited;
39 while( !tt.empty() ){
40 if( tt.size()==arg_index.size()+1 ){
41 Node t = tt.back();
42 Node op;
43 if( t.hasOperator() ){
44 if( visited.find( t )==visited.end() ){
45 visited[t] = true;
46 op = t.getOperator();
47 arg_index.push_back( 0 );
48 }else{
49 op = t;
50 arg_index.push_back( -1 );
51 }
52 }else{
53 op = t;
54 arg_index.push_back( 0 );
55 }
56 Trace("aeq-debug") << op << " ";
57 aen = &(aen->d_children[op][t.getNumChildren()]);
58 }else{
59 Node t = tt.back();
60 int i = arg_index.back();
61 if( i==-1 || i==(int)t.getNumChildren() ){
62 tt.pop_back();
63 arg_index.pop_back();
64 }else{
65 tt.push_back( t[i] );
66 arg_index[arg_index.size()-1]++;
67 }
68 }
69 }
70 Trace("aeq-debug") << std::endl;
71 if( aen->d_quant.isNull() ){
72 aen->d_quant = q;
73 }
74 return aen->d_quant;
75 }
76
registerNode(Node q,Node t,std::vector<TypeNode> & typs,std::map<TypeNode,int> & typ_count)77 Node AlphaEquivalenceTypeNode::registerNode(Node q,
78 Node t,
79 std::vector<TypeNode>& typs,
80 std::map<TypeNode, int>& typ_count)
81 {
82 AlphaEquivalenceTypeNode* aetn = this;
83 unsigned index = 0;
84 while (index < typs.size())
85 {
86 TypeNode curr = typs[index];
87 Assert( typ_count.find( curr )!=typ_count.end() );
88 Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] ";
89 aetn = &(aetn->d_children[curr][typ_count[curr]]);
90 index = index + 1;
91 }
92 Trace("aeq-debug") << " : ";
93 return aetn->d_data.registerNode(q, t);
94 }
95
addTerm(Node q)96 Node AlphaEquivalenceDb::addTerm(Node q)
97 {
98 Assert( q.getKind()==FORALL );
99 Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
100 //construct canonical quantified formula
101 Node t = d_tc->getCanonicalTerm(q[1], true);
102 Trace("aeq") << " canonical form: " << t << std::endl;
103 //compute variable type counts
104 std::map< TypeNode, int > typ_count;
105 std::vector< TypeNode > typs;
106 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
107 TypeNode tn = q[0][i].getType();
108 typ_count[tn]++;
109 if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
110 typs.push_back( tn );
111 }
112 }
113 sortTypeOrder sto;
114 sto.d_tu = d_tc;
115 std::sort( typs.begin(), typs.end(), sto );
116 Trace("aeq-debug") << " ";
117 Node ret = d_ae_typ_trie.registerNode(q, t, typs, typ_count);
118 Trace("aeq") << " ...result : " << ret << std::endl;
119 return ret;
120 }
121
AlphaEquivalence(QuantifiersEngine * qe)122 AlphaEquivalence::AlphaEquivalence(QuantifiersEngine* qe)
123 : d_aedb(qe->getTermCanonize())
124 {
125 }
126
reduceQuantifier(Node q)127 Node AlphaEquivalence::reduceQuantifier(Node q)
128 {
129 Assert(q.getKind() == FORALL);
130 Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
131 Node ret = d_aedb.addTerm(q);
132 Node lem;
133 if (ret != q)
134 {
135 // do not reduce annotated quantified formulas based on alpha equivalence
136 if (q.getNumChildren() == 2)
137 {
138 // lemma ( q <=> d_quant )
139 Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
140 Trace("alpha-eq") << " " << q << std::endl;
141 Trace("alpha-eq") << " " << ret << std::endl;
142 lem = q.eqNode(ret);
143 }
144 }
145 return lem;
146 }
147