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_compat_cxx.cpp | |
parent | 192c5592424e5db0afc72e7316c4698949a2f7e5 (diff) |
interfaces fixes and cleanups...and examples of each interface!
Diffstat (limited to 'examples/simple_vc_compat_cxx.cpp')
-rw-r--r-- | examples/simple_vc_compat_cxx.cpp | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/examples/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp new file mode 100644 index 000000000..c178d1aba --- /dev/null +++ b/examples/simple_vc_compat_cxx.cpp @@ -0,0 +1,64 @@ +/********************* */ +/*! \file simple_vc_compat_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++ compatibility interface + ** (quite similar to the old CVC3 C++ interface) + ** + ** A simple demonstration of the C++ compatibility interface (quite + ** similar to the old CVC3 C++ interface). Note that the library is + ** named "libcvc4compat," to mark it as being part of CVC4, but the + ** header file is "cvc3_compat.h" to indicate the similarity to the + ** CVC3 interface, and the namespace is "CVC3". CVC3::Expr and + ** CVC4::Expr are incompatible; to avoid confusion, it is best to not + ** include both the CVC3 and CVC4 interface headers. + **/ + +#include <iostream> + +// #include <cvc4/compat/cvc3_compat.h> +#include "compat/cvc3_compat.h" + +using namespace std; +using namespace CVC3; + +int main() { + ValidityChecker* vc = ValidityChecker::create(); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = vc->intType(); + + Expr x = vc->varExpr("x", integer); + Expr y = vc->varExpr("y", integer); + Expr zero = vc->ratExpr(0); + + Expr x_positive = vc->gtExpr(x, zero); + Expr y_positive = vc->gtExpr(y, zero); + + Expr two = vc->ratExpr(2); + Expr twox = vc->multExpr(two, x); + Expr twox_plus_y = vc->plusExpr(twox, y); + + Expr three = vc->ratExpr(3); + Expr twox_plus_y_geq_3 = vc->geExpr(twox_plus_y, three); + + Expr formula = vc->impliesExpr(vc->andExpr(x_positive, y_positive), + 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: " << vc->query(formula) << endl; + + return 0; +} |