diff options
| -rw-r--r-- | src/compat/cvc3_compat.cpp | 8 | ||||
| -rw-r--r-- | src/expr/expr.i | 4 | ||||
| -rw-r--r-- | src/util/emptyset.h | 52 |
3 files changed, 44 insertions, 20 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 427282490..dd9fcdfbd 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -341,6 +341,14 @@ bool Expr::isBoundVar() const { return getKind() == CVC4::kind::BOUND_VARIABLE; } +bool Expr::isForall() const { + return getKind() == CVC4::kind::FORALL; +} + +bool Expr::isExists() const { + return getKind() == CVC4::kind::EXISTS; +} + bool Expr::isLambda() const { // when implemented, also fix isClosure() below Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); diff --git a/src/expr/expr.i b/src/expr/expr.i index c649a5ebb..31788f06b 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -104,7 +104,9 @@ namespace CVC4 { %template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>; %template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>; %template(getConstPredicate) CVC4::Expr::getConst<CVC4::Predicate>; -%template(getConstString) CVC4::Expr::getConst<std::string>; +%template(getConstString) CVC4::Expr::getConst<CVC4::String>; +%template(getConstRegExp) CVC4::Expr::getConst<CVC4::RegExp>; +%template(getConstEmptySet) CVC4::Expr::getConst<CVC4::EmptySet>; %template(getConstBoolean) CVC4::Expr::getConst<bool>; #ifdef SWIGJAVA diff --git a/src/util/emptyset.h b/src/util/emptyset.h index 2d307b2d4..2f6c54173 100644 --- a/src/util/emptyset.h +++ b/src/util/emptyset.h @@ -1,3 +1,19 @@ +/********************* */ +/*! \file emptyset.h + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #include "cvc4_public.h" @@ -30,36 +46,34 @@ public: SetType getType() const { return d_type; } - bool operator==(const EmptySet& asa) const throw() { - return d_type == asa.d_type; + bool operator==(const EmptySet& es) const throw() { + return d_type == es.d_type; } - bool operator!=(const EmptySet& asa) const throw() { - return !(*this == asa); + bool operator!=(const EmptySet& es) const throw() { + return !(*this == es); } - bool operator<(const EmptySet& asa) const throw() { - return d_type < asa.d_type; + bool operator<(const EmptySet& es) const throw() { + return d_type < es.d_type; } - bool operator<=(const EmptySet& asa) const throw() { - return d_type <= asa.d_type; + bool operator<=(const EmptySet& es) const throw() { + return d_type <= es.d_type; } - bool operator>(const EmptySet& asa) const throw() { - return !(*this <= asa); + bool operator>(const EmptySet& es) const throw() { + return !(*this <= es); } - bool operator>=(const EmptySet& asa) const throw() { - return !(*this < asa); + bool operator>=(const EmptySet& es) const throw() { + return !(*this < es); } - };/* class EmptySet */ -std::ostream& operator<<(std::ostream& out, const EmptySet& asa) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC; struct CVC4_PUBLIC EmptySetHashFunction { - inline size_t operator()(const EmptySet& asa) const { - return TypeHashFunction()(asa.getType()); + inline size_t operator()(const EmptySet& es) const { + return TypeHashFunction()(es.getType()); } -};/* struct EmptysetHashFunction */ - +};/* struct EmptySetHashFunction */ -} +}/* CVC4 namespace */ |