Write interface with SMT solver

[eionblanc]

Final interface should flow as follows:

• Input file will contain at least one "(synth-fun lemma ... )". This should be replaced with the synthesized lemma and its necessary constant/function declarations.
• Replace appearances of "constraint" with "assert".
• Replace "check-synth" with "check-sat" and "get-model".
• Call SMT solver on synthesized lemma within Python.
• Parse SMT output model and determine the actual synthesized lemma under this model.

[eionblanc]

Helpful links:

• https://github.com/lucaspena/lemma-synthesis/blob/e98ca9c53eb280847c164f87e08821642b670da3/lemsynth/lemma_synthesis.py#L320-L321
• https://stackoverflow.com/a/12605520

[eionblanc]

CVC4 functions properly!

Issues barring z3:

• z3 is unhappy with the empty set SMTLIB standard; similar issues with set membership (see here and here); it's not immediately clear how to convert these expressions to format for z3
• z3 does output models that can easily be reformed to dictionaries as currently aligns with the lemma synthesis program (feature to take input model and generate the particular corresponding lemma)