Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/type_enumerator.h	Lines:	54	58	93.1 %
Date:	2021-11-07	Branches:	37	156	23.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Tim King, Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Enumerators for types.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__TYPE_ENUMERATOR_H
#define CVC5__THEORY__TYPE_ENUMERATOR_H

#include "base/check.h"
#include "base/exception.h"
#include "expr/node.h"
#include "expr/type_node.h"
#include "util/integer.h"

namespace cvc5 {
namespace theory {

class NoMoreValuesException : public Exception {
 public:
  NoMoreValuesException(TypeNode n)
      : Exception("No more values for type `" + n.toString() + "'")
  {
  }
};/* class NoMoreValuesException */

class TypeEnumeratorInterface {
 public:
  TypeEnumeratorInterface(TypeNode type) : d_type(type) {}

  virtual ~TypeEnumeratorInterface() {}

  /** Is this enumerator out of constants to enumerate? */
  virtual bool isFinished() = 0;

  /**
   * Get the current constant of this type.
   *
   * @throws NoMoreValuesException if no such constant exists.
   */
  virtual Node operator*() = 0;

  /** Increment the pointer to the next available constant. */
  virtual TypeEnumeratorInterface& operator++() = 0;

  /** Clone this enumerator. */
  virtual TypeEnumeratorInterface* clone() const = 0;

  /** Get the type from which we're enumerating constants. */
  TypeNode getType() const { return d_type; }

 private:
  const TypeNode d_type;
}; /* class TypeEnumeratorInterface */

/**
 * This class stores particular information that is relevant to type
 * enumeration. For finite model finding, we set d_fixed_usort=true, and store
 * the finite cardinality bounds for each uninterpreted sort encountered in the
 * model. For strings, we store the cardinality for the alphabet that we are
 * assuming.
 */
class TypeEnumeratorProperties
{
public:
 TypeEnumeratorProperties(bool fixUSortCard, uint32_t strAlphaCard)
     : d_fixed_usort_card(fixUSortCard), d_stringAlphaCard(strAlphaCard)
 {
 }
 Integer getFixedCardinality(TypeNode tn) { return d_fixed_card[tn]; }
 bool d_fixed_usort_card;
 std::map<TypeNode, Integer> d_fixed_card;
 /** Get the alphabet for strings */
 uint32_t getStringsAlphabetCard() const { return d_stringAlphaCard; }

private:
 /** The cardinality of the alphabet */
 uint32_t d_stringAlphaCard;
};

template <class T>
class TypeEnumeratorBase : public TypeEnumeratorInterface {
public:

  TypeEnumeratorBase(TypeNode type) :
    TypeEnumeratorInterface(type) {
  }

  TypeEnumeratorInterface* clone() const override
  {
    return new T(static_cast<const T&>(*this));
  }

};/* class TypeEnumeratorBase */

/** Type enumerator class.
 * Enumerates values for a type.
 * Its constructor takes the type to enumerate and a pointer to a
 * TypeEnumeratorProperties class, which this type enumerator does not own.
 */
class TypeEnumerator {
  TypeEnumeratorInterface* d_te;

  static TypeEnumeratorInterface* mkTypeEnumerator(
      TypeNode type, TypeEnumeratorProperties* tep);

 public:
  TypeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
      : d_te(mkTypeEnumerator(type, tep))
  {
  }

  TypeEnumerator(const TypeEnumerator& te) :
    d_te(te.d_te->clone()) {
  }
  TypeEnumerator(TypeEnumeratorInterface* te) : d_te(te){
  }
  TypeEnumerator& operator=(const TypeEnumerator& te) {
    delete d_te;
    d_te = te.d_te->clone();
    return *this;
  }

