improve example: make usage of enumeration theory more local to avoid unnecessary errors.

Author: kfriedberger

src/org/sosy_lab/java_smt/example/Sudoku.java

@@ -169,13 +169,11 @@ public abstract static class SudokuSolver<S> {
     private final SolverContext context;
     final BooleanFormulaManager bmgr;
     final IntegerFormulaManager imgr;
-    final EnumerationFormulaManager emgr;
 
     private SudokuSolver(SolverContext pContext) {
       context = pContext;
       bmgr = context.getFormulaManager().getBooleanFormulaManager();
       imgr = context.getFormulaManager().getIntegerFormulaManager();
-      emgr = context.getFormulaManager().getEnumerationFormulaManager();
     }
 
     abstract S getSymbols();
@@ -426,13 +424,15 @@ Integer getValue(BooleanFormula[][][] symbols, Model model, int row, int col) {
 
   public static class EnumerationBasedSudokuSolver extends SudokuSolver<EnumerationFormula[][]> {
 
+    private final EnumerationFormulaManager emgr;
     private final EnumerationFormulaType type;
     private static final String[] VALUES = {
       "ONE", "TWO", "THREE", "FOUR", "FIVE", "SIX", "SEVEN", "EIGHT", "NINE",
     };
 
     public EnumerationBasedSudokuSolver(SolverContext context) {
       super(context);
+      emgr = context.getFormulaManager().getEnumerationFormulaManager();
       type = emgr.declareEnumeration("VALUES", VALUES);
     }