Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/rep_set.h	Lines:	9	14	64.3 %
Date:	2021-09-10	Branches:	0	0	0.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.
 * ****************************************************************************
 *
 * Representative set class and utilities.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__REP_SET_H
#define CVC5__THEORY__REP_SET_H

#include <map>
#include <vector>

#include "expr/node.h"
#include "expr/type_node.h"

namespace cvc5 {
namespace theory {

class QuantifiersEngine;

/** representative set
 *
 * This class contains finite lists of values for types, typically values and
 * types that exist
 * in the equality engine of a model object.  In the following, "representative"
 * means a value that exists in this set.
 *
 * This class is used for finite model finding and other exhaustive
 * instantiation-based
 * methods. The class goes beyond just maintaining a list of values that occur
 * in the equality engine in the following ways:

 * (1) It maintains a partial mapping from representatives to a term that has
 * that value in the current
 * model.  This is important because algorithms like the instantiation method in
 * Reynolds et al CADE 2013
 * act on "term models" where domains in models are interpreted as a set of
 * representative terms. Hence,
 * instead of instantiating with e.g. uninterpreted constants u, we instantiate
 * with the corresponding term that is interpreted as u.

 * (2) It is mutable, calls to add(...) and complete(...) may modify this class
 * as necessary, for instance
 * in the case that there are no ground terms of a type that occurs in a
 * quantified formula, or for
 * exhaustive instantiation strategies that enumerate over small interpreted
 * finite types.
 */
class RepSet {
 public:
  RepSet(){}

  /** map from types to the list of representatives
   * TODO : as part of #1199, encapsulate this
   */
  std::map< TypeNode, std::vector< Node > > d_type_reps;
  /** clear the set */
  void clear();
  /** does this set have representatives of type tn? */
  bool hasType(TypeNode tn) const { return d_type_reps.count(tn) > 0; }
  /** does this set have representative n of type tn? */
  bool hasRep(TypeNode tn, Node n) const;
  /** get the number of representatives for type */
  size_t getNumRepresentatives(TypeNode tn) const;
  /** get representative at index */
  Node getRepresentative(TypeNode tn, unsigned i) const;
  /**
   * Returns the representatives of a type for a `type_node` if one exists.
   * Otherwise, returns nullptr.
   */
  const std::vector<Node>* getTypeRepsOrNull(TypeNode type_node) const;

  /** add representative n for type tn, where n has type tn */
  void add( TypeNode tn, Node n );
  /** returns index in d_type_reps for node n */
  int getIndexFor( Node n ) const;
  /** complete the list for type t
   * Resets d_type_reps[tn] and repopulates by running the type enumerator for
   * that type exhaustively.
   * This should only be called for small finite interpreted types.
   */
  bool complete( TypeNode t );
  /** get term for representative
   * Returns a term that is interpreted as representative n in the current
   * model, null otherwise.
   */
  Node getTermForRepresentative(Node n) const;
  /** set term for representative
   * Called when t is interpreted as value n. Subsequent class to
   * getTermForRepresentative( n ) will return t.
   */
  void setTermForRepresentative(Node n, Node t);
  /** get existing domain value, with possible exclusions
    *   This function returns a term in d_type_reps[tn] but not in exclude
    */
  Node getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const;
  /** debug print */
  void toStream(std::ostream& out);

 private:
  /** whether the list of representatives for types are complete */
  std::map<TypeNode, bool> d_type_complete;
  /** map from representatives to their index in d_type_reps */
  std::map<Node, int> d_tmap;
  /** map from values to terms they were assigned for */
  std::map<Node, Node> d_values_to_terms;
};/* class RepSet */

//representative domain
typedef std::vector< int > RepDomain;

class RepBoundExt;

/**
 * Representative set iterator enumeration type, which indicates how the
 * bound on a variable was determined.
 */
enum RsiEnumType
{
  // the bound on the variable is invalid
  ENUM_INVALID = 0,
  // the bound on the variable was determined in the default way, i.e. based
  // on an enumeration of terms in the model.
  ENUM_DEFAULT,
  // The bound on the variable was determined in a custom way, i.e. via a
  // quantifiers module like the BoundedIntegers module.
  ENUM_CUSTOM,
};

/** Rep set iterator.
 *
 * This class is used for iterating over (tuples of) terms
 * in the domain(s) of a RepSet.
 *
 * To use it, first it must
 * be initialized with a call to:
 * - setQuantifier or setFunctionDomain
 * which initializes the d_owner field and sets up
 * initial information.
 *
 * Then, we increment over the tuples of terms in the
 * domains of the owner of this iterator using:
 * - increment and incrementAtIndex
 *
 * TODO (#1199): this class needs further documentation.
 */
class RepSetIterator {
public:
 RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
 ~RepSetIterator() {}
 /** set that this iterator will be iterating over instantiations for a
  * quantifier */
 bool setQuantifier(Node q);
 /** set that this iterator will be iterating over the domain of a function */
 bool setFunctionDomain(Node op);
 /** increment the iterator */
 int increment();
 /** increment the iterator at index
  * This increments the i^th field of the
  * iterator, for examples, see operator next_i
  * in Figure 2 of Reynolds et al. CADE 2013.
  */
 int incrementAtIndex(int i);
 /** is the iterator finished? */
 bool isFinished() const;
 /** get domain size of the i^th field of this iterator */
 unsigned domainSize(unsigned i);
 /** Get the type of terms in the i^th field of this iterator */
 TypeNode getTypeOf(unsigned i) const;
 /**
  * Get the value for the i^th field in the tuple we are currently considering.
  * If valTerm is true, we return a term instead of a value by calling
  * RepSet::getTermForRepresentative on the value.
  */
 Node getCurrentTerm(unsigned i, bool valTerm = false) const;
 /** get the number of terms in the tuple we are considering */
 unsigned getNumTerms() const { return d_index_order.size(); }
 /** get current terms */
 void getCurrentTerms(std::vector<Node>& terms) const;
 /** get index order, returns var # */
 unsigned getIndexOrder(unsigned v) { return d_index_order[v]; }
 /** get variable order, returns index # */
 unsigned getVariableOrder(unsigned i) { return d_var_order[i]; }
 /** is incomplete
  * Returns true if we are iterating over a strict subset of
  * the domain of the quantified formula or function.
  */
 bool isIncomplete() { return d_incomplete; }
 /** debug print methods */
 void debugPrint(const char* c);
 void debugPrintSmall(const char* c);
 // TODO (#1199): these should be private
 /** enumeration type for each field */
 std::vector<RsiEnumType> d_enum_type;
 /** the current tuple we are considering */
 std::vector<int> d_index;

private:
 /** rep set associated with this iterator */
 const RepSet* d_rs;
 /** rep set external bound information for this iterator */
 RepBoundExt* d_rext;
 /** types we are considering */
 std::vector<TypeNode> d_types;
 /** for each argument, the domain we are iterating over */
 std::vector<std::vector<Node> > d_domain_elements;
 /** initialize
  * This is called when the owner of this iterator is set.
  * It initializes the typing information for the types
  * that are involved in this iterator, initializes the
  * domain elements we are iterating over, and variable
  * and index orderings we are considering.
  */
 bool initialize();
 /** owner
  * This is the term that we are iterating for, which may either be:
  * (1) a quantified formula, or
  * (2) a function.
  */
 Node d_owner;
 /** reset index, 1:success, 0:empty, -1:fail */
 int resetIndex(unsigned i, bool initial = false);
 /** set index order (see below) */
 void setIndexOrder(std::vector<unsigned>& indexOrder);
 /** do reset increment the iterator at index=counter */
 int do_reset_increment(int counter, bool initial = false);
 /** ordering for variables we are iterating over
 *  For example, given reps = { a, b } and quantifier
 *    forall( x, y, z ) P( x, y, z )
 *  with d_index_order = { 2, 0, 1 },
 *    then we consider instantiations in this order:
 *      a/x a/y a/z
 *      a/x b/y a/z
 *      b/x a/y a/z
 *      b/x b/y a/z
 *      ...
 */
 std::vector<unsigned> d_index_order;
 /** Map from variables to the index they are considered at
 * For example, if d_index_order = { 2, 0, 1 }
 *    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
 */
 std::map<unsigned, unsigned> d_var_order;
 /** incomplete flag */
 bool d_incomplete;
};/* class RepSetIterator */

/** Representative bound external
 *
 * This class manages bound information
 * for an instance of a RepSetIterator.
 * Its main functionalities are to set
 * bounds on the domain of the iterator
 * over quantifiers and function arguments.
 */
class RepBoundExt
{
 public:
  virtual ~RepBoundExt() {}
  /** set bound
   *
   * This method initializes the vector "elements"
   * with list of terms to iterate over for the i^th
   * field of owner, where owner may be :
   * (1) A function, in which case we are iterating
   *     over domain elements of its argument type,
   * (2) A quantified formula, in which case we are
   *     iterating over domain elements of the type
   *     of its i^th bound variable.
   */
  virtual RsiEnumType setBound(Node owner,
                               unsigned i,
                               std::vector<Node>& elements) = 0;
  /** reset index
   *
   * This method initializes iteration for the i^th
   * field of owner, based on the current state of
   * the iterator rsi. It initializes the vector
   * "elements" with all appropriate terms to
   * iterate over in this context.
   * initial is whether this is the first call
   * to this function for this iterator.
   *
   * This method returns false if we were unable
   * to establish (finite) bounds for the current
   * field we are considering, which indicates that
   * the iterator will terminate with a failure.
   */
  virtual bool resetIndex(RepSetIterator* rsi,
                          Node owner,
                          unsigned i,
                          bool initial,
                          std::vector<Node>& elements)
  {
    return true;
  }
  /** initialize representative set for type
   *
   * Returns true if the representative set associated
   * with this bound has been given a complete interpretation
   * for type tn.
   */
  virtual bool initializeRepresentativesForType(TypeNode tn) { return false; }
  /** get variable order
   * If this method returns true, then varOrder is the order
   * in which we want to consider variables for the iterator.
   * If this method returns false, then varOrder is unchanged
   * and the RepSetIterator is free to choose a default
   * variable order.
   */
  virtual bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
  {
    return false;
  }
};

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__REP_SET_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		* Representative set class and utilities.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__REP_SET_H
19		#define CVC5__THEORY__REP_SET_H
20
21		#include <map>
22		#include <vector>
23
24		#include "expr/node.h"
25		#include "expr/type_node.h"
26
27		namespace cvc5 {
28		namespace theory {
29
30		class QuantifiersEngine;
31
32		/** representative set
33		*
34		* This class contains finite lists of values for types, typically values and
35		* types that exist
36		* in the equality engine of a model object. In the following, "representative"
37		* means a value that exists in this set.
38		*
39		* This class is used for finite model finding and other exhaustive
40		* instantiation-based
41		* methods. The class goes beyond just maintaining a list of values that occur
42		* in the equality engine in the following ways:
43
44		* (1) It maintains a partial mapping from representatives to a term that has
45		* that value in the current
46		* model. This is important because algorithms like the instantiation method in
47		* Reynolds et al CADE 2013
48		* act on "term models" where domains in models are interpreted as a set of
49		* representative terms. Hence,
50		* instead of instantiating with e.g. uninterpreted constants u, we instantiate
51		* with the corresponding term that is interpreted as u.
52
53		* (2) It is mutable, calls to add(...) and complete(...) may modify this class
54		* as necessary, for instance
55		* in the case that there are no ground terms of a type that occurs in a
56		* quantified formula, or for
57		* exhaustive instantiation strategies that enumerate over small interpreted
58		* finite types.
59		*/
60	9910	class RepSet {
61		public:
62	9913	RepSet(){}
63
64		/** map from types to the list of representatives
65		* TODO : as part of #1199, encapsulate this
66		*/
67		std::map< TypeNode, std::vector< Node > > d_type_reps;
68		/** clear the set */
69		void clear();
70		/** does this set have representatives of type tn? */
71	15112	bool hasType(TypeNode tn) const { return d_type_reps.count(tn) > 0; }
72		/** does this set have representative n of type tn? */
73		bool hasRep(TypeNode tn, Node n) const;
74		/** get the number of representatives for type */
75		size_t getNumRepresentatives(TypeNode tn) const;
76		/** get representative at index */
77		Node getRepresentative(TypeNode tn, unsigned i) const;
78		/**
79		* Returns the representatives of a type for a `type_node` if one exists.
80		* Otherwise, returns nullptr.
81		*/
82		const std::vector<Node>* getTypeRepsOrNull(TypeNode type_node) const;
83
84		/** add representative n for type tn, where n has type tn */
85		void add( TypeNode tn, Node n );
86		/** returns index in d_type_reps for node n */
87		int getIndexFor( Node n ) const;
88		/** complete the list for type t
89		* Resets d_type_reps[tn] and repopulates by running the type enumerator for
90		* that type exhaustively.
91		* This should only be called for small finite interpreted types.
92		*/
93		bool complete( TypeNode t );
94		/** get term for representative
95		* Returns a term that is interpreted as representative n in the current
96		* model, null otherwise.
97		*/
98		Node getTermForRepresentative(Node n) const;
99		/** set term for representative
100		* Called when t is interpreted as value n. Subsequent class to
101		* getTermForRepresentative( n ) will return t.
102		*/
103		void setTermForRepresentative(Node n, Node t);
104		/** get existing domain value, with possible exclusions
105		* This function returns a term in d_type_reps[tn] but not in exclude
106		*/
107		Node getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const;
108		/** debug print */
109		void toStream(std::ostream& out);
110
111		private:
112		/** whether the list of representatives for types are complete */
113		std::map<TypeNode, bool> d_type_complete;
114		/** map from representatives to their index in d_type_reps */
115		std::map<Node, int> d_tmap;
116		/** map from values to terms they were assigned for */
117		std::map<Node, Node> d_values_to_terms;
118		};/* class RepSet */
119
120		//representative domain
121		typedef std::vector< int > RepDomain;
122
123		class RepBoundExt;
124
125		/**
126		* Representative set iterator enumeration type, which indicates how the
127		* bound on a variable was determined.
128		*/
129		enum RsiEnumType
130		{
131		// the bound on the variable is invalid
132		ENUM_INVALID = 0,
133		// the bound on the variable was determined in the default way, i.e. based
134		// on an enumeration of terms in the model.
135		ENUM_DEFAULT,
136		// The bound on the variable was determined in a custom way, i.e. via a
137		// quantifiers module like the BoundedIntegers module.
138		ENUM_CUSTOM,
139		};
140
141		/** Rep set iterator.
142		*
143		* This class is used for iterating over (tuples of) terms
144		* in the domain(s) of a RepSet.
145		*
146		* To use it, first it must
147		* be initialized with a call to:
148		* - setQuantifier or setFunctionDomain
149		* which initializes the d_owner field and sets up
150		* initial information.
151		*
152		* Then, we increment over the tuples of terms in the
153		* domains of the owner of this iterator using:
154		* - increment and incrementAtIndex
155		*
156		* TODO (#1199): this class needs further documentation.
157		*/
158		class RepSetIterator {
159		public:
160		RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
161	5439	~RepSetIterator() {}
162		/** set that this iterator will be iterating over instantiations for a
163		* quantifier */
164		bool setQuantifier(Node q);
165		/** set that this iterator will be iterating over the domain of a function */
166		bool setFunctionDomain(Node op);
167		/** increment the iterator */
168		int increment();
169		/** increment the iterator at index
170		* This increments the i^th field of the
171		* iterator, for examples, see operator next_i
172		* in Figure 2 of Reynolds et al. CADE 2013.
173		*/
174		int incrementAtIndex(int i);
175		/** is the iterator finished? */
176		bool isFinished() const;
177		/** get domain size of the i^th field of this iterator */
178		unsigned domainSize(unsigned i);
179		/** Get the type of terms in the i^th field of this iterator */
180		TypeNode getTypeOf(unsigned i) const;
181		/**
182		* Get the value for the i^th field in the tuple we are currently considering.
183		* If valTerm is true, we return a term instead of a value by calling
184		* RepSet::getTermForRepresentative on the value.
185		*/
186		Node getCurrentTerm(unsigned i, bool valTerm = false) const;
187		/** get the number of terms in the tuple we are considering */
188	108275	unsigned getNumTerms() const { return d_index_order.size(); }
189		/** get current terms */
190		void getCurrentTerms(std::vector<Node>& terms) const;
191		/** get index order, returns var # */
192		unsigned getIndexOrder(unsigned v) { return d_index_order[v]; }
193		/** get variable order, returns index # */
194	1735	unsigned getVariableOrder(unsigned i) { return d_var_order[i]; }
195		/** is incomplete
196		* Returns true if we are iterating over a strict subset of
197		* the domain of the quantified formula or function.
198		*/
199	9515	bool isIncomplete() { return d_incomplete; }
200		/** debug print methods */
201		void debugPrint(const char* c);
202		void debugPrintSmall(const char* c);
203		// TODO (#1199): these should be private
204		/** enumeration type for each field */
205		std::vector<RsiEnumType> d_enum_type;
206		/** the current tuple we are considering */
207		std::vector<int> d_index;
208
209		private:
210		/** rep set associated with this iterator */
211		const RepSet* d_rs;
212		/** rep set external bound information for this iterator */
213		RepBoundExt* d_rext;
214		/** types we are considering */
215		std::vector<TypeNode> d_types;
216		/** for each argument, the domain we are iterating over */
217		std::vector<std::vector<Node> > d_domain_elements;
218		/** initialize
219		* This is called when the owner of this iterator is set.
220		* It initializes the typing information for the types
221		* that are involved in this iterator, initializes the
222		* domain elements we are iterating over, and variable
223		* and index orderings we are considering.
224		*/
225		bool initialize();
226		/** owner
227		* This is the term that we are iterating for, which may either be:
228		* (1) a quantified formula, or
229		* (2) a function.
230		*/
231		Node d_owner;
232		/** reset index, 1:success, 0:empty, -1:fail */
233		int resetIndex(unsigned i, bool initial = false);
234		/** set index order (see below) */
235		void setIndexOrder(std::vector<unsigned>& indexOrder);
236		/** do reset increment the iterator at index=counter */
237		int do_reset_increment(int counter, bool initial = false);
238		/** ordering for variables we are iterating over
239		* For example, given reps = { a, b } and quantifier
240		* forall( x, y, z ) P( x, y, z )
241		* with d_index_order = { 2, 0, 1 },
242		* then we consider instantiations in this order:
243		* a/x a/y a/z
244		* a/x b/y a/z
245		* b/x a/y a/z
246		* b/x b/y a/z
247		* ...
248		*/
249		std::vector<unsigned> d_index_order;
250		/** Map from variables to the index they are considered at
251		* For example, if d_index_order = { 2, 0, 1 }
252		* then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
253		*/
254		std::map<unsigned, unsigned> d_var_order;
255		/** incomplete flag */
256		bool d_incomplete;
257		};/* class RepSetIterator */
258
259		/** Representative bound external
260		*
261		* This class manages bound information
262		* for an instance of a RepSetIterator.
263		* Its main functionalities are to set
264		* bounds on the domain of the iterator
265		* over quantifiers and function arguments.
266		*/
267	5439	class RepBoundExt
268		{
269		public:
270	5439	virtual ~RepBoundExt() {}
271		/** set bound
272		*
273		* This method initializes the vector "elements"
274		* with list of terms to iterate over for the i^th
275		* field of owner, where owner may be :
276		* (1) A function, in which case we are iterating
277		* over domain elements of its argument type,
278		* (2) A quantified formula, in which case we are
279		* iterating over domain elements of the type
280		* of its i^th bound variable.
281		*/
282		virtual RsiEnumType setBound(Node owner,
283		unsigned i,
284		std::vector<Node>& elements) = 0;
285		/** reset index
286		*
287		* This method initializes iteration for the i^th
288		* field of owner, based on the current state of
289		* the iterator rsi. It initializes the vector
290		* "elements" with all appropriate terms to
291		* iterate over in this context.
292		* initial is whether this is the first call
293		* to this function for this iterator.
294		*
295		* This method returns false if we were unable
296		* to establish (finite) bounds for the current
297		* field we are considering, which indicates that
298		* the iterator will terminate with a failure.
299		*/
300		virtual bool resetIndex(RepSetIterator* rsi,
301		Node owner,
302		unsigned i,
303		bool initial,
304		std::vector<Node>& elements)
305		{
306		return true;
307		}
308		/** initialize representative set for type
309		*
310		* Returns true if the representative set associated
311		* with this bound has been given a complete interpretation
312		* for type tn.
313		*/
314		virtual bool initializeRepresentativesForType(TypeNode tn) { return false; }
315		/** get variable order
316		* If this method returns true, then varOrder is the order
317		* in which we want to consider variables for the iterator.
318		* If this method returns false, then varOrder is unchanged
319		* and the RepSetIterator is free to choose a default
320		* variable order.
321		*/
322		virtual bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
323		{
324		return false;
325		}
326		};
327
328		} // namespace theory
329		} // namespace cvc5
330
331		#endif /* CVC5__THEORY__REP_SET_H */