Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/inst_match_trie.h	Lines:	10	10	100.0 %
Date:	2021-09-09	Branches:	1	2	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Inst match trie class.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H

#include <map>

#include "context/cdlist.h"
#include "context/cdo.h"
#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class QuantifiersState;

/** trie for InstMatch objects
 *
 * This class is used for storing instantiations of a quantified formula q.
 * It is a trie data structure for which entries can be added and removed.
 * This class has interfaces for adding instantiations that are either
 * represented by std::vectors or InstMatch objects (see inst_match.h).
 */
class InstMatchTrie
{
 public:
  /** index ordering */
  class ImtIndexOrder
  {
   public:
    std::vector<unsigned> d_order;
  };

 public:
  InstMatchTrie() {}
  ~InstMatchTrie() {}
  /** exists inst match
   *
   * This method considers the entry given by m, starting at the given index.
   * The domain of m is the bound variables of quantified formula q.
   * It returns true if (the suffix) of m exists in this trie.
   * If modEq is true, we check for duplication modulo equality the current
   * equalities in the equality engine of qs.
   */
  bool existsInstMatch(QuantifiersState& qs,
                       Node q,
                       const std::vector<Node>& m,
                       bool modEq = false,
                       ImtIndexOrder* imtio = nullptr,
                       unsigned index = 0);
  /** add inst match
   *
   * This method adds (the suffix of) m starting at the given index to this
   * trie, and returns true if and only if m did not already occur in this trie.
   * The domain of m is the bound variables of quantified formula q.
   * If modEq is true, we check for duplication modulo equality the current
   * equalities in the equality engine of qs.
   */
  bool addInstMatch(QuantifiersState& qs,
                    Node f,
                    const std::vector<Node>& m,
                    bool modEq = false,
                    ImtIndexOrder* imtio = nullptr,
                    bool onlyExist = false,
                    unsigned index = 0);
  /** remove inst match
   *
   * This removes (the suffix of) m starting at the given index from this trie.
   * It returns true if and only if this entry existed in this trie.
   * The domain of m is the bound variables of quantified formula q.
   */
  bool removeInstMatch(Node f,
                       const std::vector<Node>& m,
                       ImtIndexOrder* imtio = nullptr,
                       unsigned index = 0);
  /**
   * Adds the instantiations for q into insts.
   */
  void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;

  /** clear the data of this class */
  void clear();
  /** print this class */
  void print(std::ostream& out, Node q) const;
  /** the data */
  std::map<Node, InstMatchTrie> d_data;

 private:
  /** Helper for getInstantiations.*/
  void getInstantiations(Node q,
                         std::vector<std::vector<Node>>& insts,
                         std::vector<Node>& terms) const;
  /** helper for print
   * terms accumulates the path we are on in the trie.
   */
  void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
};

/** trie for InstMatch objects
 *
 * This is a context-dependent version of the above class.
 */
class CDInstMatchTrie
{
 public:
  CDInstMatchTrie(context::Context* c) : d_valid(c, false) {}
  ~CDInstMatchTrie();

  /** exists inst match
   *
   * This method considers the entry given by m, starting at the given index.
   * The domain of m is the bound variables of quantified formula q.
   * It returns true if (the suffix) of m exists in this trie.
   * If modEq is true, we check for duplication modulo equality the current
   * equalities in the equality engine of qs.
   * It additionally takes a context c, for which the entry is valid in.
   */
  bool existsInstMatch(QuantifiersState& qs,
                       Node q,
                       const std::vector<Node>& m,
                       bool modEq = false,
                       unsigned index = 0);
  /** add inst match
   *
   * This method adds (the suffix of) m starting at the given index to this
   * trie, and returns true if and only if m did not already occur in this trie.
   * The domain of m is the bound variables of quantified formula q.
   * If modEq is true, we check for duplication modulo equality the current
   * equalities in the equality engine of qs.
   * It additionally takes a context c, for which the entry is valid in.
   */
  bool addInstMatch(QuantifiersState& qs,
                    Node q,
                    const std::vector<Node>& m,
                    bool modEq = false,
                    unsigned index = 0,
                    bool onlyExist = false);
  /** remove inst match
   *
   * This removes (the suffix of) m starting at the given index from this trie.
   * It returns true if and only if this entry existed in this trie.
   * The domain of m is the bound variables of quantified formula q.
   */
  bool removeInstMatch(Node q, const std::vector<Node>& m, unsigned index = 0);
  /**
   * Adds the instantiations for q into insts.
   */
  void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;

