Allow multiple constraints in a CHC

[kjcjohnson]

Fixes #68 by allowing multiple constraints in CHCs. Note that this is just syntactic sugar - the generated CHCs still have a single constraint, but:

• multiple constraints will be merged into a single conjunction
• a single constraint will be left unchanged
• no constraint will be translated to a constraint of true

[kjcjohnson]

Also fixes #70 in the same "syntactic sugar" spirit. We now allow arbitrary SMT terms in the inputs to semantic relations, and we internally transform those to a fresh variable and a constraint. For example,

($a (E.Sem x y (+ x y)))

gets transformed into a CHC with an extra variable q such that:

• the body is (E.Sem x y q)
• the constraint is (= q (+ x y))

(q is not the real variable name. It's an auto-generated identifier.)