Add option to export a z3-formatted formulas from kclause

[paulgazz]

Currently, kclause emits a pickled dictionary from configuration option names to z3-formatted formulas representing the options' constraints. Add a command-line flag to make this output the combined z3 formula for all options. klocalizer does this internally when constructing its formula. The following code shows how that works:

import z3
import pickle

# this program will read the kclause file format, combine all
# constraints for each configuration option, and output a single
# combined z3 formula for all
path_to_kclause_file = ".kmax/5.4.0/kclause/x86_64/kclause"
with open(path_to_kclause_file, "rb") as f:
  # unpickle kclause output
  kclause_formulas = pickle.load(f)

  # parse z3 formulas for each configuration option
  kclause_constraints = {}
  for var in kclause_formulas:
    kclause_constraints[var] = [ z3.parse_smt2_string(clause) for clause in kclause_formulas[var] ]

  # collect constraints from all configuration options
  constraints = []
  for var in kclause_constraints:
    for z3_clause in kclause_constraints[var]:
      constraints.extend(z3_clause)
  s = z3.Solver()
  s.add(constraints)
  smt2_str = s.to_smt2()
  print(smt2_str)