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

[DUCK Gregory James]

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.

For example, we can encode the axioms for a partial order in CHR as follows:
     leq(x, x) <=> true;                     // Reflexive
     leq(x, y) /\ leq(y, x) ==> x = y;       // Antisymmetric
     leq(x, y) /\ leq(y, z) ==> leq(x, z);   // Transitive
Saved to a file (e.g. leq.chr), this solver can be loaded into the SMCHR
system as follows:
     $ ./smchr --solver leq.chr --solver eq
>From there we can test the satisfiability of formulae containing leq/2
constraints, e.g.
     > leq(x, y) /\ leq(y, z) /\ (not leq(x, z) \/ (x != y /\ x = z))
     UNSAT

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.

Cheers,

-Greg.