diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-15 01:03:34 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-15 01:03:34 +0000 |
commit | 3d3d6490f46f9dd7b48b02eed03a66086e32ded1 (patch) | |
tree | 7b5fa31f7efb1a1d15718a333ea01d01bf5216c0 /examples | |
parent | db91d5e5ad954b7a25eddd4a3e075584abc8bee3 (diff) |
fixes for python language binding, added python example
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Makefile.am | 1 | ||||
-rw-r--r-- | examples/SimpleVC.py | 62 |
2 files changed, 63 insertions, 0 deletions
diff --git a/examples/Makefile.am b/examples/Makefile.am index 3e05d480d..f72c20d02 100644 --- a/examples/Makefile.am +++ b/examples/Makefile.am @@ -51,6 +51,7 @@ SimpleVCCompat.class: SimpleVCCompat.java EXTRA_DIST = \ SimpleVC.java \ + SimpleVC.py \ SimpleVCCompat.java \ README diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py new file mode 100644 index 000000000..2a4fc2e5e --- /dev/null +++ b/examples/SimpleVC.py @@ -0,0 +1,62 @@ +###################### ## +##! \file SimpleVC.py +### \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 Python interface +### +### A simple demonstration of the Python interface. Compare to the +### C++ interface in simple_vc_cxx.cpp; they are quite similar. +### +### To run, use something like: +### +### PYTHONPATH=/dir/containing/CVC4.py:$PYTHONPATH \ +### python \ +### -Djava.library.path=/dir/containing/libcvc4bindings_python.so \ +### SimpleVC +#### + +from ctypes import cdll +cdll.LoadLibrary('libcvc4.so') +cdll.LoadLibrary('libcvc4parser.so') +cdll.LoadLibrary('libcvc4bindings_python.so') +import CVC4 + +def main(): + em = ExprManager() + smt = SmtEngine(em) + + # Prove that for integers x and y: + # x > 0 AND y > 0 => 2x + y >= 3 + + integer = em.integerType() + + x = em.mkVar("x", integer) + y = em.mkVar("y", integer) + zero = em.mkConst(Integer(0)) + + x_positive = em.mkExpr(kind.GT, x, zero) + y_positive = em.mkExpr(kind.GT, y, zero) + + two = em.mkConst(Integer(2)) + twox = em.mkExpr(kind.MULT, two, x) + twox_plus_y = em.mkExpr(kind.PLUS, twox, y) + + three = em.mkConst(Integer(3)) + twox_plus_y_geq_3 = em.mkExpr(kind.GEQ, twox_plus_y, three) + + formula = BoolExpr(em.mkExpr(kind.AND, x_positive, y_positive)).impExpr(BoolExpr(twox_plus_y_geq_3)) + + print "Checking validity of formula " << formula << " with CVC4." << endl + print "CVC4 should report VALID." << endl + print "Result from CVC4 is: " << smt.query(formula) << endl + + return 0 |