examples/simple_vc_compat_c.c

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