examples/SimpleVC.ml

   1 (*********************                                                        **
   2 **! \file SimpleVC.ml
   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 OCaml interface
  15 ***
  16 *** A simple demonstration of the OCaml interface.  Compare to the
  17 *** C++ interface in simple_vc_cxx.cpp; they are quite similar.
  18 ***
  19 *** To run, use something like:
  20 ***
  21 ***   LD_LIBRARY_PATH=../builds/src/bindings/ocaml/.libs \
  22 ***     ../builds/src/bindings/cvc4_ocaml_top -I ../builds/src/bindings/ocaml \
  23 ***     SimpleVC.ml
  24 ***
  25 *** After you "make install" CVC4, it's much easier; the cvc4_ocaml_top goes in
  26 *** $prefix/bin, and it's automatically set up the load the .cmo and .cmi files
  27 *** from $prefix/lib/ocaml/cvc4, in which they get installed.  Then you just
  28 *** have to: cvc4_ocaml_top -I $prefix/lib/ocaml/cvc4
  29 ***)
  30
  31 open Swig
  32 open CVC4
  33
  34 let em = new_ExprManager '()
  35 let smt = new_SmtEngine(em)
  36
  37 (* Prove that for integers x and y:
  38  *   x > 0 AND y > 0  =>  2x + y >= 3 *)
  39
  40 let integer = em->integerType()
  41
  42 let x = em->mkVar(integer) (* em->mkVar("x", integer) *)
  43 let y = em->mkVar(integer) (* em->mkVar("y", integer) *)
  44 let integerZero = new_Integer '("0", 10)
  45 let zero = em->mkConst(integerZero)
  46
  47 (* OK, this is really strange.  We can call mkExpr(36, ...) for
  48  * example, with the int value of the operator Kind we want,
  49  * or we can compute it.  But if we compute it, we have to rip
  50  * it out of its C_int, then wrap it again a C_int, in order
  51  * for the parser to make it go through. *)
  52 let geq = C_int (get_int (enum_to_int `Kind_t (``GEQ)))
  53 let gt = C_int (get_int (enum_to_int `Kind_t (``GT)))
  54 let mult = C_int (get_int (enum_to_int `Kind_t (``MULT)))
  55 let plus = C_int (get_int (enum_to_int `Kind_t (``PLUS)))
  56 let and_kind = C_int (get_int (enum_to_int `Kind_t (``AND)))
  57 let implies = C_int (get_int (enum_to_int `Kind_t (``IMPLIES)))
  58
  59 (* gt = 35, but the parser screws up if we put "geq" what follows *)
  60 let x_positive = em->mkExpr(gt, x, zero)
  61 let y_positive = em->mkExpr(gt, y, zero)
  62
  63 let integerTwo = new_Integer '("2", 10)
  64 let two = em->mkConst(integerTwo)
  65 let twox = em->mkExpr(mult, two, x)
  66 let twox_plus_y = em->mkExpr(plus, twox, y)
  67
  68 let integerThree = new_Integer '("3", 10)
  69 let three = em->mkConst(integerThree)
  70 let twox_plus_y_geq_3 = em->mkExpr(geq, twox_plus_y, three)
  71
  72 let lhs = em->mkExpr(and_kind, x_positive, y_positive)
  73
  74 (* This fails for some reason. *)
  75 (* let rhs = new_Expr(twox_plus_y_geq_3)
  76    let formula = new_Expr(lhs)->impExpr(rhs) *)
  77
  78 let formula = em->mkExpr(implies, lhs, twox_plus_y_geq_3)
  79
  80 let bformula = new_Expr(formula) in
  81
  82 print_string "Checking validity of formula " ;
  83 print_string (get_string (formula->toString ())) ;
  84 print_string " with CVC4." ;
  85 print_newline () ;
  86 print_string "CVC4 should report VALID." ;
  87 print_newline () ;
  88 print_string "Result from CVC4 is: " ;
  89 print_string (get_string (smt->query(bformula)->toString ())) ;
  90 print_newline ()
  91 ;;