examples/simple_vc_compat_c.c

   1 /*********************                                                        */
   2 /*! \file simple_vc_compat_c.c
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief A simple demonstration of the C compatibility interface
  15  ** (quite similar to the old CVC3 C interface)
  16  **
  17  ** A simple demonstration of the C compatibility interface
  18  ** (quite similar to the old CVC3 C interface).
  19  **/
  20
  21 #include <stdio.h>
  22 #include <stdlib.h>
  23
  24 /* #include <cvc4/compat/c_interface.h> /* use this after CVC4 is properly installed */
  25 #include "bindings/compat/c/c_interface.h"
  26
  27 int main() {
  28   VC vc = vc_createValidityChecker(NULL);
  29
  30   /* Prove that for integers x and y:
  31    *   x > 0 AND y > 0  =>  2x + y >= 3 */
  32
  33   Type integer = vc_intType(vc);
  34
  35   Expr x = vc_varExpr(vc, "x", integer);
  36   Expr y = vc_varExpr(vc, "y", integer);
  37   Expr zero = vc_ratExpr(vc, 0, 1);
  38
  39   Expr x_positive = vc_gtExpr(vc, x, zero);
  40   Expr y_positive = vc_gtExpr(vc, y, zero);
  41
  42   Expr two = vc_ratExpr(vc, 2, 1);
  43   Expr twox = vc_multExpr(vc, two, x);
  44   Expr twox_plus_y = vc_plusExpr(vc, twox, y);
  45
  46   Expr three = vc_ratExpr(vc, 3, 1);
  47   Expr twox_plus_y_geq_3 = vc_geExpr(vc, twox_plus_y, three);
  48
  49   Expr formula = vc_impliesExpr(vc, vc_andExpr(vc, x_positive, y_positive),
  50                                 twox_plus_y_geq_3);
  51
  52   char* formulaString = vc_printExprString(vc, formula);
  53
  54   printf("Checking validity of formula %s with CVC4.\n", formulaString);
  55   printf("CVC4 should return 1 (meaning VALID).\n");
  56   printf("Result from CVC4 is: %d\n", vc_query(vc, formula));
  57
  58   free(formulaString);
  59
  60   return 0;
  61 }