Head

GCC Code Coverage Report

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