diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-30 23:01:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-30 23:01:58 +0000 |
commit | 33e3657c15d6c760206aeaca10b5690af4a78223 (patch) | |
tree | a75475200584ab5e11981827182d979d84f6e1ff /examples/simple_vc_cxx.cpp | |
parent | 192c5592424e5db0afc72e7316c4698949a2f7e5 (diff) |
interfaces fixes and cleanups...and examples of each interface!
Diffstat (limited to 'examples/simple_vc_cxx.cpp')
-rw-r--r-- | examples/simple_vc_cxx.cpp | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp new file mode 100644 index 000000000..3b5db7c02 --- /dev/null +++ b/examples/simple_vc_cxx.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \file simple_vc_cxx.cpp + ** \verbatim + ** Original author: mdeters + ** 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 simple demonstration of the C++ interface + ** + ** A simple demonstration of the C++ interface. Compare to the Java + ** interface in SimpleVC.java; they are virtually line-by-line + ** identical. + **/ + +#include <iostream> + +//#include <cvc4.h> +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = em.integerType(); + + Expr x = em.mkVar("x", integer); + Expr y = em.mkVar("y", integer); + Expr zero = em.mkConst(Integer(0)); + + Expr x_positive = em.mkExpr(kind::GT, x, zero); + Expr y_positive = em.mkExpr(kind::GT, y, zero); + + Expr two = em.mkConst(Integer(2)); + Expr twox = em.mkExpr(kind::MULT, two, x); + Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y); + + Expr three = em.mkConst(Integer(3)); + Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three); + + BoolExpr formula = + BoolExpr(em.mkExpr(kind::AND, x_positive, y_positive)). + impExpr(BoolExpr(twox_plus_y_geq_3)); + + cout << "Checking validity of formula " << formula << " with CVC4." << endl; + cout << "CVC4 should report VALID." << endl; + cout << "Result from CVC4 is: " << smt.query(formula) << endl; + + return 0; +} |