  ~TypeEnumerator() { delete d_te; }
  bool isFinished()
  {
// On Mac clang, there appears to be a code generation bug in an exception
// block here.  For now, there doesn't appear a good workaround; just disable
// assertions on that setup.
#if defined(CVC5_ASSERTIONS) && !(defined(__clang__))
    if(d_te->isFinished()) {
      try {
        **d_te;
        Assert(false) << "expected an NoMoreValuesException to be thrown";
      } catch(NoMoreValuesException&) {
        // ignore the exception, we're just asserting that it would be thrown
        //
        // This block can crash on clang 3.0 on Mac OS, perhaps related to
        // bug:  http://llvm.org/bugs/show_bug.cgi?id=13359
        //
        // Hence the #if !(defined(__APPLE__) && defined(__clang__)) above
      }
    } else {
      try {
        **d_te;
      } catch(NoMoreValuesException&) {
        Assert(false) << "didn't expect a NoMoreValuesException to be thrown";
      }
    }
#endif /* CVC5_ASSERTIONS && !(APPLE || clang) */
    return d_te->isFinished();
  }
  Node operator*()
  {
// On Mac clang, there appears to be a code generation bug in an exception
// block above (and perhaps here, too).  For now, there doesn't appear a
// good workaround; just disable assertions on that setup.
#if defined(CVC5_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__))
    try {
      Node n = **d_te;
      Assert(n.isConst()) << "Term " << n
                          << " from type enumerator is not constant";
      Assert(!isFinished());
      return n;
    } catch(NoMoreValuesException&) {
      Assert(isFinished());
      throw;
    }
#else  /* CVC5_ASSERTIONS && !(APPLE || clang) */
    return **d_te;
#endif /* CVC5_ASSERTIONS && !(APPLE || clang) */
  }
  TypeEnumerator& operator++()
  {
    ++*d_te;
    return *this;
  }
  TypeEnumerator operator++(int)
  {
    TypeEnumerator te = *this;
    ++*d_te;
    return te;
  }

