Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/type_enumerator.h	Lines:	51	55	92.7 %
Date:	2021-08-17	Branches:	41	164	25.0 %


/******************************************************************************
 * 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 */

// AJR: 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.
class TypeEnumeratorProperties
{
public:
  TypeEnumeratorProperties() : d_fixed_usort_card(false){}
  Integer getFixedCardinality( TypeNode tn ) { return d_fixed_card[tn]; }
  bool d_fixed_usort_card;
  std::map< TypeNode, Integer > d_fixed_card;
};

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	2065	class NoMoreValuesException : public Exception {
31		public:
32	2065	NoMoreValuesException(TypeNode n)
33	2065	: Exception("No more values for type `" + n.toString() + "'")
34		{
35	2065	}
36		};/* class NoMoreValuesException */
37
38	5843	class TypeEnumeratorInterface {
39		public:
40	109091	TypeEnumeratorInterface(TypeNode type) : d_type(type) {}
41
42	114934	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	26128	TypeNode getType() const { return d_type; }
62
63		private:
64		const TypeNode d_type;
65		}; /* class TypeEnumeratorInterface */
66
67		// AJR: This class stores particular information that is relevant to type enumeration.
68		// For finite model finding, we set d_fixed_usort=true,
69		// and store the finite cardinality bounds for each uninterpreted sort encountered in the model.
70	16514	class TypeEnumeratorProperties
71		{
72		public:
73	16514	TypeEnumeratorProperties() : d_fixed_usort_card(false){}
74		Integer getFixedCardinality( TypeNode tn ) { return d_fixed_card[tn]; }
75		bool d_fixed_usort_card;
76		std::map< TypeNode, Integer > d_fixed_card;
77		};
78
79		template <class T>
80	120777	class TypeEnumeratorBase : public TypeEnumeratorInterface {
81		public:
82
83	109091	TypeEnumeratorBase(TypeNode type) :
84	109091	TypeEnumeratorInterface(type) {
85	109091	}
86
87	13449	TypeEnumeratorInterface* clone() const override
88		{
89	13449	return new T(static_cast<const T&>(*this));
90		}
91
92		};/* class TypeEnumeratorBase */
93
94		/** Type enumerator class.
95		* Enumerates values for a type.
96		* Its constructor takes the type to enumerate and a pointer to a
97		* TypeEnumeratorProperties class, which this type enumerator does not own.
98		*/
99		class TypeEnumerator {
100		TypeEnumeratorInterface* d_te;
101
102		static TypeEnumeratorInterface* mkTypeEnumerator(
103		TypeNode type, TypeEnumeratorProperties* tep);
104
105		public:
106	101389	TypeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
107	101389	: d_te(mkTypeEnumerator(type, tep))
108		{
109	101389	}
110
111	13447	TypeEnumerator(const TypeEnumerator& te) :
112	13447	d_te(te.d_te->clone()) {
113	13447	}
114	74	TypeEnumerator(TypeEnumeratorInterface* te) : d_te(te){
115	74	}
116	2	TypeEnumerator& operator=(const TypeEnumerator& te) {
117	2	delete d_te;
118	2	d_te = te.d_te->clone();
119	2	return *this;
120		}
121
122	114910	~TypeEnumerator() { delete d_te; }
123	179082	bool isFinished()
124		{
125		// On Mac clang, there appears to be a code generation bug in an exception
126		// block here. For now, there doesn't appear a good workaround; just disable
127		// assertions on that setup.
128		#if defined(CVC5_ASSERTIONS) && !(defined(__clang__))
129	179082	if(d_te->isFinished()) {
130		try {
131	2029	**d_te;
132		Assert(false) << "expected an NoMoreValuesException to be thrown";
133	2029	} catch(NoMoreValuesException&) {
134		// ignore the exception, we're just asserting that it would be thrown
135		//
136		// This block can crash on clang 3.0 on Mac OS, perhaps related to
137		// bug: http://llvm.org/bugs/show_bug.cgi?id=13359
138		//
139		// Hence the #if !(defined(__APPLE__) && defined(__clang__)) above
140		}
141		} else {
142		try {
143	177053	**d_te;
144		} catch(NoMoreValuesException&) {
145		Assert(false) << "didn't expect a NoMoreValuesException to be thrown";
146		}
147		}
148		#endif /* CVC5_ASSERTIONS && !(APPLE \|\| clang) */
149	179082	return d_te->isFinished();
150		}
151	141536	Node operator*()
152		{
153		// On Mac clang, there appears to be a code generation bug in an exception
154		// block above (and perhaps here, too). For now, there doesn't appear a
155		// good workaround; just disable assertions on that setup.
156		#if defined(CVC5_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__))
157		try {
158	283054	Node n = **d_te;
159	141518	Assert(n.isConst()) << "Term " << n
160		<< " from type enumerator is not constant";
161	141518	Assert(!isFinished());
162	283036	return n;
163	36	} catch(NoMoreValuesException&) {
164	18	Assert(isFinished());
165	18	throw;
166		}
167		#else /* CVC5_ASSERTIONS && !(APPLE \|\| clang) */
168		return **d_te;
169		#endif /* CVC5_ASSERTIONS && !(APPLE \|\| clang) */
170		}
171	35445	TypeEnumerator& operator++()
172		{
173	35445	++*d_te;
174	35445	return *this;
175		}
176	2040	TypeEnumerator operator++(int)
177		{
178	2040	TypeEnumerator te = *this;
179	2040	++*d_te;
180	2040	return te;
181		}
182
183	2082	TypeNode getType() const { return d_te->getType(); }
184		};/* class TypeEnumerator */
185
186		} // namespace theory
187		} // namespace cvc5
188
189		#endif /* CVC5__THEORY__TYPE_ENUMERATOR_H */