Searched refs:ARRAY_SELECT (Results 1 – 12 of 12) sorted by relevance
/dports/math/py-pysmt/pysmt-0.9.0/pysmt/ |
H A D | operators.py | 74 ARRAY_SELECT, # Array Select (59) 115 ARRAY_OPERATORS = frozenset([ARRAY_SELECT, ARRAY_STORE, ARRAY_VALUE]) 220 ARRAY_SELECT : "ARRAY_SELECT",
|
H A D | fnode.py | 46 ARRAY_SELECT, ARRAY_STORE, ARRAY_VALUE, 465 return self.node_type() == ARRAY_SELECT
|
H A D | oracles.py | 181 @walkers.handles(op.ITE, op.ARRAY_SELECT, op.ARRAY_STORE, op.MINUS)
|
H A D | formula.py | 1024 return self.create_node(node_type=op.ARRAY_SELECT, args=(arr, idx))
|
/dports/math/vampire/vampire-4.5.1/Inferences/ |
H A D | ArrayTheoryISE.cpp | 66 case StructuredStoreInterpretation::ARRAY_SELECT : in transformSubterm() 110 theory->convertToStructured(valueInterp)==StructuredSortInterpretation::ARRAY_SELECT)) in transformSubterm() 138 …ect = theory->getSymbolForStructuredSort(sort, Theory::StructuredSortInterpretation::ARRAY_SELECT); in transformSubterm()
|
/dports/math/vampire/vampire-4.5.1/Kernel/ |
H A D | Theory.cpp | 739 case ARRAY_SELECT: in getArity() 823 case ARRAY_SELECT: in isFunction() 913 case ARRAY_SELECT: in hasSingleSort() 933 case ARRAY_SELECT: in isPolymorphic() 1400 case ARRAY_SELECT: in getInterpretationName() 1419 case Interpretation::ARRAY_SELECT: in getArrayOperatorType()
|
H A D | Theory.hpp | 346 ARRAY_SELECT, enumerator
|
/dports/math/vampire/vampire-4.5.1/Shell/ |
H A D | TheoryAxioms.cpp | 791 …ignature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory… in addArrayExtensionalityAxioms() 849 …ignature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory… in addArrayWriteAxioms() 1102 Interpretation arraySelect = isBool ? Theory::ARRAY_BOOL_SELECT : Theory::ARRAY_SELECT; in apply()
|
/dports/math/vampire/vampire-4.5.1/Parse/ |
H A D | SMTLIB.cpp | 800 Theory::StructuredSortInterpretation::ARRAY_SELECT); in getTermSelectOrStoreFn() 805 Theory::StructuredSortInterpretation::ARRAY_SELECT); in getTermSelectOrStoreFn()
|
H A D | SMTLIB2.cpp | 1949 OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_SELECT); in parseAsBuiltinTermSymbol() 1950 unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,funType); in parseAsBuiltinTermSymbol()
|
H A D | TPTP.cpp | 1528 itp = Theory::Interpretation::ARRAY_SELECT; in endTheoryFunction()
|
/dports/math/vampire/vampire-4.5.1/SAT/ |
H A D | Z3Interfacing.cpp | 451 case Theory::ARRAY_SELECT: in getz3expr()
|