Searched refs:innerSort (Results 1 – 5 of 5) sorted by relevance
| /dports/math/vampire/vampire-4.5.1/Kernel/ |
| H A D | Sorts.hpp | 123 ArraySort(vstring name, unsigned indexSort, unsigned innerSort,unsigned id) : in ArraySort() argument
125 _indexSort(indexSort), _innerSort(innerSort) {} in ArraySort()
160 unsigned addArraySort(unsigned indexSort, unsigned innerSort);
|
| H A D | Sorts.cpp | 127 unsigned Sorts::addArraySort(const unsigned indexSort, const unsigned innerSort) in addArraySort() argument
134 name+=env.sorts->sortName(innerSort); in addArraySort()
144 ArraySort* sort = new ArraySort(name,indexSort,innerSort,result); in addArraySort()
|
| H A D | Theory.cpp | 1416 unsigned innerSort = info->getInnerSort(); in getArrayOperatorType() local
1420 return OperatorType::getFunctionType({ arraySort, indexSort }, innerSort); in getArrayOperatorType()
1426 return OperatorType::getFunctionType({ arraySort, indexSort, innerSort }, arraySort); in getArrayOperatorType()
|
| /dports/math/vampire/vampire-4.5.1/Parse/ |
| H A D | SMTLIB2.cpp | 669 unsigned innerSort = results.pop(); in declareSort() local
670 if (indexSort == SEPARATOR || innerSort == SEPARATOR) { in declareSort()
673 results.push(env.sorts->addArraySort(indexSort,innerSort)); in declareSort()
|
| H A D | TPTP.cpp | 1547 unsigned innerSort = env.sorts->getArraySort(arraySort)->getInnerSort(); in endTheoryFunction() local
1548 if (sortOf(value) != innerSort) { in endTheoryFunction()
3652 unsigned innerSort = readSort(); in readSort() local
3653 sort = env.sorts->addArraySort(indexSort, innerSort); in readSort()
|