1 2 /* 3 * File Sorts.hpp. 4 * 5 * This file is part of the source code of the software program 6 * Vampire. It is protected by applicable 7 * copyright laws. 8 * 9 * This source code is distributed under the licence found here 10 * https://vprover.github.io/license.html 11 * and in the source directory 12 * 13 * In summary, you are allowed to use Vampire for non-commercial 14 * purposes but not allowed to distribute, modify, copy, create derivatives, 15 * or use in competitions. 16 * For other uses of Vampire please contact developers for a different 17 * licence, which we will make an effort to provide. 18 */ 19 /** 20 * @file Sorts.hpp 21 * Defines class Sorts. 22 */ 23 24 #ifndef __Sorts__ 25 #define __Sorts__ 26 27 #include "Forwards.hpp" 28 29 #include "Lib/DArray.hpp" 30 #include "Lib/Map.hpp" 31 #include "Lib/Stack.hpp" 32 #include "Lib/Vector.hpp" 33 #include "Lib/Allocator.hpp" 34 #include "Lib/VString.hpp" 35 36 namespace Kernel { 37 38 class Sorts { 39 public: 40 CLASS_NAME(Sorts); 41 USE_ALLOCATOR(Sorts); 42 43 /** Various pre-defined sort */ 44 // Note that this is not closed, these will be treated as unsigned ints within the code 45 enum DefaultSorts { 46 /** The default sort of all individuals, always in the non-sorted case */ 47 SRT_DEFAULT = 0, 48 /** Boolean sort */ 49 SRT_BOOL = 1, 50 /** sort of integers */ 51 SRT_INTEGER = 2, 52 /** sort of rationals */ 53 SRT_RATIONAL = 3, 54 /** sort of reals */ 55 SRT_REAL = 4, 56 /** this is not a sort, it is just used to denote the first index of a user-define sort */ 57 FIRST_USER_SORT = 5 58 }; 59 60 /** Various structured sorts */ 61 enum class StructuredSort { 62 /** The structured sort for arrays **/ 63 ARRAY, 64 /** The structured sort for tuples */ 65 TUPLE, 66 /** not a real structured sort, it's here to denote the length of the StructuredSort enum */ 67 LAST_STRUCTURED_SORT 68 }; 69 70 Sorts(); 71 ~Sorts(); 72 73 class SortInfo 74 { 75 public: 76 CLASS_NAME(SortInfo); 77 USE_ALLOCATOR(SortInfo); 78 79 SortInfo(const vstring& name,const unsigned id, bool interpreted = false); ~SortInfo()80 virtual ~SortInfo() {} 81 name() const82 const vstring& name() const { return _name; } id() const83 const unsigned id() const { return _id; } 84 isOfStructuredSort(StructuredSort sort)85 virtual bool isOfStructuredSort(StructuredSort sort) { return false; } 86 87 protected: 88 vstring _name; 89 unsigned _id; 90 }; 91 92 /** 93 * 94 * @author Giles 95 */ 96 class StructuredSortInfo : public SortInfo 97 { 98 public: 99 CLASS_NAME(StructuredSortInfo); 100 USE_ALLOCATOR(StructuredSortInfo); 101 StructuredSortInfo(vstring name,StructuredSort sort,unsigned id)102 StructuredSortInfo(vstring name, StructuredSort sort,unsigned id): 103 SortInfo(name,id), _sort(sort) { (void)_sort; /*to suppress warning about unused*/ } 104 isOfStructuredSort(StructuredSort sort)105 bool isOfStructuredSort(StructuredSort sort) override { 106 return sort==_sort; 107 } 108 109 private: 110 StructuredSort _sort; 111 }; 112 113 /** 114 * 115 * @author Giles 116 */ 117 class ArraySort : public StructuredSortInfo 118 { 119 public: 120 CLASS_NAME(ArraySort); 121 USE_ALLOCATOR(ArraySort); 122 ArraySort(vstring name,unsigned indexSort,unsigned innerSort,unsigned id)123 ArraySort(vstring name, unsigned indexSort, unsigned innerSort,unsigned id) : 124 StructuredSortInfo(name,StructuredSort::ARRAY, id), 125 _indexSort(indexSort), _innerSort(innerSort) {} 126 getIndexSort()127 unsigned getIndexSort(){ return _indexSort; } getInnerSort()128 unsigned getInnerSort(){ return _innerSort; } 129 130 private: 131 // the SortInfo can be found using Sorts 132 unsigned _indexSort; 133 unsigned _innerSort; 134 }; 135 136 class TupleSort : public StructuredSortInfo 137 { 138 public: 139 CLASS_NAME(TupleSort); 140 USE_ALLOCATOR(TupleSort); 141 TupleSort(vstring name,unsigned id,unsigned arity,unsigned sorts[])142 TupleSort(vstring name, unsigned id, unsigned arity, unsigned sorts[]) 143 : StructuredSortInfo(name, StructuredSort::TUPLE, id), _sorts(arity) { 144 for (unsigned i = 0; i < arity; i++) { 145 _sorts[i] = sorts[i]; 146 } 147 } 148 arity() const149 unsigned arity() const { return (unsigned)_sorts.size(); } sorts()150 unsigned* sorts() { return _sorts.array(); } argument(unsigned index) const151 unsigned argument(unsigned index) const { ASS_G(arity(), index); return _sorts[index]; } 152 153 private: 154 DArray<unsigned> _sorts; 155 }; 156 157 unsigned addSort(const vstring& name, bool& added, bool interpreted); 158 unsigned addSort(const vstring& name, bool interpreted); 159 160 unsigned addArraySort(unsigned indexSort, unsigned innerSort); getArraySort(unsigned sort)161 ArraySort* getArraySort(unsigned sort){ 162 ASS(isOfStructuredSort(sort,StructuredSort::ARRAY)); 163 return static_cast<ArraySort*>(_sorts[sort]); 164 } 165 166 unsigned addTupleSort(unsigned arity, unsigned sorts[]); getTupleSort(unsigned sort)167 TupleSort* getTupleSort(unsigned sort) { 168 ASS(isOfStructuredSort(sort,StructuredSort::TUPLE)); 169 return static_cast<TupleSort*>(_sorts[sort]); 170 } 171 172 bool haveSort(const vstring& name); 173 bool findSort(const vstring& name, unsigned& idx); 174 175 VirtualIterator<unsigned> getStructuredSorts(const StructuredSort ss); 176 isStructuredSort(unsigned sort)177 bool isStructuredSort(unsigned sort) { 178 if(sort > _sorts.size()) return false; 179 SortInfo* si = _sorts[sort]; 180 for (unsigned ss = 0; ss < (unsigned)StructuredSort::LAST_STRUCTURED_SORT; ss++) { 181 if (si->isOfStructuredSort(static_cast<StructuredSort>(ss))) { 182 return true; 183 } 184 } 185 return false; 186 } 187 isOfStructuredSort(unsigned sort,StructuredSort structured)188 bool isOfStructuredSort(unsigned sort, StructuredSort structured){ 189 if(sort > _sorts.size()) return false; 190 return _sorts[sort]->isOfStructuredSort(structured); 191 } 192 193 const vstring& sortName(unsigned idx) const; 194 195 /** 196 * Return the number of sorts 197 */ count() const198 unsigned count() const { return _sorts.length(); } 199 /** true if there is a sort different from built-ins */ hasSort() const200 bool hasSort() const {return _hasSort;} 201 202 private: 203 SymbolMap _sortNames; 204 Stack<SortInfo*> _sorts; 205 /** true if there is a sort different from built-ins */ 206 bool _hasSort; 207 }; 208 209 /** 210 * The OperatorType class represents the predicate and function types (which are not sorts in first-order logic). 211 * These are determined by their kind (either PREDICATE or FUNCTION), arity, a corresponding list of argument sorts, 212 * and a return sort in the case of functions. 213 * 214 * The class stores all this data in one Vector<unsigned>*, of length arity+1, 215 * where the last element is the return sort for functions and "MAX_UNSIGNED" for predicates (which distinguishes the two kinds). 216 * 217 * The objects of this class are perfectly shared (so that equal predicate / function types correspond to equal pointers) 218 * and are obtained via static methods (to guarantee the sharing). 219 */ 220 class OperatorType 221 { 222 public: 223 CLASS_NAME(OperatorType); 224 USE_ALLOCATOR(OperatorType); 225 226 private: 227 typedef Vector<unsigned> OperatorKey; // Vector of argument sorts together with "FFFF" appended for predicates and resultSort appended for functions 228 OperatorKey* _key; 229 230 // constructors kept private OperatorType(OperatorKey * key)231 OperatorType(OperatorKey* key) : _key(key) {} 232 233 /** 234 * Convenience functions for creating a key 235 */ 236 static OperatorKey* setupKey(unsigned arity, const unsigned* sorts=0); 237 static OperatorKey* setupKey(std::initializer_list<unsigned> sorts); 238 static OperatorKey* setupKeyUniformRange(unsigned arity, unsigned argsSort); 239 240 typedef Map<OperatorKey*,OperatorType*,PointerDereferencingHash> OperatorTypes; 241 static OperatorTypes& operatorTypes(); // just a wrapper around a static OperatorTypes object, to ensure a correct initialization order 242 243 static OperatorType* getTypeFromKey(OperatorKey* key); 244 245 static const unsigned PREDICATE_FLAG = std::numeric_limits<unsigned>::max(); 246 247 public: ~OperatorType()248 ~OperatorType() { _key->deallocate(); } 249 getPredicateType(unsigned arity,const unsigned * sorts=0)250 static OperatorType* getPredicateType(unsigned arity, const unsigned* sorts=0) { 251 CALL("OperatorType::getPredicateType(unsigned,const unsigned*)"); 252 253 OperatorKey* key = setupKey(arity,sorts); 254 (*key)[arity] = PREDICATE_FLAG; 255 return getTypeFromKey(key); 256 } 257 getPredicateType(std::initializer_list<unsigned> sorts)258 static OperatorType* getPredicateType(std::initializer_list<unsigned> sorts) { 259 CALL("OperatorType::getPredicateType(std::initializer_list<unsigned>)"); 260 261 OperatorKey* key = setupKey(sorts); 262 (*key)[sorts.size()] = PREDICATE_FLAG; 263 return getTypeFromKey(key); 264 } 265 getPredicateTypeUniformRange(unsigned arity,unsigned argsSort)266 static OperatorType* getPredicateTypeUniformRange(unsigned arity, unsigned argsSort) { 267 CALL("OperatorType::getPredicateTypeUniformRange"); 268 269 OperatorKey* key = setupKeyUniformRange(arity,argsSort); 270 (*key)[arity] = PREDICATE_FLAG; 271 return getTypeFromKey(key); 272 } 273 getFunctionType(unsigned arity,const unsigned * sorts,unsigned resultSort)274 static OperatorType* getFunctionType(unsigned arity, const unsigned* sorts, unsigned resultSort) { 275 CALL("OperatorType::getFunctionType"); 276 277 OperatorKey* key = setupKey(arity,sorts); 278 (*key)[arity] = resultSort; 279 return getTypeFromKey(key); 280 } 281 getFunctionType(std::initializer_list<unsigned> sorts,unsigned resultSort)282 static OperatorType* getFunctionType(std::initializer_list<unsigned> sorts, unsigned resultSort) { 283 CALL("OperatorType::getFunctionType(std::initializer_list<unsigned>)"); 284 285 OperatorKey* key = setupKey(sorts); 286 (*key)[sorts.size()] = resultSort; 287 return getTypeFromKey(key); 288 } 289 getFunctionTypeTypeUniformRange(unsigned arity,unsigned argsSort,unsigned resultSort)290 static OperatorType* getFunctionTypeTypeUniformRange(unsigned arity, unsigned argsSort, unsigned resultSort) { 291 CALL("OperatorType::getFunctionTypeTypeUniformRange"); 292 293 OperatorKey* key = setupKeyUniformRange(arity,argsSort); 294 (*key)[arity] = resultSort; 295 return getTypeFromKey(key); 296 } 297 298 /** 299 * Convenience function for creating OperatorType for constants (as symbols). 300 * Constants are function symbols of 0 arity, so just provide the result sort. 301 */ getConstantsType(unsigned resultSort)302 static OperatorType* getConstantsType(unsigned resultSort) { return getFunctionType(0,nullptr,resultSort); } 303 arity() const304 unsigned arity() const { return _key->length()-1; } 305 arg(unsigned idx) const306 unsigned arg(unsigned idx) const 307 { 308 CALL("OperatorType::arg"); 309 return (*_key)[idx]; 310 } 311 isPredicateType() const312 bool isPredicateType() const { return (*_key)[arity()] == PREDICATE_FLAG; }; isFunctionType() const313 bool isFunctionType() const { return (*_key)[arity()] != PREDICATE_FLAG; }; result() const314 unsigned result() const { 315 CALL("OperatorType::result"); 316 ASS(isFunctionType()); 317 return (*_key)[arity()]; 318 } 319 320 vstring toString() const; 321 322 bool isSingleSortType(unsigned sort) const; isAllDefault() const323 bool isAllDefault() const { return isSingleSortType(Sorts::SRT_DEFAULT); } 324 325 private: 326 vstring argsToString() const; 327 }; 328 329 } 330 331 #endif // __Sorts__ 332