examples/SimpleVC.tcl

   1 #! /usr/bin/tclsh
   2 ##! \file SimpleVC.tcl
   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 Tcl interface
  15 ###
  16 ### A simple demonstration of the Tcl 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/tcl/.libs/CVC4.so CVC4.so
  22 ###   ./SimpleVC.tcl
  23 ####
  24
  25 load CVC4.so CVC4
  26
  27 ExprManager em
  28 SmtEngine smt em
  29
  30 # Prove that for integers x and y:
  31 #   x > 0 AND y > 0  =>  2x + y >= 3
  32
  33 set integer [ExprManager_integerType em]
  34
  35 set x [ExprManager_mkVar em "x" $integer]
  36 set y [ExprManager_mkVar em "y" $integer]
  37 set zero [ExprManager_mkConst em [Integer _ 0]]
  38
  39 set x_positive [ExprManager_mkExpr em $GT $x $zero]
  40 set y_positive [ExprManager_mkExpr em $GT $y $zero]
  41
  42 set two [ExprManager_mkConst em [Integer _ 2]]
  43 set twox [ExprManager_mkExpr em $MULT $two $x]
  44 set twox_plus_y [ExprManager_mkExpr em $PLUS $twox $y]
  45
  46 set three [ExprManager_mkConst em [Integer _ 3]]
  47 set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three]
  48
  49 set formula [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]]
  50
  51 puts "Checking validity of formula [Expr_toString $formula] with CVC4."
  52 puts "CVC4 should report VALID."
  53 puts "Result from CVC4 is: [Result_toString [SmtEngine_query smt $formula]]"
  54