| 131 | === Wanted Constraints === |

| 132 | |

| 133 | The main purpose of the solver is to discharge ``wanted`` constraints |

| 134 | (the purpose of processing given and derived constraints is to help |

| 135 | solve existing wanted goals). When we encounter a new wanted goals |

| 136 | we proceed as follows: |

| 137 | |

| 138 | 1. Try to solve the goal, using a few different strategies: |

| 139 | 1. Try to see if it matches the conclusion of an iff rule (`solveIff`). Aassumptions of rule become new wanted work. |

| 140 | 2. Try to see if it matches an axiom exactly (`solve`) |

| 141 | 3. Try the ordering solver for `<=` goals (`solveLeq`) |

| 142 | 4. Try to use a (possibly synthesized) assumption |

| 143 | |

| 144 | 2. If that didn't work: |

| 145 | 1. Wanted is added to the inert set |

| 146 | 2. Check to see if any of the existing wanteds in the inert set can be solved in terms of the new goal (`reExamineWanteds`) |

| 147 | 3. Generate new derived facts. |