encode_initial_constraints

taco_smt_encoder::expression_encoding::ta_encoding

Function encode_initial_constraints 

Source 
pub fn encode_initial_constraints<TA, C>(
    ta: &TA,
    solver: &SMTSolver,
    ctx: &C,
) -> SMTExpr
where
    TA: ThresholdAutomaton,
    C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable>,
Expand description

Encodes the initial variable and location constraints of the threshold automaton in to an SMT expression

This function encodes the initial location and variable constraints of the threshold automaton in to an SMT expression. To do so, it needs the initial configuration of the threshold automaton, which is used as an SMT variable context.