Summary:
For some Exp forms, Exp.solve is not complete, and this is necessary
since the result of solve is a substitution that needs to encode the
input equation as a conjunction of equations each between a variable
and an exp. This is tantamount to, stronger even than, the theory
being convex. So Exp.solve is not complete for some exps, and some of
those have constructors that perform some simplification. For example,
`(1 ≠ 0)` simplifies to `-1` (i.e. true). To enable deductions such as
`((x ≠ 0) = b) && x = 1 |- b = -1` needs the equality solver to
substitute through subexps of simplifiable exps like = and ≠, as it
does for interpreted exps like + and ×. At the same time, since
Exp.solve for non-interpreted exps cannot be complete, to enable
deductions such as `((x ≠ 0) = (y ≠ 0)) && x = 1 |- y ≠ 0` needs the
equality solver to congruence-close over subexps of simplifiable exps
such as = and ≠, as it does for uninterpreted exps.
To strengthen the equality solver in these sorts of cases, this diff
adds a new class of exps for = and ≠, and revises the equality solver
to handle them in a hybrid fashion between interpreted and
uninterpreted.
I am not currently sure whether or not this breaks the termination
proof, but I have also not managed to adapt usual divergent cases to
break this. One notable point is that simplifying = and ≠ exps always
produces genuinely simpler and smaller exps, in contrast to
e.g. polynomial simplification and gaussian elimination.
Note that the real solution to this problem is likely to be to
eliminate the i1 type in favor or a genuine boolean type, and
translate all integer operations on i1 to boolean/logical ones. Then
the disjunction implicit in e.g. equations between disequations would
appear as actual disjunction, and could be dealt with as such.
Reviewed By: jvillard
Differential Revision: D15424823
fbshipit-source-id: 67d62df1f
Josh Berdine
0cbcb878f9