Tools on Rewriting

Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixedsize bitvectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.
Home o Docs o Contacts o FM Tools ... * Source Code * Linux (64 bits) * Mac OS X (64 bits) * Windows (64 bits) * Windows (32 bits) ... * Manual * API Reference * Publications ...

Z3 is a highperformance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixedsize bitvectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. It can read problems in SMTLIB and Simplify formats.
numerator Properties Friends Macros Modules Pages ... * Try Z3 online at RiSE4Fun. ... Generated on Fri Oct 24 2014 23:25:20 for Z3 by doxygen 1.8.8...

CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory (or a combination of such theories). It is the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. CVC4 is intended to be an open and extensible SMT engine. It can be used as a standalone tool or as a library. It has been designed to increase the performance and reduce the memory overhead of its predecessors. CVC4 is still a research prototype and is not yet ready for public release. Users looking for an industrialstrength SMT solver are encouraged to use CVC3 instead (for now).
* Google...

MiniSmt is a simple SMT solver for nonlinear arithmetic based on MiniSat and Yices. It accepts the SMTLIB format as input, is efficient on small domains, supports reasoning about nonrational real numbers, and is able to output models.
The current stable version is 0.6. Get recent versions and view the ... Mar 9, 2014: version 0.6 released (compile with interfaced GPW)...