GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/alpha_equivalence.h Lines: 4 4 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file alpha_equivalence.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Paul Meng
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
#include "cvc4_private.h"
16
17
#ifndef CVC4__ALPHA_EQUIVALENCE_H
18
#define CVC4__ALPHA_EQUIVALENCE_H
19
20
#include "theory/quantifiers/quant_util.h"
21
22
#include "expr/term_canonize.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
/**
29
 * This trie stores a trie of the above form for each multi-set of types. For
30
 * each term t registered to this node, we store t in the appropriate
31
 * AlphaEquivalenceNode trie. For example, if t contains 2 free variables
32
 * of type T1 and 3 free variables of type T2, then it is stored at
33
 * d_children[T1][2].d_children[T2][3].
34
 */
35
30717
class AlphaEquivalenceTypeNode {
36
public:
37
 /** children of this node */
38
 std::map<std::pair<TypeNode, size_t>, AlphaEquivalenceTypeNode> d_children;
39
 /**
40
  * map from canonized quantifier bodies to a quantified formula whose
41
  * canonized body is that term.
42
  */
43
 std::map<Node, Node> d_quant;
44
 /** register node
45
  *
46
  * This registers term q to this trie. The term t is the canonical form of
47
  * q, typs/typCount represent a multi-set of types of free variables in t.
48
  */
49
 Node registerNode(Node q,
50
                   Node t,
51
                   std::vector<TypeNode>& typs,
52
                   std::map<TypeNode, size_t>& typCount);
53
};
54
55
/**
56
 * Stores a database of quantified formulas, which computes alpha-equivalence.
57
 */
58
6051
class AlphaEquivalenceDb
59
{
60
 public:
61
6054
  AlphaEquivalenceDb(expr::TermCanonize* tc) : d_tc(tc) {}
62
  /** adds quantified formula q to this database
63
   *
64
   * This function returns a quantified formula q' that is alpha-equivalent to
65
   * q. If q' != q, then q' was previously added to this database via a call
66
   * to addTerm.
67
   */
68
  Node addTerm(Node q);
69
70
 private:
71
  /** a trie per # of variables per type */
72
  AlphaEquivalenceTypeNode d_ae_typ_trie;
73
  /** pointer to the term canonize utility */
74
  expr::TermCanonize* d_tc;
75
};
76
77
/**
78
 * A quantifiers module that computes reductions based on alpha-equivalence,
79
 * using the above utilities.
80
 */
81
class AlphaEquivalence
82
{
83
 public:
84
  AlphaEquivalence(QuantifiersEngine* qe);
85
6051
  ~AlphaEquivalence(){}
86
  /** reduce quantifier
87
   *
88
   * If non-null, its return value is lemma justifying why q is reducible.
89
   * This is of the form ( q = q' ) where q' is a quantified formula that
90
   * was previously registered to this class via a call to reduceQuantifier,
91
   * and q and q' are alpha-equivalent.
92
   */
93
  Node reduceQuantifier( Node q );
94
95
 private:
96
  /** a term canonizer */
97
  expr::TermCanonize d_termCanon;
98
  /** the database of quantified formulas registered to this class */
99
  AlphaEquivalenceDb d_aedb;
100
};
101
102
}
103
}
104
}
105
106
#endif