Module ta_encoding

taco_smt_encoder::expression_encoding

Module ta_encoding 

Source
Expand description

Helper functions to encode expression of a threshold automaton into SMT constraints

Functionsยง

encode_initial_constraints
Encodes the initial variable and location constraints of the threshold automaton in to an SMT expression
encode_resilience_condition
Encode the resilience conditions of a threshold automaton into an SMT expression and return it