Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/alpha_equivalence.h	Lines:	4	4	100.0 %
Date:	2021-09-07	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Paul Meng
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Alpha equivalence checking.
 */

#include "cvc5_private.h"

#ifndef CVC5__ALPHA_EQUIVALENCE_H
#define CVC5__ALPHA_EQUIVALENCE_H

#include "theory/quantifiers/quant_util.h"

#include "expr/term_canonize.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

/**
 * This trie stores a trie of the above form for each multi-set of types. For
 * each term t registered to this node, we store t in the appropriate
 * AlphaEquivalenceNode trie. For example, if t contains 2 free variables
 * of type T1 and 3 free variables of type T2, then it is stored at
 * d_children[T1][2].d_children[T2][3].
 */
class AlphaEquivalenceTypeNode {
public:
 /** children of this node */
 std::map<std::pair<TypeNode, size_t>, AlphaEquivalenceTypeNode> d_children;
 /**
  * map from canonized quantifier bodies to a quantified formula whose
  * canonized body is that term.
  */
 std::map<Node, Node> d_quant;
 /** register node
  *
  * This registers term q to this trie. The term t is the canonical form of
  * q, typs/typCount represent a multi-set of types of free variables in t.
  */
 Node registerNode(Node q,
                   Node t,
                   std::vector<TypeNode>& typs,
                   std::map<TypeNode, size_t>& typCount);
};

/**
 * Stores a database of quantified formulas, which computes alpha-equivalence.
 */
class AlphaEquivalenceDb
{
 public:
  AlphaEquivalenceDb(expr::TermCanonize* tc) : d_tc(tc) {}
  /** adds quantified formula q to this database
   *
   * This function returns a quantified formula q' that is alpha-equivalent to
   * q. If q' != q, then q' was previously added to this database via a call
   * to addTerm.
   */
  Node addTerm(Node q);

 private:
  /** a trie per # of variables per type */
  AlphaEquivalenceTypeNode d_ae_typ_trie;
  /** pointer to the term canonize utility */
  expr::TermCanonize* d_tc;
};

/**
 * A quantifiers module that computes reductions based on alpha-equivalence,
 * using the above utilities.
 */
class AlphaEquivalence
{
 public:
  AlphaEquivalence();
  ~AlphaEquivalence(){}
  /** reduce quantifier
   *
   * If non-null, its return value is lemma justifying why q is reducible.
   * This is of the form ( q = q' ) where q' is a quantified formula that
   * was previously registered to this class via a call to reduceQuantifier,
   * and q and q' are alpha-equivalent.
   */
  Node reduceQuantifier( Node q );

 private:
  /** a term canonizer */
  expr::TermCanonize d_termCanon;
  /** the database of quantified formulas registered to this class */
  AlphaEquivalenceDb d_aedb;
};

}
}
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

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