fixes for python language binding, added python example

diff --git a/examples/Makefile.am b/examples/Makefile.am
index 3e05d480df8182d39d62ae3ccb233e0a4520bd51..f72c20d0208060c2f5142a86c4951ee3ca55360b 100644 (file)
--- 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 (file)
index 0000000..2a4fc2e
--- /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

diff --git a/src/util/datatype.i b/src/util/datatype.i
index 510b73225a734bdee95d62c3bc5d60eb8ac8c87a..23782aa2879ca01bbe1b18c8ac921c0e78dc12c1 100644 (file)
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -9,11 +9,13 @@ namespace CVC4 {
 
 %extend std::vector< CVC4::Datatype > {
   %ignore vector(size_type);
+  %ignore resize(size_type);
 };
 %template(vectorDatatype) std::vector< CVC4::Datatype >;
 
 %extend std::vector< CVC4::Datatype::Constructor > {
   %ignore vector(size_type);
+  %ignore resize(size_type);
 };
 %template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >;