1 /********************* */ 2 /*! \file type_enumerator.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Tim King, Andrew Reynolds 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 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.\endverbatim 11 ** 12 ** \brief Enumerators for types 13 ** 14 ** Enumerators for types. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__THEORY__TYPE_ENUMERATOR_H 20 #define __CVC4__THEORY__TYPE_ENUMERATOR_H 21 22 #include "base/exception.h" 23 #include "base/cvc4_assert.h" 24 #include "expr/node.h" 25 #include "expr/type_node.h" 26 27 namespace CVC4 { 28 namespace theory { 29 30 class NoMoreValuesException : public Exception { 31 public: NoMoreValuesException(TypeNode n)32 NoMoreValuesException(TypeNode n) 33 : Exception("No more values for type `" + n.toString() + "'") 34 { 35 } 36 };/* class NoMoreValuesException */ 37 38 class TypeEnumeratorInterface { 39 public: TypeEnumeratorInterface(TypeNode type)40 TypeEnumeratorInterface(TypeNode type) : d_type(type) {} 41 ~TypeEnumeratorInterface()42 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. */ getType()61 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 class TypeEnumeratorProperties 71 { 72 public: TypeEnumeratorProperties()73 TypeEnumeratorProperties() : d_fixed_usort_card(false){} getFixedCardinality(TypeNode tn)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 class TypeEnumeratorBase : public TypeEnumeratorInterface { 81 public: 82 TypeEnumeratorBase(TypeNode type)83 TypeEnumeratorBase(TypeNode type) : 84 TypeEnumeratorInterface(type) { 85 } 86 clone()87 TypeEnumeratorInterface* clone() const override 88 { 89 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 TypeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) d_te(mkTypeEnumerator (type,tep))107 : d_te(mkTypeEnumerator(type, tep)) 108 { 109 } 110 TypeEnumerator(const TypeEnumerator & te)111 TypeEnumerator(const TypeEnumerator& te) : 112 d_te(te.d_te->clone()) { 113 } TypeEnumerator(TypeEnumeratorInterface * te)114 TypeEnumerator(TypeEnumeratorInterface* te) : d_te(te){ 115 } 116 TypeEnumerator& operator=(const TypeEnumerator& te) { 117 delete d_te; 118 d_te = te.d_te->clone(); 119 return *this; 120 } 121 ~TypeEnumerator()122 ~TypeEnumerator() { delete d_te; } isFinished()123 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(CVC4_ASSERTIONS) && !(defined(__clang__)) 129 if(d_te->isFinished()) { 130 try { 131 **d_te; 132 Assert(false, "expected an NoMoreValuesException to be thrown"); 133 } 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 **d_te; 144 } catch(NoMoreValuesException&) { 145 Assert(false, "didn't expect a NoMoreValuesException to be thrown"); 146 } 147 } 148 #endif /* CVC4_ASSERTIONS && !(APPLE || clang) */ 149 return d_te->isFinished(); 150 } 151 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(CVC4_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__)) 157 try { 158 Node n = **d_te; 159 Assert(n.isConst()); 160 Assert(! isFinished()); 161 return n; catch(NoMoreValuesException &)162 } catch(NoMoreValuesException&) { 163 Assert(isFinished()); 164 throw; 165 } 166 #else /* CVC4_ASSERTIONS && !(APPLE || clang) */ 167 return **d_te; 168 #endif /* CVC4_ASSERTIONS && !(APPLE || clang) */ 169 } 170 TypeEnumerator& operator++() 171 { 172 ++*d_te; 173 return *this; 174 } 175 TypeEnumerator operator++(int) 176 { 177 TypeEnumerator te = *this; 178 ++*d_te; 179 return te; 180 } 181 getType()182 TypeNode getType() const { return d_te->getType(); } 183 };/* class TypeEnumerator */ 184 185 }/* CVC4::theory namespace */ 186 }/* CVC4 namespace */ 187 188 #endif /* __CVC4__THEORY__TYPE_ENUMERATOR_H */ 189