  /** print this class */
  void print(std::ostream& out, Node q) const;

 private:
  /** Helper for getInstantiations.*/
  void getInstantiations(Node q,
                         std::vector<std::vector<Node>>& insts,
                         std::vector<Node>& terms) const;
  /** helper for print
   * terms accumulates the path we are on in the trie.
   */
  void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
  /** the data */
  std::map<Node, CDInstMatchTrie*> d_data;
  /** is valid */
  context::CDO<bool> d_valid;
};

/** inst match trie ordered
 *
 * This is an ordered version of the context-independent instantiation match
 * trie. It stores a variable order and a base InstMatchTrie.
 */
class InstMatchTrieOrdered
{
 public:
  InstMatchTrieOrdered(InstMatchTrie::ImtIndexOrder* imtio) : d_imtio(imtio) {}
  ~InstMatchTrieOrdered() {}
  /** get the ordering */
  InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
  /** get the trie data */
  InstMatchTrie* getTrie() { return &d_imt; }
  /** add match m for quantified formula q
   *
   * This method returns true if the match m was not previously added to this
   * class. If modEq is true, we consider duplicates modulo the current
   * equalities stored in the equality engine of qs.
   */
  bool addInstMatch(QuantifiersState& qs,
                    Node q,
                    const std::vector<Node>& m,
                    bool modEq = false);
  /** returns true if this trie contains m
   *
   * This method returns true if the match m exists in this
   * class. If modEq is true, we consider duplicates modulo the current
   * equalities stored in the equality engine of qs.
   */
  bool existsInstMatch(QuantifiersState& qs,
                       Node q,
                       const std::vector<Node>& m,
                       bool modEq = false);

