Head

GCC Code Coverage Report

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


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tim King, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * Theory uf candidate generator.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H

#include "theory/theory.h"
#include "theory/uf/equality_engine.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class QuantifiersState;
class TermRegistry;

namespace inst {

/** Candidate generator
 *
 * This is the base class for generating a stream of candidate terms for
 * E-matching. Depending on the kind of trigger we are processing and its
 * overall context, we are interested in several different criteria for
 * terms. This includes:
 * - Generating a stream of all ground terms with a given operator,
 * - Generating a stream of all ground terms with a given operator in a
 * particular equivalence class,
 * - Generating a stream of all terms of a particular type,
 * - Generating all terms that are disequal from a fixed ground term,
 * and so on.
 *
 * A typical use case of an instance cg of this class is the following. Given
 * an equivalence class representative eqc:
 *
 *  cg->reset( eqc );
 *  do{
 *    Node cand = cg->getNextCandidate();
 *    ; ...if non-null, cand is a candidate...
 *  }while( !cand.isNull() );
 *
 */
class CandidateGenerator {
 public:
  CandidateGenerator(QuantifiersState& qs, TermRegistry& tr);
  virtual ~CandidateGenerator(){}
  /** reset instantiation round
   *
   * This is called at the beginning of each instantiation round.
   */
  virtual void resetInstantiationRound() {}
  /** reset for equivalence class eqc
   *
   * This indicates that this class should generate a stream of candidate terms
   * based on its criteria that occur in the equivalence class of eqc, or
   * any equivalence class if eqc is null.
   */
  virtual void reset( Node eqc ) = 0;
  /** get the next candidate */
  virtual Node getNextCandidate() = 0;
  /** is n a legal candidate? */
  bool isLegalCandidate(Node n);

 protected:
  /** Reference to the quantifiers state */
  QuantifiersState& d_qs;
  /** Reference to the term registry */
  TermRegistry& d_treg;
};

/* the default candidate generator class
 *
 * This class may generate candidates for E-matching based on several modes:
 * (1) cand_term_db: iterate over all ground terms for the given operator,
 * (2) cand_term_ident: generate the given input term as a candidate,
 * (3) cand_term_eqc: iterate over all terms in an equivalence class, returning
 * those with the proper operator as candidates.
 */
class CandidateGeneratorQE : public CandidateGenerator
{
  friend class CandidateGeneratorQEDisequal;

 public:
  CandidateGeneratorQE(QuantifiersState& qs, TermRegistry& tr, Node pat);
  /** reset */
  void reset(Node eqc) override;
  /** get next candidate */
  Node getNextCandidate() override;
  /** tell this class to exclude candidates from equivalence class r */
  void excludeEqc(Node r) { d_exclude_eqc[r] = true; }
  /** is r an excluded equivalence class? */
  bool isExcludedEqc(Node r)
  {
    return d_exclude_eqc.find(r) != d_exclude_eqc.end();
  }
 protected:
  /** reset this class for matching operator op in equivalence class eqc */
  void resetForOperator(Node eqc, Node op);
  /** the default implementation of getNextCandidate. */
  Node getNextCandidateInternal();
  /** operator you are looking for */
  Node d_op;
  /** the equality class iterator (for cand_term_eqc) */
  eq::EqClassIterator d_eqc_iter;
  /** the TermDb index of the current ground term (for cand_term_db) */
  int d_term_iter;
  /** the TermDb index of the current ground term (for cand_term_db) */
  int d_term_iter_limit;
  /** the current equivalence class */
  Node d_eqc;
  /** candidate generation modes */
  enum {
    cand_term_db,
    cand_term_ident,
    cand_term_eqc,
    cand_term_none,
  };
  /** the current mode of this candidate generator */
  short d_mode;
  /** is n a legal candidate of the required operator? */
  virtual bool isLegalOpCandidate(Node n);
  /** the equivalence classes that we have excluded from candidate generation */
  std::map< Node, bool > d_exclude_eqc;

};

/**
 * Generate terms based on a disequality, that is, we match (= t[x] s[x])
 * with equalities (= g1 g2) in the equivalence class of false.
 */
class CandidateGeneratorQELitDeq : public CandidateGenerator
{
 public:
  /**
   * mpat is an equality that we are matching to equalities in the equivalence
   * class of false
   */
  CandidateGeneratorQELitDeq(QuantifiersState& qs, TermRegistry& tr, Node mpat);
  /** reset */
  void reset(Node eqc) override;
  /** get next candidate */
  Node getNextCandidate() override;

 private:
  /** the equality class iterator for false */
  eq::EqClassIterator d_eqc_false;
  /**
   * equality you are trying to match against ground equalities that are
   * assigned to false
   */
  Node d_match_pattern;
  /** type of the terms we are generating */
  TypeNode d_match_pattern_type;
};

/**
 * Generate all terms of the proper sort that occur in the current context.
 */
class CandidateGeneratorQEAll : public CandidateGenerator
{
 private:
  //the equality classes iterator
  eq::EqClassesIterator d_eq;
  //equality you are trying to match equalities for
  Node d_match_pattern;
  TypeNode d_match_pattern_type;
  // quantifier/index for the variable we are matching
  Node d_f;
  unsigned d_index;
  //first time
  bool d_firstTime;

 public:
  CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat);
  /** reset */
  void reset(Node eqc) override;
  /** get next candidate */
  Node getNextCandidate() override;
};

/** candidate generation constructor expand
 *
 * This modifies the candidates t1, ..., tn generated by CandidateGeneratorQE
 * so that they are "expansions" of a fixed datatype constructor C. Assuming
 * C has arity m, we instead return the stream:
 *   C(sel_1( t1 ), ..., sel_m( tn )) ... C(sel_1( t1 ), ..., C( sel_m( tn ))
 * where sel_1 ... sel_m are the selectors of C.
 */
class CandidateGeneratorConsExpand : public CandidateGeneratorQE
{
 public:
  CandidateGeneratorConsExpand(QuantifiersState& qs,
                               TermRegistry& tr,
                               Node mpat);
  /** reset */
  void reset(Node eqc) override;
  /** get next candidate */
  Node getNextCandidate() override;

 protected:
  /** the (datatype) type of the input match pattern */
  TypeNode d_mpat_type;
  /** we don't care about the operator of n */
  bool isLegalOpCandidate(Node n) override;
};

/**
 * Candidate generator for selector applications, which considers both
 * internal terms corresponding to correctly and incorrectly applied selectors.
 */
class CandidateGeneratorSelector : public CandidateGeneratorQE
{
 public:
  CandidateGeneratorSelector(QuantifiersState& qs, TermRegistry& tr, Node mpat);
  /** reset */
  void reset(Node eqc) override;
  /**
   * Get next candidate, returns matching candidates that are ground terms
   * of the selector operator, followed by those that are applications of the
   * UF corresponding to an invocation of applying this selector to an
   * application of the wrong constructor.
   */
  Node getNextCandidate() override;
 protected:
  /** the selector operator */
  Node d_selOp;
  /** the UF operator */
  Node d_ufOp;
};

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

