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
20using namespace cvc5;
21
22int 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
16import io.github.cvc5.*;
17
18public class HelloWorld
19{
20 public static void main(String[] args)
21 {
22 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 Context.deletePointers();
29 }
30}
examples/api/python/pythonic/helloworld.py
1from cvc5.pythonic import *
2
3if __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
17import cvc5
18from cvc5 import Kind
19
20if __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)