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/SimpleVC.rb | |
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/SimpleVC.rb')
-rw-r--r-- | examples/SimpleVC.rb | 57 |
1 files changed, 57 insertions, 0 deletions
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 + |