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 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A very simple cvc5 example.
11 */
12
13#include <cvc5/cvc5.h>
14
15#include <iostream>
16
17using namespace cvc5;
18
19int main()
20{
21 TermManager tm;
22 Solver slv(tm);
23 Term helloworld = tm.mkConst(tm.getBooleanSort(), "Hello World!");
24 std::cout << helloworld << " is " << slv.checkSatAssuming(helloworld)
25 << std::endl;
26 return 0;
27}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A very simple cvc5 example.
11 */
12
13#include <cvc5/c/cvc5.h>
14#include <stdio.h>
15
16int main()
17{
18 Cvc5TermManager* tm = cvc5_term_manager_new();
19 Cvc5* slv = cvc5_new(tm);
20 Cvc5Term hello = cvc5_mk_const(tm, cvc5_get_boolean_sort(tm), "Hello World!");
21 Cvc5Term assumptions[1] = {hello};
22 printf("%s is %s\n",
23 cvc5_term_to_string(hello),
24 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
25 cvc5_delete(slv);
26 cvc5_term_manager_delete(tm);
27 return 0;
28}
examples/api/java/HelloWorld.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A very simple CVC5 tutorial example.
11 */
12
13import io.github.cvc5.*;
14
15public class HelloWorld
16{
17 public static void main(String[] args)
18 {
19 TermManager tm = new TermManager();
20 Solver slv = new Solver(tm);
21 {
22 Term helloworld = tm.mkConst(tm.getBooleanSort(), "Hello World!");
23
24 System.out.println(helloworld + " is " + slv.checkSatAssuming(helloworld));
25 }
26 Context.deletePointers();
27 }
28}
examples/api/python/pythonic/helloworld.py
1###############################################################################
2# This file is part of the cvc5 project.
3#
4# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5# in the top-level source directory and their institutional affiliations.
6# All rights reserved. See the file COPYING in the top-level source
7# directory for licensing information.
8# #############################################################################
9#
10# A very simple cvc5 example.
11##
12from cvc5.pythonic import *
13
14if __name__ == '__main__':
15 var = Bool('Hello World!')
16 solve(var)
examples/api/python/helloworld.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A very simple example, adapted from helloworld-new.cpp
12##
13
14import cvc5
15from cvc5 import Kind
16
17if __name__ == "__main__":
18 tm = cvc5.TermManager()
19 slv = cvc5.Solver(tm)
20 helloworld = tm.mkConst(tm.getBooleanSort(), "Hello World!")
21 print(helloworld, "is", slv.checkSatAssuming(helloworld))
examples/api/smtlib/helloworld.smt2
1(set-logic QF_UF)
2(declare-const |Hello World!| Bool)
3(assert (not |Hello World!|))
4(check-sat)