GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/alpha_equivalence.cpp Lines: 53 55 96.4 %
Date: 2021-03-22 Branches: 106 244 43.4 %

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