Expand description
A rewrite of the one IR, proven: the obligation tensor_graph::smt prints for two graphs, discharged by Z3.
A rewrite is proven when every lemma of its obligation holds: its premises are satisfiable — the facts it assumes hold of some input, so nothing follows from them vacuously — and its premises with its goal are not: no input and no meaning of the ops the IR leaves open makes the lemma’s two terms differ, or a read of the rewritten graph stray out of range.
Enums§
- Verdict
- What Z3 says of one obligation.
Functions§
- discharge
- Discharge
o: every lemma, each given up totimeout_msfor each of its two checks. The first lemma that is not proven gives the verdict.