 private:
  /** the ordering */
  InstMatchTrie::ImtIndexOrder* d_imtio;
  /** the data of this class */
  InstMatchTrie d_imt;
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Mathias Preiner
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		* Inst match trie class.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
19		#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
20
21		#include <map>
22
23		#include "context/cdlist.h"
24		#include "context/cdo.h"
25		#include "expr/node.h"
26
27		namespace cvc5 {
28		namespace theory {
29		namespace quantifiers {
30
31		class QuantifiersState;
32
33		/** trie for InstMatch objects
34		*
35		* This class is used for storing instantiations of a quantified formula q.
36		* It is a trie data structure for which entries can be added and removed.
37		* This class has interfaces for adding instantiations that are either
38		* represented by std::vectors or InstMatch objects (see inst_match.h).
39		*/
40	39	class InstMatchTrie
41		{
42		public:
43		/** index ordering */
44	46	class ImtIndexOrder
45		{
46		public:
47		std::vector<unsigned> d_order;
48		};
49
50		public:
51	79351	InstMatchTrie() {}
52	79390	~InstMatchTrie() {}
53		/** exists inst match
54		*
55		* This method considers the entry given by m, starting at the given index.
56		* The domain of m is the bound variables of quantified formula q.
57		* It returns true if (the suffix) of m exists in this trie.
58		* If modEq is true, we check for duplication modulo equality the current
59		* equalities in the equality engine of qs.
60		*/
61		bool existsInstMatch(QuantifiersState& qs,
62		Node q,
63		const std::vector<Node>& m,
64		bool modEq = false,
65		ImtIndexOrder* imtio = nullptr,
66		unsigned index = 0);
67		/** add inst match
68		*
69		* This method adds (the suffix of) m starting at the given index to this
70		* trie, and returns true if and only if m did not already occur in this trie.
71		* The domain of m is the bound variables of quantified formula q.
72		* If modEq is true, we check for duplication modulo equality the current
73		* equalities in the equality engine of qs.
74		*/
75		bool addInstMatch(QuantifiersState& qs,
76		Node f,
77		const std::vector<Node>& m,
78		bool modEq = false,
79		ImtIndexOrder* imtio = nullptr,
80		bool onlyExist = false,
81		unsigned index = 0);
82		/** remove inst match
83		*
84		* This removes (the suffix of) m starting at the given index from this trie.
85		* It returns true if and only if this entry existed in this trie.
86		* The domain of m is the bound variables of quantified formula q.
87		*/
88		bool removeInstMatch(Node f,
89		const std::vector<Node>& m,
90		ImtIndexOrder* imtio = nullptr,
91		unsigned index = 0);
92		/**
93		* Adds the instantiations for q into insts.
94		*/
95		void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
96
97		/** clear the data of this class */
98		void clear();
99		/** print this class */
100		void print(std::ostream& out, Node q) const;
101		/** the data */
102		std::map<Node, InstMatchTrie> d_data;
103
104		private:
105		/** Helper for getInstantiations.*/
106		void getInstantiations(Node q,
107		std::vector<std::vector<Node>>& insts,
108		std::vector<Node>& terms) const;
109		/** helper for print
110		* terms accumulates the path we are on in the trie.
111		*/
112		void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
113		};
114
115		/** trie for InstMatch objects
116		*
117		* This is a context-dependent version of the above class.
118		*/
119		class CDInstMatchTrie
120		{
121		public:
122	7130	CDInstMatchTrie(context::Context* c) : d_valid(c, false) {}
123		~CDInstMatchTrie();
124
125		/** exists inst match
126		*
127		* This method considers the entry given by m, starting at the given index.
128		* The domain of m is the bound variables of quantified formula q.
129		* It returns true if (the suffix) of m exists in this trie.
130		* If modEq is true, we check for duplication modulo equality the current
131		* equalities in the equality engine of qs.
132		* It additionally takes a context c, for which the entry is valid in.
133		*/
134		bool existsInstMatch(QuantifiersState& qs,
135		Node q,
136		const std::vector<Node>& m,
137		bool modEq = false,
138		unsigned index = 0);
139		/** add inst match
140		*
141		* This method adds (the suffix of) m starting at the given index to this
142		* trie, and returns true if and only if m did not already occur in this trie.
143		* The domain of m is the bound variables of quantified formula q.
144		* If modEq is true, we check for duplication modulo equality the current
145		* equalities in the equality engine of qs.
146		* It additionally takes a context c, for which the entry is valid in.
147		*/
148		bool addInstMatch(QuantifiersState& qs,
149		Node q,
150		const std::vector<Node>& m,
151		bool modEq = false,
152		unsigned index = 0,
153		bool onlyExist = false);
154		/** remove inst match
155		*
156		* This removes (the suffix of) m starting at the given index from this trie.
157		* It returns true if and only if this entry existed in this trie.
158		* The domain of m is the bound variables of quantified formula q.
159		*/
160		bool removeInstMatch(Node q, const std::vector<Node>& m, unsigned index = 0);
161		/**
162		* Adds the instantiations for q into insts.
163		*/
164		void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
165
166		/** print this class */
167		void print(std::ostream& out, Node q) const;
168
169		private:
170		/** Helper for getInstantiations.*/
171		void getInstantiations(Node q,
172		std::vector<std::vector<Node>>& insts,
173		std::vector<Node>& terms) const;
174		/** helper for print
175		* terms accumulates the path we are on in the trie.
176		*/
177		void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
178		/** the data */
179		std::map<Node, CDInstMatchTrie*> d_data;
180		/** is valid */
181		context::CDO<bool> d_valid;
182		};
183
184		/** inst match trie ordered
185		*
186		* This is an ordered version of the context-independent instantiation match
187		* trie. It stores a variable order and a base InstMatchTrie.
188		*/
189	39	class InstMatchTrieOrdered
190		{
191		public:
192	23	InstMatchTrieOrdered(InstMatchTrie::ImtIndexOrder* imtio) : d_imtio(imtio) {}
193	62	~InstMatchTrieOrdered() {}
194		/** get the ordering */
195	2283	InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
196		/** get the trie data */
197	1426	InstMatchTrie* getTrie() { return &d_imt; }
198		/** add match m for quantified formula q
199		*
200		* This method returns true if the match m was not previously added to this
201		* class. If modEq is true, we consider duplicates modulo the current
202		* equalities stored in the equality engine of qs.
203		*/
204		bool addInstMatch(QuantifiersState& qs,
205		Node q,
206		const std::vector<Node>& m,
207		bool modEq = false);
208		/** returns true if this trie contains m
209		*
210		* This method returns true if the match m exists in this
211		* class. If modEq is true, we consider duplicates modulo the current
212		* equalities stored in the equality engine of qs.
213		*/
214		bool existsInstMatch(QuantifiersState& qs,
215		Node q,
216		const std::vector<Node>& m,
217		bool modEq = false);
218
219		private:
220		/** the ordering */
221		InstMatchTrie::ImtIndexOrder* d_imtio;
222		/** the data of this class */
223		InstMatchTrie d_imt;
224		};
225
226		} // namespace quantifiers
227		} // namespace theory
228		} // namespace cvc5
229
230		#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */