Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/type_enumerator.h	Lines:	49	49	100.0 %
Date:	2021-09-07	Branches:	50	92	54.3 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * An enumerator for datatypes.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H
#define CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H

#include "expr/dtype.h"
#include "expr/kind.h"
#include "expr/type_node.h"
#include "expr/uninterpreted_constant.h"
#include "options/quantifiers_options.h"
#include "theory/type_enumerator.h"

namespace cvc5 {
namespace theory {
namespace datatypes {


class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
  /** type properties */
  TypeEnumeratorProperties * d_tep;
  /** The datatype we're enumerating */
  const DType& d_datatype;
  /** extra cons */
  unsigned d_has_debruijn;
  /** type */
  TypeNode d_type;
  /** The datatype constructor we're currently enumerating */
  unsigned d_ctor;
  /** The first term to consider in the enumeration */
  Node d_zeroTerm;
  /** Whether we are currently considering the above term */
  bool d_zeroTermActive;
  /** list of type enumerators (one for each type in a selector argument) */
  std::map< TypeNode, unsigned > d_te_index;
  std::vector< TypeEnumerator > d_children;
  //std::vector< DatatypesEnumerator > d_dt_children;
  /** terms produced for types */
  std::map< TypeNode, std::vector< Node > > d_terms;
  /** arg type of each selector, for each constructor */
  std::vector< std::vector< TypeNode > > d_sel_types;
  /** current index for each argument, for each constructor */
  std::vector< std::vector< unsigned > > d_sel_index;
  /** current sum of argument indicies for each constructor */
  std::vector< int > d_sel_sum;
  /** current bound on the number of times we can iterate argument enumerators */
  unsigned d_size_limit;
  /** child */
  bool d_child_enum;

  bool hasCyclesDt(const DType& dt)
  {
    return dt.isRecursiveSingleton(d_type)
           || dt.getCardinalityClass(d_type) == CardinalityClass::INFINITE;
  }
  bool hasCycles( TypeNode tn ){
    if( tn.isDatatype() ){
      const DType& dt = tn.getDType();
      return hasCyclesDt( dt );
    }else{
      return false;
    }
  }

  Node getTermEnum( TypeNode tn, unsigned i );

  bool increment( unsigned index );

  Node getCurrentTerm( unsigned index );

  void init();

 public:
  DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
      : TypeEnumeratorBase<DatatypesEnumerator>(type),
        d_tep(tep),
        d_datatype(type.getDType()),
        d_type(type),
        d_ctor(0),
        d_zeroTermActive(false)
  {
    d_child_enum = false;
    init();
  }
  DatatypesEnumerator(TypeNode type,
                      bool childEnum,
                      TypeEnumeratorProperties* tep = nullptr)
      : TypeEnumeratorBase<DatatypesEnumerator>(type),
        d_tep(tep),
        d_datatype(type.getDType()),
        d_type(type),
        d_ctor(0),
        d_zeroTermActive(false)
  {
    d_child_enum = childEnum;
    init();
  }
  DatatypesEnumerator(const DatatypesEnumerator& de)
      : TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
        d_tep(de.d_tep),
        d_datatype(de.d_datatype),
        d_type(de.d_type),
        d_ctor(de.d_ctor),
        d_zeroTerm(de.d_zeroTerm),
        d_zeroTermActive(de.d_zeroTermActive)
  {
    for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){
      d_te_index[it->first] = it->second;
    }
    for( std::map< TypeNode, std::vector< Node > >::const_iterator it = de.d_terms.begin(); it != de.d_terms.end(); ++it ){
      d_terms[it->first].insert( d_terms[it->first].end(), it->second.begin(), it->second.end() );
    }
    for( unsigned i=0; i<de.d_sel_types.size(); i++ ){
      d_sel_types.push_back( std::vector< TypeNode >() );
      d_sel_types[i].insert( d_sel_types[i].end(), de.d_sel_types[i].begin(), de.d_sel_types[i].end() );
    }
    for( unsigned i=0; i<de.d_sel_index.size(); i++ ){
      d_sel_index.push_back( std::vector< unsigned >() );
      d_sel_index[i].insert( d_sel_index[i].end(), de.d_sel_index[i].begin(), de.d_sel_index[i].end() );
    }

    d_children.insert( d_children.end(), de.d_children.begin(), de.d_children.end() );
    d_sel_sum.insert( d_sel_sum.end(), de.d_sel_sum.begin(), de.d_sel_sum.end() );
    d_size_limit = de.d_size_limit;
    d_has_debruijn = de.d_has_debruijn;
    d_child_enum = de.d_child_enum;
  }

  Node operator*() override
  {
    Debug("dt-enum-debug") << ": get term " << this << std::endl;
    if (d_zeroTermActive)
    {
      return d_zeroTerm;
    }
    else if (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
    {
      return getCurrentTerm( d_ctor );
    }
    throw NoMoreValuesException(getType());
  }

  DatatypesEnumerator& operator++() override;

  bool isFinished() override
  {
    return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors();
  }

};/* DatatypesEnumerator */

}  // namespace datatypes
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_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		* An enumerator for datatypes.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H
19		#define CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H
20
21		#include "expr/dtype.h"
22		#include "expr/kind.h"
23		#include "expr/type_node.h"
24		#include "expr/uninterpreted_constant.h"
25		#include "options/quantifiers_options.h"
26		#include "theory/type_enumerator.h"
27
28		namespace cvc5 {
29		namespace theory {
30		namespace datatypes {
31
32
33	176874	class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
34		/** type properties */
35		TypeEnumeratorProperties * d_tep;
36		/** The datatype we're enumerating */
37		const DType& d_datatype;
38		/** extra cons */
39		unsigned d_has_debruijn;
40		/** type */
41		TypeNode d_type;
42		/** The datatype constructor we're currently enumerating */
43		unsigned d_ctor;
44		/** The first term to consider in the enumeration */
45		Node d_zeroTerm;
46		/** Whether we are currently considering the above term */
47		bool d_zeroTermActive;
48		/** list of type enumerators (one for each type in a selector argument) */
49		std::map< TypeNode, unsigned > d_te_index;
50		std::vector< TypeEnumerator > d_children;
51		//std::vector< DatatypesEnumerator > d_dt_children;
52		/** terms produced for types */
53		std::map< TypeNode, std::vector< Node > > d_terms;
54		/** arg type of each selector, for each constructor */
55		std::vector< std::vector< TypeNode > > d_sel_types;
56		/** current index for each argument, for each constructor */
57		std::vector< std::vector< unsigned > > d_sel_index;
58		/** current sum of argument indicies for each constructor */
59		std::vector< int > d_sel_sum;
60		/** current bound on the number of times we can iterate argument enumerators */
61		unsigned d_size_limit;
62		/** child */
63		bool d_child_enum;
64
65	153	bool hasCyclesDt(const DType& dt)
66		{
67	459	return dt.isRecursiveSingleton(d_type)
68	612	\|\| dt.getCardinalityClass(d_type) == CardinalityClass::INFINITE;
69		}
70		bool hasCycles( TypeNode tn ){
71		if( tn.isDatatype() ){
72		const DType& dt = tn.getDType();
73		return hasCyclesDt( dt );
74		}else{
75		return false;
76		}
77		}
78
79		Node getTermEnum( TypeNode tn, unsigned i );
80
81		bool increment( unsigned index );
82
83		Node getCurrentTerm( unsigned index );
84
85		void init();
86
87		public:
88	82940	DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
89	82940	: TypeEnumeratorBase<DatatypesEnumerator>(type),
90		d_tep(tep),
91	82940	d_datatype(type.getDType()),
92		d_type(type),
93		d_ctor(0),
94	165880	d_zeroTermActive(false)
95		{
96	82940	d_child_enum = false;
97	82940	init();
98	82940	}
99	74	DatatypesEnumerator(TypeNode type,
100		bool childEnum,
101		TypeEnumeratorProperties* tep = nullptr)
102	74	: TypeEnumeratorBase<DatatypesEnumerator>(type),
103		d_tep(tep),
104	74	d_datatype(type.getDType()),
105		d_type(type),
106		d_ctor(0),
107	148	d_zeroTermActive(false)
108		{
109	74	d_child_enum = childEnum;
110	74	init();
111	74	}
112	5423	DatatypesEnumerator(const DatatypesEnumerator& de)
113	16269	: TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
114	5423	d_tep(de.d_tep),
115	5423	d_datatype(de.d_datatype),
116		d_type(de.d_type),
117	5423	d_ctor(de.d_ctor),
118		d_zeroTerm(de.d_zeroTerm),
119	32538	d_zeroTermActive(de.d_zeroTermActive)
120		{
121	5740	for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){
122	317	d_te_index[it->first] = it->second;
123		}
124	5740	for( std::map< TypeNode, std::vector< Node > >::const_iterator it = de.d_terms.begin(); it != de.d_terms.end(); ++it ){
125	317	d_terms[it->first].insert( d_terms[it->first].end(), it->second.begin(), it->second.end() );
126		}
127	30395	for( unsigned i=0; i<de.d_sel_types.size(); i++ ){
128	24972	d_sel_types.push_back( std::vector< TypeNode >() );
129	24972	d_sel_types[i].insert( d_sel_types[i].end(), de.d_sel_types[i].begin(), de.d_sel_types[i].end() );
130		}
131	30395	for( unsigned i=0; i<de.d_sel_index.size(); i++ ){
132	24972	d_sel_index.push_back( std::vector< unsigned >() );
133	24972	d_sel_index[i].insert( d_sel_index[i].end(), de.d_sel_index[i].begin(), de.d_sel_index[i].end() );
134		}
135
136	5423	d_children.insert( d_children.end(), de.d_children.begin(), de.d_children.end() );
137	5423	d_sel_sum.insert( d_sel_sum.end(), de.d_sel_sum.begin(), de.d_sel_sum.end() );
138	5423	d_size_limit = de.d_size_limit;
139	5423	d_has_debruijn = de.d_has_debruijn;
140	5423	d_child_enum = de.d_child_enum;
141	5423	}
142
143	212823	Node operator*() override
144		{
145	212823	Debug("dt-enum-debug") << ": get term " << this << std::endl;
146	212823	if (d_zeroTermActive)
147		{
148	167193	return d_zeroTerm;
149		}
150	45630	else if (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
151		{
152	44678	return getCurrentTerm( d_ctor );
153		}
154	952	throw NoMoreValuesException(getType());
155		}
156
157		DatatypesEnumerator& operator++() override;
158
159	312332	bool isFinished() override
160		{
161	312332	return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors();
162		}
163
164		};/* DatatypesEnumerator */
165
166		} // namespace datatypes
167		} // namespace theory
168		} // namespace cvc5
169
170		#endif /* CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H */