From: Andres Noetzli Date: Thu, 20 Feb 2020 17:02:58 +0000 (-0800) Subject: Remove parser from bindings (#3779) X-Git-Tag: cvc5-1.0.0~3629 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=92f5835e86e6741eb6b273047e0a003212a8b638;p=cvc5.git Remove parser from bindings (#3779) --- diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 589890ead..b8452d1aa 100644 --- 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 6ed620960..97462170e 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -75,7 +75,6 @@ std::set 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 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 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 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 index 7e5579c49..000000000 --- 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 index accb4826c..000000000 --- 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 index 2a76e2b7a..000000000 --- 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 index 37c3bd30f..000000000 --- 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 index 37aefb901..000000000 --- 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 index 6b77356bc..000000000 --- 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 index 39f67e6f5..000000000 --- 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 index bd28fa8e5..000000000 --- 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 iterator() - { - return CVC4::JavaIteratorAdapter( - *$self); - } -} - -// CommandSequence is "iterable" on the Java side -%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; -// add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter " - 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::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; - -#endif /* SWIGJAVA */