diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-26 14:39:56 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-26 14:39:56 +0000 |
commit | d4de9caf21439e5b34b0b254e6de7a97c67817b5 (patch) | |
tree | a4831ddf25abc235d01a4a4f78ec27e106309dde /examples/SimpleVC.py | |
parent | 945fb9f4c3ab671d47748a3a021a8481b705beac (diff) |
some fixes to language bindings and function visibility
Diffstat (limited to 'examples/SimpleVC.py')
-rwxr-xr-x | examples/SimpleVC.py | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py index a1cd1a6bd..18be0fdc0 100755 --- a/examples/SimpleVC.py +++ b/examples/SimpleVC.py @@ -24,7 +24,7 @@ #### import CVC4 -from CVC4 import ExprManager, SmtEngine, Integer, Expr +from CVC4 import ExprManager, SmtEngine, Rational, Expr import sys @@ -39,16 +39,16 @@ def main(): x = em.mkVar("x", integer) y = em.mkVar("y", integer) - zero = em.mkConst(Integer(0)) + zero = em.mkConst(Rational(0)) x_positive = em.mkExpr(CVC4.GT, x, zero) y_positive = em.mkExpr(CVC4.GT, y, zero) - two = em.mkConst(Integer(2)) + two = em.mkConst(Rational(2)) twox = em.mkExpr(CVC4.MULT, two, x) twox_plus_y = em.mkExpr(CVC4.PLUS, twox, y) - three = em.mkConst(Integer(3)) + three = em.mkConst(Rational(3)) twox_plus_y_geq_3 = em.mkExpr(CVC4.GEQ, twox_plus_y, three) formula = Expr(em.mkExpr(CVC4.AND, x_positive, y_positive)).impExpr(Expr(twox_plus_y_geq_3)) |