examples/SimpleVC.rb

   1 #! /usr/bin/ruby
   2 ##! \file SimpleVC.rb
   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 Ruby interface
  15 ###
  16 ### A simple demonstration of the Ruby 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 ###   ln -s ../builds/src/bindings/ruby/.libs/CVC4.so CVC4.so
  22 ###   ./SimpleVC.rb
  23 ####
  24
  25 require 'CVC4'
  26 include CVC4 # CVC4::Integer still has to be qualified
  27
  28 em = ExprManager.new
  29 smt = SmtEngine.new(em)
  30
  31 # Prove that for integers x and y:
  32 #   x > 0 AND y > 0  =>  2x + y >= 3
  33
  34 integer = em.integerType
  35
  36 x = em.mkVar("x", integer)
  37 y = em.mkVar("y", integer)
  38 zero = em.mkConst(CVC4::Integer.new(0))
  39
  40 x_positive = em.mkExpr(GT, x, zero)
  41 y_positive = em.mkExpr(GT, y, zero)
  42
  43 two = em.mkConst(CVC4::Integer.new(2))
  44 twox = em.mkExpr(MULT, two, x)
  45 twox_plus_y = em.mkExpr(PLUS, twox, y)
  46
  47 three = em.mkConst(CVC4::Integer.new(3))
  48 twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three)
  49
  50 formula = Expr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(Expr.new(twox_plus_y_geq_3))
  51
  52 puts "Checking entailment of formula " + formula.toString + " with CVC4."
  53 puts "CVC4 should report ENTAILED."
  54 puts "Result from CVC4 is: " + smt.checkEntailed(formula).toString
  55
  56 exit
  57