From 8406fd17c82dd3caa5d769d07e2c122e937df688 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 16 Aug 2012 01:29:19 +0000 Subject: [PATCH] some fixes for language bindings --- examples/SimpleVC.java | 7 +++---- src/expr/expr_manager.i | 1 - 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index 8159cdc0e..a5e2d4e4f 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -34,7 +34,6 @@ **/ import edu.nyu.acsys.CVC4.*; -import edu.nyu.acsys.CVC4.Integer;// to override java.lang.Integer name lookup public class SimpleVC { public static void main(String[] args) { @@ -50,16 +49,16 @@ public class SimpleVC { Expr x = em.mkVar("x", integer); Expr y = em.mkVar("y", integer); - Expr zero = em.mkConst(new Integer(0)); + Expr zero = em.mkConst(new Rational(0)); Expr x_positive = em.mkExpr(Kind.GT, x, zero); Expr y_positive = em.mkExpr(Kind.GT, y, zero); - Expr two = em.mkConst(new Integer(2)); + Expr two = em.mkConst(new Rational(2)); Expr twox = em.mkExpr(Kind.MULT, two, x); Expr twox_plus_y = em.mkExpr(Kind.PLUS, twox, y); - Expr three = em.mkConst(new Integer(3)); + Expr three = em.mkConst(new Rational(3)); Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three); BoolExpr formula = diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index 375976330..960ba8f84 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -17,7 +17,6 @@ %include "expr/expr_manager.h" -%template(mkConst) CVC4::ExprManager::mkConst< CVC4::Integer >; %template(mkConst) CVC4::ExprManager::mkConst< CVC4::Rational >; %include "expr/expr_manager.h" -- 2.30.2