diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-28 22:59:58 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-28 22:59:58 +0000 |
commit | 91673d6cefa63bc0f706101946e0c01fcd429071 (patch) | |
tree | 8fa80213fb916675f37f4a1a1bcd431bcc017f7f /examples/api/helloworld.cpp | |
parent | f0ebc08cf865d654a6d7ca4361775db8a64b1f62 (diff) |
Adding the helloworld.cpp example.
Diffstat (limited to 'examples/api/helloworld.cpp')
-rw-r--r-- | examples/api/helloworld.cpp | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp new file mode 100644 index 000000000..26b081a79 --- /dev/null +++ b/examples/api/helloworld.cpp @@ -0,0 +1,30 @@ +/********************* */ +/*! \file helloworld.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A very simple CVC4 example + ** + ** A very simple CVC4 tutorial example. + **/ + +#include <iostream> +#warning "To use helloworld.cpp as given in the wiki, instead of make examples, change the following two includes lines." +#include "smt/smt_engine.h" // for use with make examples +//#include <cvc4/cvc4.h> // To follow the wiki +using namespace CVC4; +int main() { + ExprManager em; + Expr helloworld = em.mkVar("Hello World!", em.booleanType()); + SmtEngine smt(&em); + std::cout << helloworld << " is " << smt.query(helloworld) << std::endl; + return 0; +} |