8abc3f65a396fbd1652dab077ef033ec91306b33
1 /********************* */
2 /*! \file alpha_equivalence.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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
12 ** \brief Alpha equivalence checking
16 #include "theory/quantifiers/alpha_equivalence.h"
17 #include "theory/quantifiers/term_database.h"
21 using namespace CVC4::theory
;
22 using namespace CVC4::theory::quantifiers
;
23 using namespace CVC4::kind
;
25 struct sortTypeOrder
{
27 bool operator() (TypeNode i
, TypeNode j
) {
28 return d_tdb
->getIdForType( i
)<d_tdb
->getIdForType( j
);
32 bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode
* aen
, QuantifiersEngine
* qe
, Node q
, std::vector
< Node
>& tt
, std::vector
< int >& arg_index
) {
34 if( tt
.size()==arg_index
.size()+1 ){
36 Node op
= t
.hasOperator() ? t
.getOperator() : t
;
37 arg_index
.push_back( 0 );
38 Trace("aeq-debug") << op
<< " ";
39 aen
= &(aen
->d_children
[op
][t
.getNumChildren()]);
42 int i
= arg_index
.back();
43 if( i
==(int)t
.getNumChildren() ){
48 arg_index
[arg_index
.size()-1]++;
52 Trace("aeq-debug") << std::endl
;
53 if( aen
->d_quant
.isNull() ){
57 if( q
.getNumChildren()==2 ){
58 //lemma ( q <=> d_quant )
59 Trace("quant-ae") << "Alpha equivalent : " << std::endl
;
60 Trace("quant-ae") << " " << q
<< std::endl
;
61 Trace("quant-ae") << " " << aen
->d_quant
<< std::endl
;
62 qe
->getOutputChannel().lemma( q
.iffNode( aen
->d_quant
) );
65 //do not reduce annotated quantified formulas based on alpha equivalence
71 bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode
* aetn
,
72 QuantifiersEngine
* qe
, Node q
, Node t
, std::vector
< TypeNode
>& typs
, std::map
< TypeNode
, int >& typ_count
, int index
){
73 while( index
<(int)typs
.size() ){
74 TypeNode curr
= typs
[index
];
75 Assert( typ_count
.find( curr
)!=typ_count
.end() );
76 Trace("aeq-debug") << "[" << curr
<< " " << typ_count
[curr
] << "] ";
77 aetn
= &(aetn
->d_children
[curr
][typ_count
[curr
]]);
80 std::vector
< Node
> tt
;
81 std::vector
< int > arg_index
;
83 Trace("aeq-debug") << " : ";
84 return AlphaEquivalenceNode::registerNode( &(aetn
->d_data
), qe
, q
, tt
, arg_index
);
87 bool AlphaEquivalence::reduceQuantifier( Node q
) {
88 Assert( q
.getKind()==FORALL
);
89 Trace("aeq") << "Alpha equivalence : register " << q
<< std::endl
;
90 //construct canonical quantified formula
91 Node t
= d_qe
->getTermDatabase()->getCanonicalTerm( q
[1], true );
92 Trace("aeq") << " canonical form: " << t
<< std::endl
;
93 //compute variable type counts
94 std::map
< TypeNode
, int > typ_count
;
95 std::vector
< TypeNode
> typs
;
96 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
97 TypeNode tn
= q
[0][i
].getType();
99 if( std::find( typs
.begin(), typs
.end(), tn
)==typs
.end() ){
100 typs
.push_back( tn
);
104 sto
.d_tdb
= d_qe
->getTermDatabase();
105 std::sort( typs
.begin(), typs
.end(), sto
);
106 Trace("aeq-debug") << " ";
107 bool ret
= !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie
, d_qe
, q
, t
, typs
, typ_count
);
108 Trace("aeq") << " ...result : " << ret
<< std::endl
;