pub fn obligation(
reference: &TensorGraph,
rewritten: &TensorGraph,
) -> Result<Obligation, SmtError>Expand description
The obligation that rewritten means what reference means: for every input and every meaning of the ops the
meaning leaves open, wherever the reference’s reads are in range, the rewritten graph’s are too and every tensor both
keep holds the same values. A tensor of one name is the same tensor in both.