From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 15 Nov 2011 01:32:27 +0000 (+0000)
Subject: additional minor changes to get python binding on better footing
X-Git-Tag: cvc5-1.0.0~8383
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=15193d5207679b24cd2f310f71c9428971564b53;p=cvc5.git

additional minor changes to get python binding on better footing
---

diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py
index 2a4fc2e5e..545e095f9 100644
--- a/examples/SimpleVC.py
+++ b/examples/SimpleVC.py
@@ -18,17 +18,14 @@
 ###
 ### To run, use something like:
 ###
-###   PYTHONPATH=/dir/containing/CVC4.py:$PYTHONPATH \
-###   python \
-###     -Djava.library.path=/dir/containing/libcvc4bindings_python.so \
-###     SimpleVC
+###   ln -s ../builds/src/bindings/.libs/libcvc4bindings_python.so.0.0.0 _CVC4.so
+###   PYTHONPATH=../builds/src/bindings/python python SimpleVC.py
 ####
 
-from ctypes import cdll
-cdll.LoadLibrary('libcvc4.so')
-cdll.LoadLibrary('libcvc4parser.so')
-cdll.LoadLibrary('libcvc4bindings_python.so')
 import CVC4
+from CVC4 import ExprManager, SmtEngine, Integer, BoolExpr
+
+import sys
 
 def main():
   em = ExprManager()
@@ -43,20 +40,24 @@ def main():
   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)
+  x_positive = em.mkExpr(CVC4.GT, x, zero)
+  y_positive = em.mkExpr(CVC4.GT, y, zero)
 
   two = em.mkConst(Integer(2))
-  twox = em.mkExpr(kind.MULT, two, x)
-  twox_plus_y = em.mkExpr(kind.PLUS, twox, y)
+  twox = em.mkExpr(CVC4.MULT, two, x)
+  twox_plus_y = em.mkExpr(CVC4.PLUS, twox, y)
 
   three = em.mkConst(Integer(3))
-  twox_plus_y_geq_3 = em.mkExpr(kind.GEQ, twox_plus_y, three)
+  twox_plus_y_geq_3 = em.mkExpr(CVC4.GEQ, twox_plus_y, three)
 
-  formula = BoolExpr(em.mkExpr(kind.AND, x_positive, y_positive)).impExpr(BoolExpr(twox_plus_y_geq_3))
+  formula = BoolExpr(em.mkExpr(CVC4.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
+  print "Checking validity of formula " + formula.toString() + " with CVC4."
+  print "CVC4 should report VALID."
+  print "Result from CVC4 is: " + smt.query(formula).toString()
 
   return 0
+
+if __name__ == '__main__':
+  sys.exit(main())
+
diff --git a/src/util/pseudoboolean.cpp b/src/util/pseudoboolean.cpp
index 3fa7a774e..655cd8277 100644
--- a/src/util/pseudoboolean.cpp
+++ b/src/util/pseudoboolean.cpp
@@ -29,7 +29,7 @@ Pseudoboolean::Pseudoboolean(int i) {
   d_value = (i == 1);
 }
 
-Pseudoboolean::Pseudoboolean(const Integer& i) {
+Pseudoboolean::Pseudoboolean(const CVC4::Integer& i) {
   CheckArgument(i == 0 || i == 1, i);
   d_value = (i == 1);
 }
@@ -42,7 +42,7 @@ Pseudoboolean::operator int() const {
   return d_value ? 1 : 0;
 }
 
-Pseudoboolean::operator Integer() const {
+Pseudoboolean::operator CVC4::Integer() const {
   return d_value ? 1 : 0;
 }
 
diff --git a/src/util/pseudoboolean.h b/src/util/pseudoboolean.h
index 6d0d4fd26..03cde2d98 100644
--- a/src/util/pseudoboolean.h
+++ b/src/util/pseudoboolean.h
@@ -31,11 +31,11 @@ class Pseudoboolean {
 public:
   Pseudoboolean(bool b);
   Pseudoboolean(int i);
-  Pseudoboolean(const Integer& i);
+  Pseudoboolean(const CVC4::Integer& i);
 
   operator bool() const;
   operator int() const;
-  operator Integer() const;
+  operator CVC4::Integer() const;
 
 };/* class Pseudoboolean */
 
diff --git a/src/util/pseudoboolean.i b/src/util/pseudoboolean.i
index 2505a7c1e..78c373aa1 100644
--- a/src/util/pseudoboolean.i
+++ b/src/util/pseudoboolean.i
@@ -4,7 +4,7 @@
 
 %rename(toBool) CVC4::Pseudoboolean::operator bool() const;
 %rename(toInt) CVC4::Pseudoboolean::operator int() const;
-%rename(toInteger) CVC4::Pseudoboolean::operator Integer() const;
+%rename(toInteger) CVC4::Pseudoboolean::operator CVC4::Integer() const;
 
 %ignore CVC4::operator<<(std::ostream&, CVC4::Pseudoboolean);