Update DevelopersGuide.md

DevelopersGuide.md

@@ -27,6 +27,7 @@ Two problems are "equisatisfiable" when the answer to the question of their sati
 Equivalent problems are always equisatisfiable, but equisatisfiable problems need not be equivalent.
 Equisatisfiable problems do not need to have the same signature; the only thing that matters is the answer to their satisfiability questions is the same.
 
+Elements of a bounded sort are called domain elements.
 The "unbounded" version of problem is the problem obtained by removing the scopes on any bound sorts.
 
 A problem is "formulaically bound" if the following condition holds: the only interpretations that satisfy the unbounded version of the problem are those that satisfy the original (bounded) version.
@@ -35,7 +36,7 @@ If a problem is formulaically bound, it is equisatisfiable with its unbounded ve
 The basic algorithm that Fortress implements consists of the following steps.
 
 
-1. Negation Normal Form (NNF): The formulas of the problem are transformed into negation normal form, where negations are pushed down as far as possible into the formulas. The resulting problem is equivalent to the first.
+1. Negation Normal Form (NNF): The formulas of the problem are transformed into negation normal form, where negations are pushed down as far as possible into the formulas. The resulting problem is equivalent to the original problem.
 
 2. Skolemization: Existential quantifiers are eliminated by replacing them with functions and constants that act as witnesses for the existential quantifiers.
 The signature is changed by the introduction of new functions and constants.
@@ -45,14 +46,14 @@ Given this condition however, the resulting problem is equisatisfiable to the in
 3. Symmetry Breaking: Additional constraints are added to reduce the number of interpretations that need to be checked by the solver.
 The resulting problem is equisatisfiable to the input to this step.
 
-4. Universal Quantifier Expansion: Universal quantifiers of bounded sorts are expanded by taking each possible instantiation and then taking their conjunction.
+4. Universal Quantifier Expansion: Universal quantifiers of bounded sorts are expanded by taking each possible instantiation of the domain elements and then taking their conjunction.
 The resulting problem is equivalent to the input to this step.
 
 5. Simplification: The formulas are simplified as much as possible.
-The resulting problem is equivalent to the input to this step.
+The resulting problem is equivalent to the input of this step.
 
-6. Range Formulas: Range formulas are introduced, which use the scopes to explicitly list the possible output values of each function and constant.
-These range formulas are quantifier-free, so as to not introduce any more quantifiers after universal expansion.
+6. Range Formulas: Range formulas are introduced, which use the domain elements of the bounded scopes to explicitly list the possible output values of each function and constant.
+These range formulas are quantifier-free, and do not introduce any more quantifiers after universal expansion.
 The resulting problem is both equisatisfiable to the input to this step and *formulaically bound*.
 
 7. Domain Elimination: Constants are introduced to "simulate" the domain elements.
@@ -62,18 +63,14 @@ The domain elements are then replaced with their respective constants.
 The resulting problem is equisatisfiable to the input to this step, and contains no domain elements.
 This operation also maintains the property of being formulaically bound. 
 
-8. Scope Removal and SMT Invocation: The unbounded version of this final problem is converted into a format that is accepted by an SMT solver (the problem contains no domain elements, so this can be done).
+8. SMT solving: The problem is converted into a format that is accepted by an SMT solver (the problem contains no domain elements, so this can be done).
 The SMT solver is then invoked.
-Whatever result the solver returns is then returned to the user.
-
-
-All that Fortress needs to guarantee is that after its transformations, the final problem is equisatisfiable to the first input problem.
+Whatever result the solver returns is returned to the user.
 
-After applying the above transformations, the final problem is:
+After applying the above transformations to a problem with bounds for every sort, the final problem is:
 * equisatisfiable to the original problem, and
 * formulaically bound (so its scopes can be removed).
-
-Therefore, removing the scopes still leaves a problem equisatisfiable to the original, and, provided the SMT solver gives a correct result, so too does Fortress.
+All that Fortress needs to guarantee is that after its transformations, the final problem is equisatisfiable to the first input problem.
 
 If the original problem gives a scope for every sort, then because of the universal expansion step, there are no quantifiers in the final unbounded problem sent to the SMT solver.
 Such problems fall under the fragment of first-order logic called the logic of equality with uninterpreted functions (EUF), which is decidable.