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, Andrew Reynolds
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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
20 using namespace cvc5;
21
22 int main()
23 {
24 Solver slv;
25 Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!");
26 std::cout << helloworld << " is " << slv.checkSatAssuming(helloworld)
27 << std::endl;
28 return 0;
29 }
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-2022 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
16 import io.github.cvc5.*;
17
18 public class HelloWorld
19 {
20 public static void main(String[] args)
21 {
22 try (Solver slv = new Solver())
23 {
24 Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!");
25
26 System.out.println(helloworld + " is " + slv.checkSatAssuming(helloworld));
27 }
28 }
29 }
examples/api/python/pythonic/helloworld.py
1 from cvc5.pythonic import *
2
3 if __name__ == '__main__':
4 var = Bool('Hello World!')
5 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-2022 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
17 import cvc5
18 from cvc5 import Kind
19
20 if __name__ == "__main__":
21 slv = cvc5.Solver()
22 helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!")
23 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)