diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-11-15 01:32:27 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-11-15 01:32:27 +0000 |
| commit | 15193d5207679b24cd2f310f71c9428971564b53 (patch) | |
| tree | 65407ed8821be30b91ae898a93f1b78902cc37c4 /examples | |
| parent | 3d3d6490f46f9dd7b48b02eed03a66086e32ded1 (diff) | |
additional minor changes to get python binding on better footing
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/SimpleVC.py | 35 |
1 files changed, 18 insertions, 17 deletions
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()) + |