Summary:
For non-linear polynomial equations, the solver can currently choose
to solve for a variable that occurs in a non-linear subterm, leading
to a non-idepotent solution substitution. For example, `x - y + (x ×
z) = 0` could be solved for `x`, leading to `x ↦ y - (x × z)` where
`x` is solved in terms of itself. This diff refines Term.solve_zero_eq
to avoid such cyclic solutions.
Reviewed By: jvillard
Differential Revision: D20637482
fbshipit-source-id: 6d7df85c3
Summary:
Ensure all entry points check the representation invariant before
returning, and strengthen it to check the constraints on preference
between representative terms, and to check that the relation is
closed.
Reviewed By: jvillard
Differential Revision: D20612566
fbshipit-source-id: b345397c4
Summary:
Fix the crash in
```
(And_eq () (Var (id 10) (name v))
(Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1)))
((xs ()) (sat true) (rep ())))
```
The solver for interpreted functions relies on the solution
substitutions containing mappings from variables to interpreted
applications, and never in the reverse. When solving equations
involving polynomials, this constraint is specifically
established. But for equalities involving only monomials, it could
happen that e.g. `x` was chosen as the representative of `a × b`,
which violates this constraint.
Reviewed By: jvillard
Differential Revision: D20596422
fbshipit-source-id: 69b026f03
Summary:
It is more convenient, and harder to misunderstand, if the verbose
tracing setting comes commented-out after the default non-verbose
setting.
Reviewed By: jvillard
Differential Revision: D20583755
fbshipit-source-id: 06ecb0e9a
Summary:
Move files, adjust build system, etc.
This also separates out the ppx_trace conditional compilation debug
tracing machinery into an independent package and library.
Reviewed By: jvillard
Differential Revision: D20322876
fbshipit-source-id: a50522462
Josh Berdine