Function DeclareSort

lean_py/z3/core.py:234–235 · view source on GitHub ↗

(name: str)

Source from the content-addressed store, hash-verified

232
233
234	def DeclareSort(name: str) -> UninterpretedSortRef:
235	return UninterpretedSortRef(UninterpASTSort(name))
236
237
238	class BitVecSortRef(SortRef):

resolve_sortMethod · 0.90

process_commandMethod · 0.90

test_socrates_syllogismMethod · 0.90

test_uninterpreted_sort_varsMethod · 0.90

test_consts_uninterpretedMethod · 0.90

test_uninterp_sort_nameMethod · 0.90

test_sort_kind_uninterpretedMethod · 0.90

test_function_declMethod · 0.90

test_uninterpreted_sort_trackedMethod · 0.90

test_socratesMethod · 0.90

test_uninterpreted_sort_fieldMethod · 0.90

test_uninterp_sort_field_disjointnessMethod · 0.90

UninterpASTSortClass · 0.90

UninterpretedSortRefClass · 0.85

test_socrates_syllogismMethod · 0.72

test_uninterpreted_sort_varsMethod · 0.72

test_consts_uninterpretedMethod · 0.72

test_uninterp_sort_nameMethod · 0.72

test_sort_kind_uninterpretedMethod · 0.72

test_function_declMethod · 0.72

test_uninterpreted_sort_trackedMethod · 0.72

test_socratesMethod · 0.72

test_uninterpreted_sort_fieldMethod · 0.72

test_uninterp_sort_field_disjointnessMethod · 0.72

test_congruenceMethod · 0.72

test_congruence_binaryMethod · 0.72