From c241cf3bef737a58162868d51a2c773c5af5abbf Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 20 Sep 2011 14:58:30 +0000 Subject: [PATCH] Merge from "swig" branch: language binding for Java is compiling and linking. Enable with --enable-language-bindings=java --- config/bindings.m4 | 2 +- library_versions | 14 ++++++++- src/Makefile.am | 5 +-- src/bindings/Makefile.am | 47 +++++++++++++++++----------- src/bindings/swig.h | 38 ++++++++++++++++++++++ src/cvc4.i | 42 +++++++++++++++++++++++++ src/expr/Makefile.am | 8 ++++- src/expr/command.i | 12 +++++++ src/expr/declaration_scope.i | 5 +++ src/expr/expr.i | 25 +++++++++++++++ src/expr/expr_manager.i | 5 +++ src/expr/kind.i | 11 +++++++ src/expr/type.cpp | 14 ++++++++- src/expr/type.h | 19 +++++++++-- src/expr/type.i | 33 +++++++++++++++++++ src/expr/type_node.h | 35 ++++++++++++++++++++- src/smt/Makefile.am | 6 ++++ src/smt/bad_option_exception.i | 5 +++ src/smt/modal_exception.i | 5 +++ src/smt/no_such_function_exception.i | 5 +++ src/smt/smt_engine.h | 20 ------------ src/smt/smt_engine.i | 5 +++ src/util/Assert.i | 5 +++ src/util/Makefile.am | 22 ++++++++++++- src/util/array.i | 5 +++ src/util/ascription_type.i | 11 +++++++ src/util/bitvector.i | 28 +++++++++++++++++ src/util/bool.i | 5 +++ src/util/cardinality.h | 5 --- src/util/cardinality.i | 23 ++++++++++++++ src/util/configuration.i | 5 +++ src/util/datatype.i | 22 +++++++++++++ src/util/exception.h | 9 ++++-- src/util/exception.i | 7 +++++ src/util/hash.h | 3 ++ src/util/hash.i | 5 +++ src/util/integer.h.in | 6 ---- src/util/integer.i | 29 +++++++++++++++++ src/util/language.i | 10 ++++++ src/util/matcher.h | 2 +- src/util/options.i | 9 ++++++ src/util/output.h | 4 +++ src/util/output.i | 10 ++++++ src/util/pseudoboolean.i | 11 +++++++ src/util/rational.h.in | 6 ---- src/util/rational.i | 29 +++++++++++++++++ src/util/rational_cln_imp.h | 5 +++ src/util/rational_gmp_imp.h | 5 +++ src/util/result.i | 14 +++++++++ src/util/sexpr.i | 7 +++++ src/util/stats.i | 21 +++++++++++++ src/util/subrange_bound.i | 10 ++++++ 52 files changed, 625 insertions(+), 69 deletions(-) create mode 100644 src/bindings/swig.h create mode 100644 src/cvc4.i create mode 100644 src/expr/command.i create mode 100644 src/expr/declaration_scope.i create mode 100644 src/expr/expr.i create mode 100644 src/expr/expr_manager.i create mode 100644 src/expr/kind.i create mode 100644 src/expr/type.i create mode 100644 src/smt/bad_option_exception.i create mode 100644 src/smt/modal_exception.i create mode 100644 src/smt/no_such_function_exception.i create mode 100644 src/smt/smt_engine.i create mode 100644 src/util/Assert.i create mode 100644 src/util/array.i create mode 100644 src/util/ascription_type.i create mode 100644 src/util/bitvector.i create mode 100644 src/util/bool.i create mode 100644 src/util/cardinality.i create mode 100644 src/util/configuration.i create mode 100644 src/util/datatype.i create mode 100644 src/util/exception.i create mode 100644 src/util/hash.i create mode 100644 src/util/integer.i create mode 100644 src/util/language.i create mode 100644 src/util/options.i create mode 100644 src/util/output.i create mode 100644 src/util/pseudoboolean.i create mode 100644 src/util/rational.i create mode 100644 src/util/result.i create mode 100644 src/util/sexpr.i create mode 100644 src/util/stats.i create mode 100644 src/util/subrange_bound.i diff --git a/config/bindings.m4 b/config/bindings.m4 index cdab33e3e..8231411ed 100644 --- a/config/bindings.m4 +++ b/config/bindings.m4 @@ -58,7 +58,7 @@ else c++) AC_MSG_RESULT([C++ is built by default]);; java) JAVA_INCLUDES="-I/usr/lib/jvm/java-6-sun-1.6.0.26/include -I/usr/lib/jvm/java-6-sun-1.6.0.26/include/linux" - cvc4_build_java_binding=yes + cvc4_build_java_bindings=yes AC_MSG_RESULT([Java support will be built]);; csharp) binding_error=yes diff --git a/library_versions b/library_versions index d344bc763..2ff790479 100644 --- a/library_versions +++ b/library_versions @@ -1,4 +1,7 @@ -# Format is CVC4-RELEASE-VERSION-REGEXP (LIBRARY:VERSION)* +# library_versions +# +# Format is: +# CVC4-RELEASE-VERSION-REGEXP (LIBRARY:VERSION)* # # This file contains library version release information. # Lines are matched while processing configure.ac (and generating @@ -8,5 +11,14 @@ # column, are then used. If there are no matching lines, an error # is raised and the configure script is not generated. # +# When a new CVC4 release is cut, this library_versions file should +# be extended to provide library version information for that +# release. PLEASE DON'T REMOVE LINES (or edit historical lines) +# from this file unless they are truly in error and the release +# wasn't made with that erroneous information; this file should +# ultimately provide a nice historical log of the mapping between +# CVC4 release numbers and the corresponding interface version +# information of libraries. +# 0\..* libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0 1\.0 libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0 diff --git a/src/Makefile.am b/src/Makefile.am index e6c00c943..199accf85 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -17,7 +17,7 @@ AM_CPPFLAGS = \ -I@srcdir@/include -I@srcdir@ -I@builddir@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = lib expr util context theory prop smt printer bindings . parser compat main +SUBDIRS = lib expr util context theory prop smt printer . parser compat bindings main lib_LTLIBRARIES = libcvc4.la if HAVE_CXXTESTGEN @@ -57,7 +57,8 @@ EXTRA_DIST = \ include/cvc4parser_private.h \ include/cvc4parser_public.h \ include/cvc4_private.h \ - include/cvc4_public.h + include/cvc4_public.h \ + cvc4.i subversion_versioninfo.cpp: svninfo $(AM_V_GEN)( \ diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index cd314f957..7c4d7c5a3 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -4,8 +4,10 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) lib_LTLIBRARIES = +data_DATA = if CVC4_LANGUAGE_BINDING_JAVA lib_LTLIBRARIES += libcvc4bindings_java.la +data_DATA += cvc4.jar endif # cvc4bindings_csharp.so \ # cvc4bindings_perl.so \ @@ -36,23 +38,30 @@ BUILT_SOURCES = \ CLEANFILES = \ $(BUILT_SOURCES) \ - cvc4.java \ - cvc4.cs \ - cvc4JNI.java \ - cvc4.php \ - cvc4PINVOKE.cs \ - cvc4.pm \ - cvc4.py \ - php_cvc4.h + .swig_deps \ + $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \ + cvc4.jar -java.lo: java.cpp; $(LTCXXCOMPILE) $(JAVA_INCLUDES) -o $@ $< -java.cpp:: -csharp.cpp:: -perl.cpp:: -php.cpp:: -python.cpp:: -ocaml.cpp:: -ruby.cpp:: -tcl.cpp:: -$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))):: %.cpp: @srcdir@/../smt/smt_engine.h - $(AM_V_GEN)$(SWIG) -w503 -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -module cvc4 -c++ -$(patsubst %.cpp,%,$@) -o $@ $< +java.lo: java.cpp; $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $< +cvc4.jar: java.cpp; $(AM_V_GEN)jar cf $@ -C java . +java.cpp: +csharp.cpp: +perl.cpp: +php.cpp: +python.cpp: +ocaml.cpp: +ruby.cpp: +tcl.cpp: +$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i + $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@) + $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -module cvc4 -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys -o $@ $< + +$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i + $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -module cvc4 -c++ -MM -o $(patsubst %.d,%.cpp,$@) $< +# .PHONY so they get rebuilt each time +.PHONY: .swig_deps $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) +.swig_deps: $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) + $(AM_V_GEN)cat $+ >$@ +@mk_include@ .swig_deps + +clean-local:; rm -fr $(patsubst %.cpp,%,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) diff --git a/src/bindings/swig.h b/src/bindings/swig.h new file mode 100644 index 000000000..7dec263f6 --- /dev/null +++ b/src/bindings/swig.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file swig.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Common swig checks and definitions + ** + ** Common swig checks and definitions, when generating swig interfaces. + **/ + +#ifndef __CVC4__BINDINGS__SWIG_H +#define __CVC4__BINDINGS__SWIG_H + +#ifndef SWIG +# error This file should only be included when generating swig interfaces. +#endif /* SWIG */ + +#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x020000 +# error CVC4 bindings require swig version 2.0.0 or later, sorry. +#endif /* SWIG_VERSION */ + +%import "cvc4_public.h" +%import "util/tls.h" + +// swig doesn't like the __thread storage class... +#define __thread +// ...or GCC attributes +#define __attribute__(x) + +#endif /* __CVC4__BINDINGS__SWIG_H */ diff --git a/src/cvc4.i b/src/cvc4.i new file mode 100644 index 000000000..4c574f16c --- /dev/null +++ b/src/cvc4.i @@ -0,0 +1,42 @@ +%import "bindings/swig.h" + +%module cvc4 +%nspace; + +%{ +namespace CVC4 {} +using namespace CVC4; +%} + +%include "util/integer.i" +%include "util/rational.i" +%include "util/exception.i" +%include "util/language.i" +%include "util/options.i" +%include "util/cardinality.i" +%include "util/stats.i" +%include "util/bool.i" +%include "util/sexpr.i" +%include "util/datatype.i" +%include "util/output.i" +%include "util/result.i" +%include "util/configuration.i" +%include "util/Assert.i" +%include "util/bitvector.i" +%include "util/subrange_bound.i" +%include "util/array.i" +%include "util/ascription_type.i" +%include "util/pseudoboolean.i" +%include "util/hash.i" + +%include "expr/command.i" +%include "expr/declaration_scope.i" +%include "expr/kind.i" +%include "expr/type.i" +%include "expr/expr.i" +%include "expr/expr_manager.i" + +%include "smt/smt_engine.i" +%include "smt/bad_option_exception.i" +%include "smt/no_such_function_exception.i" +%include "smt/modal_exception.i" diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 738604f90..03de15706 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -52,7 +52,13 @@ EXTRA_DIST = \ type_checker_template.cpp \ mkkind \ mkmetakind \ - mkexpr + mkexpr \ + expr_manager.i \ + declaration_scope.i \ + command.i \ + type.i \ + kind.i \ + expr.i BUILT_SOURCES = \ kind.h \ diff --git a/src/expr/command.i b/src/expr/command.i new file mode 100644 index 000000000..3a029b785 --- /dev/null +++ b/src/expr/command.i @@ -0,0 +1,12 @@ +%{ +#include "expr/command.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const Command&); +%ignore CVC4::operator<<(std::ostream&, const Command*); +%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status); + +%rename(beginConst) CVC4::CommandSequence::begin() const; +%rename(endConst) CVC4::CommandSequence::end() const; + +%include "expr/command.h" diff --git a/src/expr/declaration_scope.i b/src/expr/declaration_scope.i new file mode 100644 index 000000000..e32c4ee4f --- /dev/null +++ b/src/expr/declaration_scope.i @@ -0,0 +1,5 @@ +%{ +#include "expr/declaration_scope.h" +%} + +%include "expr/declaration_scope.h" diff --git a/src/expr/expr.i b/src/expr/expr.i new file mode 100644 index 000000000..ff4d219a2 --- /dev/null +++ b/src/expr/expr.i @@ -0,0 +1,25 @@ +%{ +#include "expr/expr.h" +%} + +%rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const; + +%ignore CVC4::operator<<(std::ostream&, const Expr&); +%ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&); + +%ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth); +%ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes); +%ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage); + +%rename(assign) CVC4::Expr::operator=(const Expr&); +%rename(equals) CVC4::Expr::operator==(const Expr&) const; +%ignore CVC4::Expr::operator!=(const Expr&) const; +%rename(less) CVC4::Expr::operator<(const Expr&) const; +%rename(lessEqual) CVC4::Expr::operator<=(const Expr&) const; +%rename(greater) CVC4::Expr::operator>(const Expr&) const; +%rename(greaterEqual) CVC4::Expr::operator>=(const Expr&) const; + +%rename(getChild) CVC4::Expr::operator[](unsigned i) const; +%ignore CVC4::Expr::operator bool() const;// can just use isNull() + +%include "expr/expr.h" diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i new file mode 100644 index 000000000..739da614a --- /dev/null +++ b/src/expr/expr_manager.i @@ -0,0 +1,5 @@ +%{ +#include "expr/expr_manager.h" +%} + +%include "expr/expr_manager.h" diff --git a/src/expr/kind.i b/src/expr/kind.i new file mode 100644 index 000000000..1c17f3ff9 --- /dev/null +++ b/src/expr/kind.i @@ -0,0 +1,11 @@ +%{ +#include "expr/kind.h" +%} + +%ignore CVC4::kind::operator<<(std::ostream&, CVC4::Kind); +%ignore CVC4::operator<<(std::ostream&, TypeConstant); +%ignore CVC4::theory::operator<<(std::ostream&, TheoryId); + +%ignore CVC4::theory::operator++(TheoryId&); + +%include "expr/kind.h" diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 28bcb460f..ff47c6eae 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -114,6 +114,18 @@ bool Type::operator<(const Type& t) const { return *d_typeNode < *t.d_typeNode; } +bool Type::operator<=(const Type& t) const { + return *d_typeNode <= *t.d_typeNode; +} + +bool Type::operator>(const Type& t) const { + return *d_typeNode > *t.d_typeNode; +} + +bool Type::operator>=(const Type& t) const { + return *d_typeNode >= *t.d_typeNode; +} + Type Type::substitute(const Type& type, const Type& replacement) const { NodeManagerScope nms(d_nodeManager); return makeType(d_typeNode->substitute(*type.d_typeNode, @@ -610,7 +622,7 @@ BooleanType TesterType::getRangeType() const { return BooleanType(makeType(d_nodeManager->booleanType())); } -size_t TypeHashFunction::operator()(const Type& t) { +size_t TypeHashFunction::operator()(const Type& t) const { return TypeNodeHashFunction()(NodeManager::fromType(t)); } diff --git a/src/expr/type.h b/src/expr/type.h index 5bff8d12a..f470f0874 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -63,7 +63,7 @@ class Type; /** Strategy for hashing Types */ struct CVC4_PUBLIC TypeHashFunction { /** Return a hash code for type t */ - size_t operator()(const CVC4::Type& t); + size_t operator()(const CVC4::Type& t) const; };/* struct TypeHashFunction */ /** @@ -84,7 +84,7 @@ class CVC4_PUBLIC Type { friend class NodeManager; friend class TypeNode; friend struct TypeHashStrategy; - friend std::ostream& operator<<(std::ostream& out, const Type& t); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t); protected: @@ -190,6 +190,21 @@ public: */ bool operator<(const Type& t) const; + /** + * An ordering on Types so they can be stored in maps, etc. + */ + bool operator<=(const Type& t) const; + + /** + * An ordering on Types so they can be stored in maps, etc. + */ + bool operator>(const Type& t) const; + + /** + * An ordering on Types so they can be stored in maps, etc. + */ + bool operator>=(const Type& t) const; + /** * Is this the Boolean type? * @return true if the type is a Boolean type diff --git a/src/expr/type.i b/src/expr/type.i new file mode 100644 index 000000000..314903342 --- /dev/null +++ b/src/expr/type.i @@ -0,0 +1,33 @@ +%{ +#include "expr/type.h" +%} + +%rename(apply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const; + +%ignore CVC4::operator<<(std::ostream&, const Type&); + +%rename(assign) CVC4::Type::operator=(const Type&); +%rename(equals) CVC4::Type::operator==(const Type&) const; +%ignore CVC4::Type::operator!=(const Type&) const; +%rename(less) CVC4::Type::operator<(const Type&) const; +%rename(lessEqual) CVC4::Type::operator<=(const Type&) const; +%rename(greater) CVC4::Type::operator>(const Type&) const; +%rename(greaterEqual) CVC4::Type::operator>=(const Type&) const; + +%rename(toBooleanType) CVC4::Type::operator BooleanType() const; +%rename(toIntegerType) CVC4::Type::operator IntegerType() const; +%rename(toRealType) CVC4::Type::operator RealType() const; +%rename(toPseudobooleanType) CVC4::Type::operator PseudobooleanType() const; +%rename(toBitVectorType) CVC4::Type::operator BitVectorType() const; +%rename(toFunctionType) CVC4::Type::operator FunctionType() const; +%rename(toTupleType) CVC4::Type::operator TupleType() const; +%rename(toArrayType) CVC4::Type::operator ArrayType() const; +%rename(toDatatypeType) CVC4::Type::operator DatatypeType() const; +%rename(toConstructorType) CVC4::Type::operator ConstructorType() const; +%rename(toSelectorType) CVC4::Type::operator SelectorType() const; +%rename(toTesterType) CVC4::Type::operator TesterType() const; +%rename(toSortType) CVC4::Type::operator SortType() const; +%rename(toSortConstructorType) CVC4::Type::operator SortConstructorType() const; +%rename(toKindType) CVC4::Type::operator KindType() const; + +%include "expr/type.h" diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 25af3aae6..966611764 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -179,12 +179,45 @@ public: * that subexpressions have to be smaller than the enclosing expressions. * * @param typeNode the node to compare to - * @return true if this expression is smaller + * @return true if this expression is lesser */ inline bool operator<(const TypeNode& typeNode) const { return d_nv->d_id < typeNode.d_nv->d_id; } + /** + * We compare by expression ids so, keeping things deterministic and having + * that subexpressions have to be smaller than the enclosing expressions. + * + * @param typeNode the node to compare to + * @return true if this expression is lesser or equal + */ + inline bool operator<=(const TypeNode& typeNode) const { + return d_nv->d_id <= typeNode.d_nv->d_id; + } + + /** + * We compare by expression ids so, keeping things deterministic and having + * that subexpressions have to be smaller than the enclosing expressions. + * + * @param typeNode the node to compare to + * @return true if this expression is greater + */ + inline bool operator>(const TypeNode& typeNode) const { + return d_nv->d_id > typeNode.d_nv->d_id; + } + + /** + * We compare by expression ids so, keeping things deterministic and having + * that subexpressions have to be smaller than the enclosing expressions. + * + * @param typeNode the node to compare to + * @return true if this expression is greater or equal + */ + inline bool operator>=(const TypeNode& typeNode) const { + return d_nv->d_id >= typeNode.d_nv->d_id; + } + /** * Returns the i-th child of this node. * diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 2f9f08302..3e777ec89 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -11,3 +11,9 @@ libsmt_la_SOURCES = \ modal_exception.h \ bad_option_exception.h \ no_such_function_exception.h + +EXTRA_DIST = \ + bad_option_exception.i \ + no_such_function_exception.i \ + modal_exception.i \ + smt_engine.i diff --git a/src/smt/bad_option_exception.i b/src/smt/bad_option_exception.i new file mode 100644 index 000000000..ddb0e3919 --- /dev/null +++ b/src/smt/bad_option_exception.i @@ -0,0 +1,5 @@ +%{ +#include "smt/bad_option_exception.h" +%} + +%include "smt/bad_option_exception.h" diff --git a/src/smt/modal_exception.i b/src/smt/modal_exception.i new file mode 100644 index 000000000..d82d95666 --- /dev/null +++ b/src/smt/modal_exception.i @@ -0,0 +1,5 @@ +%{ +#include "smt/modal_exception.h" +%} + +%include "smt/modal_exception.h" diff --git a/src/smt/no_such_function_exception.i b/src/smt/no_such_function_exception.i new file mode 100644 index 000000000..0c67ad0d3 --- /dev/null +++ b/src/smt/no_such_function_exception.i @@ -0,0 +1,5 @@ +%{ +#include "smt/no_such_function_exception.h" +%} + +%include "smt/no_such_function_exception.h" diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 698f9ba2e..d2abf2fce 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -23,26 +23,6 @@ #include -#if SWIG -%include "cvc4_public.h" -%include "util/rational.h" -%include "util/exception.h" -%include "expr/kind.h" -%include "util/integer.h" -%include "util/cardinality.h" -%include "util/sexpr.h" -%include "util/language.h" -%include "expr/type.h" -%include "expr/expr.h" -%include "expr/expr_manager.h" -%{ -#include "util/integer.h" -#include "expr/expr_manager.h" -#include "expr/type.h" -#include "expr/expr.h" -%} -#endif - #include "context/cdlist_forward.h" #include "context/cdmap_forward.h" #include "context/cdset_forward.h" diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i new file mode 100644 index 000000000..64a4f93e2 --- /dev/null +++ b/src/smt/smt_engine.i @@ -0,0 +1,5 @@ +%{ +#include "smt/smt_engine.h" +%} + +%include "smt/smt_engine.h" diff --git a/src/util/Assert.i b/src/util/Assert.i new file mode 100644 index 000000000..11881982b --- /dev/null +++ b/src/util/Assert.i @@ -0,0 +1,5 @@ +%{ +#include "util/Assert.h" +%} + +%include "util/Assert.h" diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 7f5fb459e..b8bdfabeb 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -139,4 +139,24 @@ EXTRA_DIST = \ rational_gmp_imp.cpp \ rational.h.in \ integer.h.in \ - tls.h.in + tls.h.in \ + integer.i \ + stats.i \ + bool.i \ + sexpr.i \ + datatype.i \ + output.i \ + cardinality.i \ + result.i \ + configuration.i \ + Assert.i \ + bitvector.i \ + subrange_bound.i \ + exception.i \ + language.i \ + array.i \ + options.i \ + ascription_type.i \ + rational.i \ + pseudoboolean.i \ + hash.i diff --git a/src/util/array.i b/src/util/array.i new file mode 100644 index 000000000..593ce9490 --- /dev/null +++ b/src/util/array.i @@ -0,0 +1,5 @@ +%{ +#include "util/array.h" +%} + +%include "util/array.h" diff --git a/src/util/ascription_type.i b/src/util/ascription_type.i new file mode 100644 index 000000000..b0b57d5f9 --- /dev/null +++ b/src/util/ascription_type.i @@ -0,0 +1,11 @@ +%{ +#include "util/ascription_type.h" +%} + + +%rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const; +%ignore CVC4::AscriptionType::operator!=(const AscriptionType&) const; + +%ignore CVC4::operator<<(std::ostream&, AscriptionType); + +%include "util/ascription_type.h" diff --git a/src/util/bitvector.i b/src/util/bitvector.i new file mode 100644 index 000000000..085a59b2d --- /dev/null +++ b/src/util/bitvector.i @@ -0,0 +1,28 @@ +%{ +#include "util/bitvector.h" +%} + +%ignore CVC4::BitVector::BitVector(unsigned, unsigned); + +%rename(assign) CVC4::BitVector::operator=(const BitVector&); +%rename(equals) CVC4::BitVector::operator==(const BitVector&) const; +%ignore CVC4::BitVector::operator!=(const BitVector&) const; +%rename(plus) CVC4::BitVector::operator+(const BitVector&) const; +%rename(minus) CVC4::BitVector::operator-(const BitVector&) const; +%rename(minus) CVC4::BitVector::operator-() const; +%rename(times) CVC4::BitVector::operator*(const BitVector&) const; +%rename(complement) CVC4::BitVector::operator~() const; + +%rename(equals) CVC4::BitVectorExtract::operator==(const BitVectorExtract&) const; + +%rename(toUnsigned) CVC4::BitVectorSize::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorRepeat::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorZeroExtend::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorSignExtend::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorRotateLeft::operator unsigned() const; +%rename(toUnsigned) CVC4::BitVectorRotateRight::operator unsigned() const; + +%ignore CVC4::operator<<(std::ostream&, const BitVector&); +%ignore CVC4::operator<<(std::ostream&, const BitVectorExtract&); + +%include "util/bitvector.h" diff --git a/src/util/bool.i b/src/util/bool.i new file mode 100644 index 000000000..39c1c35d4 --- /dev/null +++ b/src/util/bool.i @@ -0,0 +1,5 @@ +%{ +#include "util/bool.h" +%} + +%include "util/bool.h" diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 6985ae38e..e08f09bb6 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -22,11 +22,6 @@ #ifndef __CVC4__CARDINALITY_H #define __CVC4__CARDINALITY_H -#if SWIG -%include "util/integer.h" -%include "util/Assert.h" -#endif /* SWIG */ - #include #include diff --git a/src/util/cardinality.i b/src/util/cardinality.i new file mode 100644 index 000000000..760f746c0 --- /dev/null +++ b/src/util/cardinality.i @@ -0,0 +1,23 @@ +%{ +#include "util/cardinality.h" +%} + +%feature("valuewrapper") CVC4::Cardinality::Beth; + +%rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&); +%rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&); +%rename(powerAssign) CVC4::Cardinality::operator^=(const Cardinality&); +%rename(plus) CVC4::Cardinality::operator+(const Cardinality&) const; +%rename(times) CVC4::Cardinality::operator*(const Cardinality&) const; +%rename(power) CVC4::Cardinality::operator^(const Cardinality&) const; +%rename(equals) CVC4::Cardinality::operator==(const Cardinality&) const; +%ignore CVC4::Cardinality::operator!=(const Cardinality&) const; +%rename(less) CVC4::Cardinality::operator<(const Cardinality&) const; +%rename(lessEqual) CVC4::Cardinality::operator<=(const Cardinality&) const; +%rename(greater) CVC4::Cardinality::operator>(const Cardinality&) const; +%rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const; + +%ignore CVC4::operator<<(std::ostream&, const Cardinality&); +%ignore CVC4::operator<<(std::ostream&, Cardinality::Beth); + +%include "util/cardinality.h" diff --git a/src/util/configuration.i b/src/util/configuration.i new file mode 100644 index 000000000..17c1b974b --- /dev/null +++ b/src/util/configuration.i @@ -0,0 +1,5 @@ +%{ +#include "util/configuration.h" +%} + +%include "util/configuration.h" diff --git a/src/util/datatype.i b/src/util/datatype.i new file mode 100644 index 000000000..802f227eb --- /dev/null +++ b/src/util/datatype.i @@ -0,0 +1,22 @@ +%{ +#include "util/datatype.h" +%} + +%rename(equals) CVC4::Datatype::operator==(const Datatype&) const; +%ignore CVC4::Datatype::operator!=(const Datatype&) const; + +%rename(beginConst) CVC4::Datatype::begin() const; +%rename(endConst) CVC4::Datatype::end() const; + +%rename(getConstructor) CVC4::Datatype::operator[](size_t) const; + +%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const; +%ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const; +%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const; +%ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const; + +%ignore CVC4::operator<<(std::ostream&, const Datatype&); +%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&); +%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&); + +%include "util/datatype.h" diff --git a/src/util/exception.h b/src/util/exception.h index 1b1eb224e..43a0354ca 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -30,16 +30,20 @@ namespace CVC4 { class CVC4_PUBLIC Exception { protected: std::string d_msg; + public: // Constructors Exception() : d_msg("Unknown exception") {} Exception(const std::string& msg) : d_msg(msg) {} Exception(const char* msg) : d_msg(msg) {} + // Destructor virtual ~Exception() throw() {} + // NON-VIRTUAL METHOD for setting and printing the error message void setMessage(const std::string& msg) { d_msg = msg; } std::string getMessage() const { return d_msg; } + /** * Get this exception as a string. Note that * cout << ex.toString(); @@ -57,16 +61,17 @@ public: toStream(ss); return ss.str(); } + /** * Printing: feel free to redefine toStream(). When overridden in * a derived class, it's recommended that this method print the * type of exception before the actual message. */ virtual void toStream(std::ostream& os) const { os << d_msg; } - // No need to overload operator<< for the inherited classes - friend std::ostream& operator<<(std::ostream& os, const Exception& e); + };/* class Exception */ +inline std::ostream& operator<<(std::ostream& os, const Exception& e) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& os, const Exception& e) { e.toStream(os); return os; diff --git a/src/util/exception.i b/src/util/exception.i new file mode 100644 index 000000000..d3ff896d2 --- /dev/null +++ b/src/util/exception.i @@ -0,0 +1,7 @@ +%{ +#include "util/exception.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const Exception&); + +%include "util/exception.h" diff --git a/src/util/hash.h b/src/util/hash.h index 10211970f..bd3fee597 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -22,6 +22,9 @@ #ifndef __CVC4__HASH_H #define __CVC4__HASH_H +// in case it's not been declared as a namespace yet +namespace __gnu_cxx {} + #include namespace std { using namespace __gnu_cxx; } diff --git a/src/util/hash.i b/src/util/hash.i new file mode 100644 index 000000000..f2f1e6652 --- /dev/null +++ b/src/util/hash.i @@ -0,0 +1,5 @@ +%{ +#include "util/hash.h" +%} + +%include "util/hash.h" diff --git a/src/util/integer.h.in b/src/util/integer.h.in index b2973081d..b62feb512 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -26,14 +26,8 @@ #ifdef CVC4_CLN_IMP # include "util/integer_cln_imp.h" -# if SWIG - %include "util/integer_cln_imp.h" -# endif /* SWIG */ #endif /* CVC4_CLN_IMP */ #ifdef CVC4_GMP_IMP # include "util/integer_gmp_imp.h" -# if SWIG - %include "util/integer_gmp_imp.h" -# endif /* SWIG */ #endif /* CVC4_GMP_IMP */ diff --git a/src/util/integer.i b/src/util/integer.i new file mode 100644 index 000000000..4aaa532a7 --- /dev/null +++ b/src/util/integer.i @@ -0,0 +1,29 @@ +%{ +#include "util/integer.h" +%} + +%ignore CVC4::Integer::Integer(int); +%ignore CVC4::Integer::Integer(unsigned int); + +%rename(assign) CVC4::Integer::operator=(const Integer&); +%rename(equals) CVC4::Integer::operator==(const Integer&) const; +%ignore CVC4::Integer::operator!=(const Integer&) const; +%rename(plus) CVC4::Integer::operator+(const Integer&) const; +%rename(minus) CVC4::Integer::operator-() const; +%rename(minus) CVC4::Integer::operator-(const Integer&) const; +%rename(times) CVC4::Integer::operator*(const Integer&) const; +%rename(dividedBy) CVC4::Integer::operator/(const Integer&) const; +%rename(modulo) CVC4::Integer::operator%(const Integer&) const; +%rename(plusAssign) CVC4::Integer::operator+=(const Integer&); +%rename(minusAssign) CVC4::Integer::operator-=(const Integer&); +%rename(timesAssign) CVC4::Integer::operator*=(const Integer&); +%rename(dividedByAssign) CVC4::Integer::operator/=(const Integer&); +%rename(moduloAssign) CVC4::Integer::operator%=(const Integer&); +%rename(less) CVC4::Integer::operator<(const Integer&) const; +%rename(lessEqual) CVC4::Integer::operator<=(const Integer&) const; +%rename(greater) CVC4::Integer::operator>(const Integer&) const; +%rename(greaterEqual) CVC4::Integer::operator>=(const Integer&) const; + +%ignore CVC4::operator<<(std::ostream&, const Integer&); + +%include "util/integer.h" diff --git a/src/util/language.i b/src/util/language.i new file mode 100644 index 000000000..cd261a73c --- /dev/null +++ b/src/util/language.i @@ -0,0 +1,10 @@ +%{ +#include "util/language.h" +%} + +%import "util/language.h" + +%ignore CVC4::operator<<(std::ostream&, CVC4::language::input::Language); +%ignore CVC4::operator<<(std::ostream&, CVC4::language::output::Language); + +%include "util/language.h" diff --git a/src/util/matcher.h b/src/util/matcher.h index 6daceb8fd..871fe528f 100644 --- a/src/util/matcher.h +++ b/src/util/matcher.h @@ -16,7 +16,7 @@ ** A class representing a type matcher. **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__MATCHER_H #define __CVC4__MATCHER_H diff --git a/src/util/options.i b/src/util/options.i new file mode 100644 index 000000000..ad4815a33 --- /dev/null +++ b/src/util/options.i @@ -0,0 +1,9 @@ +%{ +#include "util/options.h" +%} + +%ignore CVC4::operator<<(std::ostream&, Options::SimplificationMode); +%ignore CVC4::operator<<(std::ostream&, Options::ArithPivotRule); + +%import "util/exception.h" +%include "util/options.h" diff --git a/src/util/output.h b/src/util/output.h index e096ff028..da1efe68a 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -23,6 +23,7 @@ #include #include +#include #include #include #include @@ -71,6 +72,9 @@ class CVC4_PUBLIC CVC4ostream { /** The endl manipulator (why do we need to keep this?) */ std::ostream& (*const d_endl)(std::ostream&); + // do not allow use + CVC4ostream& operator=(const CVC4ostream&); + public: CVC4ostream() : d_os(NULL), diff --git a/src/util/output.i b/src/util/output.i new file mode 100644 index 000000000..c2729203a --- /dev/null +++ b/src/util/output.i @@ -0,0 +1,10 @@ +%{ +#include "util/output.h" +%} + +%import "util/output.h" + +%feature("valuewrapper") CVC4::null_streambuf; +%feature("valuewrapper") std::ostream; + +%include "util/output.h" diff --git a/src/util/pseudoboolean.i b/src/util/pseudoboolean.i new file mode 100644 index 000000000..2505a7c1e --- /dev/null +++ b/src/util/pseudoboolean.i @@ -0,0 +1,11 @@ +%{ +#include "util/pseudoboolean.h" +%} + +%rename(toBool) CVC4::Pseudoboolean::operator bool() const; +%rename(toInt) CVC4::Pseudoboolean::operator int() const; +%rename(toInteger) CVC4::Pseudoboolean::operator Integer() const; + +%ignore CVC4::operator<<(std::ostream&, CVC4::Pseudoboolean); + +%include "util/pseudoboolean.h" diff --git a/src/util/rational.h.in b/src/util/rational.h.in index 17c1e31fc..13cdb059b 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -26,14 +26,8 @@ #ifdef CVC4_CLN_IMP # include "util/rational_cln_imp.h" -# if SWIG - %include "util/rational_cln_imp.h" -# endif /* SWIG */ #endif /* CVC4_CLN_IMP */ #ifdef CVC4_GMP_IMP # include "util/rational_gmp_imp.h" -# if SWIG - %include "util/rational_gmp_imp.h" -# endif /* SWIG */ #endif /* CVC4_GMP_IMP */ diff --git a/src/util/rational.i b/src/util/rational.i new file mode 100644 index 000000000..512d3ea50 --- /dev/null +++ b/src/util/rational.i @@ -0,0 +1,29 @@ +%{ +#include "util/rational.h" +%} + +%ignore CVC4::Rational::Rational(int); +%ignore CVC4::Rational::Rational(unsigned int); +%ignore CVC4::Rational::Rational(int, int); +%ignore CVC4::Rational::Rational(unsigned int, unsigned int); + +%rename(assign) CVC4::Rational::operator=(const Rational&); +%rename(equals) CVC4::Rational::operator==(const Rational&) const; +%ignore CVC4::Rational::operator!=(const Rational&) const; +%rename(plus) CVC4::Rational::operator+(const Rational&) const; +%rename(minus) CVC4::Rational::operator-() const; +%rename(minus) CVC4::Rational::operator-(const Rational&) const; +%rename(times) CVC4::Rational::operator*(const Rational&) const; +%rename(dividedBy) CVC4::Rational::operator/(const Rational&) const; +%rename(plusAssign) CVC4::Rational::operator+=(const Rational&); +%rename(minusAssign) CVC4::Rational::operator-=(const Rational&); +%rename(timesAssign) CVC4::Rational::operator*=(const Rational&); +%rename(dividedByAssign) CVC4::Rational::operator/=(const Rational&); +%rename(less) CVC4::Rational::operator<(const Rational&) const; +%rename(lessEqual) CVC4::Rational::operator<=(const Rational&) const; +%rename(greater) CVC4::Rational::operator>(const Rational&) const; +%rename(greaterEqual) CVC4::Rational::operator>=(const Rational&) const; + +%ignore CVC4::operator<<(std::ostream&, const Rational&); + +%include "util/rational.h" diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index a883500f9..2f2c14ed8 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -258,6 +258,11 @@ public: return (*this); } + Rational& operator/=(const Rational& y){ + d_value /= y.d_value; + return (*this); + } + /** Returns a string representing the rational in the given base. */ std::string toString(int base = 10) const { std::stringstream ss; diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index b97965169..37c3c8364 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -239,6 +239,11 @@ public: return (*this); } + Rational& operator/=(const Rational& y){ + d_value /= y.d_value; + return (*this); + } + /** Returns a string representing the rational in the given base. */ std::string toString(int base = 10) const { return d_value.get_str(base); diff --git a/src/util/result.i b/src/util/result.i new file mode 100644 index 000000000..c0d86b30a --- /dev/null +++ b/src/util/result.i @@ -0,0 +1,14 @@ +%{ +#include "util/result.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const Result& r); + +%rename(equals) CVC4::Result::operator==(const Result& r) const; +%ignore CVC4::Result::operator!=(const Result& r) const; + +%ignore CVC4::operator<<(std::ostream&, enum Result::Sat); +%ignore CVC4::operator<<(std::ostream&, enum Result::Validity); +%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); + +%include "util/result.h" diff --git a/src/util/sexpr.i b/src/util/sexpr.i new file mode 100644 index 000000000..c925f9f95 --- /dev/null +++ b/src/util/sexpr.i @@ -0,0 +1,7 @@ +%{ +#include "util/sexpr.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const SExpr&); + +%include "util/sexpr.h" diff --git a/src/util/stats.i b/src/util/stats.i new file mode 100644 index 000000000..48828cb7e --- /dev/null +++ b/src/util/stats.i @@ -0,0 +1,21 @@ +%{ +#include "util/stats.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const ::timespec&); + +%rename(increment) CVC4::IntStat::operator++(); +%rename(plusAssign) CVC4::IntStat::operator+=(int64_t); + +%rename(plusAssign) CVC4::operator+=(::timespec&, const ::timespec&); +%rename(minusAssign) CVC4::operator-=(::timespec&, const ::timespec&); +%rename(plus) CVC4::operator+(const ::timespec&, const ::timespec&); +%rename(minus) CVC4::operator-(const ::timespec&, const ::timespec&); +%rename(equals) CVC4::operator==(const ::timespec&, const ::timespec&); +%ignore CVC4::operator!=(const ::timespec&, const ::timespec&); +%rename(less) CVC4::operator<(const ::timespec&, const ::timespec&); +%rename(lessEqual) CVC4::operator<=(const ::timespec&, const ::timespec&); +%rename(greater) CVC4::operator>(const ::timespec&, const ::timespec&); +%rename(greaterEqual) CVC4::operator>=(const ::timespec&, const ::timespec&); + +%include "util/stats.h" diff --git a/src/util/subrange_bound.i b/src/util/subrange_bound.i new file mode 100644 index 000000000..6b02414ab --- /dev/null +++ b/src/util/subrange_bound.i @@ -0,0 +1,10 @@ +%{ +#include "util/subrange_bound.h" +%} + +%rename(equals) CVC4::SubrangeBound::operator==(const SubrangeBound&) const; +%ignore CVC4::SubrangeBound::operator!=(const SubrangeBound&) const; + +%ignore CVC4::operator<<(std::ostream&, const SubrangeBound&); + +%include "util/subrange_bound.h" -- 2.30.2