Tools on Rewriting

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...

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.
Yices 2 can process input written in the SMTLIB notation (both versions 2.0 and 1.2 are supported). ... The current release is Yices 2.2.2 (released August 6, 2014) ... Previous Releases (binary on...

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)...

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.
____________________ ... All Data Structures Namespaces Files Functions Variables Typedefs Enumerations E numerator Properties Friends Macros Groups Pages ... IFRAME: MSearchResults ... * Python A...