Suggestion: Add front-end for Constrained Horn Clauses

[blishko]

As discussed at TACAS, it would be great if Theta could support CHC front-end. The language is a simple extension of SMT-LIB, format described here. At least transition systems (1 uninterpreted predicate and 3 clauses) and linear systems of CHCs (at most 1 uninterpreted predicate in the body of every clause) should directly map to STS and CFA in Theta's representation, I believe.

Then Theta could participate in CHC-COMP, which would be great for the CHC community.

[hajduakos]

Thanks @blishko for the discussion and the suggestion! I've posted this in the Theta team Slack, hopefully someone can start working on this soon.