CVC4

From CVC4
Jump to: navigation, search

CVC4 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

CVC4 is the most recent of a series of popular SMT provers, which originated at Stanford University with the SVC system. CVC4 is a from-scratch redesign and reimplementation of earlier solvers; it is designed for flexibility as a research tool and performance as an industrial SMT solver.

CVC4 works with a version of first-order logic and has a wide variety of features including:

  • several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;
  • support for quantifiers;
  • an interactive text-based interface;
  • a rich C++ API for embedding in other systems;
  • model generation abilities;
  • source compatibility with much of the CVC3 API via a "compatibility library";
  • essentially no limit on its use for research or commercial purposes (see license).