diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/README | 6 | ||||
| -rw-r--r-- | examples/SimpleVC.rb | 57 |
2 files changed, 62 insertions, 1 deletions
diff --git a/examples/README b/examples/README index 1ba0a54e6..0861092e7 100644 --- a/examples/README +++ b/examples/README @@ -9,4 +9,8 @@ directory. With the default configuration, you'll find them in builds/examples in the top-level source directory (if you configured your own build directory, you'll find them there). --- Morgan Deters <mdeters@cs.nyu.edu> Fri, 30 Sep 2011 16:19:46 -0400 +Many of the examples (python, ocaml, ruby, etc.) do not need to be +compiled to run. These are not compiled by "make"---see the comments +in the files for ideas on how to run them. + +-- Morgan Deters <mdeters@cs.nyu.edu> Wed, 16 Nov 2011 02:48:19 -0500 diff --git a/examples/SimpleVC.rb b/examples/SimpleVC.rb new file mode 100644 index 000000000..ef4d82983 --- /dev/null +++ b/examples/SimpleVC.rb @@ -0,0 +1,57 @@ +###################### ## +##! \file SimpleVC.rb +### \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 Ruby interface +### +### A simple demonstration of the Ruby interface. Compare to the +### C++ interface in simple_vc_cxx.cpp; they are quite similar. +### +### To run, use something like: +### +### ln -s ../builds/src/bindings/.libs/libcvc4bindings_ruby.so.0.0.0 CVC4.so +### ruby SimpleVC.rb +#### + +require 'CVC4' +include CVC4 # CVC4::Integer still has to be qualified + +em = ExprManager.new +smt = SmtEngine.new(em) + +# Prove that for integers x and y: +# x > 0 AND y > 0 => 2x + y >= 3 + +integer = em.integerType + +x = em.mkVar("x", integer) +y = em.mkVar("y", integer) +zero = em.mkConst(CVC4::Integer.new(0)) + +x_positive = em.mkExpr(GT, x, zero) +y_positive = em.mkExpr(GT, y, zero) + +two = em.mkConst(CVC4::Integer.new(2)) +twox = em.mkExpr(MULT, two, x) +twox_plus_y = em.mkExpr(PLUS, twox, y) + +three = em.mkConst(CVC4::Integer.new(3)) +twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three) + +formula = BoolExpr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(BoolExpr.new(twox_plus_y_geq_3)) + +puts "Checking validity of formula " + formula.toString + " with CVC4." +puts "CVC4 should report VALID." +puts "Result from CVC4 is: " + smt.query(formula).toString + +exit + |