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}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz
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/c/cvc5.h>
17#include <stdio.h>
18
19int main()
20{
21 Cvc5TermManager* tm = cvc5_term_manager_new();
22 Cvc5* slv = cvc5_new(tm);
23 Cvc5Term hello = cvc5_mk_const(tm, cvc5_get_boolean_sort(tm), "Hello World!");
24 Cvc5Term assumptions[1] = {hello};
25 printf("%s is %s\n",
26 cvc5_term_to_string(hello),
27 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
28 cvc5_delete(slv);
29 cvc5_term_manager_delete(tm);
30 return 0;
31}
examples/api/java/HelloWorld.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Morgan Deters, Andrew Reynolds
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 tutorial example.
14 */
15
16import io.github.cvc5.*;
17
18public class HelloWorld
19{
20 public static void main(String[] args)
21 {
22 TermManager tm = new TermManager();
23 Solver slv = new Solver(tm);
24 {
25 Term helloworld = tm.mkConst(tm.getBooleanSort(), "Hello World!");
26
27 System.out.println(helloworld + " is " + slv.checkSatAssuming(helloworld));
28 }
29 Context.deletePointers();
30 }
31}
examples/api/python/pythonic/helloworld.py
1###############################################################################
2# Top contributors (to current version):
3# Alex Ozdemir
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##
15from cvc5.pythonic import *
16
17if __name__ == '__main__':
18 var = Bool('Hello World!')
19 solve(var)
examples/api/python/helloworld.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Alex Ozdemir, Makai Mann, Andrew Reynolds
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# A very simple example, adapted from helloworld-new.cpp
15##
16
17import cvc5
18from cvc5 import Kind
19
20if __name__ == "__main__":
21 tm = cvc5.TermManager()
22 slv = cvc5.Solver(tm)
23 helloworld = tm.mkConst(tm.getBooleanSort(), "Hello World!")
24 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)