Archsat is a prototype SMT solver combining traditional SMT solvingtechniques for ground resoning, tableaux method and rewriting forquantified formulas, and superposition for unification modulo equalities andmodulo rewriting.
MIT (see file LICENSE).
The easiest way to install archsat is to pin the repo and let opaminstall the package (after having pinned the dev repos formsat anddolmen):
opam pin add archsat /path/to/git/repo
Once installed via opam, anarchsat binary should be available the path,as well as manpages for archsat.
One can install archsat manually, though it requires dependencies to be explicitlyinstalled. The list of dependencies can be found in theopam file at the root ofthe repository. One can then run:
MANDIR=/some/path BINDIR=/some/other/path make install
Specifying theMANDIR andBINDIR is necessary to specify where to installthe binary and the manpages.
The archsat repo includes some tests for the binary, in thetests directory,these can be run using the command:
For unit tests of internal functions, seesrc/README.md.
The common and profiling options of the archsat binary should be fairly well documentedin the manpage (as well as when using the--help command). Advanced options may requiresome more knowledge of the prover's internals to be used correctly.
In case of unhelpful or unsufficiently clear explanations, don't hesitateto submit a bug report.