Head

GCC Code Coverage Report

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


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tim King, 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.
 * ****************************************************************************
 *
 * Extended theory interface.
 *
 * This implements a generic module, used by theory solvers, for performing
 * "context-dependent simplification", as described in Reynolds et al
 * "Designing Theory Solvers with Extensions", FroCoS 2017.
 *
 * At a high level, this technique implements a generic inference scheme based
 * on the combination of SAT-context-dependent equality reasoning and
 * SAT-context-indepedent rewriting.
 *
 * As a simple example, say
 * (1) TheoryStrings tells us that the following facts hold in the SAT context:
 *     x = "A" ^ str.contains( str.++( x, z ), "B" ) = true.
 * (2) The Rewriter tells us that:
 *     str.contains( str.++( "A", z ), "B" ) ----> str.contains( z, "B" ).
 * From this, this class may infer that the following lemma is T-valid:
 *   x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" )
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__EXT_THEORY_H
#define CVC5__THEORY__EXT_THEORY_H

#include <map>

#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdo.h"
#include "context/context.h"
#include "expr/node.h"
#include "theory/theory_inference_manager.h"

namespace cvc5 {
namespace theory {

class OutputChannel;

/** Reasons for why a term was marked reduced */
enum class ExtReducedId
{
  UNKNOWN,
  // the extended function substitutes+rewrites to a constant
  SR_CONST,
  // the extended function was reduced by the callback
  REDUCTION,
  // the extended function substitutes+rewrites to zero
  ARITH_SR_ZERO,
  // the extended function substitutes+rewrites to a linear (non-zero) term
  ARITH_SR_LINEAR,
  // an extended string function substitutes+rewrites to a constant
  STRINGS_SR_CONST,
  // a negative str.contains was reduced to a disequality
  STRINGS_NEG_CTN_DEQ,
  // a positive str.contains was reduced to an equality
  STRINGS_POS_CTN,
  // a str.contains was subsumed by another based on a decomposition
  STRINGS_CTN_DECOMPOSE,
  // reduced via an intersection inference
  STRINGS_REGEXP_INTER,
  // subsumed due to intersection reasoning
  STRINGS_REGEXP_INTER_SUBSUME,
  // subsumed due to RE inclusion reasoning for positive memberships
  STRINGS_REGEXP_INCLUDE,
  // subsumed due to RE inclusion reasoning for negative memberships
  STRINGS_REGEXP_INCLUDE_NEG,
};
/**
 * Converts an ext reduced identifier to a string.
 *
 * @param id The ext reduced identifier
 * @return The name of the ext reduced identifier
 */
const char* toString(ExtReducedId id);

/**
 * Writes an ext reduced identifier to a stream.
 *
 * @param out The stream to write to
 * @param id The ext reduced identifier to write to the stream
 * @return The stream
 */
std::ostream& operator<<(std::ostream& out, ExtReducedId id);

/**
 * A callback class for ExtTheory below. This class is responsible for
 * determining how to apply context-dependent simplification.
 */
class ExtTheoryCallback
{
 public:
  virtual ~ExtTheoryCallback() {}
  /*
   * Get current substitution at an effort
   * @param effort The effort identifier
   * @param vars The variables to get a substitution for
   * @param subs The terms to substitute for variables, in order. This vector
   * should be updated to one the same size as vars.
   * @param exp The map containing the explanation for each variable. Together
   * with subs, we have that:
   *   ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
   * @return true if any (non-identity) substitution was added to subs.
   */
  virtual bool getCurrentSubstitution(int effort,
                                      const std::vector<Node>& vars,
                                      std::vector<Node>& subs,
                                      std::map<Node, std::vector<Node> >& exp);

  /*
   * Is extended function n reduced? This returns true if n is reduced to a
   * form that requires no further interaction from the theory.
   *
   * @param effort The effort identifier
   * @param n The term to reduce
   * @param on The original form of n, before substitution
   * @param exp The explanation of on = n
   * @param id If this method returns true, then id is updated to the reason
   * why n was reduced.
   * @return true if n is reduced.
   */
  virtual bool isExtfReduced(
      int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id);

  /**
   * Get reduction for node n.
   * If return value is true, then n is reduced.
   * If satDep is updated to false, then n is reduced independent of the
   * SAT context (e.g. by a lemma that persists at this
   * user-context level).
   * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
   * and return value of this method should be true.
   */
  virtual bool getReduction(int effort, Node n, Node& nr, bool& satDep);
};

/** Extended theory class
 *
 * This class is used for constructing generic extensions to theory solvers.
 * In particular, it provides methods for "context-dependent simplification"
 * and "model-based refinement". For details, see Reynolds et al "Design
 * Theory Solvers with Extensions", FroCoS 2017.
 *
 * It maintains:
 * (1) A set of "extended function" kinds (d_extf_kind),
 * (2) A database of active/inactive extended function terms (d_ext_func_terms)
 * that have been registered to the class.
 *
 * This class has methods doInferences/doReductions, which send out lemmas
 * based on the current set of active extended function terms. The former
 * is based on context-dependent simplification, where this class asks the
 * underlying theory for a "derivable substitution", whereby extended functions
 * may be reducable.
 */
class ExtTheory
{
  using NodeBoolMap = context::CDHashMap<Node, bool>;
  using NodeExtReducedIdMap = context::CDHashMap<Node, ExtReducedId>;
  using NodeSet = context::CDHashSet<Node>;

 public:
  /** constructor
   *
   * If cacheEnabled is false, we do not cache results of getSubstitutedTerm.
   */
  ExtTheory(ExtTheoryCallback& p,
            context::Context* c,
            context::UserContext* u,
            TheoryInferenceManager& im);
  virtual ~ExtTheory() {}
  /** Tells this class to treat terms with Kind k as extended functions */
  void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
  /** Is kind k treated as an extended function by this class? */
  bool hasFunctionKind(Kind k) const
  {
    return d_extf_kind.find(k) != d_extf_kind.end();
  }
  /** register term
   *
   * Registers term n with this class. Adds n to the set of extended function
   * terms known by this class (d_ext_func_terms) if n is an extended function,
   * that is, if addFunctionKind( n.getKind() ) was called.
   */
  void registerTerm(Node n);
  /** set n as reduced/inactive
   *
   * If satDep = false, then n remains inactive in the duration of this
   * user-context level
   */
  void markReduced(Node n, ExtReducedId rid, bool satDep = true);
  /** getSubstitutedTerms
   *
   *  input : effort, terms
   *  output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i.
   *
   * For each i, sterms[i] = term[i] * sigma for some "derivable substitution"
   * sigma. We obtain derivable substitutions and their explanations via calls
   * to the underlying theory's Theory::getCurrentSubstitution method.
   */
  void getSubstitutedTerms(int effort,
                           const std::vector<Node>& terms,
                           std::vector<Node>& sterms,
                           std::vector<std::vector<Node> >& exp);
  /**
   * Same as above, but for a single term. We return the substituted form of
   * term and add its explanation to exp.
   */
  Node getSubstitutedTerm(int effort, Node term, std::vector<Node>& exp);
  /** doInferences
   *
   * This function performs "context-dependent simplification". The method takes
   * as input:
   *  effort: an identifier used to determine which terms we reduce and the
   *          form of the derivable substitution we will use,
   *  terms: the set of terms to simplify,
   *  batch: if this flag is true, we send lemmas for all terms; if it is false
   *         we send a lemma for the first applicable term.
   *
   * Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms
   * and c is a constant, c = rewrite( t*sigma ) where exp |= sigma. These
   * lemmas are determined by asking the underlying theory for a derivable
   * substitution (through getCurrentSubstitution with getSubstitutedTerm)
   * above, applying this substitution to terms in terms, rewriting
   * the result and checking with the theory whether the resulting term is
   * in reduced form (isExtfReduced).
   *
   * This method adds the extended terms that are still active to nred, and
   * returns true if and only if a lemma of the above form was sent.
   */
  bool doInferences(int effort,
                    const std::vector<Node>& terms,
                    std::vector<Node>& nred,
                    bool batch = true);
  /**
   * Calls the above function, where terms is getActive(), the set of currently
   * active terms.
   */
  bool doInferences(int effort, std::vector<Node>& nred, bool batch = true);
  /** doReductions
   *
   * This method has the same interface as doInferences. In contrast to
   * doInfereces, this method will send reduction lemmas of the form ( t = t' )
   * where t is in terms and t' is an equivalent reduced term.
   */
  bool doReductions(int effort,
                    const std::vector<Node>& terms,
                    std::vector<Node>& nred,
                    bool batch = true);
  bool doReductions(int effort, std::vector<Node>& nred, bool batch = true);

  /** get the set of all extended function terms from d_ext_func_terms */
  void getTerms(std::vector<Node>& terms);
  /** is there at least one active extended function term? */
  bool hasActiveTerm() const;
  /** is n an active extended function term? */
  bool isActive(Node n) const;
  /**
   * Same as above, but rid is updated to the reason if this method returns
   * false.
   */
  bool isActive(Node n, ExtReducedId& rid) const;
  /** get the set of active terms from d_ext_func_terms */
  std::vector<Node> getActive() const;
  /** get the set of active terms from d_ext_func_terms of kind k */
  std::vector<Node> getActive(Kind k) const;

 private:
  /** returns the set of variable subterms of n */
  static std::vector<Node> collectVars(Node n);
  /** is n context dependent inactive? */
  bool isContextIndependentInactive(Node n) const;
  /**
   * Same as above, but rid is updated to the reason if this method returns
   * true.
   */
  bool isContextIndependentInactive(Node n, ExtReducedId& rid) const;
  /** do inferences internal */
  bool doInferencesInternal(int effort,
                            const std::vector<Node>& terms,
                            std::vector<Node>& nred,
                            bool batch,
                            bool isRed);
  /** send lemma on the output channel */
  bool sendLemma(Node lem, InferenceId id, bool preprocess = false);
  /** reference to the callback */
  ExtTheoryCallback& d_parent;
  /** inference manager used to send lemmas */
  TheoryInferenceManager& d_im;
  /** the true node */
  Node d_true;
  /** extended function terms, map to whether they are active */
  NodeBoolMap d_ext_func_terms;
  /** mapping to why extended function terms are inactive */
  NodeExtReducedIdMap d_extfExtReducedIdMap;
  /**
   * The set of terms from d_ext_func_terms that are SAT-context-independent
   * inactive. For instance, a term t is SAT-context-independent inactive if
   * a reduction lemma of the form t = t' was added in this user-context level.
   */
  NodeExtReducedIdMap d_ci_inactive;
  /**
   * Watched term for checking if any non-reduced extended functions exist.
   * This is an arbitrary active member of d_ext_func_terms.
   */
  context::CDO<Node> d_has_extf;
  /** the set of kinds we are treated as extended functions */
  std::map<Kind, bool> d_extf_kind;
  /** information for each term in d_ext_func_terms */
  class ExtfInfo
  {
   public:
    /** all variables in this term */
    std::vector<Node> d_vars;
  };
  std::map<Node, ExtfInfo> d_extf_info;