#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Tim King, Morgan Deters
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		* Theory uf candidate generator.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
19		#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
20
21		#include "theory/theory.h"
22		#include "theory/uf/equality_engine.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28		class QuantifiersState;
29		class TermRegistry;
30
31		namespace inst {
32
33		/** Candidate generator
34		*
35		* This is the base class for generating a stream of candidate terms for
36		* E-matching. Depending on the kind of trigger we are processing and its
37		* overall context, we are interested in several different criteria for
38		* terms. This includes:
39		* - Generating a stream of all ground terms with a given operator,
40		* - Generating a stream of all ground terms with a given operator in a
41		* particular equivalence class,
42		* - Generating a stream of all terms of a particular type,
43		* - Generating all terms that are disequal from a fixed ground term,
44		* and so on.
45		*
46		* A typical use case of an instance cg of this class is the following. Given
47		* an equivalence class representative eqc:
48		*
49		* cg->reset( eqc );
50		* do{
51		* Node cand = cg->getNextCandidate();
52		* ; ...if non-null, cand is a candidate...
53		* }while( !cand.isNull() );
54		*
55		*/
56		class CandidateGenerator {
57		public:
58		CandidateGenerator(QuantifiersState& qs, TermRegistry& tr);
59	35091	virtual ~CandidateGenerator(){}
60		/** reset instantiation round
61		*
62		* This is called at the beginning of each instantiation round.
63		*/
64	248053	virtual void resetInstantiationRound() {}
65		/** reset for equivalence class eqc
66		*
67		* This indicates that this class should generate a stream of candidate terms
68		* based on its criteria that occur in the equivalence class of eqc, or
69		* any equivalence class if eqc is null.
70		*/
71		virtual void reset( Node eqc ) = 0;
72		/** get the next candidate */
73		virtual Node getNextCandidate() = 0;
74		/** is n a legal candidate? */
75		bool isLegalCandidate(Node n);
76
77		protected:
78		/** Reference to the quantifiers state */
79		QuantifiersState& d_qs;
80		/** Reference to the term registry */
81		TermRegistry& d_treg;
82		};
83
84		/* the default candidate generator class
85		*
86		* This class may generate candidates for E-matching based on several modes:
87		* (1) cand_term_db: iterate over all ground terms for the given operator,
88		* (2) cand_term_ident: generate the given input term as a candidate,
89		* (3) cand_term_eqc: iterate over all terms in an equivalence class, returning
90		* those with the proper operator as candidates.
91		*/
92	66751	class CandidateGeneratorQE : public CandidateGenerator
93		{
94		friend class CandidateGeneratorQEDisequal;
95
96		public:
97		CandidateGeneratorQE(QuantifiersState& qs, TermRegistry& tr, Node pat);
98		/** reset */
99		void reset(Node eqc) override;
100		/** get next candidate */
101		Node getNextCandidate() override;
102		/** tell this class to exclude candidates from equivalence class r */
103	2076	void excludeEqc(Node r) { d_exclude_eqc[r] = true; }
104		/** is r an excluded equivalence class? */
105	344744	bool isExcludedEqc(Node r)
106		{
107	344744	return d_exclude_eqc.find(r) != d_exclude_eqc.end();
108		}
109		protected:
110		/** reset this class for matching operator op in equivalence class eqc */
111		void resetForOperator(Node eqc, Node op);
112		/** the default implementation of getNextCandidate. */
113		Node getNextCandidateInternal();
114		/** operator you are looking for */
115		Node d_op;
116		/** the equality class iterator (for cand_term_eqc) */
117		eq::EqClassIterator d_eqc_iter;
118		/** the TermDb index of the current ground term (for cand_term_db) */
119		int d_term_iter;
120		/** the TermDb index of the current ground term (for cand_term_db) */
121		int d_term_iter_limit;
122		/** the current equivalence class */
123		Node d_eqc;
124		/** candidate generation modes */
125		enum {
126		cand_term_db,
127		cand_term_ident,
128		cand_term_eqc,
129		cand_term_none,
130		};
131		/** the current mode of this candidate generator */
132		short d_mode;
133		/** is n a legal candidate of the required operator? */
134		virtual bool isLegalOpCandidate(Node n);
135		/** the equivalence classes that we have excluded from candidate generation */
136		std::map< Node, bool > d_exclude_eqc;
137
138		};
139
140		/**
141		* Generate terms based on a disequality, that is, we match (= t[x] s[x])
142		* with equalities (= g1 g2) in the equivalence class of false.
143		*/
144	14	class CandidateGeneratorQELitDeq : public CandidateGenerator
145		{
146		public:
147		/**
148		* mpat is an equality that we are matching to equalities in the equivalence
149		* class of false
150		*/
151		CandidateGeneratorQELitDeq(QuantifiersState& qs, TermRegistry& tr, Node mpat);
152		/** reset */
153		void reset(Node eqc) override;
154		/** get next candidate */
155		Node getNextCandidate() override;
156
157		private:
158		/** the equality class iterator for false */
159		eq::EqClassIterator d_eqc_false;
160		/**
161		* equality you are trying to match against ground equalities that are
162		* assigned to false
163		*/
164		Node d_match_pattern;
165		/** type of the terms we are generating */
166		TypeNode d_match_pattern_type;
167		};
168
169		/**
170		* Generate all terms of the proper sort that occur in the current context.
171		*/
172	142	class CandidateGeneratorQEAll : public CandidateGenerator
173		{
174		private:
175		//the equality classes iterator
176		eq::EqClassesIterator d_eq;
177		//equality you are trying to match equalities for
178		Node d_match_pattern;
179		TypeNode d_match_pattern_type;
180		// quantifier/index for the variable we are matching
181		Node d_f;
182		unsigned d_index;
183		//first time
184		bool d_firstTime;
185
186		public:
187		CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat);
188		/** reset */
189		void reset(Node eqc) override;
190		/** get next candidate */
191		Node getNextCandidate() override;
192		};
193
194		/** candidate generation constructor expand
195		*
196		* This modifies the candidates t1, ..., tn generated by CandidateGeneratorQE
197		* so that they are "expansions" of a fixed datatype constructor C. Assuming
198		* C has arity m, we instead return the stream:
199		* C(sel_1( t1 ), ..., sel_m( tn )) ... C(sel_1( t1 ), ..., C( sel_m( tn ))
200		* where sel_1 ... sel_m are the selectors of C.
201		*/
202	6034	class CandidateGeneratorConsExpand : public CandidateGeneratorQE
203		{
204		public:
205		CandidateGeneratorConsExpand(QuantifiersState& qs,
206		TermRegistry& tr,
207		Node mpat);
208		/** reset */
209		void reset(Node eqc) override;
210		/** get next candidate */
211		Node getNextCandidate() override;
212
213		protected:
214		/** the (datatype) type of the input match pattern */
215		TypeNode d_mpat_type;
216		/** we don't care about the operator of n */
217		bool isLegalOpCandidate(Node n) override;
218		};
219
220		/**
221		* Candidate generator for selector applications, which considers both
222		* internal terms corresponding to correctly and incorrectly applied selectors.
223		*/
224	516	class CandidateGeneratorSelector : public CandidateGeneratorQE
225		{
226		public:
227		CandidateGeneratorSelector(QuantifiersState& qs, TermRegistry& tr, Node mpat);
228		/** reset */
229		void reset(Node eqc) override;
230		/**
231		* Get next candidate, returns matching candidates that are ground terms
232		* of the selector operator, followed by those that are applications of the
233		* UF corresponding to an invocation of applying this selector to an
234		* application of the wrong constructor.
235		*/
236		Node getNextCandidate() override;
237		protected:
238		/** the selector operator */
239		Node d_selOp;
240		/** the UF operator */
241		Node d_ufOp;
242		};
243
244		} // namespace inst
245		} // namespace quantifiers
246		} // namespace theory
247		} // namespace cvc5
248
249		#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */