Bindings work (ocaml bindings are now sort of working); also minor cleanup

5 files changed, 97 insertions, 5 deletions

diff --git a/examples/Makefile.am b/examples/Makefile.am
index f72c20d02..46de3689b 100644
--- a/examples/Makefile.am
+++ b/examples/Makefile.am
@@ -52,6 +52,7 @@ SimpleVCCompat.class: SimpleVCCompat.java
 EXTRA_DIST = \
 	SimpleVC.java \
 	SimpleVC.py \
+	SimpleVC.ml \
 	SimpleVCCompat.java \
 	README
 
diff --git a/examples/SimpleVC.ml b/examples/SimpleVC.ml
new file mode 100644
index 000000000..f7caa9e3d
--- /dev/null
+++ b/examples/SimpleVC.ml
@@ -0,0 +1,91 @@
+(*********************                                                        **
+**! \file SimpleVC.ml
+*** \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 OCaml interface
+***
+*** A simple demonstration of the OCaml interface.  Compare to the
+*** C++ interface in simple_vc_cxx.cpp; they are quite similar.
+***
+*** To run, use something like:
+***
+***   LD_LIBRARY_PATH=../builds/src/bindings/.libs \
+***     ../builds/src/bindings/cvc4_ocaml_top -I ../builds/src/bindings/ocaml \
+***     SimpleVC.ml
+***
+*** After you "make install" CVC4, it's much easier; the cvc4_ocaml_top goes in
+*** $prefix/bin, and it's automatically set up the load the .cmo and .cmi files
+*** from $prefix/lib/ocaml/cvc4, in which they get installed.  Then you just
+*** have to: cvc4_ocaml_top -I $prefix/lib/ocaml/cvc4
+***)
+
+open Swig
+open CVC4
+
+let em = new_ExprManager '()
+let smt = new_SmtEngine(em)
+
+(* Prove that for integers x and y:
+ *   x > 0 AND y > 0  =>  2x + y >= 3 *)
+
+let integer = em->integerType()
+
+let x = em->mkVar(integer) (* em->mkVar("x", integer) *)
+let y = em->mkVar(integer) (* em->mkVar("y", integer) *)
+let integerZero = new_Integer '("0", 10)
+let zero = em->mkConst(integerZero)
+
+(* OK, this is really strange.  We can call mkExpr(36, ...) for
+ * example, with the int value of the operator Kind we want,
+ * or we can compute it.  But if we compute it, we have to rip
+ * it out of its C_int, then wrap it again a C_int, in order
+ * for the parser to make it go through. *)
+let geq = C_int (get_int (enum_to_int `Kind_t (``GEQ)))
+let gt = C_int (get_int (enum_to_int `Kind_t (``GT)))
+let mult = C_int (get_int (enum_to_int `Kind_t (``MULT)))
+let plus = C_int (get_int (enum_to_int `Kind_t (``PLUS)))
+let and_kind = C_int (get_int (enum_to_int `Kind_t (``AND)))
+let implies = C_int (get_int (enum_to_int `Kind_t (``IMPLIES)))
+
+(* gt = 35, but the parser screws up if we put "geq" what follows *)
+let x_positive = em->mkExpr(gt, x, zero)
+let y_positive = em->mkExpr(gt, y, zero)
+
+let integerTwo = new_Integer '("2", 10)
+let two = em->mkConst(integerTwo)
+let twox = em->mkExpr(mult, two, x)
+let twox_plus_y = em->mkExpr(plus, twox, y)
+
+let integerThree = new_Integer '("3", 10)
+let three = em->mkConst(integerThree)
+let twox_plus_y_geq_3 = em->mkExpr(geq, twox_plus_y, three)
+
+let lhs = em->mkExpr(and_kind, x_positive, y_positive)
+
+(* This fails for some reason. *)
+(* let rhs = new_BoolExpr(twox_plus_y_geq_3)
+   let formula = new_BoolExpr(lhs)->impExpr(rhs) *)
+
+let formula = em->mkExpr(implies, lhs, twox_plus_y_geq_3)
+
+let bformula = new_BoolExpr(formula) in
+
+print_string "Checking validity of formula " ;
+print_string (get_string (formula->toString ())) ;
+print_string " with CVC4." ;
+print_newline () ;
+print_string "CVC4 should report VALID." ;
+print_newline () ;
+print_string "Result from CVC4 is: " ;
+print_string (get_string (smt->query(bformula)->toString ())) ;
+print_newline ()
+;;
diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c
index 9bcb52280..f45df65f5 100644
--- a/examples/simple_vc_compat_c.c
+++ b/examples/simple_vc_compat_c.c
@@ -21,14 +21,14 @@
 #include <stdio.h>
 #include <stdlib.h>
 
-// #include <cvc4/compat/c_interface.h>
+/* #include <cvc4/compat/c_interface.h> /* use this after CVC4 is properly installed */
 #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
+  /* Prove that for integers x and y:
+   *   x > 0 AND y > 0  =>  2x + y >= 3 */
 
   Type integer = vc_intType(vc);
 
diff --git a/examples/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp
index c178d1aba..0cb99f4be 100644
--- a/examples/simple_vc_compat_cxx.cpp
+++ b/examples/simple_vc_compat_cxx.cpp
@@ -25,7 +25,7 @@
 
 #include <iostream>
 
-// #include <cvc4/compat/cvc3_compat.h>
+// #include <cvc4/compat/cvc3_compat.h> // use this after CVC4 is properly installed
 #include "compat/cvc3_compat.h"
 
 using namespace std;
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 3b5db7c02..819b1fc97 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -20,7 +20,7 @@
 
 #include <iostream>
 
-//#include <cvc4.h>
+//#include <cvc4.h> // use this after CVC4 is properly installed
 #include "smt/smt_engine.h"
 
 using namespace std;