diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-04 14:59:19 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 16:59:19 -0500 |
commit | 747a9a248da073911e1c0da34c38f0648421a087 (patch) | |
tree | 98449a71c66d0ad427b8c8dc6f0ed1b9fbccdfbe /examples/simple_vc_compat_c.c | |
parent | 29bf7d6a937ab50c4dd92a30d7beb36a4001ead6 (diff) |
Remove CVC3 compatibility layer (#2418)
Diffstat (limited to 'examples/simple_vc_compat_c.c')
-rw-r--r-- | examples/simple_vc_compat_c.c | 60 |
1 files changed, 0 insertions, 60 deletions
diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c deleted file mode 100644 index ff913dd83..000000000 --- a/examples/simple_vc_compat_c.c +++ /dev/null @@ -1,60 +0,0 @@ -/********************* */ -/*! \file simple_vc_compat_c.c - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 <stdio.h> -#include <stdlib.h> - -// Use this after CVC4 is properly installed. -// #include <cvc4/bindings/compat/c/c_interface.h> -#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; -} |