Pre-solve equality constraints to reduce number of constraint variables hitting back end solvers

[jyluo]

Across all of the type systems supported, we typically have equality constraints expressed between constant slots and variable slots, which can be pre-solved to reduced the number of constraint variables and constraints in the system, and which are then encoded into SAT or SMT formulas.

Enabling this requires slots in constraints to be replaceable (always from a variable slot to a constant slot) in this pre-solving phase, eg:

original constraints

@9 == @Top
@8 <: @9

slot solution after solving equalities:

@9 := @Top 

constraints after solving equalities:

@8 <: @Top

Rough algo:

For eqc in equality constraints
   if eqc is between a constant slot CS and a variable slot V
      update V's solution  V := CS
      delete eqc from constraint set
      for c in all constraints
         if c is expressed over V, replace V in c with CS
         check to see if updated c is unsat, if so, generate error warning
         check to see if updated c is always sat, if so, delete c from constraint set
until fixpoint

Should be O(n^2) relative to number of constraints.

Details:

1. if unsat, a minimal unsat core needs to be generated (by back-propagating from the unsat constraint and looking up all involved slots)

2. Constraints are currently hashed on their component slots, this may need to change to ensure that a constraint with an updated slot does not collide with another constraint already present in the constraint set.