LIBCVC4(3)

💖 LIBCVC4 💖

okay bestie, so this is libcvc4 from the CVC4 Library Interfaces section — it's the library interface for the CVC4 theorem prover and honestly? she's kind of a big deal. 🎀

---

✨ SYNOPSIS ✨

so like, imagine a tiny lil program that looks exactly like this:

#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;
}

and she gives you the output:

"cvc4" says that 1 + 2 = 3

no cap, she literally just did math for you. main character behavior fr. 💅

---

🌸 DESCRIPTION 🌸

the main classes you're gonna be obsessed with in CVC4's API are ExprManager, SmtEngine, plus a few related ones like Expr and Type.

so like, ExprManager is the one you use to build up expressions and types. think of her as the arts-and-crafts table where everything gets made. 🎨

and SmtEngine? she's used primarily to make assertions, check satisfiability/validity, and extract models and proofs. she's the one asking the real questions and getting receipts. 👑

---

🦋 SEE ALSO 🦋

• cvc4(1)
• libcvc4parser(3)

also!! the CVC4 wiki has genuinely useful info about the design and internals of CVC4, and it's maintained right here: http://cvc4.cs.stanford.edu/wiki/ — go read it, iykyk 📚✨

---

and that's the whole page, bestie 🫶 this was CVC4 release CVC4_RELEASE_STRING, dated 2024-03-31, filed under LIBCVC4(3). periodt. 💜