  TypeNode getType() const { return d_te->getType(); }
};/* class TypeEnumerator */

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__TYPE_ENUMERATOR_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Tim King, Andrew Reynolds
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		* Enumerators for types.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__TYPE_ENUMERATOR_H
19		#define CVC5__THEORY__TYPE_ENUMERATOR_H
20
21		#include "base/check.h"
22		#include "base/exception.h"
23		#include "expr/node.h"
24		#include "expr/type_node.h"
25		#include "util/integer.h"
26
27		namespace cvc5 {
28		namespace theory {
29
30	3183	class NoMoreValuesException : public Exception {
31		public:
32	3183	NoMoreValuesException(TypeNode n)
33	3183	: Exception("No more values for type `" + n.toString() + "'")
34		{
35	3183	}
36		};/* class NoMoreValuesException */
37
38	5903	class TypeEnumeratorInterface {
39		public:
40	224863	TypeEnumeratorInterface(TypeNode type) : d_type(type) {}
41
42	230766	virtual ~TypeEnumeratorInterface() {}
43
44		/** Is this enumerator out of constants to enumerate? */
45		virtual bool isFinished() = 0;
46
47		/**
48		* Get the current constant of this type.
49		*
50		* @throws NoMoreValuesException if no such constant exists.
51		*/
52		virtual Node operator*() = 0;
53
54		/** Increment the pointer to the next available constant. */
55		virtual TypeEnumeratorInterface& operator++() = 0;
56
57		/** Clone this enumerator. */
58		virtual TypeEnumeratorInterface* clone() const = 0;
59
60		/** Get the type from which we're enumerating constants. */
61	27658	TypeNode getType() const { return d_type; }
62
63		private:
64		const TypeNode d_type;
65		}; /* class TypeEnumeratorInterface */
66
67		/**
68		* This class stores particular information that is relevant to type
69		* enumeration. For finite model finding, we set d_fixed_usort=true, and store
70		* the finite cardinality bounds for each uninterpreted sort encountered in the
71		* model. For strings, we store the cardinality for the alphabet that we are
72		* assuming.
73		*/
74	24989	class TypeEnumeratorProperties
75		{
76		public:
77	24989	TypeEnumeratorProperties(bool fixUSortCard, uint32_t strAlphaCard)
78	24989	: d_fixed_usort_card(fixUSortCard), d_stringAlphaCard(strAlphaCard)
79		{
80	24989	}
81		Integer getFixedCardinality(TypeNode tn) { return d_fixed_card[tn]; }
82		bool d_fixed_usort_card;
83		std::map<TypeNode, Integer> d_fixed_card;
84		/** Get the alphabet for strings */
85	74	uint32_t getStringsAlphabetCard() const { return d_stringAlphaCard; }
86
87		private:
88		/** The cardinality of the alphabet */
89		uint32_t d_stringAlphaCard;
90		};
91
92		template <class T>
93	236669	class TypeEnumeratorBase : public TypeEnumeratorInterface {
94		public:
95
96	224863	TypeEnumeratorBase(TypeNode type) :
97	224863	TypeEnumeratorInterface(type) {
98	224863	}
99
100	13585	TypeEnumeratorInterface* clone() const override
101		{
102	13585	return new T(static_cast<const T&>(*this));
103		}
104
105		};/* class TypeEnumeratorBase */
106
107		/** Type enumerator class.
108		* Enumerates values for a type.
109		* Its constructor takes the type to enumerate and a pointer to a
110		* TypeEnumeratorProperties class, which this type enumerator does not own.
111		*/
112		class TypeEnumerator {
113		TypeEnumeratorInterface* d_te;
114
115		static TypeEnumeratorInterface* mkTypeEnumerator(
116		TypeNode type, TypeEnumeratorProperties* tep);
117
118		public:
119	217079	TypeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
120	217079	: d_te(mkTypeEnumerator(type, tep))
121		{
122	217079	}
123
124	13583	TypeEnumerator(const TypeEnumerator& te) :
125	13583	d_te(te.d_te->clone()) {
126	13583	}
127	78	TypeEnumerator(TypeEnumeratorInterface* te) : d_te(te){
128	78	}
129	2	TypeEnumerator& operator=(const TypeEnumerator& te) {
130	2	delete d_te;
131	2	d_te = te.d_te->clone();
132	2	return *this;
133		}
134
135	230740	~TypeEnumerator() { delete d_te; }
136	294323	bool isFinished()
137		{
138		// On Mac clang, there appears to be a code generation bug in an exception
139		// block here. For now, there doesn't appear a good workaround; just disable
140		// assertions on that setup.
141		#if defined(CVC5_ASSERTIONS) && !(defined(__clang__))
142	294323	if(d_te->isFinished()) {
143		try {
144	3147	**d_te;
145		Assert(false) << "expected an NoMoreValuesException to be thrown";
146	3147	} catch(NoMoreValuesException&) {
147		// ignore the exception, we're just asserting that it would be thrown
148		//
149		// This block can crash on clang 3.0 on Mac OS, perhaps related to
150		// bug: http://llvm.org/bugs/show_bug.cgi?id=13359
151		//
152		// Hence the #if !(defined(__APPLE__) && defined(__clang__)) above
153		}
154		} else {
155		try {
156	291176	**d_te;
157		} catch(NoMoreValuesException&) {
158		Assert(false) << "didn't expect a NoMoreValuesException to be thrown";
159		}
160		}
161		#endif /* CVC5_ASSERTIONS && !(APPLE \|\| clang) */
162	294323	return d_te->isFinished();
163		}
164	256522	Node operator*()
165		{
166		// On Mac clang, there appears to be a code generation bug in an exception
167		// block above (and perhaps here, too). For now, there doesn't appear a
168		// good workaround; just disable assertions on that setup.
169		#if defined(CVC5_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__))
170		try {
171	513026	Node n = **d_te;
172	256504	Assert(n.isConst()) << "Term " << n
173		<< " from type enumerator is not constant";
174	256504	Assert(!isFinished());
175	513008	return n;
176	36	} catch(NoMoreValuesException&) {
177	18	Assert(isFinished());
178	18	throw;
179		}
180		#else /* CVC5_ASSERTIONS && !(APPLE \|\| clang) */
181		return **d_te;
182		#endif /* CVC5_ASSERTIONS && !(APPLE \|\| clang) */
183		}
184	35668	TypeEnumerator& operator++()
185		{
186	35668	++*d_te;
187	35668	return *this;
188		}
189	2040	TypeEnumerator operator++(int)
190		{
191	2040	TypeEnumerator te = *this;
192	2040	++*d_te;
193	2040	return te;
194		}
195
196	2082	TypeNode getType() const { return d_te->getType(); }
197		};/* class TypeEnumerator */
198
199		} // namespace theory
200		} // namespace cvc5
201
202		#endif /* CVC5__THEORY__TYPE_ENUMERATOR_H */