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()23int 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