diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-16 14:19:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-16 14:19:16 +0000 |
commit | ebba5e92588a500a7384f7337968758386db7888 (patch) | |
tree | 6a24e20b557e7359c1b10db24aa7cf48a9578974 /examples | |
parent | f55dfd4df98fbecbd0ef0f86da79d537457109d6 (diff) |
Fix "make dist". Fixes to python and ruby bindings; ruby example written. They should both work out of the box, now, with swig 2.0.4 at least. "make install" likely still needs to be adjusted to install them sensibly.
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 + |