From d4de9caf21439e5b34b0b254e6de7a97c67817b5 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 26 Nov 2012 14:39:56 +0000 Subject: [PATCH] some fixes to language bindings and function visibility --- examples/SimpleVC.py | 8 ++++---- src/parser/input.h | 4 ++-- src/smt/smt_engine.i | 1 + 3 files changed, 7 insertions(+), 6 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)) diff --git a/src/parser/input.h b/src/parser/input.h index 586b35231..0203ed806 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -45,7 +45,7 @@ public: }; /** Wrapper around an input stream. */ -class InputStream { +class CVC4_PUBLIC InputStream { /** The name of this input stream. */ std::string d_name; @@ -73,7 +73,7 @@ public: /** Get the name of this input stream. */ const std::string getName() const; -}; +};/* class InputStream */ class Parser; diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i index 7fdb59467..c53bb8ce5 100644 --- a/src/smt/smt_engine.i +++ b/src/smt/smt_engine.i @@ -4,5 +4,6 @@ %ignore CVC4::SmtEngine::getProof; %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*); +%ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*); %include "smt/smt_engine.h" -- 2.30.2