View Source cure_pattern_encoder (cure v0.7.0)

Summary

Functions

check_exhaustiveness(Patterns, Type)

Check if patterns are exhaustive Returns {complete} or {incomplete, [MissingPatterns]}

encode_pattern(Pattern, Type)

Encode a single pattern as an SMT constraint Returns an SMT-LIB expression that is true when value matches pattern

encode_patterns_disjunction(Patterns, Type)

Encode multiple patterns as a disjunction (OR) Returns constraint that is true if ANY pattern matches

find_missing_pattern(CoveredPatterns, Type)

Find a missing pattern using SMT Returns {ok, Pattern} if a missing pattern is found, or exhaustive if complete

model_to_pattern(Model, Type)

Convert Z3 model to Cure pattern

type_to_smt_sort(Primitive_type)

Convert Cure type to SMT sort

Functions

check_exhaustiveness(Patterns, Type)

-spec check_exhaustiveness([term()], term()) -> {complete} | {incomplete, [term()]} | {error, term()}.

Check if patterns are exhaustive Returns {complete} or {incomplete, [MissingPatterns]}

encode_pattern(Pattern, Type)

-spec encode_pattern(term(), term()) -> iolist().

Encode a single pattern as an SMT constraint Returns an SMT-LIB expression that is true when value matches pattern

encode_patterns_disjunction(Patterns, Type)

-spec encode_patterns_disjunction([term()], term()) -> iolist().

Encode multiple patterns as a disjunction (OR) Returns constraint that is true if ANY pattern matches

find_missing_pattern(CoveredPatterns, Type)

-spec find_missing_pattern([term()], term()) -> {missing, term()} | exhaustive | {error, term()}.

Find a missing pattern using SMT Returns {ok, Pattern} if a missing pattern is found, or exhaustive if complete

model_to_pattern(Model, Type)

-spec model_to_pattern(term(), term()) -> term().

Convert Z3 model to Cure pattern

type_to_smt_sort(Primitive_type)

-spec type_to_smt_sort(term()) -> iolist().

Convert Cure type to SMT sort