Merge from "swig" branch: language binding for Java is compiling and linking. Enable...

diff --git a/config/bindings.m4 b/config/bindings.m4
index cdab33e3ea6773bd3aa0b3c254fa37b43c97ca6d..8231411edd8c379a5da67582cfff523536e14dc0 100644 (file)
--- 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 d344bc76337ca2c13d2cbb862a8e86d2e2570214..2ff79047971428b99632349d1667784a99ddc2ed 100644 (file)
--- 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 e6c00c9435e1614b8dff175a3a164e29cb71467f..199accf850bdd8a94d5ab767bfb0a9d6d18d10b3 100644 (file)
--- 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 cd314f957148351514d024115dfd2fefecac9e6e..7c4d7c5a36d8dd70eb22b391c9e9aac070f44646 100644 (file)
--- 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 (file)
index 0000000..7dec263
--- /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 (file)
index 0000000..4c574f1
--- /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 738604f90fb9a1da2b670c640953a573d54dd957..03de15706a9331be2710ad3edfda3f6a31f73313 100644 (file)
--- 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 (file)
index 0000000..3a029b7
--- /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 (file)
index 0000000..e32c4ee
--- /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 (file)
index 0000000..ff4d219
--- /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 (file)
index 0000000..739da61
--- /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 (file)
index 0000000..1c17f3f
--- /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 28bcb460fdfb35fe9d05c57679aaf372706e0afe..ff47c6eae53ee1c15fe1c199d2af799448015599 100644 (file)
--- 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 5bff8d12a74ea3f35c7ab8c45c737c7318485b7f..f470f087458ec4994abf39a6d3884fc902624034 100644 (file)
--- 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 (file)
index 0000000..3149033
--- /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 25af3aae67a9ee077b534a59e306c781f86aa2c3..966611764e0cd03693f1527390ceb6e5f2457c4d 100644 (file)
--- 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 2f9f08302707791e72fbf3ca855000638bf781a7..3e777ec892bceefc66279e8c3493625163434c32 100644 (file)
--- 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 (file)
index 0000000..ddb0e39
--- /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 (file)
index 0000000..d82d956
--- /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 (file)
index 0000000..0c67ad0
--- /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 698f9ba2eaacacef8aba3aed080433a5e23f87e7..d2abf2fce1cdc9daefd01a0070cfc04fff5a2457 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -23,26 +23,6 @@
 
 #include <vector>
 
-#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 (file)
index 0000000..64a4f93
--- /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 (file)
index 0000000..1188198
--- /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 7f5fb459ec5477e8d340dbdd3c5008758ff75ae3..b8bdfabeb46db403ebbf9d1f070d70dddbffcd1b 100644 (file)
--- 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 (file)
index 0000000..593ce94
--- /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 (file)
index 0000000..b0b57d5
--- /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 (file)
index 0000000..085a59b
--- /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 (file)
index 0000000..39c1c35
--- /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 6985ae38ea88fec26e383069d20d50e586743821..e08f09bb673f62ba215460ed5522b8ab5c504720 100644 (file)
--- 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 <iostream>
 #include <utility>
 

diff --git a/src/util/cardinality.i b/src/util/cardinality.i
new file mode 100644 (file)
index 0000000..760f746
--- /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 (file)
index 0000000..17c1b97
--- /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 (file)
index 0000000..802f227
--- /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 1b1eb224e97bf19c0f73e4da809eea568e9b89e7..43a0354cacffe56a45062cf7fe6dbe17a9509b68 100644 (file)
--- 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 (file)
index 0000000..d3ff896
--- /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 10211970ff100f657bad32a0c3b040772510a5f3..bd3fee5979781b118e29486f3f1069281e662ca4 100644 (file)
--- 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 <ext/hash_map>
 namespace std { using namespace __gnu_cxx; }
 

diff --git a/src/util/hash.i b/src/util/hash.i
new file mode 100644 (file)
index 0000000..f2f1e66
--- /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 b2973081dd577655e6fcaa4cea394b18e5996b9e..b62feb512a3d982b93c6de64a64e55c8f3284f95 100644 (file)
--- 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 (file)
index 0000000..4aaa532
--- /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 (file)
index 0000000..cd261a7
--- /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 6daceb8fd588408050b03e11883d428b9f96401a..871fe528fe4516a002bf390fe2a90fdd67dd158f 100644 (file)
--- 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 (file)
index 0000000..ad4815a
--- /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 e096ff028a3ef301193458cd3ee2a1b61dad8762..da1efe68a578a156580d963c33936d5c65b6e54b 100644 (file)
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -23,6 +23,7 @@
 
 #include <ios>
 #include <iostream>
+#include <streambuf>
 #include <string>
 #include <cstdio>
 #include <cstdarg>
@@ -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 (file)
index 0000000..c272920
--- /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 (file)
index 0000000..2505a7c
--- /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 17c1e31fcd846d910c104d964682b38c6b0a5376..13cdb059b9a04564447dc2357cb3ac9f52ce4660 100644 (file)
--- 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 (file)
index 0000000..512d3ea
--- /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 a883500f992c175321ce7acd7267d587a829d03a..2f2c14ed81b8cf258e509f8b0c3f81b368143f3b 100644 (file)
--- 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 b97965169dffdbdc8a5f1f959d608171cc6a6507..37c3c8364f3fadfda25b322f09fc335619af0e78 100644 (file)
--- 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 (file)
index 0000000..c0d86b3
--- /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 (file)
index 0000000..c925f9f
--- /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 (file)
index 0000000..48828cb
--- /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 (file)
index 0000000..6b02414
--- /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"