  // cache of all lemmas sent
  NodeSet d_lemmas;
  NodeSet d_pp_lemmas;
};

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__EXT_THEORY_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Tim King, 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		* Extended theory interface.
14		*
15		* This implements a generic module, used by theory solvers, for performing
16		* "context-dependent simplification", as described in Reynolds et al
17		* "Designing Theory Solvers with Extensions", FroCoS 2017.
18		*
19		* At a high level, this technique implements a generic inference scheme based
20		* on the combination of SAT-context-dependent equality reasoning and
21		* SAT-context-indepedent rewriting.
22		*
23		* As a simple example, say
24		* (1) TheoryStrings tells us that the following facts hold in the SAT context:
25		* x = "A" ^ str.contains( str.++( x, z ), "B" ) = true.
26		* (2) The Rewriter tells us that:
27		* str.contains( str.++( "A", z ), "B" ) ----> str.contains( z, "B" ).
28		* From this, this class may infer that the following lemma is T-valid:
29		* x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" )
30		*/
31
32		#include "cvc5_private.h"
33
34		#ifndef CVC5__THEORY__EXT_THEORY_H
35		#define CVC5__THEORY__EXT_THEORY_H
36
37		#include <map>
38
39		#include "context/cdhashmap.h"
40		#include "context/cdhashset.h"
41		#include "context/cdo.h"
42		#include "context/context.h"
43		#include "expr/node.h"
44		#include "theory/theory_inference_manager.h"
45
46		namespace cvc5 {
47		namespace theory {
48
49		class OutputChannel;
50
51		/** Reasons for why a term was marked reduced */
52		enum class ExtReducedId
53		{
54		UNKNOWN,
55		// the extended function substitutes+rewrites to a constant
56		SR_CONST,
57		// the extended function was reduced by the callback
58		REDUCTION,
59		// the extended function substitutes+rewrites to zero
60		ARITH_SR_ZERO,
61		// the extended function substitutes+rewrites to a linear (non-zero) term
62		ARITH_SR_LINEAR,
63		// an extended string function substitutes+rewrites to a constant
64		STRINGS_SR_CONST,
65		// a negative str.contains was reduced to a disequality
66		STRINGS_NEG_CTN_DEQ,
67		// a positive str.contains was reduced to an equality
68		STRINGS_POS_CTN,
69		// a str.contains was subsumed by another based on a decomposition
70		STRINGS_CTN_DECOMPOSE,
71		// reduced via an intersection inference
72		STRINGS_REGEXP_INTER,
73		// subsumed due to intersection reasoning
74		STRINGS_REGEXP_INTER_SUBSUME,
75		// subsumed due to RE inclusion reasoning for positive memberships
76		STRINGS_REGEXP_INCLUDE,
77		// subsumed due to RE inclusion reasoning for negative memberships
78		STRINGS_REGEXP_INCLUDE_NEG,
79		};
80		/**
81		* Converts an ext reduced identifier to a string.
82		*
83		* @param id The ext reduced identifier
84		* @return The name of the ext reduced identifier
85		*/
86		const char* toString(ExtReducedId id);
87
88		/**
89		* Writes an ext reduced identifier to a stream.
90		*
91		* @param out The stream to write to
92		* @param id The ext reduced identifier to write to the stream
93		* @return The stream
94		*/
95		std::ostream& operator<<(std::ostream& out, ExtReducedId id);
96
97		/**
98		* A callback class for ExtTheory below. This class is responsible for
99		* determining how to apply context-dependent simplification.
100		*/
101	15138	class ExtTheoryCallback
102		{
103		public:
104	15133	virtual ~ExtTheoryCallback() {}
105		/*
106		* Get current substitution at an effort
107		* @param effort The effort identifier
108		* @param vars The variables to get a substitution for
109		* @param subs The terms to substitute for variables, in order. This vector
110		* should be updated to one the same size as vars.
111		* @param exp The map containing the explanation for each variable. Together
112		* with subs, we have that:
113		* ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
114		* @return true if any (non-identity) substitution was added to subs.
115		*/
116		virtual bool getCurrentSubstitution(int effort,
117		const std::vector<Node>& vars,
118		std::vector<Node>& subs,
119		std::map<Node, std::vector<Node> >& exp);
120
121		/*
122		* Is extended function n reduced? This returns true if n is reduced to a
123		* form that requires no further interaction from the theory.
124		*
125		* @param effort The effort identifier
126		* @param n The term to reduce
127		* @param on The original form of n, before substitution
128		* @param exp The explanation of on = n
129		* @param id If this method returns true, then id is updated to the reason
130		* why n was reduced.
131		* @return true if n is reduced.
132		*/
133		virtual bool isExtfReduced(
134		int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id);
135
136		/**
137		* Get reduction for node n.
138		* If return value is true, then n is reduced.
139		* If satDep is updated to false, then n is reduced independent of the
140		* SAT context (e.g. by a lemma that persists at this
141		* user-context level).
142		* If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
143		* and return value of this method should be true.
144		*/
145		virtual bool getReduction(int effort, Node n, Node& nr, bool& satDep);
146		};
147
148		/** Extended theory class
149		*
150		* This class is used for constructing generic extensions to theory solvers.
151		* In particular, it provides methods for "context-dependent simplification"
152		* and "model-based refinement". For details, see Reynolds et al "Design
153		* Theory Solvers with Extensions", FroCoS 2017.
154		*
155		* It maintains:
156		* (1) A set of "extended function" kinds (d_extf_kind),
157		* (2) A database of active/inactive extended function terms (d_ext_func_terms)
158		* that have been registered to the class.
159		*
160		* This class has methods doInferences/doReductions, which send out lemmas
161		* based on the current set of active extended function terms. The former
162		* is based on context-dependent simplification, where this class asks the
163		* underlying theory for a "derivable substitution", whereby extended functions
164		* may be reducable.
165		*/
166		class ExtTheory
167		{
168		using NodeBoolMap = context::CDHashMap<Node, bool>;
169		using NodeExtReducedIdMap = context::CDHashMap<Node, ExtReducedId>;
170		using NodeSet = context::CDHashSet<Node>;
171
172		public:
173		/** constructor
174		*
175		* If cacheEnabled is false, we do not cache results of getSubstitutedTerm.
176		*/
177		ExtTheory(ExtTheoryCallback& p,
178		context::Context* c,
179		context::UserContext* u,
180		TheoryInferenceManager& im);
181	15133	virtual ~ExtTheory() {}
182		/** Tells this class to treat terms with Kind k as extended functions */
183	219892	void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
184		/** Is kind k treated as an extended function by this class? */
185	152	bool hasFunctionKind(Kind k) const
186		{
187	152	return d_extf_kind.find(k) != d_extf_kind.end();
188		}
189		/** register term
190		*
191		* Registers term n with this class. Adds n to the set of extended function
192		* terms known by this class (d_ext_func_terms) if n is an extended function,
193		* that is, if addFunctionKind( n.getKind() ) was called.
194		*/
195		void registerTerm(Node n);
196		/** set n as reduced/inactive
197		*
198		* If satDep = false, then n remains inactive in the duration of this
199		* user-context level
200		*/
201		void markReduced(Node n, ExtReducedId rid, bool satDep = true);
202		/** getSubstitutedTerms
203		*
204		* input : effort, terms
205		* output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i.
206		*
207		* For each i, sterms[i] = term[i] * sigma for some "derivable substitution"
208		* sigma. We obtain derivable substitutions and their explanations via calls
209		* to the underlying theory's Theory::getCurrentSubstitution method.
210		*/
211		void getSubstitutedTerms(int effort,
212		const std::vector<Node>& terms,
213		std::vector<Node>& sterms,
214		std::vector<std::vector<Node> >& exp);
215		/**
216		* Same as above, but for a single term. We return the substituted form of
217		* term and add its explanation to exp.
218		*/
219		Node getSubstitutedTerm(int effort, Node term, std::vector<Node>& exp);
220		/** doInferences
221		*
222		* This function performs "context-dependent simplification". The method takes
223		* as input:
224		* effort: an identifier used to determine which terms we reduce and the
225		* form of the derivable substitution we will use,
226		* terms: the set of terms to simplify,
227		* batch: if this flag is true, we send lemmas for all terms; if it is false
228		* we send a lemma for the first applicable term.
229		*
230		* Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms
231		* and c is a constant, c = rewrite( t*sigma ) where exp \|= sigma. These
232		* lemmas are determined by asking the underlying theory for a derivable
233		* substitution (through getCurrentSubstitution with getSubstitutedTerm)
234		* above, applying this substitution to terms in terms, rewriting
235		* the result and checking with the theory whether the resulting term is
236		* in reduced form (isExtfReduced).
237		*
238		* This method adds the extended terms that are still active to nred, and
239		* returns true if and only if a lemma of the above form was sent.
240		*/
241		bool doInferences(int effort,
242		const std::vector<Node>& terms,
243		std::vector<Node>& nred,
244		bool batch = true);
245		/**
246		* Calls the above function, where terms is getActive(), the set of currently
247		* active terms.
248		*/
249		bool doInferences(int effort, std::vector<Node>& nred, bool batch = true);
250		/** doReductions
251		*
252		* This method has the same interface as doInferences. In contrast to
253		* doInfereces, this method will send reduction lemmas of the form ( t = t' )
254		* where t is in terms and t' is an equivalent reduced term.
255		*/
256		bool doReductions(int effort,
257		const std::vector<Node>& terms,
258		std::vector<Node>& nred,
259		bool batch = true);
260		bool doReductions(int effort, std::vector<Node>& nred, bool batch = true);
261
262		/** get the set of all extended function terms from d_ext_func_terms */
263		void getTerms(std::vector<Node>& terms);
264		/** is there at least one active extended function term? */
265		bool hasActiveTerm() const;
266		/** is n an active extended function term? */
267		bool isActive(Node n) const;
268		/**
269		* Same as above, but rid is updated to the reason if this method returns
270		* false.
271		*/
272		bool isActive(Node n, ExtReducedId& rid) const;
273		/** get the set of active terms from d_ext_func_terms */
274		std::vector<Node> getActive() const;
275		/** get the set of active terms from d_ext_func_terms of kind k */
276		std::vector<Node> getActive(Kind k) const;
277
278		private:
279		/** returns the set of variable subterms of n */
280		static std::vector<Node> collectVars(Node n);
281		/** is n context dependent inactive? */
282		bool isContextIndependentInactive(Node n) const;
283		/**
284		* Same as above, but rid is updated to the reason if this method returns
285		* true.
286		*/
287		bool isContextIndependentInactive(Node n, ExtReducedId& rid) const;
288		/** do inferences internal */
289		bool doInferencesInternal(int effort,
290		const std::vector<Node>& terms,
291		std::vector<Node>& nred,
292		bool batch,
293		bool isRed);
294		/** send lemma on the output channel */
295		bool sendLemma(Node lem, InferenceId id, bool preprocess = false);
296		/** reference to the callback */
297		ExtTheoryCallback& d_parent;
298		/** inference manager used to send lemmas */
299		TheoryInferenceManager& d_im;
300		/** the true node */
301		Node d_true;
302		/** extended function terms, map to whether they are active */
303		NodeBoolMap d_ext_func_terms;
304		/** mapping to why extended function terms are inactive */
305		NodeExtReducedIdMap d_extfExtReducedIdMap;
306		/**
307		* The set of terms from d_ext_func_terms that are SAT-context-independent
308		* inactive. For instance, a term t is SAT-context-independent inactive if
309		* a reduction lemma of the form t = t' was added in this user-context level.
310		*/
311		NodeExtReducedIdMap d_ci_inactive;
312		/**
313		* Watched term for checking if any non-reduced extended functions exist.
314		* This is an arbitrary active member of d_ext_func_terms.
315		*/
316		context::CDO<Node> d_has_extf;
317		/** the set of kinds we are treated as extended functions */
318		std::map<Kind, bool> d_extf_kind;
319		/** information for each term in d_ext_func_terms */
320	21254	class ExtfInfo
321		{
322		public:
323		/** all variables in this term */
324		std::vector<Node> d_vars;
325		};
326		std::map<Node, ExtfInfo> d_extf_info;
327
328		// cache of all lemmas sent
329		NodeSet d_lemmas;
330		NodeSet d_pp_lemmas;
331		};
332
333		} // namespace theory
334		} // namespace cvc5
335
336		#endif /* CVC5__THEORY__EXT_THEORY_H */