1 /*********************                                                        */
2 /*! \file helloworld.cpp
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Tim King, Aina Niemetz
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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.\endverbatim
11  **
12  ** \brief A very simple CVC4 example
13  **
14  ** A very simple CVC4 tutorial example.
15  **/
16 
17 #include <iostream>
18 
19 //#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
20 #include "smt/smt_engine.h"
21 
22 using namespace CVC4;
main()23 int main() {
24   ExprManager em;
25   Expr helloworld = em.mkVar("Hello World!", em.booleanType());
26   SmtEngine smt(&em);
27   std::cout << helloworld << " is " << smt.query(helloworld) << std::endl;
28   return 0;
29 }
30