From: Morgan Deters Date: Wed, 21 Sep 2011 03:26:13 +0000 (+0000) Subject: considerable bindings interface work, some improvements to build X-Git-Tag: cvc5-1.0.0~8462 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b1689612bb2ff984aa90cd84093ffc043d78ba9;p=cvc5.git considerable bindings interface work, some improvements to build --- diff --git a/configure.ac b/configure.ac index 8a1039bd9..d4ea2ef48 100644 --- a/configure.ac +++ b/configure.ac @@ -835,6 +835,30 @@ else AC_MSG_RESULT([no (user didn't request it)]) fi +# Java +AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)]) +AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)]) +AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)]) +if test "$cvc4_build_java_bindings"; then + dnl AM_PROG_GCJ + if test -z "$JAVA"; then + AC_CHECK_PROGS(JAVA, java, java, []) + else + AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", []) + fi + if test -z "$JAVAC"; then + AC_CHECK_PROGS(JAVAC, javac gcj, javac, []) + if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi + else + AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", []) + fi + if test -z "$JAR"; then + AC_CHECK_PROGS(JAR, jar, jar, []) + else + AC_CHECK_PROG(JAR, "$JAR", "$JAR", []) + fi +fi + # Prepare configure output if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index 227f239da..31ad8c71f 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -1,3 +1,17 @@ +# LIBCVC4BINDINGS_VERSION (-version-info) is in the form current:revision:age +# +# current - +# increment if interfaces have been added, removed or changed +# revision - +# increment if source code has changed +# set to zero if current is incremented +# age - +# increment if interfaces have been added +# set to zero if interfaces have been removed +# or changed +# +LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ + AM_CPPFLAGS = \ -D__BUILDING_CVC4BINDINGSLIB \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. @@ -8,6 +22,11 @@ data_DATA = if CVC4_LANGUAGE_BINDING_JAVA lib_LTLIBRARIES += libcvc4bindings_java.la data_DATA += cvc4.jar +libcvc4bindings_java_la_LDFLAGS = \ + -version-info $(LIBCVC4BINDINGS_VERSION) +libcvc4bindings_java_la_LIBADD = \ + -L@builddir@/.. -lcvc4 \ + -L@builddir@/../parser -lcvc4parser endif # cvc4bindings_csharp.so \ # cvc4bindings_perl.so \ @@ -18,13 +37,13 @@ endif # cvc4bindings_tcl.so nodist_libcvc4bindings_java_la_SOURCES = java.cpp -#nodist_cvc4bindings_csharp_so_SOURCES = csharp.cpp -#nodist_cvc4bindings_perl_so_SOURCES = perl.cpp -#nodist_cvc4bindings_php_so_SOURCES = php.cpp -#nodist_cvc4bindings_python_so_SOURCES = python.cpp -#nodist_cvc4bindings_ocaml_so_SOURCES = ocaml.cpp -#nodist_cvc4bindings_ruby_so_SOURCES = ruby.cpp -#nodist_cvc4bindings_tcl_so_SOURCES = tcl.cpp +nodist_libcvc4bindings_csharp_la_SOURCES = csharp.cpp +nodist_libcvc4bindings_perl_la_SOURCES = perl.cpp +nodist_libcvc4bindings_php_la_SOURCES = php.cpp +nodist_libcvc4bindings_python_la_SOURCES = python.cpp +nodist_libcvc4bindings_ocaml_la_SOURCES = ocaml.cpp +nodist_libcvc4bindings_ruby_la_SOURCES = ruby.cpp +nodist_libcvc4bindings_tcl_la_SOURCES = tcl.cpp BUILT_SOURCES = \ java.cpp \ @@ -42,8 +61,16 @@ CLEANFILES = \ $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \ cvc4.jar -java.lo: java.cpp; $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $< -cvc4.jar: java.cpp; $(AM_V_GEN)jar cf $@ -C java . +java.lo: java.cpp + $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $< +cvc4.jar: java.cpp + $(AM_V_GEN) \ + (cd java; \ + rm -fr classes; \ + mkdir -p classes; \ + $(JAVAC) -classpath . -d classes `find . -name '*.java'`; \ + cd classes); \ + $(JAR) cf $@ -C java/classes . java.cpp: csharp.cpp: perl.cpp: @@ -54,10 +81,10 @@ 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 $@ $< + $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -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,$@) $< + $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -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))) diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am index 905eaa6c4..1e64a61bb 100644 --- a/src/compat/Makefile.am +++ b/src/compat/Makefile.am @@ -19,7 +19,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) if CVC4_BUILD_LIBCOMPAT -nobase_lib_LTLIBRARIES = libcvc4compat.la +lib_LTLIBRARIES = libcvc4compat.la if HAVE_CXXTESTGEN noinst_LTLIBRARIES = libcvc4compat_noinst.la endif @@ -29,9 +29,13 @@ libcvc4compat_la_LDFLAGS = \ libcvc4compat_noinst_la_LDFLAGS = libcvc4compat_la_LIBADD = \ - @builddir@/../lib/libreplacements.la + @builddir@/../lib/libreplacements.la \ + -L@builddir@/.. -lcvc4 \ + -L@builddir@/../parser -lcvc4parser libcvc4compat_noinst_la_LIBADD = \ - @builddir@/../lib/libreplacements.la + @builddir@/../lib/libreplacements.la \ + -L@builddir@/.. -lcvc4 \ + -L@builddir@/../parser -lcvc4parser libcvc4compat_la_SOURCES = \ cvc3_compat.h \ diff --git a/src/cvc4.i b/src/cvc4.i index 4c574f16c..e69150b7b 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -1,20 +1,33 @@ %import "bindings/swig.h" -%module cvc4 -%nspace; +%module CVC4 +// nspace completely broken with Java packaging +//%nspace; %{ -namespace CVC4 {} +namespace CVC4 { class Exception; } using namespace CVC4; %} +%exception { + try { + $action + } catch(CVC4::Exception& e) { + ::std::cerr << e << ::std::endl; + jclass clazz = jenv->FindClass("java/lang/RuntimeException"); + jenv->ThrowNew(clazz, e.toString().c_str()); + } +} + +%include "std_string.i" // map std::string to java.lang.String + %include "util/integer.i" %include "util/rational.i" +%include "util/stats.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" @@ -40,3 +53,5 @@ using namespace CVC4; %include "smt/bad_option_exception.i" %include "smt/no_such_function_exception.i" %include "smt/modal_exception.i" + +%include "parser/cvc4parser.i" diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index e95e434fe..616a7c8ff 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -506,7 +506,7 @@ protected: friend class ExprManager; friend class NodeManager; friend class TypeCheckingException; - friend std::ostream& operator<<(std::ostream& out, const Expr& e); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); template friend class NodeTemplate; };/* class Expr */ diff --git a/src/expr/kind.i b/src/expr/kind.i index 1c17f3ff9..95c350cf3 100644 --- a/src/expr/kind.i +++ b/src/expr/kind.i @@ -8,4 +8,6 @@ %ignore CVC4::theory::operator++(TheoryId&); +%rename(Kind) CVC4::kind::Kind_t; + %include "expr/kind.h" diff --git a/src/expr/type.cpp b/src/expr/type.cpp index ff47c6eae..0edc7579b 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -184,7 +184,7 @@ bool Type::isBoolean() const { /** Cast to a Boolean type */ Type::operator BooleanType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isBoolean()); + Assert(isNull() || isBoolean()); return BooleanType(*this); } @@ -197,7 +197,7 @@ bool Type::isInteger() const { /** Cast to a integer type */ Type::operator IntegerType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isInteger()); + Assert(isNull() || isInteger()); return IntegerType(*this); } @@ -210,7 +210,7 @@ bool Type::isReal() const { /** Cast to a real type */ Type::operator RealType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isReal()); + Assert(isNull() || isReal()); return RealType(*this); } @@ -223,7 +223,7 @@ bool Type::isPseudoboolean() const { /** Cast to a pseudoboolean type */ Type::operator PseudobooleanType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isPseudoboolean()); + Assert(isNull() || isPseudoboolean()); return PseudobooleanType(*this); } @@ -236,14 +236,14 @@ bool Type::isBitVector() const { /** Cast to a bit-vector type */ Type::operator BitVectorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isBitVector()); + Assert(isNull() || isBitVector()); return BitVectorType(*this); } /** Cast to a Constructor type */ Type::operator DatatypeType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isDatatype()); + Assert(isNull() || isDatatype()); return DatatypeType(*this); } @@ -256,7 +256,7 @@ bool Type::isDatatype() const { /** Cast to a Constructor type */ Type::operator ConstructorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isConstructor()); + Assert(isNull() || isConstructor()); return ConstructorType(*this); } @@ -269,7 +269,7 @@ bool Type::isConstructor() const { /** Cast to a Selector type */ Type::operator SelectorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isSelector()); + Assert(isNull() || isSelector()); return SelectorType(*this); } @@ -282,7 +282,7 @@ bool Type::isSelector() const { /** Cast to a Tester type */ Type::operator TesterType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isTester()); + Assert(isNull() || isTester()); return TesterType(*this); } @@ -310,7 +310,7 @@ bool Type::isPredicate() const { /** Cast to a function type */ Type::operator FunctionType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isFunction()); + Assert(isNull() || isFunction()); return FunctionType(*this); } @@ -323,7 +323,7 @@ bool Type::isTuple() const { /** Cast to a tuple type */ Type::operator TupleType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isTuple()); + Assert(isNull() || isTuple()); return TupleType(*this); } @@ -348,7 +348,7 @@ bool Type::isSort() const { /** Cast to a sort type */ Type::operator SortType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isSort()); + Assert(isNull() || isSort()); return SortType(*this); } @@ -361,7 +361,7 @@ bool Type::isSortConstructor() const { /** Cast to a sort type */ Type::operator SortConstructorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isSortConstructor()); + Assert(isNull() || isSortConstructor()); return SortConstructorType(*this); } @@ -374,7 +374,7 @@ bool Type::isKind() const { /** Cast to a kind type */ Type::operator KindType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Assert(isKind()); + Assert(isNull() || isKind()); return KindType(*this); } @@ -392,7 +392,7 @@ vector FunctionType::getArgTypes() const { Type FunctionType::getRangeType() const { NodeManagerScope nms(d_nodeManager); - Assert(isFunction()); + Assert(isNull() || isFunction()); return makeType(d_typeNode->getRangeType()); } @@ -447,78 +447,78 @@ SortType SortConstructorType::instantiate(const std::vector& params) const BooleanType::BooleanType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isBoolean()); + Assert(isNull() || isBoolean()); } IntegerType::IntegerType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isInteger()); + Assert(isNull() || isInteger()); } RealType::RealType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isReal()); + Assert(isNull() || isReal()); } PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isPseudoboolean()); + Assert(isNull() || isPseudoboolean()); } BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isBitVector()); + Assert(isNull() || isBitVector()); } DatatypeType::DatatypeType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isDatatype()); + Assert(isNull() || isDatatype()); } ConstructorType::ConstructorType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isConstructor()); + Assert(isNull() || isConstructor()); } SelectorType::SelectorType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isSelector()); + Assert(isNull() || isSelector()); } TesterType::TesterType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isTester()); + Assert(isNull() || isTester()); } FunctionType::FunctionType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isFunction()); + Assert(isNull() || isFunction()); } TupleType::TupleType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isTuple()); + Assert(isNull() || isTuple()); } ArrayType::ArrayType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isArray()); + Assert(isNull() || isArray()); } KindType::KindType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isKind()); + Assert(isNull() || isKind()); } SortType::SortType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isSort()); + Assert(isNull() || isSort()); } SortConstructorType::SortConstructorType(const Type& t) throw(AssertionException) : Type(t) { - Assert(isSortConstructor()); + Assert(isNull() || isSortConstructor()); } unsigned BitVectorType::getSize() const { diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 42a306752..d53ae55a0 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -17,9 +17,9 @@ libmain_a_SOURCES = \ cvc4_SOURCES = cvc4_LDADD = \ libmain.a \ - ../parser/libcvc4parser.la \ - ../libcvc4.la \ - ../lib/libreplacements.la \ + @builddir@/../parser/libcvc4parser.la \ + @builddir@/../libcvc4.la \ + @builddir@/../lib/libreplacements.la \ $(READLINE_LDFLAGS) BUILT_SOURCES = \ diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index f1802c6c5..d87db20f5 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -19,7 +19,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = smt smt2 cvc -nobase_lib_LTLIBRARIES = libcvc4parser.la +lib_LTLIBRARIES = libcvc4parser.la if HAVE_CXXTESTGEN noinst_LTLIBRARIES = libcvc4parser_noinst.la endif @@ -32,12 +32,14 @@ libcvc4parser_la_LIBADD = \ @builddir@/smt/libparsersmt.la \ @builddir@/smt2/libparsersmt2.la \ @builddir@/cvc/libparsercvc.la \ - @builddir@/../lib/libreplacements.la + @builddir@/../lib/libreplacements.la \ + -L@builddir@/.. -lcvc4 libcvc4parser_noinst_la_LIBADD = \ @builddir@/smt/libparsersmt.la \ @builddir@/smt2/libparsersmt2.la \ @builddir@/cvc/libparsercvc.la \ - @builddir@/../lib/libreplacements.la + @builddir@/../lib/libreplacements.la \ + -L@builddir@/.. -lcvc4 libcvc4parser_la_SOURCES = \ antlr_input.h \ diff --git a/src/parser/cvc4parser.i b/src/parser/cvc4parser.i new file mode 100644 index 000000000..2ad3bf01d --- /dev/null +++ b/src/parser/cvc4parser.i @@ -0,0 +1,15 @@ +%import "bindings/swig.h" + +%module CVC4Parser +// nspace completely broken with Java packaging +//%nspace; + +%{ +namespace CVC4 {} +using namespace CVC4; +%} + +%include "parser/parser_exception.i" +%include "parser/input.i" +%include "parser/parser.i" +%include "parser/parser_builder.i" diff --git a/src/parser/input.i b/src/parser/input.i new file mode 100644 index 000000000..2a76e2b7a --- /dev/null +++ b/src/parser/input.i @@ -0,0 +1,5 @@ +%{ +#include "parser/input.h" +%} + +%include "parser/input.h" diff --git a/src/parser/parser.h b/src/parser/parser.h index 5ce016b85..46544559a 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -53,12 +53,13 @@ enum DeclarationCheck { CHECK_UNDECLARED, /** Don't check anything */ CHECK_NONE -}; +};/* enum DeclarationCheck */ /** * Returns a string representation of the given object (for * debugging). */ +inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) { switch(check) { case CHECK_NONE: @@ -80,12 +81,13 @@ enum SymbolType { SYM_VARIABLE, /** Sorts */ SYM_SORT -}; +};/* enum SymbolType */ /** * Returns a string representation of the given object (for * debugging). */ +inline std::ostream& operator<<(std::ostream& out, SymbolType type) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, SymbolType type) { switch(type) { case SYM_VARIABLE: diff --git a/src/parser/parser.i b/src/parser/parser.i new file mode 100644 index 000000000..55119be9a --- /dev/null +++ b/src/parser/parser.i @@ -0,0 +1,14 @@ +%{ +#include "parser/parser.h" +%} + +namespace CVC4 { + namespace parser { + enum DeclarationCheck; + enum SymbolType; + %ignore operator<<(std::ostream&, DeclarationCheck); + %ignore operator<<(std::ostream&, SymbolType); + }/* namespace CVC4::parser */ +}/* namespace CVC4 */ + +%include "parser/parser.h" diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 6f4f051ec..0463a079f 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -23,7 +23,7 @@ #include -#include "input.h" +#include "parser/input.h" #include "util/language.h" diff --git a/src/parser/parser_builder.i b/src/parser/parser_builder.i new file mode 100644 index 000000000..6b77356bc --- /dev/null +++ b/src/parser/parser_builder.i @@ -0,0 +1,5 @@ +%{ +#include "parser/parser_builder.h" +%} + +%include "parser/parser_builder.h" diff --git a/src/parser/parser_exception.i b/src/parser/parser_exception.i new file mode 100644 index 000000000..5be81034d --- /dev/null +++ b/src/parser/parser_exception.i @@ -0,0 +1,7 @@ +%{ +#include "parser/parser_exception.h" +%} + +%ignore CVC4::parser::ParserException::ParserException(const char*); + +%include "parser/parser_exception.h" diff --git a/src/smt/bad_option_exception.i b/src/smt/bad_option_exception.i index ddb0e3919..eeded5a45 100644 --- a/src/smt/bad_option_exception.i +++ b/src/smt/bad_option_exception.i @@ -2,4 +2,6 @@ #include "smt/bad_option_exception.h" %} +%ignore CVC4::BadOptionException::BadOptionException(const char*); + %include "smt/bad_option_exception.h" diff --git a/src/smt/modal_exception.i b/src/smt/modal_exception.i index d82d95666..15b8150cf 100644 --- a/src/smt/modal_exception.i +++ b/src/smt/modal_exception.i @@ -2,4 +2,6 @@ #include "smt/modal_exception.h" %} +%ignore CVC4::ModalException::ModalException(const char*); + %include "smt/modal_exception.h" diff --git a/src/util/Assert.i b/src/util/Assert.i index 11881982b..b43c36520 100644 --- a/src/util/Assert.i +++ b/src/util/Assert.i @@ -2,4 +2,7 @@ #include "util/Assert.h" %} +%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException; +%ignore CVC4::InternalErrorException::InternalErrorException(const char*, const char*, unsigned, const char*, ...); + %include "util/Assert.h" diff --git a/src/util/exception.i b/src/util/exception.i index d3ff896d2..52ff28922 100644 --- a/src/util/exception.i +++ b/src/util/exception.i @@ -3,5 +3,6 @@ %} %ignore CVC4::operator<<(std::ostream&, const Exception&); +%ignore CVC4::Exception::Exception(const char*); %include "util/exception.h" diff --git a/src/util/hash.i b/src/util/hash.i index f2f1e6652..470447fc3 100644 --- a/src/util/hash.i +++ b/src/util/hash.i @@ -2,4 +2,6 @@ #include "util/hash.h" %} +%rename(apply) CVC4::StringHashFunction::operator()(const std::string&) const; + %include "util/hash.h" diff --git a/src/util/language.i b/src/util/language.i index cd261a73c..28e0eb5ac 100644 --- a/src/util/language.i +++ b/src/util/language.i @@ -2,9 +2,33 @@ #include "util/language.h" %} -%import "util/language.h" +namespace CVC4 { + namespace language { + namespace input { + %ignore operator<<(std::ostream&, Language); + }/* CVC4::language::input namespace */ -%ignore CVC4::operator<<(std::ostream&, CVC4::language::input::Language); -%ignore CVC4::operator<<(std::ostream&, CVC4::language::output::Language); + namespace output { + %ignore operator<<(std::ostream&, Language); + }/* CVC4::language::output namespace */ + }/* CVC4::language namespace */ +}/* CVC4 namespace */ + +// These clash in the monolithic Java namespace, so we rename them. +%rename(InputLanguage) CVC4::language::input::Language; +%rename(OutputLanguage) CVC4::language::output::Language; + +%rename(INPUT_LANG_AUTO) CVC4::language::input::LANG_AUTO; +%rename(INPUT_LANG_SMTLIB) CVC4::language::input::LANG_SMTLIB; +%rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2; +%rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4; +%rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX; + +%rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO; +%rename(OUTPUT_LANG_SMTLIB) CVC4::language::output::LANG_SMTLIB; +%rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2; +%rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4; +%rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST; +%rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX; %include "util/language.h" diff --git a/src/util/options.i b/src/util/options.i index ad4815a33..9e0caccd6 100644 --- a/src/util/options.i +++ b/src/util/options.i @@ -5,5 +5,4 @@ %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.i b/src/util/output.i index c2729203a..10653c2f8 100644 --- a/src/util/output.i +++ b/src/util/output.i @@ -2,9 +2,13 @@ #include "util/output.h" %} -%import "util/output.h" - %feature("valuewrapper") CVC4::null_streambuf; %feature("valuewrapper") std::ostream; +// There are issues with SWIG's attempted wrapping of these variables when +// it tries to generate the getters and setters. For now, just ignore them. +%ignore CVC4::null_sb; +%ignore CVC4::null_os; +%ignore CVC4::DumpC::dump_cout; + %include "util/output.h" diff --git a/src/util/stats.h b/src/util/stats.h index 7d3e33a6f..42cd73c3d 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -212,7 +212,7 @@ public: return ss.str(); } -};/* class DataStat */ +};/* class ReadOnlyDataStat */ /** diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java new file mode 100644 index 000000000..8151300f4 --- /dev/null +++ b/test/system/CVC4JavaTest.java @@ -0,0 +1,50 @@ +import edu.nyu.acsys.CVC4.CVC4; + +import edu.nyu.acsys.CVC4.SmtEngine; +import edu.nyu.acsys.CVC4.ExprManager; +import edu.nyu.acsys.CVC4.Expr; +import edu.nyu.acsys.CVC4.Type; +import edu.nyu.acsys.CVC4.BoolExpr; +import edu.nyu.acsys.CVC4.Kind; +import edu.nyu.acsys.CVC4.Configuration; + +//import edu.nyu.acsys.CVC4.Exception; + +import edu.nyu.acsys.CVC4.Parser; +import edu.nyu.acsys.CVC4.ParserBuilder; + +public class CVC4JavaTest { + public static void main(String[] args) { + try { + System.loadLibrary("cvc4bindings_java"); + + CVC4.getDebugChannel().on("current"); + +System.out.println(Configuration.about()); +System.out.println("constructing"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + +System.out.println("getting type"); + Type t = em.booleanType(); +System.out.println("making vars"); + Expr a = em.mkVar("a", em.booleanType()); + Expr b = em.mkVar("b", em.booleanType()); +System.out.println("making sausage"); + BoolExpr e = new BoolExpr(em.mkExpr(Kind.AND, a, b)); + +System.out.println("about to check"); + + System.out.println(smt.checkSat(e)); + + System.out.println(smt.getStatisticsRegistry()); + + System.exit(1); + } catch(Exception e) { + System.err.println(e); + System.exit(1); + } + } +} + diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 4f0fcea14..0f80aa454 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -1,15 +1,23 @@ TESTS_ENVIRONMENT = +TEST_EXTENSIONS = .class TESTS = \ boilerplate \ ouroborous # cvc3_main +if CVC4_LANGUAGE_BINDING_JAVA +TESTS += CVC4JavaTest.class +endif + +CLASS_LOG_COMPILER = @srcdir@/run_java_test $(JAVA) -classpath .:@abs_top_builddir@/src/bindings/cvc4.jar -Djava.library.path=$(abs_top_builddir)/src/bindings/.libs:$(abs_top_builddir)/src/.libs + # Things that aren't tests but that tests rely on and need to # go into the distribution TEST_DEPS_DIST = \ cvc3_main.cpp \ cvc3_george.h \ - cvc3_george.cpp + cvc3_george.cpp \ + CVC4JavaTest.java # Make-level dependencies; these don't go in the source distribution # but should trigger a re-compile of all unit tests. Libraries are @@ -54,12 +62,25 @@ LIBADD = \ @abs_top_builddir@/src/libcvc4.la # WHEN SYSTEM TESTS ARE ADDED, BUILD LIKE THIS: -$(TESTS:%=%.lo): %.lo: %.cpp +$(filter-out %.class.lo,$(TESTS:%=%.lo)): %.lo: %.cpp $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $+ -$(TESTS): %: %.lo $(LIBADD) +$(filter-out %.class,$(TESTS)): %: %.lo $(LIBADD) $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $< cvc3_main: cvc3_george.lo $(LIBADD) $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $+ +CVC4JavaTest.class: CVC4JavaTest.java @abs_top_builddir@/src/bindings/cvc4.jar @abs_top_builddir@/src/bindings/libcvc4bindings_java.la + $(AM_V_JAVAC)$(JAVAC) -classpath @abs_top_builddir@/src/bindings/cvc4.jar -d $(builddir) $< +#CVC4JavaTest: CVC4JavaTest.class +# $(AM_V_GEN)( \ +# echo "#!/bin/bash"; \ +# echo "exec $(JAVA) -classpath @abs_top_builddir@/src/bindings/cvc4.jar -Djava.library.path=@abs_top_builddir@/src/bindings/.libs CVC4JavaTest"; \ +# ) >$@; \ +# chmod +x $@ + +# for silent automake rules +AM_V_JAVAC = $(am__v_JAVAC_$(V)) +am__v_JAVAC_ = $(am__v_JAVAC_$(AM_DEFAULT_VERBOSITY)) +am__v_JAVAC_0 = @echo " JAVAC " $@; # trick automake into setting LTCXXCOMPILE, CXXLINK, etc. if CVC4_FALSE diff --git a/test/system/run_java_test b/test/system/run_java_test new file mode 100755 index 000000000..205d869f2 --- /dev/null +++ b/test/system/run_java_test @@ -0,0 +1,14 @@ +#!/bin/bash +# +# run_java_test +# Morgan Deters, September 2011 +# +# The purpose of this script is to change an automake test command +# line into something that a JVM likes. In particular, any dir/Foo.class +# listed on the command line is stripped of its dir/ and its .class extension. +# Works only for tests in the default package. +# +args=("$@") +args[$((${#args}))]="$(echo "${args[${#args}]}" | sed 's,\(.*\/\)\?\(.*\)\.class$,\2,')" +echo "${args[@]}" +exec "${args[@]}"