Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/alpha_equivalence.h	Lines:	6	6	100.0 %
Date:	2021-11-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 "expr/term_canonize.h"
#include "proof/eager_proof_generator.h"
#include "smt/env_obj.h"
#include "theory/quantifiers/quant_util.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

/**
 * This trie stores a trie for each multi-set of types. For each term t
 * registered to this node, we store t in the appropriate
 * AlphaEquivalenceTypeNode 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, bool sortCommChildren)
      : d_tc(tc), d_sortCommutativeOpChildren(sortCommChildren)
  {
  }
  /** 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);
  /**
   * Add term with substitution, which additionally finds a set of terms such
   * that q' * subs is alpha-equivalent (possibly modulo rewriting) to q, where
   * q' is the return quantified formula.
   */
  Node addTermWithSubstitution(Node q,
                               std::vector<Node>& vars,
                               std::vector<Node>& subs);

 private:
  /**
   * Add term to the trie, where t is the canonized form of the body of
   * quantified formula q. Returns the quantified formula, if any, that already
   * had been added to this class, or q otherwise.
   */
  Node addTermToTypeTrie(Node t, Node q);
  /** a trie per # of variables per type */
  AlphaEquivalenceTypeNode d_ae_typ_trie;
  /** pointer to the term canonize utility */
  expr::TermCanonize* d_tc;
  /** whether to sort children of commutative operators during canonization. */
  bool d_sortCommutativeOpChildren;
  /**
   * Maps quantified formulas to variables map, used for tracking substitutions
   * in addTermWithSubstitution. The range in d_bvmap[q] contains the mapping
   * from canonical free variables to variables in q.
   */
  std::map<Node, std::map<Node, TNode> > d_bvmap;
};

/**
 * A quantifiers module that computes reductions based on alpha-equivalence,
 * using the above utilities.
 */
class AlphaEquivalence : protected EnvObj
{
 public:
  AlphaEquivalence(Env& env);
  ~AlphaEquivalence(){}
  /** reduce quantifier
   *
   * If non-null, its return value is a trust node containing the lemma
   * justifying why q is reducible.  This lemma 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.
   */
  TrustNode reduceQuantifier(Node q);

 private:
  /** a term canonizer */
  expr::TermCanonize d_termCanon;
  /** the database of quantified formulas registered to this class */
  AlphaEquivalenceDb d_aedb;
  /** Pointer to the proof node manager */
  ProofNodeManager* d_pnm;
  /** An eager proof generator storing alpha equivalence proofs.*/
  std::unique_ptr<EagerProofGenerator> d_pfAlpha;
  /** Are proofs enabled for this object? */
  bool isProofEnabled() const;
};

}
}
}  // 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 "expr/term_canonize.h"
22		#include "proof/eager_proof_generator.h"
23		#include "smt/env_obj.h"
24		#include "theory/quantifiers/quant_util.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace quantifiers {
29
30		/**
31		* This trie stores a trie for each multi-set of types. For each term t
32		* registered to this node, we store t in the appropriate
33		* AlphaEquivalenceTypeNode trie. For example, if t contains 2 free variables of
34		* type T1 and 3 free variables of type T2, then it is stored at
35		* d_children[T1][2].d_children[T2][3].
36		*/
37	46009	class AlphaEquivalenceTypeNode {
38		public:
39		/** children of this node */
40		std::map<std::pair<TypeNode, size_t>, AlphaEquivalenceTypeNode> d_children;
41		/**
42		* map from canonized quantifier bodies to a quantified formula whose
43		* canonized body is that term.
44		*/
45		std::map<Node, Node> d_quant;
46		/** register node
47		*
48		* This registers term q to this trie. The term t is the canonical form of
49		* q, typs/typCount represent a multi-set of types of free variables in t.
50		*/
51		Node registerNode(Node q,
52		Node t,
53		std::vector<TypeNode>& typs,
54		std::map<TypeNode, size_t>& typCount);
55		};
56
57		/**
58		* Stores a database of quantified formulas, which computes alpha-equivalence.
59		*/
60	12145	class AlphaEquivalenceDb
61		{
62		public:
63	12150	AlphaEquivalenceDb(expr::TermCanonize* tc, bool sortCommChildren)
64	12150	: d_tc(tc), d_sortCommutativeOpChildren(sortCommChildren)
65		{
66	12150	}
67		/** adds quantified formula q to this database
68		*
69		* This function returns a quantified formula q' that is alpha-equivalent to
70		* q. If q' != q, then q' was previously added to this database via a call
71		* to addTerm.
72		*/
73		Node addTerm(Node q);
74		/**
75		* Add term with substitution, which additionally finds a set of terms such
76		* that q' * subs is alpha-equivalent (possibly modulo rewriting) to q, where
77		* q' is the return quantified formula.
78		*/
79		Node addTermWithSubstitution(Node q,
80		std::vector<Node>& vars,
81		std::vector<Node>& subs);
82
83		private:
84		/**
85		* Add term to the trie, where t is the canonized form of the body of
86		* quantified formula q. Returns the quantified formula, if any, that already
87		* had been added to this class, or q otherwise.
88		*/
89		Node addTermToTypeTrie(Node t, Node q);
90		/** a trie per # of variables per type */
91		AlphaEquivalenceTypeNode d_ae_typ_trie;
92		/** pointer to the term canonize utility */
93		expr::TermCanonize* d_tc;
94		/** whether to sort children of commutative operators during canonization. */
95		bool d_sortCommutativeOpChildren;
96		/**
97		* Maps quantified formulas to variables map, used for tracking substitutions
98		* in addTermWithSubstitution. The range in d_bvmap[q] contains the mapping
99		* from canonical free variables to variables in q.
100		*/
101		std::map<Node, std::map<Node, TNode> > d_bvmap;
102		};
103
104		/**
105		* A quantifiers module that computes reductions based on alpha-equivalence,
106		* using the above utilities.
107		*/
108		class AlphaEquivalence : protected EnvObj
109		{
110		public:
111		AlphaEquivalence(Env& env);
112	24290	~AlphaEquivalence(){}
113		/** reduce quantifier
114		*
115		* If non-null, its return value is a trust node containing the lemma
116		* justifying why q is reducible. This lemma is of the form ( q = q' ) where
117		* q' is a quantified formula that was previously registered to this class via
118		* a call to reduceQuantifier, and q and q' are alpha-equivalent.
119		*/
120		TrustNode reduceQuantifier(Node q);
121
122		private:
123		/** a term canonizer */
124		expr::TermCanonize d_termCanon;
125		/** the database of quantified formulas registered to this class */
126		AlphaEquivalenceDb d_aedb;
127		/** Pointer to the proof node manager */
128		ProofNodeManager* d_pnm;
129		/** An eager proof generator storing alpha equivalence proofs.*/
130		std::unique_ptr<EagerProofGenerator> d_pfAlpha;
131		/** Are proofs enabled for this object? */
132		bool isProofEnabled() const;
133		};
134
135		}
136		}
137		} // namespace cvc5
138
139		#endif