diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-15 22:34:18 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-15 22:34:18 +0000 |
commit | 78af7dfd469b43c17c3ad582a094068484955037 (patch) | |
tree | 2d05cf1390731e1c7fd8d433768c9b436ff60baf /examples | |
parent | 15193d5207679b24cd2f310f71c9428971564b53 (diff) |
Bindings work (ocaml bindings are now sort of working); also minor cleanup
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Makefile.am | 1 | ||||
-rw-r--r-- | examples/SimpleVC.ml | 91 | ||||
-rw-r--r-- | examples/simple_vc_compat_c.c | 6 | ||||
-rw-r--r-- | examples/simple_vc_compat_cxx.cpp | 2 | ||||
-rw-r--r-- | examples/simple_vc_cxx.cpp | 2 |
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; |