1 /********************* */
2 /*! \file alpha_equivalence.h
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
15 #include "cvc4_private.h"
17 #ifndef __CVC4__ALPHA_EQUIVALENCE_H
18 #define __CVC4__ALPHA_EQUIVALENCE_H
21 #include "theory/quantifiers_engine.h"
25 namespace quantifiers
{
27 class AlphaEquivalenceNode
{
29 std::map
< Node
, std::map
< int, AlphaEquivalenceNode
> > d_children
;
31 static bool registerNode( AlphaEquivalenceNode
* aen
, QuantifiersEngine
* qe
, Node q
, std::vector
< Node
>& tt
, std::vector
< int >& arg_index
);
34 class AlphaEquivalenceTypeNode
{
36 std::map
< TypeNode
, std::map
< int, AlphaEquivalenceTypeNode
> > d_children
;
37 AlphaEquivalenceNode d_data
;
38 static bool registerNode( AlphaEquivalenceTypeNode
* aetn
,
39 QuantifiersEngine
* qe
, Node q
, Node t
, std::vector
< TypeNode
>& typs
, std::map
< TypeNode
, int >& typ_count
, int index
= 0 );
42 class AlphaEquivalence
{
44 QuantifiersEngine
* d_qe
;
45 //per # of variables per type
46 AlphaEquivalenceTypeNode d_ae_typ_trie
;
48 AlphaEquivalence( QuantifiersEngine
* qe
) : d_qe( qe
){}
51 bool reduceQuantifier( Node q
);