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]]"
+