diff options
Diffstat (limited to 'examples/SimpleVC.tcl')
-rwxr-xr-x | examples/SimpleVC.tcl | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/examples/SimpleVC.tcl b/examples/SimpleVC.tcl new file mode 100755 index 000000000..d2030f044 --- /dev/null +++ b/examples/SimpleVC.tcl @@ -0,0 +1,54 @@ +#! /usr/bin/tclsh +##! \file SimpleVC.tcl +### \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 Tcl interface +### +### A simple demonstration of the Tcl 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/tcl/.libs/CVC4.so CVC4.so +### ./SimpleVC.tcl +#### + +load CVC4.so CVC4 + +ExprManager em +SmtEngine smt em + +# Prove that for integers x and y: +# x > 0 AND y > 0 => 2x + y >= 3 + +set integer [ExprManager_integerType em] + +set x [ExprManager_mkVar em "x" $integer] +set y [ExprManager_mkVar em "y" $integer] +set zero [ExprManager_mkConst em [Integer _ 0]] + +set x_positive [ExprManager_mkExpr em $GT $x $zero] +set y_positive [ExprManager_mkExpr em $GT $y $zero] + +set two [ExprManager_mkConst em [Integer _ 2]] +set twox [ExprManager_mkExpr em $MULT $two $x] +set twox_plus_y [ExprManager_mkExpr em $PLUS $twox $y] + +set three [ExprManager_mkConst em [Integer _ 3]] +set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three] + +set formula [BoolExpr_impExpr [BoolExpr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [BoolExpr _2 $twox_plus_y_geq_3]] + +puts "Checking validity of formula [Expr_toString $formula] with CVC4." +puts "CVC4 should report VALID." +puts "Result from CVC4 is: [Result_toString [SmtEngine_query smt $formula]]" + |