Remove parser from bindings (#3779)

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 589890ead45b1e0dbe1a68191d891b4ef6f10fd6..b8452d1aa07dcda140609d3cea23e85d2f7f1960 100644 (file)
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -22,8 +22,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/ArrayType.java
   ${CMAKE_CURRENT_BINARY_DIR}/AscriptionType.java
   ${CMAKE_CURRENT_BINARY_DIR}/AscriptionTypeHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/AssertCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BenchmarkStatus.java
   ${CMAKE_CURRENT_BINARY_DIR}/BitVector.java
   ${CMAKE_CURRENT_BINARY_DIR}/BitVectorBitOf.java
   ${CMAKE_CURRENT_BINARY_DIR}/BitVectorBitOfHashFunction.java
@@ -37,8 +35,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/BitVectorSize.java
   ${CMAKE_CURRENT_BINARY_DIR}/BitVectorType.java
   ${CMAKE_CURRENT_BINARY_DIR}/BitVectorZeroExtend.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BlockModelCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BlockModelValuesCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/BoolHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/BooleanType.java
   ${CMAKE_CURRENT_BINARY_DIR}/CVC4.java
@@ -49,25 +45,11 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/Cardinality.java
   ${CMAKE_CURRENT_BINARY_DIR}/CardinalityBeth.java
   ${CMAKE_CURRENT_BINARY_DIR}/CardinalityUnknown.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CheckSatAssumingCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CheckSatCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CheckSynthCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Command.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommandFailure.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommandInterrupted.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommandPrintSuccess.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommandRecoverableFailure.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommandSequence.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommandStatus.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommandSuccess.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommandUnsupported.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CommentCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/Configuration.java
   ${CMAKE_CURRENT_BINARY_DIR}/ConstructorType.java
   ${CMAKE_CURRENT_BINARY_DIR}/Datatype.java
   ${CMAKE_CURRENT_BINARY_DIR}/DatatypeConstructor.java
   ${CMAKE_CURRENT_BINARY_DIR}/DatatypeConstructorArg.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeDeclarationCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/DatatypeHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/DatatypeIndexConstant.java
   ${CMAKE_CURRENT_BINARY_DIR}/DatatypeIndexConstantHashFunction.java
@@ -75,24 +57,9 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/DatatypeSelfType.java
   ${CMAKE_CURRENT_BINARY_DIR}/DatatypeType.java
   ${CMAKE_CURRENT_BINARY_DIR}/DatatypeUnresolvedType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DeclarationCheck.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DeclarationDefinitionCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DeclarationSequence.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DeclareFunctionCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DeclareSygusFunctionCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DeclareSygusPrimedVarCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DeclareSygusVarCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DeclareTypeCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DefineFunctionCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DefineFunctionRecCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DefineNamedFunctionCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DefineTypeCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/EchoCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/EmptyCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/EmptySet.java
   ${CMAKE_CURRENT_BINARY_DIR}/EmptySetHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/Exception.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ExpandDefinitionsCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/ExportUnsupportedException.java
   ${CMAKE_CURRENT_BINARY_DIR}/Expr.java
   ${CMAKE_CURRENT_BINARY_DIR}/ExprHashFunction.java
@@ -113,28 +80,12 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToUBV.java
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java
   ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetAbductCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetAssertionsCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetAssignmentCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetInfoCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetInstantiationsCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetModelCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetOptionCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetQuantifierEliminationCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetSynthSolutionCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetUnsatAssumptionsCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetUnsatCoreCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/GetValueCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Input.java
   ${CMAKE_CURRENT_BINARY_DIR}/InputLanguage.java
-  ${CMAKE_CURRENT_BINARY_DIR}/InputStream.java
-  ${CMAKE_CURRENT_BINARY_DIR}/InputStreamException.java
   ${CMAKE_CURRENT_BINARY_DIR}/IntToBitVector.java
   ${CMAKE_CURRENT_BINARY_DIR}/Integer.java
   ${CMAKE_CURRENT_BINARY_DIR}/IntegerHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/IntegerType.java
   ${CMAKE_CURRENT_BINARY_DIR}/JavaInputStreamAdapter.java
-  ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_CommandSequence.java
   ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_Datatype.java
   ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_DatatypeConstructor.java
   ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_Expr.java
@@ -151,18 +102,8 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java
   ${CMAKE_CURRENT_BINARY_DIR}/Options.java
   ${CMAKE_CURRENT_BINARY_DIR}/OutputLanguage.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ParseOp.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Parser.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ParserBuilder.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ParserEndOfFileException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ParserException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ParserExprStream.java
-  ${CMAKE_CURRENT_BINARY_DIR}/PopCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/PrettySExprs.java
   ${CMAKE_CURRENT_BINARY_DIR}/Proof.java
-  ${CMAKE_CURRENT_BINARY_DIR}/PushCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/QueryCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/QuitCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/Rational.java
   ${CMAKE_CURRENT_BINARY_DIR}/RationalHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/RealType.java
@@ -172,8 +113,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/RecordUpdateHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/RecoverableModalException.java
   ${CMAKE_CURRENT_BINARY_DIR}/RegExpType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ResetAssertionsCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ResetCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/Result.java
   ${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java
   ${CMAKE_CURRENT_BINARY_DIR}/RoundingModeType.java
@@ -182,7 +121,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SExprType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__api__Solver.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__options__InstFormatMode.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_LemmaChannels.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Listener.java
@@ -196,19 +134,10 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__unordered_mapT_CVC4__Expr_CVC4__ProofLetCount_CVC4__ExprHashFunction_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructorArg_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructor_t.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__SygusGTerm_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_std__pairT_CVC4__Expr_CVC4__Expr_t_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_std__vectorT_std__string_t_t.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ScopeException.java
   ${CMAKE_CURRENT_BINARY_DIR}/SelectorType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SetBenchmarkLogicCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SetBenchmarkStatusCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SetExpressionNameCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SetInfoCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SetOptionCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/SetType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SetUserAttributeCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SimplifyCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.java
   ${CMAKE_CURRENT_BINARY_DIR}/SortConstructorType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SortType.java
@@ -216,13 +145,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/Statistics.java
   ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java
   ${CMAKE_CURRENT_BINARY_DIR}/StringType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SygusConstraintCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SygusGTerm.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SygusInvConstraintCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
   ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
   ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdate.java
@@ -241,7 +164,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/hashmapExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/pairStringType.java
   ${CMAKE_CURRENT_BINARY_DIR}/setOfType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorCommandPtr.java
   ${CMAKE_CURRENT_BINARY_DIR}/vectorDatatype.java
   ${CMAKE_CURRENT_BINARY_DIR}/vectorDatatypeType.java
   ${CMAKE_CURRENT_BINARY_DIR}/vectorExpr.java

diff --git a/src/cvc4.i b/src/cvc4.i
index 6ed620960a786201a2740f51bc5fc4a9df01df7c..97462170e905684c29410cd2c244a0fcba578fe9 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -75,7 +75,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %}
 #endif /* SWIGPYTHON */
 
-%template(vectorCommandPtr) std::vector< CVC4::Command* >;
 %template(vectorType) std::vector< CVC4::Type >;
 %template(vectorExpr) std::vector< CVC4::Expr >;
 %template(vectorUnsignedInt) std::vector< unsigned int >;
@@ -164,7 +163,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %typemap(throws) CVC4::UnsafeInterruptException = CVC4::Exception;
 %typemap(throws) UnsafeInterruptException = CVC4::Exception;
 %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
-%typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
 
 // Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above
 %typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{
@@ -227,28 +225,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private";
 %javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private";
 
-%exception CVC4::parser::Parser::nextCommand() %{
-  try {
-    CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
-    $action
-  } catch(CVC4::Exception& e) {
-    std::stringstream ss;
-    ss << e.what() << ": " << e.getMessage();
-    std::string explanation = ss.str();
-    SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
-  }
-%}
-%exception CVC4::parser::Parser::nextExpression() %{
-  try {
-    CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
-    $action
-  } catch(CVC4::Exception& e) {
-    std::stringstream ss;
-    ss << e.what() << ": " << e.getMessage();
-    std::string explanation = ss.str();
-    SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
-  }
-%}
 %exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{
   try {
     jenv->DeleteGlobalRef(arg1->getInputStream());
@@ -347,12 +323,9 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "expr/expr.i"
 %include "expr/expr_manager.i"
 %include "expr/expr_stream.i"
-%include "expr/symbol_table.i"
 %include "expr/variable_type_map.i"
 %include "options/option_exception.i"
 %include "options/options.i"
-%include "parser/cvc4parser.i"
-%include "smt/command.i"
 %include "smt/logic_exception.i"
 %include "theory/logic_info.i"
 %include "theory/theory_id.i"

diff --git a/src/expr/symbol_table.i b/src/expr/symbol_table.i
deleted file mode 100644 (file)
index 7e5579c..0000000
--- a/src/expr/symbol_table.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "expr/symbol_table.h"
-%}
-
-%include "expr/symbol_table.h"

diff --git a/src/parser/cvc4parser.i b/src/parser/cvc4parser.i
deleted file mode 100644 (file)
index accb482..0000000
--- a/src/parser/cvc4parser.i
+++ /dev/null
@@ -1,16 +0,0 @@
-%import "bindings/swig.h"
-
-%module CVC4Parser
-// nspace completely broken with Java packaging
-//%nspace;
-
-%{
-namespace CVC4 {}
-using namespace CVC4;
-%}
-
-%include "parser/input.i"
-%include "parser/parse_op.i"
-%include "parser/parser.i"
-%include "parser/parser_builder.i"
-%include "parser/parser_exception.i"

diff --git a/src/parser/input.i b/src/parser/input.i
deleted file mode 100644 (file)
index 2a76e2b..0000000
--- a/src/parser/input.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "parser/input.h"
-%}
-
-%include "parser/input.h"

diff --git a/src/parser/parse_op.i b/src/parser/parse_op.i
deleted file mode 100644 (file)
index 37c3bd3..0000000
--- a/src/parser/parse_op.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "parser/parse_op.h"
-%}
-
-%include "parser/parse_op.h"

diff --git a/src/parser/parser.i b/src/parser/parser.i
deleted file mode 100644 (file)
index 37aefb9..0000000
--- a/src/parser/parser.i
+++ /dev/null
@@ -1,32 +0,0 @@
-%{
-#include "parser/parser.h"
-%}
-
-namespace CVC4 {
-  namespace parser {
-    enum DeclarationCheck;
-    enum SymbolType;
-    %ignore operator<<(std::ostream&, DeclarationCheck);
-    %ignore operator<<(std::ostream&, SymbolType);
-
-    class ParserExprStream : public CVC4::ExprStream {
-      Parser* d_parser;
-    public:
-      ParserExprStream(Parser* parser) : d_parser(parser) {}
-      ~ParserExprStream() { delete d_parser; }
-      Expr nextExpr() { return d_parser->nextExpression(); }
-    };/* class Parser::ExprStream */
-  }/* namespace CVC4::parser */
-}/* namespace CVC4 */
-
-%ignore CVC4::parser::Parser::ExprStream;
-
-%include "parser/parser.h"
-
-%{
-namespace CVC4 {
-  namespace parser {
-    typedef CVC4::parser::Parser::ExprStream ParserExprStream;
-  }
-}
-%}

diff --git a/src/parser/parser_builder.i b/src/parser/parser_builder.i
deleted file mode 100644 (file)
index 6b77356..0000000
--- a/src/parser/parser_builder.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "parser/parser_builder.h"
-%}
-
-%include "parser/parser_builder.h"

