Merge from "swig" branch: language binding for Java is compiling and linking. Enable with --enable-language-bindings=java

10 files changed, 162 insertions, 5 deletions

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:
 
@@ -191,6 +191,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,13 +179,46 @@ 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.
    *
    * @param i the index of the child