interfaces fixes and cleanups...and examples of each interface!

1 files changed, 61 insertions, 0 deletions

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 <stdio.h>
+#include <stdlib.h>
+
+// #include <cvc4/compat/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;
+}