Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/candidate_generator.h	Lines:	16	16	100.0 %
Date:	2021-09-16	Branches:	6	12	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);
  /** Identify this generator (for debugging, etc..) */
  virtual std::string identify() const = 0;

 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();
  }
  /** Identify this generator (for debugging, etc..) */
  std::string identify() const override { return "CandidateGeneratorQE"; }

 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;
  /** Identify this generator (for debugging, etc..) */
  std::string identify() const override { return "CandidateGeneratorQELitDeq"; }

 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;
  /** Identify this generator (for debugging, etc..) */
  std::string identify() const override { return "CandidateGeneratorQEAll"; }

 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;
  /** Identify this generator (for debugging, etc..) */
  std::string identify() const override
  {
    return "CandidateGeneratorConsExpand";
  }

 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;
  /** Identify this generator (for debugging, etc..) */
  std::string identify() const override { return "CandidateGeneratorSelector"; }

 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		/** Identify this generator (for debugging, etc..) */
77		virtual std::string identify() const = 0;
78
79		protected:
80		/** Reference to the quantifiers state */
81		QuantifiersState& d_qs;
82		/** Reference to the term registry */
83		TermRegistry& d_treg;
84		};
85
86		/* the default candidate generator class
87		*
88		* This class may generate candidates for E-matching based on several modes:
89		* (1) cand_term_db: iterate over all ground terms for the given operator,
90		* (2) cand_term_ident: generate the given input term as a candidate,
91		* (3) cand_term_eqc: iterate over all terms in an equivalence class, returning
92		* those with the proper operator as candidates.
93		*/
94	66751	class CandidateGeneratorQE : public CandidateGenerator
95		{
96		friend class CandidateGeneratorQEDisequal;
97
98		public:
99		CandidateGeneratorQE(QuantifiersState& qs, TermRegistry& tr, Node pat);
100		/** reset */
101		void reset(Node eqc) override;
102		/** get next candidate */
103		Node getNextCandidate() override;
104		/** tell this class to exclude candidates from equivalence class r */
105	2076	void excludeEqc(Node r) { d_exclude_eqc[r] = true; }
106		/** is r an excluded equivalence class? */
107	344745	bool isExcludedEqc(Node r)
108		{
109	344745	return d_exclude_eqc.find(r) != d_exclude_eqc.end();
110		}
111		/** Identify this generator (for debugging, etc..) */
112	31738	std::string identify() const override { return "CandidateGeneratorQE"; }
113
114		protected:
115		/** reset this class for matching operator op in equivalence class eqc */
116		void resetForOperator(Node eqc, Node op);
117		/** the default implementation of getNextCandidate. */
118		Node getNextCandidateInternal();
119		/** operator you are looking for */
120		Node d_op;
121		/** the equality class iterator (for cand_term_eqc) */
122		eq::EqClassIterator d_eqc_iter;
123		/** the TermDb index of the current ground term (for cand_term_db) */
124		int d_term_iter;
125		/** the TermDb index of the current ground term (for cand_term_db) */
126		int d_term_iter_limit;
127		/** the current equivalence class */
128		Node d_eqc;
129		/** candidate generation modes */
130		enum {
131		cand_term_db,
132		cand_term_ident,
133		cand_term_eqc,
134		cand_term_none,
135		};
136		/** the current mode of this candidate generator */
137		short d_mode;
138		/** is n a legal candidate of the required operator? */
139		virtual bool isLegalOpCandidate(Node n);
140		/** the equivalence classes that we have excluded from candidate generation */
141		std::map< Node, bool > d_exclude_eqc;
142
143		};
144
145		/**
146		* Generate terms based on a disequality, that is, we match (= t[x] s[x])
147		* with equalities (= g1 g2) in the equivalence class of false.
148		*/
149	14	class CandidateGeneratorQELitDeq : public CandidateGenerator
150		{
151		public:
152		/**
153		* mpat is an equality that we are matching to equalities in the equivalence
154		* class of false
155		*/
156		CandidateGeneratorQELitDeq(QuantifiersState& qs, TermRegistry& tr, Node mpat);
157		/** reset */
158		void reset(Node eqc) override;
159		/** get next candidate */
160		Node getNextCandidate() override;
161		/** Identify this generator (for debugging, etc..) */
162	7	std::string identify() const override { return "CandidateGeneratorQELitDeq"; }
163
164		private:
165		/** the equality class iterator for false */
166		eq::EqClassIterator d_eqc_false;
167		/**
168		* equality you are trying to match against ground equalities that are
169		* assigned to false
170		*/
171		Node d_match_pattern;
172		/** type of the terms we are generating */
173		TypeNode d_match_pattern_type;
174		};
175
176		/**
177		* Generate all terms of the proper sort that occur in the current context.
178		*/
179	142	class CandidateGeneratorQEAll : public CandidateGenerator
180		{
181		private:
182		//the equality classes iterator
183		eq::EqClassesIterator d_eq;
184		//equality you are trying to match equalities for
185		Node d_match_pattern;
186		TypeNode d_match_pattern_type;
187		// quantifier/index for the variable we are matching
188		Node d_f;
189		unsigned d_index;
190		//first time
191		bool d_firstTime;
192		/** Identify this generator (for debugging, etc..) */
193	71	std::string identify() const override { return "CandidateGeneratorQEAll"; }
194
195		public:
196		CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat);
197		/** reset */
198		void reset(Node eqc) override;
199		/** get next candidate */
200		Node getNextCandidate() override;
201		};
202
203		/** candidate generation constructor expand
204		*
205		* This modifies the candidates t1, ..., tn generated by CandidateGeneratorQE
206		* so that they are "expansions" of a fixed datatype constructor C. Assuming
207		* C has arity m, we instead return the stream:
208		* C(sel_1( t1 ), ..., sel_m( tn )) ... C(sel_1( t1 ), ..., C( sel_m( tn ))
209		* where sel_1 ... sel_m are the selectors of C.
210		*/
211	6034	class CandidateGeneratorConsExpand : public CandidateGeneratorQE
212		{
213		public:
214		CandidateGeneratorConsExpand(QuantifiersState& qs,
215		TermRegistry& tr,
216		Node mpat);
217		/** reset */
218		void reset(Node eqc) override;
219		/** get next candidate */
220		Node getNextCandidate() override;
221		/** Identify this generator (for debugging, etc..) */
222	3017	std::string identify() const override
223		{
224	3017	return "CandidateGeneratorConsExpand";
225		}
226
227		protected:
228		/** the (datatype) type of the input match pattern */
229		TypeNode d_mpat_type;
230		/** we don't care about the operator of n */
231		bool isLegalOpCandidate(Node n) override;
232		};
233
234		/**
235		* Candidate generator for selector applications, which considers both
236		* internal terms corresponding to correctly and incorrectly applied selectors.
237		*/
238	516	class CandidateGeneratorSelector : public CandidateGeneratorQE
239		{
240		public:
241		CandidateGeneratorSelector(QuantifiersState& qs, TermRegistry& tr, Node mpat);
242		/** reset */
243		void reset(Node eqc) override;
244		/**
245		* Get next candidate, returns matching candidates that are ground terms
246		* of the selector operator, followed by those that are applications of the
247		* UF corresponding to an invocation of applying this selector to an
248		* application of the wrong constructor.
249		*/
250		Node getNextCandidate() override;
251		/** Identify this generator (for debugging, etc..) */
252	258	std::string identify() const override { return "CandidateGeneratorSelector"; }
253
254		protected:
255		/** the selector operator */
256		Node d_selOp;
257		/** the UF operator */
258		Node d_ufOp;
259		};
260
261		} // namespace inst
262		} // namespace quantifiers
263		} // namespace theory
264		} // namespace cvc5
265
266		#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */