Hello World

This example shows the very basic usage of the API. We create a solver, declare a Boolean variable and check whether it is entailed (by true , as nothing has been asserted to the solver).

examples/api/cpp/helloworld.cpp

 1/******************************************************************************
 2 * Top contributors (to current version):
 3 *   Aina Niemetz, Tim King, Mathias Preiner
 4 *
 5 * This file is part of the cvc5 project.
 6 *
 7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
 8 * in the top-level source directory and their institutional affiliations.
 9 * All rights reserved.  See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A very simple cvc5 example.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20using namespace cvc5;
21
22int main()
23{
24  TermManager tm;
25  Solver slv(tm);
26  Term helloworld = tm.mkConst(tm.getBooleanSort(), "Hello World!");
27  std::cout << helloworld << " is " << slv.checkSatAssuming(helloworld)
28            << std::endl;
29  return 0;
30}