CVC4
From CVC4
(Redirected from CVC Portal)
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).