diff --git a/src/parser/parser_exception.i b/src/parser/parser_exception.i
deleted file mode 100644 (file)
index 39f67e6..0000000
--- a/src/parser/parser_exception.i
+++ /dev/null
@@ -1,8 +0,0 @@
-%{
-#include "parser/parser_exception.h"
-%}
-
-%ignore CVC4::parser::ParserException::ParserException(const char*);
-%ignore CVC4::parser::ParserEndOfFileException::ParserEndOfFileException(const char*);
-
-%include "parser/parser_exception.h"

diff --git a/src/smt/command.i b/src/smt/command.i
deleted file mode 100644 (file)
index bd28fa8..0000000
--- a/src/smt/command.i
+++ /dev/null
@@ -1,72 +0,0 @@
-%{
-#include "smt/command.h"
-
-#ifdef SWIGJAVA
-
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
-
-#endif /* SWIGJAVA */
-%}
-
-%ignore CVC4::operator<<(std::ostream&, const Command&);
-%ignore CVC4::operator<<(std::ostream&, const Command*);
-%ignore CVC4::operator<<(std::ostream&, const CommandStatus&);
-%ignore CVC4::operator<<(std::ostream&, const CommandStatus*);
-%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status);
-%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess);
-
-%ignore CVC4::GetProofCommand;
-
-#ifdef SWIGJAVA
-
-// Instead of CommandSequence::begin() and end(), create an
-// iterator() method on the Java side that returns a Java-style
-// Iterator.
-%ignore CVC4::CommandSequence::begin();
-%ignore CVC4::CommandSequence::end();
-%ignore CVC4::CommandSequence::begin() const;
-%ignore CVC4::CommandSequence::end() const;
-%extend CVC4::CommandSequence {
-  CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*> iterator()
-  {
-    return CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*>(
-        *$self);
-  }
-}
-
-// CommandSequence is "iterable" on the Java side
-%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.stanford.CVC4.Command>";
-
-// the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*> "java.util.Iterator<edu.stanford.CVC4.Command>";
-// add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*> "
-  public void remove() {
-    throw new java.lang.UnsupportedOperationException();
-  }
-
-  public edu.stanford.CVC4.Command next() {
-    if(hasNext()) {
-      return getNext();
-    } else {
-      throw new java.util.NoSuchElementException();
-    }
-  }
-"
-// getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*>::getNext() "private";
-
-#endif /* SWIGJAVA */
-
-%include "smt/command.h"
-
-#ifdef SWIGJAVA
-
-%include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
-
-%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*>;
-
-#endif /* SWIGJAVA */