Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/type_enumerator.h	Lines:	51	55	92.7 %
Date:	2021-05-22	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"

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