[SMT-LIB] The SMCHR system version 1.0 released.

[Martin Brain]

On Mon, 2013-09-30 at 17:41 +0800, DUCK Gregory James wrote:
> Hi,
> 
> Version 1.0 of the SMCHR system has been released.  Download it from here:
> 
>      http://www.comp.nus.edu.sg/~gregory/smchr/
> 
> The SMCHR system is a new SMT solver implementation that allows solvers to 
> be implemented in the Constraint Handling Rules (CHR) programming 
> language.
<snip>
> In addition to CHR solvers, the SMCHR system supports several built-in 
> solvers including linear arithmetic, bounds propagation, union-find 
> equality, heaps, etc.  More information and other examples are available 
> from the website.

I was really interested in your tool but I find it slightly bizaar that
you've posted it to the SMT-LIB mailing list when your website says:

"As SMCHR system was designed to be simple and easy to use, we solemnly
guarantee never to support the SMTLIB syntax."

which makes it sound like you have some kind of fundamental opposition
to the purpose of this list?



Obviously what you implement in your tool is entirely up to you.
However SMT-LIB was designed to support interoperability of tools and
sharing of benchmarks rather than human readability or write-ability, in
fact (to quote the SMT-LIB standard):

"Preferring ease of parsing over human readability is reasonable in this
context not only because SMT-LIB benchmarks are meant to be read by
solvers but also because they are produced in the first place by
automated tools like verification condition generators or translators
from other formats."

So critiquing it for not being more compact / human orientated is
perhaps missing the point of SMT-LIB?  I think there is a separate need
for human orientated, logical modeling languages -- hell, that's was
part of my PhD.  But, from my experience, I'd say there are big
advantages to separating that from a machine interface to the solver.


Cheers,
 - Martin