From 3d3d6490f46f9dd7b48b02eed03a66086e32ded1 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 15 Nov 2011 01:03:34 +0000
Subject: [PATCH] fixes for python language binding, added python example

---
 examples/Makefile.am |  1 +
 examples/SimpleVC.py | 62 ++++++++++++++++++++++++++++++++++++++++++++
 src/util/datatype.i  |  2 ++
 3 files changed, 65 insertions(+)
 create mode 100644 examples/SimpleVC.py

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
diff --git a/src/util/datatype.i b/src/util/datatype.i
index 510b73225..23782aa28 100644
--- 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 >;
 
-- 
2.30.2