Home
last modified time | relevance | path

Searched refs:ARRAY_SELECT (Results 1 – 12 of 12) sorted by relevance

/dports/math/py-pysmt/pysmt-0.9.0/pysmt/
H A Doperators.py74 ARRAY_SELECT, # Array Select (59)
115 ARRAY_OPERATORS = frozenset([ARRAY_SELECT, ARRAY_STORE, ARRAY_VALUE])
220 ARRAY_SELECT : "ARRAY_SELECT",
H A Dfnode.py46 ARRAY_SELECT, ARRAY_STORE, ARRAY_VALUE,
465 return self.node_type() == ARRAY_SELECT
H A Doracles.py181 @walkers.handles(op.ITE, op.ARRAY_SELECT, op.ARRAY_STORE, op.MINUS)
H A Dformula.py1024 return self.create_node(node_type=op.ARRAY_SELECT, args=(arr, idx))
/dports/math/vampire/vampire-4.5.1/Inferences/
H A DArrayTheoryISE.cpp66 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 DTheory.cpp739 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 DTheory.hpp346 ARRAY_SELECT, enumerator
/dports/math/vampire/vampire-4.5.1/Shell/
H A DTheoryAxioms.cpp791 …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 DSMTLIB.cpp800 Theory::StructuredSortInterpretation::ARRAY_SELECT); in getTermSelectOrStoreFn()
805 Theory::StructuredSortInterpretation::ARRAY_SELECT); in getTermSelectOrStoreFn()
H A DSMTLIB2.cpp1949 OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_SELECT); in parseAsBuiltinTermSymbol()
1950 unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,funType); in parseAsBuiltinTermSymbol()
H A DTPTP.cpp1528 itp = Theory::Interpretation::ARRAY_SELECT; in endTheoryFunction()
/dports/math/vampire/vampire-4.5.1/SAT/
H A DZ3Interfacing.cpp451 case Theory::ARRAY_SELECT: in getz3expr()