blob: 4e1c76c5a90374623a95d7004c102409aa444549 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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 [Expr_impExpr [Expr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [Expr _2 $twox_plus_y_geq_3]]
puts "Checking entailment of formula [Expr_toString $formula] with CVC4."
puts "CVC4 should report ENTAILED."
puts "Result from CVC4 is: [Result_toString [SmtEngine_checkEntailed smt $formula]]"
|
