Sometimes, we can end up calling update with a self-relation
about a variable (x REL x). In this case, there is no need
to record anything: the relation is unsatisfiable if and only
if it doesn't contain eq.
This also helps avoiding infinite loop in next CL that will
introduce transitive closure of relations.
Passes toolstash -cmp.
Change-Id: Ic408452ec1c13653f22ada35466ec98bc14aaa8e
Reviewed-on: https://go-review.googlesource.com/100276
Reviewed-by: Austin Clements <austin@google.com>
return
}
+ // Self-fact. It's wasteful to register it into the facts
+ // table, so just note whether it's satisfiable
+ if v == w {
+ if r&eq == 0 {
+ ft.unsat = true
+ }
+ return
+ }
+
if lessByID(w, v) {
v, w = w, v
r = reverseBits[r]