libcvc43
A library interface for the cvc4 theorem prover
Usage
A small program like:
#include <iostream>
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
using namespace CVC4;
int main() {
ExprManager em;
SmtEngine smt(&em);
Expr onePlusTwo = em.mkExpr(kind::PLUS,
em.mkConst(Rational(1)),
em.mkConst(Rational(2)));
std::cout << language::SetLanguage(language::output::LANG_CVC4)
<< smt.getInfo("name")
<< " says that 1 + 2 = "
<< smt.simplify(onePlusTwo)
<< std::endl;
return 0;
}
gives the output:
"cvc4" says that 1 + 2 = 3
Overview
The main classes of interest in CVC4's API are ExprManager, SmtEngine, and a few related ones like Expr and Type.
The ExprManager is used to build up expressions and types, and the SmtEngine is used primarily to make assertions, check satisfiability/validity, and extract models and proofs.
Releases
4 releases since Debian 11 (Bullseye); the text changed 3 times.