From 33e3657c15d6c760206aeaca10b5690af4a78223 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 30 Sep 2011 23:01:58 +0000 Subject: interfaces fixes and cleanups...and examples of each interface! --- examples/simple_vc_compat_c.c | 61 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 examples/simple_vc_compat_c.c (limited to 'examples/simple_vc_compat_c.c') diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c new file mode 100644 index 000000000..9bcb52280 --- /dev/null +++ b/examples/simple_vc_compat_c.c @@ -0,0 +1,61 @@ +/********************* */ +/*! \file simple_vc_compat_c.c + ** \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). + **/ + +#include +#include + +// #include +#include "bindings/compat/c/c_interface.h" + +int main() { + VC vc = vc_createValidityChecker(NULL); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = vc_intType(vc); + + Expr x = vc_varExpr(vc, "x", integer); + Expr y = vc_varExpr(vc, "y", integer); + Expr zero = vc_ratExpr(vc, 0, 1); + + Expr x_positive = vc_gtExpr(vc, x, zero); + Expr y_positive = vc_gtExpr(vc, y, zero); + + Expr two = vc_ratExpr(vc, 2, 1); + Expr twox = vc_multExpr(vc, two, x); + Expr twox_plus_y = vc_plusExpr(vc, twox, y); + + Expr three = vc_ratExpr(vc, 3, 1); + Expr twox_plus_y_geq_3 = vc_geExpr(vc, twox_plus_y, three); + + Expr formula = vc_impliesExpr(vc, vc_andExpr(vc, x_positive, y_positive), + twox_plus_y_geq_3); + + char* formulaString = vc_printExprString(vc, formula); + + printf("Checking validity of formula %s with CVC4.\n", formulaString); + printf("CVC4 should return 1 (meaning VALID).\n"); + printf("Result from CVC4 is: %d\n", vc_query(vc, formula)); + + free(formulaString); + + return 0; +} -- cgit v1.2.3