Home
last modified time | relevance | path

Searched refs:getArrayConstituentType (Results 1 – 10 of 10) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/arrays/
H A Dtheory_arrays_type_rules.h43 return arrayType.getArrayConstituentType(); in computeType()
61 if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ in computeType()
62 Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl; in computeType()
H A Dtype_enumerator.h47 d_constituentType(type.getArrayConstituentType()),
H A Dtheory_arrays.cpp1186 defaultValuesSet.add(nrep.getType().getArrayConstituentType(), (*it).second); in collectModelInfo()
1202 TypeNode valueType = nrep.getType().getArrayConstituentType(); in collectModelInfo()
/dports/math/cvc4/CVC4-1.7/src/theory/builtin/
H A Dtheory_builtin_rewriter.cpp127 atn = atn.getArrayConstituentType(); in getFunctionTypeForArrayType()
294 Assert( curr.getType().isSubtypeOf( array_type.getArrayConstituentType() ) ); in getArrayRepresentationForLambdaRec()
/dports/math/cvc4/CVC4-1.7/src/expr/
H A Dtype_node.h507 TypeNode getArrayConstituentType() const;
894 inline TypeNode TypeNode::getArrayConstituentType() const { in getArrayConstituentType() function
H A Dtype_node.cpp105 TypeNode tnc = getArrayConstituentType(); in isInterpretedFinite()
H A Dtype.cpp522 return makeType(d_typeNode->getArrayConstituentType()); in getConstituentType()
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory_model_builder.cpp193 || involvesUSort(tn.getArrayConstituentType()); in involvesUSort()
259 addToTypeList(tn.getArrayConstituentType(), type_list, visiting); in addToTypeList()
/dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/
H A Dunconstrained_simplifier.cpp601 current.getType().getArrayConstituentType(), currentSub); in processUnconstrained()
/dports/math/cvc4/CVC4-1.7/src/printer/smt2/
H A Dsmt2_printer.cpp899 TypeNode elemType = n[0].getType().getArrayConstituentType(); in toStream()
904 …TypeNode elemType = TypeNode::leastCommonTypeNode( n[0].getType().getArrayConstituentType(), n[2].… in toStream()