In my post on Z3, I created an extension method for proving an equation. This extension method used a switch statement to analyze a result and return a string. This is a bad practice: the mapping of one type to another is trapped in code. What if I wanted to move this mapping to a configuration file, a resource file, or a database? Even if I didn’t want to do that, I feel an imperative switch statement isn’t as readable as a declarative statement. Favor Declarative over Imperative. Below is the original code snippet.

public static string Prove(this Context context, Term term)
 {
     context.Push();
     Term not = context.MkNot(term);
     context.AssertCnstr(not);
     switch (context.Check())
     {
         case LBool.False:
             return "valid";
         case LBool.Undef:
             return "unknown";
         case LBool.True:
             return "invalid";
     }
     return null;
 }

When you see case statements simply return or an assign an item, you know you can perform this refactoring. You will create a generic dictionary of both types and use it instead. Here is the refactored example.

public static string Prove(this Context context, Term term)
{
    var checkResults = new Dictionary<LBool, string>
    {
        { LBool.False, "valid" },
        { LBool.Undef, "unknown" },
        { LBool.True, "invalid" }
    };

    context.Push();
    Term not = context.MkNot(term);
    context.AssertCnstr(not);
    
    return checkResults[context.Check()];            
}

The great thing about this is that you have the mappings side by side. Since it is in a dictionary format, it is loadable from another location; the mapping is no longer tied to the code.