diff options
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/parser/antlr_input.cpp | 20 | ||||
| -rw-r--r-- | src/parser/antlr_input.h | 3 | ||||
| -rw-r--r-- | src/parser/antlr_input_imports.cpp | 12 | ||||
| -rw-r--r-- | src/parser/cvc/Cvc.g | 14 | ||||
| -rw-r--r-- | src/parser/cvc/cvc.cpp | 2 | ||||
| -rw-r--r-- | src/parser/cvc/cvc.h | 8 | ||||
| -rw-r--r-- | src/parser/input.h | 7 | ||||
| -rw-r--r-- | src/parser/input_parser.cpp | 6 | ||||
| -rw-r--r-- | src/parser/input_parser.h | 9 | ||||
| -rw-r--r-- | src/parser/parser.cpp | 905 | ||||
| -rw-r--r-- | src/parser/parser.h | 740 | ||||
| -rw-r--r-- | src/parser/parser_builder.cpp | 152 | ||||
| -rw-r--r-- | src/parser/parser_builder.h | 135 | ||||
| -rw-r--r-- | src/parser/parser_state.cpp | 933 | ||||
| -rw-r--r-- | src/parser/parser_state.h | 775 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 28 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 18 | ||||
| -rw-r--r-- | src/parser/tptp/tptp.cpp | 4 | ||||
| -rw-r--r-- | src/parser/tptp/tptp.h | 7 |
20 files changed, 1864 insertions, 1918 deletions
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 81c7646f3..ceb3037d9 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -48,8 +48,8 @@ set(libcvc5parser_src_files parse_op.h parser.cpp parser.h - parser_builder.cpp - parser_builder.h + parser_state.cpp + parser_state.h parser_exception.h smt2/smt2.cpp smt2/smt2.h diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 73d1b89b5..7d8839c49 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -16,6 +16,7 @@ #include "parser/antlr_input.h" #include <antlr3.h> + #include <limits> #include "base/check.h" @@ -26,8 +27,8 @@ #include "parser/cvc/cvc_input.h" #include "parser/input.h" #include "parser/memory_mapped_input_buffer.h" -#include "parser/parser.h" #include "parser/parser_exception.h" +#include "parser/parser_state.h" #include "parser/smt2/smt2_input.h" #include "parser/smt2/sygus_input.h" #include "parser/tptp/tptp_input.h" @@ -267,11 +268,11 @@ pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() { void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); - Assert(lexer != NULL); - Parser *parser = (Parser*)(lexer->super); - Assert(parser != NULL); - AntlrInput *input = (AntlrInput*) parser->getInput(); - Assert(input != NULL); + Assert(lexer != nullptr); + ParserState* state = (ParserState*)(lexer->super); + Assert(state != nullptr); + AntlrInput* input = (AntlrInput*)state->getInput(); + Assert(input != nullptr); /* Call the error display routine *if* there's not already a * parse error pending. If a parser error is pending, this @@ -513,13 +514,14 @@ void AntlrInput::setAntlr3Lexer(pANTLR3_LEXER pLexer) { d_lexer->rec->state->tokSource->nextToken = &nextToken; } -void AntlrInput::setParser(Parser& parser) { +void AntlrInput::setParserState(ParserState* state) +{ // ANTLR isn't using super in the lexer or the parser, AFAICT. // We could also use @lexer/parser::context to add a field to the generated // objects, but then it would have to be declared separately in every // language's grammar and we'd have to in the address of the field anyway. - d_lexer->super = &parser; - d_parser->super = &parser; + d_lexer->super = state; + d_parser->super = state; } void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) { diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index c74962188..2c265714a 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -31,6 +31,7 @@ #include "parser/input.h" #include "parser/line_buffer.h" #include "parser/parser_exception.h" +#include "parser/parser_state.h" namespace cvc5 { namespace parser { @@ -209,7 +210,7 @@ protected: void setAntlr3Parser(pANTLR3_PARSER pParser); /** Set the Parser object for this input. */ - void setParser(Parser& parser) override; + void setParserState(ParserState* state) override; };/* class AntlrInput */ inline std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) { diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index c04349491..5b1dec5b5 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -56,8 +56,8 @@ #include "base/check.h" #include "parser/antlr_input.h" -#include "parser/parser.h" #include "parser/parser_exception.h" +#include "parser/parser_state.h" using namespace std; @@ -92,11 +92,11 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // Dig the cvc5 objects out of the ANTLR3 mess pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); - Assert(antlr3Parser != NULL); - Parser *parser = (Parser*)(antlr3Parser->super); - Assert(parser != NULL); - AntlrInput *input = (AntlrInput*) parser->getInput() ; - Assert(input != NULL); + Assert(antlr3Parser != nullptr); + ParserState* state = (ParserState*)(antlr3Parser->super); + Assert(state != nullptr); + AntlrInput* input = (AntlrInput*)state->getInput(); + Assert(input != nullptr); // Signal we are in error recovery now recognizer->state->errorRecovery = ANTLR3_TRUE; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 6e3332651..0061fed1e 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -429,7 +429,7 @@ unsigned findPivot(const std::vector<unsigned>& operators, return pivot; }/* findPivot() */ -cvc5::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, +cvc5::api::Term createPrecedenceTree(ParserState* state, api::Solver* solver, const std::vector<cvc5::api::Term>& expressions, const std::vector<unsigned>& operators, unsigned startIndex, unsigned stopIndex) { @@ -447,9 +447,9 @@ cvc5::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, bool negate; api::Kind k = getOperatorKind(operators[pivot], negate); cvc5::api::Term lhs = createPrecedenceTree( - parser, solver, expressions, operators, startIndex, pivot); + state, solver, expressions, operators, startIndex, pivot); cvc5::api::Term rhs = createPrecedenceTree( - parser, solver, expressions, operators, pivot + 1, stopIndex); + state, solver, expressions, operators, pivot + 1, stopIndex); if (lhs.getSort().isSet()) { @@ -475,7 +475,7 @@ cvc5::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, return negate ? e.notTerm() : e; }/* createPrecedenceTree() recursive variant */ -api::Term createPrecedenceTree(Parser* parser, api::Solver* s, +api::Term createPrecedenceTree(ParserState* state, api::Solver* s, const std::vector<cvc5::api::Term>& expressions, const std::vector<unsigned>& operators) { if(Debug.isOn("prec") && operators.size() > 1) { @@ -489,7 +489,7 @@ api::Term createPrecedenceTree(Parser* parser, api::Solver* s, } api::Term e = createPrecedenceTree( - parser, s, expressions, operators, 0, expressions.size() - 1); + state, s, expressions, operators, 0, expressions.size() - 1); if(Debug.isOn("prec") && operators.size() > 1) { language::SetLanguage::Scope ls(Debug("prec"), language::output::LANG_AST); Debug("prec") << "=> " << e << std::endl; @@ -566,7 +566,7 @@ namespace cvc5 { #include "base/output.h" #include "parser/antlr_input.h" -#include "parser/parser.h" +#include "parser/parser_state.h" #define REPEAT_COMMAND(k, CommandCtor) \ ({ \ @@ -588,7 +588,7 @@ using namespace cvc5::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ #undef PARSER_STATE -#define PARSER_STATE ((Parser*)PARSER->super) +#define PARSER_STATE ((ParserState*)PARSER->super) #undef SOLVER #define SOLVER PARSER_STATE->getSolver() #undef MK_TERM diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp index 0f87e42cd..abe45378e 100644 --- a/src/parser/cvc/cvc.cpp +++ b/src/parser/cvc/cvc.cpp @@ -21,7 +21,7 @@ namespace parser { void Cvc::forceLogic(const std::string& logic) { - Parser::forceLogic(logic); + ParserState::forceLogic(logic); preemptCommand(new SetBenchmarkLogicCommand(logic)); } diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h index 23fbd0f7e..bb1bb197d 100644 --- a/src/parser/cvc/cvc.h +++ b/src/parser/cvc/cvc.h @@ -19,15 +19,15 @@ #define CVC5__PARSER__CVC_H #include "api/cpp/cvc5.h" -#include "parser/parser.h" +#include "parser/parser_state.h" namespace cvc5 { namespace parser { -class Cvc : public Parser +class Cvc : public ParserState { - friend class ParserBuilder; + friend class Parser; public: void forceLogic(const std::string& logic) override; @@ -41,7 +41,7 @@ class Cvc : public Parser InputLanguage lang, bool strictMode = false, bool parseOnly = false) - : Parser(solver, sm, lang, strictMode, parseOnly) + : ParserState(solver, sm, lang, strictMode, parseOnly) { } }; diff --git a/src/parser/input.h b/src/parser/input.h index 250fa94aa..eb7456f5a 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -35,6 +35,8 @@ class Command; namespace parser { +class ParserState; + class InputStreamException : public Exception { public: @@ -81,7 +83,8 @@ class Parser; */ class CVC5_EXPORT Input { - friend class Parser; // for parseError, parseCommand, parseExpr + friend class Parser; // for setParserState + friend class ParserState; // for parseError, parseCommand, parseExpr friend class InputParser; // for parseError, parseCommand, parseExpr friend class ParserBuilder; @@ -172,7 +175,7 @@ class CVC5_EXPORT Input virtual api::Term parseExpr() = 0; /** Set the Parser object for this input. */ - virtual void setParser(Parser& parser) = 0; + virtual void setParserState(ParserState* state) = 0; }; /* class Input */ diff --git a/src/parser/input_parser.cpp b/src/parser/input_parser.cpp index 01bd77b8d..62b74d398 100644 --- a/src/parser/input_parser.cpp +++ b/src/parser/input_parser.cpp @@ -17,7 +17,7 @@ #include "base/output.h" #include "parser/input.h" -#include "parser/parser.h" +#include "parser/parser_state.h" #include "smt/command.h" namespace cvc5 { @@ -82,7 +82,9 @@ api::Term InputParser::nextExpression() return result; } -InputParser::InputParser(Parser* state, Input* input) +bool InputParser::done() { return d_state->done(); } + +InputParser::InputParser(ParserState* state, Input* input) : d_state(state), d_input(input) { } diff --git a/src/parser/input_parser.h b/src/parser/input_parser.h index a96aa0d7e..088f791c5 100644 --- a/src/parser/input_parser.h +++ b/src/parser/input_parser.h @@ -31,6 +31,7 @@ namespace parser { class Input; class Parser; +class ParserState; /** * This class is the main interface for retrieving commands and expressions @@ -39,6 +40,7 @@ class Parser; class CVC5_EXPORT InputParser { friend Parser; + friend ParserState; public: /** Parse and return the next command. */ @@ -47,6 +49,9 @@ class CVC5_EXPORT InputParser /** Parse and return the next expression. */ api::Term nextExpression(); + /** Is this input parser done? */ + bool done(); + private: /** * Constructor. @@ -54,10 +59,10 @@ class CVC5_EXPORT InputParser * @param state The parser state to use. * @param input The input to parse. This class takes ownership. */ - InputParser(Parser* state, Input* input); + InputParser(ParserState* state, Input* input); /** The parser state */ - Parser* d_state; + ParserState* d_state; /** The underlying input */ std::unique_ptr<Input> d_input; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 8512f55eb..2dae6632b 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -10,896 +10,109 @@ * directory for licensing information. * **************************************************************************** * - * Parser state implementation. + * API of the cvc5 parser implementation. */ #include "parser/parser.h" -#include <clocale> -#include <fstream> #include <iostream> -#include <iterator> -#include <memory> -#include <sstream> -#include <unordered_set> #include "api/cpp/cvc5.h" -#include "base/check.h" -#include "base/output.h" -#include "expr/kind.h" #include "options/options.h" +#include "parser/cvc/cvc.h" #include "parser/input.h" #include "parser/input_parser.h" -#include "parser/parser_exception.h" -#include "smt/command.h" - -using namespace std; -using namespace cvc5::kind; +#include "parser/smt2/smt2.h" +#include "parser/tptp/tptp.h" namespace cvc5 { namespace parser { -Parser::Parser(api::Solver* solver, - SymbolManager* sm, - InputLanguage lang, - bool strictMode, - bool parseOnly) - : d_symman(sm), - d_lang(lang), - d_symtab(sm->getSymbolTable()), - d_assertionLevel(0), - d_anonymousFunctionCount(0), - d_done(true), - d_checksEnabled(true), - d_strictMode(strictMode), - d_parseOnly(parseOnly), - d_canIncludeFile(true), - d_logicIsForced(false), - d_forcedLogic(), - d_solver(solver) -{ -} - -Parser::~Parser() { - for (std::list<Command*>::iterator iter = d_commandQueue.begin(); - iter != d_commandQueue.end(); ++iter) { - Command* command = *iter; - delete command; - } - d_commandQueue.clear(); -} - -std::unique_ptr<InputParser> Parser::parseFile(const std::string& fname, - bool useMmap) -{ - d_input = Input::newFileInput(d_lang, fname, useMmap); - d_input->setParser(*this); - d_done = false; - return std::unique_ptr<InputParser>(new InputParser(this, d_input)); -} - -std::unique_ptr<InputParser> Parser::parseStream(const std::string& name, - std::istream& stream) -{ - d_input = Input::newStreamInput(d_lang, stream, name); - d_input->setParser(*this); - d_done = false; - return std::unique_ptr<InputParser>(new InputParser(this, d_input)); -} - -std::unique_ptr<InputParser> Parser::parseString(const std::string& name, - const std::string& str) -{ - d_input = Input::newStringInput(d_lang, str, name); - d_input->setParser(*this); - d_done = false; - return std::unique_ptr<InputParser>(new InputParser(this, d_input)); -} - -api::Solver* Parser::getSolver() const { return d_solver; } - -api::Term Parser::getSymbol(const std::string& name, SymbolType type) -{ - checkDeclaration(name, CHECK_DECLARED, type); - Assert(isDeclared(name, type)); - Assert(type == SYM_VARIABLE); - // Functions share var namespace - return d_symtab->lookup(name); -} - -void Parser::forceLogic(const std::string& logic) -{ - Assert(!d_logicIsForced); - d_logicIsForced = true; - d_forcedLogic = logic; -} - -api::Term Parser::getVariable(const std::string& name) -{ - return getSymbol(name, SYM_VARIABLE); -} - -api::Term Parser::getFunction(const std::string& name) -{ - return getSymbol(name, SYM_VARIABLE); -} - -api::Term Parser::getExpressionForName(const std::string& name) -{ - api::Sort t; - return getExpressionForNameAndType(name, t); -} - -api::Term Parser::getExpressionForNameAndType(const std::string& name, - api::Sort t) -{ - Assert(isDeclared(name)); - // first check if the variable is declared and not overloaded - api::Term expr = getVariable(name); - if(expr.isNull()) { - // the variable is overloaded, try with type if the type exists - if(!t.isNull()) { - // if we decide later to support annotations for function types, this will update to - // separate t into ( argument types, return type ) - expr = getOverloadedConstantForType(name, t); - if(expr.isNull()) { - parseError("Cannot get overloaded constant for type ascription."); - } - }else{ - parseError("Overloaded constants must be type cast."); - } - } - // now, post-process the expression - Assert(!expr.isNull()); - api::Sort te = expr.getSort(); - if (te.isConstructor() && te.getConstructorArity() == 0) - { - // nullary constructors have APPLY_CONSTRUCTOR kind with no children - expr = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, expr); - } - return expr; -} - -bool Parser::getTesterName(api::Term cons, std::string& name) { return false; } - -api::Kind Parser::getKindForFunction(api::Term fun) -{ - api::Sort t = fun.getSort(); - if (t.isFunction()) - { - return api::APPLY_UF; - } - else if (t.isConstructor()) - { - return api::APPLY_CONSTRUCTOR; - } - else if (t.isSelector()) - { - return api::APPLY_SELECTOR; - } - else if (t.isTester()) - { - return api::APPLY_TESTER; - } - else if (t.isUpdater()) - { - return api::APPLY_UPDATER; - } - return api::UNDEFINED_KIND; -} - -api::Sort Parser::getSort(const std::string& name) -{ - checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - Assert(isDeclared(name, SYM_SORT)); - api::Sort t = d_symtab->lookupType(name); - return t; -} - -api::Sort Parser::getSort(const std::string& name, - const std::vector<api::Sort>& params) -{ - checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - Assert(isDeclared(name, SYM_SORT)); - api::Sort t = d_symtab->lookupType(name, params); - return t; -} - -size_t Parser::getArity(const std::string& sort_name) { - checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); - Assert(isDeclared(sort_name, SYM_SORT)); - return d_symtab->lookupArity(sort_name); -} - -/* Returns true if name is bound to a boolean variable. */ -bool Parser::isBoolean(const std::string& name) { - api::Term expr = getVariable(name); - return !expr.isNull() && expr.getSort().isBoolean(); -} - -bool Parser::isFunctionLike(api::Term fun) -{ - if(fun.isNull()) { - return false; - } - api::Sort type = fun.getSort(); - return type.isFunction() || type.isConstructor() || type.isTester() || - type.isSelector(); -} - -/* Returns true if name is bound to a function returning boolean. */ -bool Parser::isPredicate(const std::string& name) { - api::Term expr = getVariable(name); - return !expr.isNull() && expr.getSort().isPredicate(); -} - -api::Term Parser::bindVar(const std::string& name, - const api::Sort& type, - bool levelZero, - bool doOverload) -{ - bool globalDecls = d_symman->getGlobalDeclarations(); - Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl; - api::Term expr = d_solver->mkConst(type, name); - defineVar(name, expr, globalDecls || levelZero, doOverload); - return expr; -} - -api::Term Parser::bindBoundVar(const std::string& name, const api::Sort& type) -{ - Debug("parser") << "bindBoundVar(" << name << ", " << type << ")" - << std::endl; - api::Term expr = d_solver->mkVar(type, name); - defineVar(name, expr); - return expr; -} - -std::vector<api::Term> Parser::bindBoundVars( - std::vector<std::pair<std::string, api::Sort> >& sortedVarNames) -{ - std::vector<api::Term> vars; - for (std::pair<std::string, api::Sort>& i : sortedVarNames) - { - vars.push_back(bindBoundVar(i.first, i.second)); - } - return vars; -} - -std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names, - const api::Sort& type, - bool levelZero, - bool doOverload) -{ - std::vector<api::Term> vars; - for (unsigned i = 0; i < names.size(); ++i) { - vars.push_back(bindVar(names[i], type, levelZero, doOverload)); - } - return vars; -} - -std::vector<api::Term> Parser::bindBoundVars( - const std::vector<std::string> names, const api::Sort& type) -{ - std::vector<api::Term> vars; - for (unsigned i = 0; i < names.size(); ++i) { - vars.push_back(bindBoundVar(names[i], type)); - } - return vars; -} - -void Parser::defineVar(const std::string& name, - const api::Term& val, - bool levelZero, - bool doOverload) -{ - Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl; - if (!d_symtab->bind(name, val, levelZero, doOverload)) - { - std::stringstream ss; - ss << "Cannot bind " << name << " to symbol of type " << val.getSort(); - ss << ", maybe the symbol has already been defined?"; - parseError(ss.str()); - } - Assert(isDeclared(name)); -} - -void Parser::defineType(const std::string& name, - const api::Sort& type, - bool levelZero, - bool skipExisting) -{ - if (skipExisting && isDeclared(name, SYM_SORT)) - { - Assert(d_symtab->lookupType(name) == type); - return; - } - d_symtab->bindType(name, type, levelZero); - Assert(isDeclared(name, SYM_SORT)); -} - -void Parser::defineType(const std::string& name, - const std::vector<api::Sort>& params, - const api::Sort& type, - bool levelZero) -{ - d_symtab->bindType(name, params, type, levelZero); - Assert(isDeclared(name, SYM_SORT)); -} - -void Parser::defineParameterizedType(const std::string& name, - const std::vector<api::Sort>& params, - const api::Sort& type) -{ - if (Debug.isOn("parser")) { - Debug("parser") << "defineParameterizedType(" << name << ", " - << params.size() << ", ["; - if (params.size() > 0) { - copy(params.begin(), - params.end() - 1, - ostream_iterator<api::Sort>(Debug("parser"), ", ")); - Debug("parser") << params.back(); - } - Debug("parser") << "], " << type << ")" << std::endl; - } - defineType(name, params, type); -} - -api::Sort Parser::mkSort(const std::string& name) -{ - Debug("parser") << "newSort(" << name << ")" << std::endl; - bool globalDecls = d_symman->getGlobalDeclarations(); - api::Sort type = d_solver->mkUninterpretedSort(name); - defineType(name, type, globalDecls); - return type; -} - -api::Sort Parser::mkSortConstructor(const std::string& name, size_t arity) -{ - Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" - << std::endl; - bool globalDecls = d_symman->getGlobalDeclarations(); - api::Sort type = d_solver->mkSortConstructorSort(name, arity); - defineType(name, vector<api::Sort>(arity), type, globalDecls); - return type; -} - -api::Sort Parser::mkUnresolvedType(const std::string& name) -{ - api::Sort unresolved = d_solver->mkUninterpretedSort(name); - defineType(name, unresolved); - d_unresolved.insert(unresolved); - return unresolved; -} - -api::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name, - size_t arity) -{ - api::Sort unresolved = d_solver->mkSortConstructorSort(name, arity); - defineType(name, vector<api::Sort>(arity), unresolved); - d_unresolved.insert(unresolved); - return unresolved; -} - -api::Sort Parser::mkUnresolvedTypeConstructor( - const std::string& name, const std::vector<api::Sort>& params) -{ - Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() - << ")" << std::endl; - api::Sort unresolved = d_solver->mkSortConstructorSort(name, params.size()); - defineType(name, params, unresolved); - api::Sort t = getSort(name, params); - d_unresolved.insert(unresolved); - return unresolved; -} - -api::Sort Parser::mkUnresolvedType(const std::string& name, size_t arity) +Parser::Parser(api::Solver* solver, SymbolManager* sm, const Options& options) + : d_solver(solver), + d_symman(sm), + d_lang(options.getInputLanguage()), + d_state(nullptr) { - if (arity == 0) + bool strictMode = options.getStrictParsing(); + bool parseOnly = options.getParseOnly(); + switch (d_lang) { - return mkUnresolvedType(name); - } - return mkUnresolvedTypeConstructor(name, arity); -} - -bool Parser::isUnresolvedType(const std::string& name) { - if (!isDeclared(name, SYM_SORT)) { - return false; - } - return d_unresolved.find(getSort(name)) != d_unresolved.end(); -} - -std::vector<api::Sort> Parser::bindMutualDatatypeTypes( - std::vector<api::DatatypeDecl>& datatypes, bool doOverload) -{ - try { - std::vector<api::Sort> types = - d_solver->mkDatatypeSorts(datatypes, d_unresolved); - - Assert(datatypes.size() == types.size()); - bool globalDecls = d_symman->getGlobalDeclarations(); - - for (unsigned i = 0; i < datatypes.size(); ++i) { - api::Sort t = types[i]; - const api::Datatype& dt = t.getDatatype(); - const std::string& name = dt.getName(); - Debug("parser-idt") << "define " << name << " as " << t << std::endl; - if (isDeclared(name, SYM_SORT)) { - throw ParserException(name + " already declared"); - } - if (t.isParametricDatatype()) + case language::input::LANG_SYGUS_V2: + d_state.reset( + new Smt2(d_solver, d_symman, d_lang, strictMode, parseOnly)); + break; + case language::input::LANG_TPTP: + d_state.reset( + new Tptp(d_solver, d_symman, d_lang, strictMode, parseOnly)); + break; + default: + if (language::isInputLang_smt2(d_lang)) { - std::vector<api::Sort> paramTypes = t.getDatatypeParamSorts(); - defineType(name, paramTypes, t, globalDecls); + d_state.reset( + new Smt2(d_solver, d_symman, d_lang, strictMode, parseOnly)); } else { - defineType(name, t, globalDecls); - } - std::unordered_set< std::string > consNames; - std::unordered_set< std::string > selNames; - for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) - { - const api::DatatypeConstructor& ctor = dt[j]; - api::Term constructor = ctor.getConstructorTerm(); - Debug("parser-idt") << "+ define " << constructor << std::endl; - string constructorName = ctor.getName(); - if(consNames.find(constructorName)==consNames.end()) { - if(!doOverload) { - checkDeclaration(constructorName, CHECK_UNDECLARED); - } - defineVar(constructorName, constructor, globalDecls, doOverload); - consNames.insert(constructorName); - }else{ - throw ParserException(constructorName + " already declared in this datatype"); - } - std::string testerName; - if (getTesterName(constructor, testerName)) - { - api::Term tester = ctor.getTesterTerm(); - Debug("parser-idt") << "+ define " << testerName << std::endl; - if (!doOverload) - { - checkDeclaration(testerName, CHECK_UNDECLARED); - } - defineVar(testerName, tester, globalDecls, doOverload); - } - for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++) - { - const api::DatatypeSelector& sel = ctor[k]; - api::Term selector = sel.getSelectorTerm(); - Debug("parser-idt") << "+++ define " << selector << std::endl; - string selectorName = sel.getName(); - if(selNames.find(selectorName)==selNames.end()) { - if(!doOverload) { - checkDeclaration(selectorName, CHECK_UNDECLARED); - } - defineVar(selectorName, selector, globalDecls, doOverload); - selNames.insert(selectorName); - }else{ - throw ParserException(selectorName + " already declared in this datatype"); - } - } - } - } - - // These are no longer used, and the ExprManager would have - // complained of a bad substitution if anything is left unresolved. - // Clear out the set. - d_unresolved.clear(); - - // throw exception if any datatype is not well-founded - for (unsigned i = 0; i < datatypes.size(); ++i) { - const api::Datatype& dt = types[i].getDatatype(); - if (!dt.isCodatatype() && !dt.isWellFounded()) { - throw ParserException(dt.getName() + " is not well-founded"); + d_state.reset( + new Cvc(d_solver, d_symman, d_lang, strictMode, parseOnly)); } - } - return types; - } catch (IllegalArgumentException& ie) { - throw ParserException(ie.getMessage()); + break; } -} -api::Sort Parser::mkFlatFunctionType(std::vector<api::Sort>& sorts, - api::Sort range, - std::vector<api::Term>& flattenVars) -{ - if (range.isFunction()) + if (options.getSemanticChecks()) { - std::vector<api::Sort> domainTypes = range.getFunctionDomainSorts(); - for (unsigned i = 0, size = domainTypes.size(); i < size; i++) - { - sorts.push_back(domainTypes[i]); - // the introduced variable is internal (not parsable) - std::stringstream ss; - ss << "__flatten_var_" << i; - api::Term v = d_solver->mkVar(domainTypes[i], ss.str()); - flattenVars.push_back(v); - } - range = range.getFunctionCodomainSort(); + d_state->enableChecks(); } - if (sorts.empty()) + else { - return range; + d_state->disableChecks(); } - return d_solver->mkFunctionSort(sorts, range); -} -api::Sort Parser::mkFlatFunctionType(std::vector<api::Sort>& sorts, - api::Sort range) -{ - if (sorts.empty()) - { - // no difference - return range; - } - if (Debug.isOn("parser")) - { - Debug("parser") << "mkFlatFunctionType: range " << range << " and domains "; - for (api::Sort t : sorts) - { - Debug("parser") << " " << t; - } - Debug("parser") << "\n"; - } - while (range.isFunction()) + if (options.getFilesystemAccess()) { - std::vector<api::Sort> domainTypes = range.getFunctionDomainSorts(); - sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end()); - range = range.getFunctionCodomainSort(); + d_state->allowIncludeFile(); } - return d_solver->mkFunctionSort(sorts, range); -} - -api::Term Parser::mkHoApply(api::Term expr, const std::vector<api::Term>& args) -{ - for (unsigned i = 0; i < args.size(); i++) + else { - expr = d_solver->mkTerm(api::HO_APPLY, expr, args[i]); + d_state->disallowIncludeFile(); } - return expr; -} -api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) -{ - api::Kind k = t.getKind(); - if (k == api::EMPTYSET) + if (options.wasSetByUserForceLogicString()) { - t = d_solver->mkEmptySet(s); - } - else if (k == api::EMPTYBAG) - { - t = d_solver->mkEmptyBag(s); - } - else if (k == api::CONST_SEQUENCE) - { - if (!s.isSequence()) - { - std::stringstream ss; - ss << "Type ascription on empty sequence must be a sequence, got " << s; - parseError(ss.str()); - } - if (!t.getConstSequenceElements().empty()) - { - std::stringstream ss; - ss << "Cannot apply a type ascription to a non-empty sequence"; - parseError(ss.str()); - } - t = d_solver->mkEmptySequence(s.getSequenceElementSort()); - } - else if (k == api::UNIVERSE_SET) - { - t = d_solver->mkUniverseSet(s); - } - else if (k == api::SEP_NIL) - { - t = d_solver->mkSepNil(s); - } - else if (k == api::APPLY_CONSTRUCTOR) - { - std::vector<api::Term> children(t.begin(), t.end()); - // apply type ascription to the operator and reconstruct - children[0] = applyTypeAscription(children[0], s); - t = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, children); - } - // !!! temporary until datatypes are refactored in the new API - api::Sort etype = t.getSort(); - if (etype.isConstructor()) - { - // Type ascriptions only have an effect on the node structure if this is a - // parametric datatype. - if (s.isParametricDatatype()) - { - // get the datatype that t belongs to - api::Sort etyped = etype.getConstructorCodomainSort(); - api::Datatype d = etyped.getDatatype(); - // lookup by name - api::DatatypeConstructor dc = d.getConstructor(t.toString()); - // ask the constructor for the specialized constructor term - t = dc.getSpecializedConstructorTerm(s); - } - // the type of t does not match the sort s by design (constructor type - // vs datatype type), thus we use an alternative check here. - if (t.getSort().getConstructorCodomainSort() != s) - { - std::stringstream ss; - ss << "Type ascription on constructor not satisfied, term " << t - << " expected sort " << s << " but has sort " - << t.getSort().getConstructorCodomainSort(); - parseError(ss.str()); - } - return t; - } - // otherwise, nothing to do - // check that the type is correct - if (t.getSort() != s) - { - std::stringstream ss; - ss << "Type ascription not satisfied, term " << t << " expected sort " << s - << " but has sort " << t.getSort(); - parseError(ss.str()); - } - return t; -} - -bool Parser::isDeclared(const std::string& name, SymbolType type) { - switch (type) { - case SYM_VARIABLE: return d_symtab->isBound(name); - case SYM_SORT: - return d_symtab->isBoundType(name); - } - Assert(false); // Unhandled(type); - return false; -} - -void Parser::checkDeclaration(const std::string& varName, - DeclarationCheck check, - SymbolType type, - std::string notes) -{ - if (!d_checksEnabled) { - return; - } - - switch (check) { - case CHECK_DECLARED: - if (!isDeclared(varName, type)) { - parseError("Symbol '" + varName + "' not declared as a " + - (type == SYM_VARIABLE ? "variable" : "type") + - (notes.size() == 0 ? notes : "\n" + notes)); - } - break; - - case CHECK_UNDECLARED: - if (isDeclared(varName, type)) { - parseError("Symbol '" + varName + "' previously declared as a " + - (type == SYM_VARIABLE ? "variable" : "type") + - (notes.size() == 0 ? notes : "\n" + notes)); - } - break; - - case CHECK_NONE: - break; - - default: Assert(false); // Unhandled(check); + LogicInfo tmp(options.getForceLogicString()); + d_state->forceLogic(tmp.getLogicString()); } } -void Parser::checkFunctionLike(api::Term fun) -{ - if (d_checksEnabled && !isFunctionLike(fun)) { - stringstream ss; - ss << "Expecting function-like symbol, found '"; - ss << fun; - ss << "'"; - parseError(ss.str()); - } -} - -bool Parser::hasCommand() { return !d_commandQueue.empty(); } - -void Parser::addOperator(api::Kind kind) { d_logicOperators.insert(kind); } - -void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); } - -Command* Parser::getNextCommand() -{ - Assert(!d_commandQueue.empty()); - Command* cmd = d_commandQueue.front(); - d_commandQueue.pop_front(); - return cmd; -} - -void Parser::attributeNotSupported(const std::string& attr) { - if (d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) { - stringstream ss; - ss << "warning: Attribute '" << attr - << "' not supported (ignoring this and all following uses)"; - d_input->warning(ss.str()); - d_attributesWarnedAbout.insert(attr); - } -} - -size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); } - -void Parser::pushScope(bool isUserContext) -{ - d_symman->pushScope(isUserContext); -} - -void Parser::popScope() +std::unique_ptr<InputParser> Parser::parseFile(const std::string& fname, + bool useMmap) { - d_symman->popScope(); + Input* input = Input::newFileInput(d_lang, fname, useMmap); + d_state->setInput(input); + input->setParserState(d_state.get()); + d_state->setDone(false); + return std::unique_ptr<InputParser>(new InputParser(d_state.get(), input)); } -void Parser::reset() {} - -SymbolManager* Parser::getSymbolManager() { return d_symman; } - -std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) +std::unique_ptr<InputParser> Parser::parseStream(const std::string& name, + std::istream& stream) { - std::wstring ws; - { - std::setlocale(LC_ALL, "en_US.utf8"); - std::mbtowc(nullptr, nullptr, 0); - const char* end = s.data() + s.size(); - const char* ptr = s.data(); - for (wchar_t c; ptr != end; ) { - int res = std::mbtowc(&c, ptr, end - ptr); - if (res == -1) { - std::cerr << "Invalid escape sequence in " << s << std::endl; - break; - } else if (res == 0) { - break; - } else { - ws += c; - ptr += res; - } - } - } - - std::vector<unsigned> str; - unsigned i = 0; - while (i < ws.size()) - { - // get the current character - if (ws[i] != '\\') - { - // don't worry about printable here - str.push_back(static_cast<unsigned>(ws[i])); - ++i; - continue; - } - // slash is always escaped - ++i; - if (i >= ws.size()) - { - // slash cannot be the last character if we are parsing escape sequences - std::stringstream serr; - serr << "Escape sequence at the end of string: \"" << s - << "\" should be handled by lexer"; - parseError(serr.str()); - } - switch (ws[i]) - { - case 'n': - { - str.push_back(static_cast<unsigned>('\n')); - i++; - } - break; - case 't': - { - str.push_back(static_cast<unsigned>('\t')); - i++; - } - break; - case 'v': - { - str.push_back(static_cast<unsigned>('\v')); - i++; - } - break; - case 'b': - { - str.push_back(static_cast<unsigned>('\b')); - i++; - } - break; - case 'r': - { - str.push_back(static_cast<unsigned>('\r')); - i++; - } - break; - case 'f': - { - str.push_back(static_cast<unsigned>('\f')); - i++; - } - break; - case 'a': - { - str.push_back(static_cast<unsigned>('\a')); - i++; - } - break; - case '\\': - { - str.push_back(static_cast<unsigned>('\\')); - i++; - } - break; - case 'x': - { - bool isValid = false; - if (i + 2 < ws.size()) - { - if (std::isxdigit(ws[i + 1]) && std::isxdigit(ws[i + 2])) - { - std::wstringstream shex; - shex << ws[i + 1] << ws[i + 2]; - unsigned val; - shex >> std::hex >> val; - str.push_back(val); - i += 3; - isValid = true; - } - } - if (!isValid) - { - std::stringstream serr; - serr << "Illegal String Literal: \"" << s - << "\", must have two digits after \\x"; - parseError(serr.str()); - } - } - break; - default: - { - if (std::isdigit(ws[i])) - { - // octal escape sequences TODO : revisit (issue #1251). - unsigned num = static_cast<unsigned>(ws[i]) - 48; - bool flag = num < 4; - if (i + 1 < ws.size() && num < 8 && std::isdigit(ws[i + 1]) - && ws[i + 1] < '8') - { - num = num * 8 + static_cast<unsigned>(ws[i + 1]) - 48; - if (flag && i + 2 < ws.size() && std::isdigit(ws[i + 2]) - && ws[i + 2] < '8') - { - num = num * 8 + static_cast<unsigned>(ws[i + 2]) - 48; - str.push_back(num); - i += 3; - } - else - { - str.push_back(num); - i += 2; - } - } - else - { - str.push_back(num); - i++; - } - } - } - } - } - return str; + Input* input = Input::newStreamInput(d_lang, stream, name); + d_state->setInput(input); + input->setParserState(d_state.get()); + d_state->setDone(false); + return std::unique_ptr<InputParser>(new InputParser(d_state.get(), input)); } -api::Term Parser::mkStringConstant(const std::string& s) +std::unique_ptr<InputParser> Parser::parseString(const std::string& name, + const std::string& str) { - if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage())) - { - return d_solver->mkString(s, true); - } - // otherwise, we must process ad-hoc escape sequences - std::vector<unsigned> str = processAdHocStringEsc(s); - return d_solver->mkString(str); + Input* input = Input::newStringInput(d_lang, str, name); + d_state->setInput(input); + input->setParserState(d_state.get()); + d_state->setDone(false); + return std::unique_ptr<InputParser>(new InputParser(d_state.get(), input)); } } // namespace parser diff --git a/src/parser/parser.h b/src/parser/parser.h index a22b24a0c..5eb339355 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A collection of state for use by parser implementations. + * API of the cvc5 parser. */ #include "cvc5parser_public.h" @@ -18,205 +18,35 @@ #ifndef CVC5__PARSER__PARSER_H #define CVC5__PARSER__PARSER_H -#include <list> #include <memory> -#include <set> #include <string> #include "api/cpp/cvc5.h" #include "cvc5_export.h" -#include "expr/kind.h" #include "expr/symbol_manager.h" -#include "expr/symbol_table.h" -#include "parser/input.h" -#include "parser/parse_op.h" -#include "parser/parser_exception.h" -#include "util/unsafe_interrupt_exception.h" +#include "options/options.h" +#include "parser/parser_state.h" namespace cvc5 { - -// Forward declarations -class Command; -class ResourceManager; - namespace parser { -class Input; - -/** Types of checks for the symbols */ -enum DeclarationCheck { - /** Enforce that the symbol has been declared */ - CHECK_DECLARED, - /** Enforce that the symbol has not been declared */ - 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); -inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) { - switch(check) { - case CHECK_NONE: - return out << "CHECK_NONE"; - case CHECK_DECLARED: - return out << "CHECK_DECLARED"; - case CHECK_UNDECLARED: - return out << "CHECK_UNDECLARED"; - default: - return out << "DeclarationCheck!UNKNOWN"; - } -} - -/** - * Types of symbols. Used to define namespaces. - */ -enum SymbolType { - /** Variables */ - 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); -inline std::ostream& operator<<(std::ostream& out, SymbolType type) { - switch(type) { - case SYM_VARIABLE: - return out << "SYM_VARIABLE"; - case SYM_SORT: - return out << "SYM_SORT"; - default: - return out << "SymbolType!UNKNOWN"; - } -} - -/** - * This class encapsulates all of the state of a parser, including the - * name of the file, line number and column information, and in-scope - * declarations. + * This class encapsulates a parser that can be used to parse expressions and + * commands from files, streams, and strings. */ class CVC5_EXPORT Parser { friend class ParserBuilder; - private: - /** The input that we're parsing. */ - Input* d_input; - - /** - * Reference to the symbol manager, which manages the symbol table used by - * this parser. - */ - SymbolManager* d_symman; - - /** The language that we are parsing. */ - InputLanguage d_lang; - - /** - * This current symbol table used by this parser, from symbol manager. - */ - SymbolTable* d_symtab; - - /** - * The level of the assertions in the declaration scope. Things declared - * after this level are bindings from e.g. a let, a quantifier, or a - * lambda. - */ - size_t d_assertionLevel; - - /** How many anonymous functions we've created. */ - size_t d_anonymousFunctionCount; - - /** Are we done */ - bool d_done; - - /** Are semantic checks enabled during parsing? */ - bool d_checksEnabled; - - /** Are we parsing in strict mode? */ - bool d_strictMode; - - /** Are we only parsing? */ - bool d_parseOnly; - - /** - * Can we include files? (Set to false for security purposes in - * e.g. the online version.) - */ - bool d_canIncludeFile; - - /** - * Whether the logic has been forced with --force-logic. - */ - bool d_logicIsForced; - - /** - * The logic, if d_logicIsForced == true. - */ - std::string d_forcedLogic; - - /** The set of operators available in the current logic. */ - std::set<api::Kind> d_logicOperators; - - /** The set of attributes already warned about. */ - std::set<std::string> d_attributesWarnedAbout; - - /** - * The current set of unresolved types. We can get by with this NOT - * being on the scope, because we can only have one DATATYPE - * definition going on at one time. This is a bit hackish; we - * depend on mkMutualDatatypeTypes() to check everything and clear - * this out. - */ - std::set<api::Sort> d_unresolved; - - /** - * "Preemption commands": extra commands implied by subterms that - * should be issued before the currently-being-parsed command is - * issued. Used to support SMT-LIBv2 ":named" attribute on terms. - * - * Owns the memory of the Commands in the queue. - */ - std::list<Command*> d_commandQueue; - - /** Lookup a symbol in the given namespace (as specified by the type). - * Only returns a symbol if it is not overloaded, returns null otherwise. - */ - api::Term getSymbol(const std::string& var_name, SymbolType type); - - protected: - /** The API Solver object. */ - api::Solver* d_solver; - + public: /** - * Create a parser state. - * - * @attention The parser takes "ownership" of the given - * input and will delete it on destruction. + * Create a parser. * * @param solver solver API object * @param symm reference to the symbol manager - * @param input the parser input - * @param strictMode whether to incorporate strict(er) compliance checks - * @param parseOnly whether we are parsing only (and therefore certain checks - * need not be performed, like those about unimplemented features, @see - * unimplementedFeature()) + * @param options The options for the parser */ - Parser(api::Solver* solver, - SymbolManager* sm, - InputLanguage lang, - bool strictMode = false, - bool parseOnly = false); - - public: - virtual ~Parser(); + Parser(api::Solver* solver, SymbolManager* sm, const Options& options); /** * Parse a file with this parser. @@ -248,553 +78,21 @@ class CVC5_EXPORT Parser std::unique_ptr<InputParser> parseString(const std::string& name, const std::string& str); - /** Get the associated solver. */ - api::Solver* getSolver() const; - - /** Get the associated input. */ - Input* getInput() const { return d_input; } - - /** Get unresolved sorts */ - inline std::set<api::Sort>& getUnresolvedSorts() { return d_unresolved; } - - /** - * Check if we are done -- either the end of input has been reached, or some - * error has been encountered. - * @return true if parser is done - */ - inline bool done() const { - return d_done; - } - - /** Sets the done flag */ - inline void setDone(bool done = true) { - d_done = done; - } - - /** Enable semantic checks during parsing. */ - void enableChecks() { d_checksEnabled = true; } - - /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ - void disableChecks() { d_checksEnabled = false; } - - /** Enable strict parsing, according to the language standards. */ - void enableStrictMode() { d_strictMode = true; } - - /** Disable strict parsing. Allows certain syntactic infelicities to - pass without comment. */ - void disableStrictMode() { d_strictMode = false; } - - bool strictModeEnabled() { return d_strictMode; } - - void allowIncludeFile() { d_canIncludeFile = true; } - void disallowIncludeFile() { d_canIncludeFile = false; } - bool canIncludeFile() const { return d_canIncludeFile; } - - /** Expose the functionality from SMT/SMT2 parsers, while making - implementation optional by returning false by default. */ - virtual bool logicIsSet() { return false; } - - virtual void forceLogic(const std::string& logic); - - const std::string& getForcedLogic() const { return d_forcedLogic; } - bool logicIsForced() const { return d_logicIsForced; } - - /** - * Gets the variable currently bound to name. - * - * @param name the name of the variable - * @return the variable expression - * Only returns a variable if its name is not overloaded, returns null otherwise. - */ - api::Term getVariable(const std::string& name); - - /** - * Gets the function currently bound to name. - * - * @param name the name of the variable - * @return the variable expression - * Only returns a function if its name is not overloaded, returns null otherwise. - */ - api::Term getFunction(const std::string& name); - - /** - * Returns the expression that name should be interpreted as, based on the current binding. - * - * The symbol name should be declared. - * This creates the expression that the string "name" should be interpreted as. - * Typically this corresponds to a variable, but it may also correspond to - * a nullary constructor or a defined function. - * Only returns an expression if its name is not overloaded, returns null otherwise. - */ - virtual api::Term getExpressionForName(const std::string& name); - - /** - * Returns the expression that name should be interpreted as, based on the current binding. - * - * This is the same as above but where the name has been type cast to t. - */ - virtual api::Term getExpressionForNameAndType(const std::string& name, - api::Sort t); - - /** - * If this method returns true, then name is updated with the tester name - * for constructor cons. - * - * In detail, notice that (user-defined) datatypes associate a unary predicate - * for each constructor, called its "tester". This symbol is automatically - * defined when a datatype is defined. The tester name for a constructor - * (e.g. "cons") depends on the language: - * - In smt versions < 2.6, the (non-standard) syntax is "is-cons", - * - In smt versions >= 2.6, the indexed symbol "(_ is cons)" is used. Thus, - * no tester symbol is necessary, since "is" is a builtin symbol. We still use - * the above syntax if strict mode is disabled. - * - In cvc, the syntax for testers is "is_cons". - */ - virtual bool getTesterName(api::Term cons, std::string& name); - - /** - * Returns the kind that should be used for applications of expression fun. - * This is a generalization of ExprManager::operatorToKind that also - * handles variables whose types are "function-like", i.e. where - * checkFunctionLike(fun) returns true. - * - * For examples of the latter, this function returns - * APPLY_UF if fun has function type, - * APPLY_CONSTRUCTOR if fun has constructor type. - */ - api::Kind getKindForFunction(api::Term fun); - - /** - * Returns a sort, given a name. - * @param sort_name the name to look up - */ - api::Sort getSort(const std::string& sort_name); - - /** - * Returns a (parameterized) sort, given a name and args. - */ - api::Sort getSort(const std::string& sort_name, - const std::vector<api::Sort>& params); - - /** - * Returns arity of a (parameterized) sort, given a name and args. - */ - size_t getArity(const std::string& sort_name); - - /** - * Checks if a symbol has been declared. - * @param name the symbol name - * @param type the symbol type - * @return true iff the symbol has been declared with the given type - */ - bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE); - - /** - * Checks if the declaration policy we want to enforce holds - * for the given symbol. - * @param name the symbol to check - * @param check the kind of check to perform - * @param type the type of the symbol - * @param notes notes to add to a parse error (if one is generated) - * @throws ParserException if checks are enabled and the check fails - */ - void checkDeclaration(const std::string& name, - DeclarationCheck check, - SymbolType type = SYM_VARIABLE, - std::string notes = ""); - - /** - * Checks whether the given expression is function-like, i.e. - * it expects arguments. This is checked by looking at the type - * of fun. Examples of function types are function, constructor, - * selector, tester. - * @param fun the expression to check - * @throws ParserException if checks are enabled and fun is not - * a function - */ - void checkFunctionLike(api::Term fun); - - /** Create a new cvc5 variable expression of the given type. - * - * It is inserted at context level zero in the symbol table if levelZero is - * true, or if we are using global declarations. - * - * If a symbol with name already exists, - * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the - * new expression. - */ - api::Term bindVar(const std::string& name, - const api::Sort& type, - bool levelZero = false, - bool doOverload = false); - - /** - * Create a set of new cvc5 variable expressions of the given type. - * - * It is inserted at context level zero in the symbol table if levelZero is - * true, or if we are using global declarations. - * - * For each name, if a symbol with name already exists, - * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the - * new expression. - */ - std::vector<api::Term> bindVars(const std::vector<std::string> names, - const api::Sort& type, - bool levelZero = false, - bool doOverload = false); - - /** - * Create a new cvc5 bound variable expression of the given type. This binds - * the symbol name to that variable in the current scope. - */ - api::Term bindBoundVar(const std::string& name, const api::Sort& type); - /** - * Create a new cvc5 bound variable expressions of the given names and types. - * Like the method above, this binds these names to those variables in the - * current scope. - */ - std::vector<api::Term> bindBoundVars( - std::vector<std::pair<std::string, api::Sort> >& sortedVarNames); - - /** - * Create a set of new cvc5 bound variable expressions of the given type. - * - * For each name, if a symbol with name already exists, - * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the - * new expression. - */ - std::vector<api::Term> bindBoundVars(const std::vector<std::string> names, - const api::Sort& type); - - /** Create a new variable definition (e.g., from a let binding). - * levelZero is set if the binding must be done at level 0. - * If a symbol with name already exists, - * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the new expression. - */ - void defineVar(const std::string& name, - const api::Term& val, - bool levelZero = false, - bool doOverload = false); - - /** - * Create a new type definition. - * - * @param name The name of the type - * @param type The type that should be associated with the name - * @param levelZero If true, the type definition is considered global and - * cannot be removed by popping the user context - * @param skipExisting If true, the type definition is ignored if the same - * symbol has already been defined. It is assumed that - * the definition is the exact same as the existing one. - */ - void defineType(const std::string& name, - const api::Sort& type, - bool levelZero = false, - bool skipExisting = false); - - /** - * Create a new (parameterized) type definition. - * - * @param name The name of the type - * @param params The type parameters - * @param type The type that should be associated with the name - * @param levelZero If true, the type definition is considered global and - * cannot be removed by poppoing the user context - */ - void defineType(const std::string& name, - const std::vector<api::Sort>& params, - const api::Sort& type, - bool levelZero = false); - - /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ - void defineParameterizedType(const std::string& name, - const std::vector<api::Sort>& params, - const api::Sort& type); - - /** - * Creates a new sort with the given name. - */ - api::Sort mkSort(const std::string& name); - - /** - * Creates a new sort constructor with the given name and arity. - */ - api::Sort mkSortConstructor(const std::string& name, size_t arity); - - /** - * Creates a new "unresolved type," used only during parsing. - */ - api::Sort mkUnresolvedType(const std::string& name); - - /** - * Creates a new unresolved (parameterized) type constructor of the given - * arity. - */ - api::Sort mkUnresolvedTypeConstructor(const std::string& name, size_t arity); - /** - * Creates a new unresolved (parameterized) type constructor given the type - * parameters. - */ - api::Sort mkUnresolvedTypeConstructor(const std::string& name, - const std::vector<api::Sort>& params); - - /** - * Creates a new unresolved (parameterized) type constructor of the given - * arity. Calls either mkUnresolvedType or mkUnresolvedTypeConstructor - * depending on the arity. - */ - api::Sort mkUnresolvedType(const std::string& name, size_t arity); - - /** - * Returns true IFF name is an unresolved type. - */ - bool isUnresolvedType(const std::string& name); - - /** - * Creates and binds sorts of a list of mutually-recursive datatype - * declarations. - * - * For each symbol defined by the datatype, if a symbol with name already - * exists, then if doOverload is true, we create overloaded operators. Else, if - * doOverload is false, the existing expression is shadowed by the new - * expression. - */ - std::vector<api::Sort> bindMutualDatatypeTypes( - std::vector<api::DatatypeDecl>& datatypes, bool doOverload = false); - - /** make flat function type - * - * Returns the "flat" function type corresponding to the function taking - * argument types "sorts" and range type "range". A flat function type is - * one whose range is not a function. Notice that if sorts is empty and range - * is not a function, then this function returns range itself. - * - * If range is a function type, we add its function argument sorts to sorts - * and consider its function range as the new range. For each sort S added - * to sorts in this process, we add a new bound variable of sort S to - * flattenVars. - * - * For example: - * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ): - * - returns the the function type (-> Int (-> Real Real) Int Bool) - * - updates sorts to { Int, (-> Real Real), Int }, - * - updates flattenVars to { x }, where x is bound variable of type Int. - * - * Notice that this method performs only one level of flattening, for example, - * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}): - * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool)) - * - updates sorts to { Int, (-> Real Real), Int }, - * - updates flattenVars to { x }, where x is bound variable of type Int. - * - * This method is required so that we do not return functions - * that have function return type (these give an unhandled exception - * in the ExprManager). For examples of the equivalence between function - * definitions in the proposed higher-order extension of the smt2 language, - * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf. - * - * The argument flattenVars is needed in the case of defined functions - * with function return type. These have implicit arguments, for instance: - * (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x))) - * is equivalent to the command: - * (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z)) - * where @ is (higher-order) application. In this example, z is added to - * flattenVars. - */ - api::Sort mkFlatFunctionType(std::vector<api::Sort>& sorts, - api::Sort range, - std::vector<api::Term>& flattenVars); - - /** make flat function type - * - * Same as above, but does not take argument flattenVars. - * This is used when the arguments of the function are not important (for - * instance, if we are only using this type in a declare-fun). - */ - api::Sort mkFlatFunctionType(std::vector<api::Sort>& sorts, api::Sort range); - - /** make higher-order apply - * - * This returns the left-associative curried application of (function) expr to - * the arguments in args. - * - * For example, mkHoApply( f, { a, b }, 0 ) returns - * (HO_APPLY (HO_APPLY f a) b) - * - * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where - * args[i].getType() = Ti - * for each i where 0 <= i < args.size(). If expr is not of this - * type, the expression returned by this method will not be well typed. - */ - api::Term mkHoApply(api::Term expr, const std::vector<api::Term>& args); - - /** Apply type ascription - * - * Return term t with a type ascription applied to it. This is used for - * syntax like (as t T) in smt2 and t::T in the CVC language. This includes: - * - (as emptyset (Set T)) - * - (as emptybag (Bag T)) - * - (as univset (Set T)) - * - (as sep.nil T) - * - (cons T) - * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor. - * - * The term to ascribe t is a term whose kind and children (but not type) - * are equivalent to that of the term returned by this method. - * - * Notice that method is not necessarily a cast. In actuality, the above terms - * should be understood as symbols indexed by types. However, SMT-LIB does not - * permit types as indices, so we must use, e.g. (as emptyset (Set T)) - * instead of (_ emptyset (Set T)). - * - * @param t The term to ascribe a type - * @param s The sort to ascribe - * @return Term t with sort s ascribed. - */ - api::Term applyTypeAscription(api::Term t, api::Sort s); - - /** - * Add an operator to the current legal set. - * - * @param kind the built-in operator to add - */ - void addOperator(api::Kind kind); - - /** Is there a command in the queue? */ - bool hasCommand(); - - /** - * Preempt the next returned command with other ones; used to - * support the :named attribute in SMT-LIBv2, which implicitly - * inserts a new command before the current one. Also used in TPTP - * because function and predicate symbols are implicitly declared. - */ - void preemptCommand(Command* cmd); - - /** Get the next command from the queue. */ - Command* getNextCommand(); - - /** Is the symbol bound to a boolean variable? */ - bool isBoolean(const std::string& name); - - /** Is fun a function (or function-like thing)? - * Currently this means its type is either a function, constructor, tester, or selector. - */ - bool isFunctionLike(api::Term fun); - - /** Is the symbol bound to a predicate? */ - bool isPredicate(const std::string& name); - - /** Issue a warning to the user. */ - void warning(const std::string& msg) { d_input->warning(msg); } - /** Issue a warning to the user, but only once per attribute. */ - void attributeNotSupported(const std::string& attr); - - /** Raise a parse error with the given message. */ - inline void parseError(const std::string& msg) { d_input->parseError(msg); } - /** Unexpectedly encountered an EOF */ - inline void unexpectedEOF(const std::string& msg) - { - d_input->parseError(msg, true); - } - - /** - * If we are parsing only, don't raise an exception; if we are not, - * raise a parse error with the given message. There is no actual - * parse error, everything is as expected, but we cannot create the - * Expr, Type, or other requested thing yet due to internal - * limitations. Even though it's not a parse error, we throw a - * parse error so that the input line and column information is - * available. - * - * Think quantifiers. We don't have a TheoryQuantifiers yet, so we - * have no kind::FORALL or kind::EXISTS. But we might want to - * support parsing quantifiers (just not doing anything with them). - * So this mechanism gives you a way to do it with --parse-only. - */ - inline void unimplementedFeature(const std::string& msg) - { - if(!d_parseOnly) { - parseError("Unimplemented feature: " + msg); - } - } - - /** - * Gets the current declaration level. - */ - size_t scopeLevel() const; + private: + /** The API Solver object. */ + api::Solver* d_solver; /** - * Pushes a scope. All subsequent symbol declarations made are only valid in - * this scope, i.e. they are deleted on the next call to popScope. - * - * The argument isUserContext is true, when we are pushing a user context - * e.g. via the smt2 command (push n). This may also include one initial - * pushScope when the parser is initialized. User-context pushes and pops - * have an impact on both expression names and the symbol table, whereas - * other pushes and pops only have an impact on the symbol table. + * Reference to the symbol manager, which manages the symbol table used by + * this parser. */ - void pushScope(bool isUserContext = false); - - void popScope(); - - virtual void reset(); - - /** Return the symbol manager used by this parser. */ - SymbolManager* getSymbolManager(); - - //------------------------ operator overloading - /** is this function overloaded? */ - bool isOverloadedFunction(api::Term fun) - { - return d_symtab->isOverloadedFunction(fun); - } - - /** Get overloaded constant for type. - * If possible, it returns a defined symbol with name - * that has type t. Otherwise returns null expression. - */ - api::Term getOverloadedConstantForType(const std::string& name, api::Sort t) - { - return d_symtab->getOverloadedConstantForType(name, t); - } + SymbolManager* d_symman; - /** - * If possible, returns a defined function for a name - * and a vector of expected argument types. Otherwise returns - * null expression. - */ - api::Term getOverloadedFunctionForTypes(const std::string& name, - std::vector<api::Sort>& argTypes) - { - return d_symtab->getOverloadedFunctionForTypes(name, argTypes); - } - //------------------------ end operator overloading - /** - * Make string constant - * - * This makes the string constant based on the string s. This may involve - * processing ad-hoc escape sequences (if the language is not - * SMT-LIB 2.6 or higher), or otherwise calling the solver to construct - * the string. - */ - api::Term mkStringConstant(const std::string& s); + /** The language that we are parsing. */ + InputLanguage d_lang; - /** ad-hoc string escaping - * - * Returns the (internal) vector of code points corresponding to processing - * the escape sequences in string s. This is to support string inputs that - * do no comply with the SMT-LIB standard. - * - * This method handles escape sequences, including \n, \t, \v, \b, \r, \f, \a, - * \\, \x[N] and octal escape sequences of the form \[c1]([c2]([c3])?)? where - * c1, c2, c3 are digits from 0 to 7. - */ - std::vector<unsigned> processAdHocStringEsc(const std::string& s); -}; /* class Parser */ + std::unique_ptr<ParserState> d_state; +}; } // namespace parser } // namespace cvc5 diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp deleted file mode 100644 index 179bc1ab2..000000000 --- a/src/parser/parser_builder.cpp +++ /dev/null @@ -1,152 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Christopher L. Conway, Morgan Deters, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A builder for parsers. - */ - -// This must be included first. -#include "parser/parser_builder.h" - -#include <string> - -#include "api/cpp/cvc5.h" -#include "base/check.h" -#include "cvc/cvc.h" -#include "options/options.h" -#include "parser/antlr_input.h" -#include "parser/input.h" -#include "parser/parser.h" -#include "smt2/smt2.h" -#include "tptp/tptp.h" - -namespace cvc5 { -namespace parser { - -ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm) - : d_solver(solver), d_symman(sm) -{ - init(solver, sm); -} - -ParserBuilder::ParserBuilder(api::Solver* solver, - SymbolManager* sm, - const Options& options) - : d_solver(solver), d_symman(sm) -{ - init(solver, sm); - withOptions(options); -} - -void ParserBuilder::init(api::Solver* solver, SymbolManager* sm) -{ - d_lang = language::input::LANG_AUTO; - d_solver = solver; - d_symman = sm; - d_checksEnabled = true; - d_strictMode = false; - d_canIncludeFile = true; - d_parseOnly = false; - d_logicIsForced = false; - d_forcedLogic = ""; -} - -Parser* ParserBuilder::build() -{ - Parser* parser = NULL; - switch (d_lang) - { - case language::input::LANG_SYGUS_V2: - parser = new Smt2(d_solver, d_symman, d_lang, d_strictMode, d_parseOnly); - break; - case language::input::LANG_TPTP: - parser = new Tptp(d_solver, d_symman, d_lang, d_strictMode, d_parseOnly); - break; - default: - if (language::isInputLang_smt2(d_lang)) - { - parser = - new Smt2(d_solver, d_symman, d_lang, d_strictMode, d_parseOnly); - } - else - { - parser = new Cvc(d_solver, d_symman, d_lang, d_strictMode, d_parseOnly); - } - break; - } - - if( d_checksEnabled ) { - parser->enableChecks(); - } else { - parser->disableChecks(); - } - - if( d_canIncludeFile ) { - parser->allowIncludeFile(); - } else { - parser->disallowIncludeFile(); - } - - if( d_logicIsForced ) { - parser->forceLogic(d_forcedLogic); - } - - return parser; -} - -ParserBuilder& ParserBuilder::withChecks(bool flag) { - d_checksEnabled = flag; - return *this; -} - -ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) { - d_lang = lang; - return *this; -} - -ParserBuilder& ParserBuilder::withParseOnly(bool flag) { - d_parseOnly = flag; - return *this; -} - -ParserBuilder& ParserBuilder::withOptions(const Options& options) { - ParserBuilder& retval = *this; - retval = - retval.withInputLanguage(options.getInputLanguage()) - .withChecks(options.getSemanticChecks()) - .withStrictMode(options.getStrictParsing()) - .withParseOnly(options.getParseOnly()) - .withIncludeFile(options.getFilesystemAccess()); - if(options.wasSetByUserForceLogicString()) { - LogicInfo tmp(options.getForceLogicString()); - retval = retval.withForcedLogic(tmp.getLogicString()); - } - return retval; -} - -ParserBuilder& ParserBuilder::withStrictMode(bool flag) { - d_strictMode = flag; - return *this; -} - -ParserBuilder& ParserBuilder::withIncludeFile(bool flag) { - d_canIncludeFile = flag; - return *this; -} - -ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) { - d_logicIsForced = true; - d_forcedLogic = logic; - return *this; -} - -} // namespace parser -} // namespace cvc5 diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h deleted file mode 100644 index 992ca408a..000000000 --- a/src/parser/parser_builder.h +++ /dev/null @@ -1,135 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Christopher L. Conway, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A builder for parsers. - */ - -#include "cvc5parser_public.h" - -#ifndef CVC5__PARSER__PARSER_BUILDER_H -#define CVC5__PARSER__PARSER_BUILDER_H - -#include <string> - -#include "cvc5_export.h" -#include "options/language.h" -#include "parser/input.h" - -namespace cvc5 { - -namespace api { -class Solver; -} - -class Options; -class SymbolManager; - -namespace parser { - -class Parser; - -/** - * A builder for input language parsers. <code>build()</code> can be - * called any number of times on an instance and will generate a fresh - * parser each time. - */ -class CVC5_EXPORT ParserBuilder -{ - /** The input language */ - InputLanguage d_lang; - - /** The API Solver object. */ - api::Solver* d_solver; - - /** The symbol manager */ - SymbolManager* d_symman; - - /** Should semantic checks be enabled during parsing? */ - bool d_checksEnabled; - - /** Should we parse in strict mode? */ - bool d_strictMode; - - /** Should we allow include-file commands? */ - bool d_canIncludeFile; - - /** Are we parsing only? */ - bool d_parseOnly; - - /** Is the logic forced by the user? */ - bool d_logicIsForced; - - /** The forced logic name */ - std::string d_forcedLogic; - - /** Initialize this parser builder */ - void init(api::Solver* solver, SymbolManager* sm); - - public: - /** Create a parser builder using the given Solver and filename. */ - ParserBuilder(api::Solver* solver, SymbolManager* sm); - - ParserBuilder(api::Solver* solver, - SymbolManager* sm, - const Options& options); - - /** Build the parser, using the current settings. */ - Parser* build(); - - /** Should semantic checks be enabled in the parser? (Default: yes) */ - ParserBuilder& withChecks(bool flag = true); - - /** - * Set the input language to be used by the parser. - * - * (Default: LANG_AUTO) - */ - ParserBuilder& withInputLanguage(InputLanguage lang); - - /** - * Are we only parsing, or doing something with the resulting - * commands and expressions? This setting affects whether the - * parser will raise certain errors about unimplemented features, - * even if there isn't a parsing error, because the result of the - * parse would otherwise be an incorrect parse tree and the error - * would go undetected. This is specifically for circumstances - * where the parser is ahead of the functionality present elsewhere - * in cvc5 (such as quantifiers, subtypes, records, etc. in the CVC - * language parser). - */ - ParserBuilder& withParseOnly(bool flag = true); - - /** Derive settings from the given options. */ - ParserBuilder& withOptions(const Options& options); - - /** - * Should the parser use strict mode? - * - * (Default: no) - */ - ParserBuilder& withStrictMode(bool flag = true); - - /** - * Should the include-file commands be enabled? - * - * (Default: yes) - */ - ParserBuilder& withIncludeFile(bool flag = true); - - /** Set the parser to use the given logic string. */ - ParserBuilder& withForcedLogic(const std::string& logic); -}; /* class ParserBuilder */ - -} // namespace parser -} // namespace cvc5 - -#endif /* CVC5__PARSER__PARSER_BUILDER_H */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp new file mode 100644 index 000000000..4caa5569d --- /dev/null +++ b/src/parser/parser_state.cpp @@ -0,0 +1,933 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Parser state implementation. + */ + +#include "parser/parser_state.h" + +#include <clocale> +#include <fstream> +#include <iostream> +#include <iterator> +#include <memory> +#include <sstream> +#include <unordered_set> + +#include "api/cpp/cvc5.h" +#include "base/check.h" +#include "base/output.h" +#include "expr/kind.h" +#include "options/options.h" +#include "parser/input.h" +#include "parser/input_parser.h" +#include "parser/parser_exception.h" +#include "smt/command.h" + +using namespace std; +using namespace cvc5::kind; + +namespace cvc5 { +namespace parser { + +ParserState::~ParserState() +{ + for (std::list<Command*>::iterator iter = d_commandQueue.begin(); + iter != d_commandQueue.end(); + ++iter) + { + Command* command = *iter; + delete command; + } + d_commandQueue.clear(); +} + +api::Solver* ParserState::getSolver() const { return d_solver; } + +void ParserState::forceLogic(const std::string& logic) +{ + Assert(!d_logicIsForced); + d_logicIsForced = true; + d_forcedLogic = logic; +} + +api::Term ParserState::getVariable(const std::string& name) +{ + return getSymbol(name, SYM_VARIABLE); +} + +api::Term ParserState::getFunction(const std::string& name) +{ + return getSymbol(name, SYM_VARIABLE); +} + +api::Term ParserState::getExpressionForName(const std::string& name) +{ + api::Sort t; + return getExpressionForNameAndType(name, t); +} + +api::Term ParserState::getExpressionForNameAndType(const std::string& name, + api::Sort t) +{ + Assert(isDeclared(name)); + // first check if the variable is declared and not overloaded + api::Term expr = getVariable(name); + if (expr.isNull()) + { + // the variable is overloaded, try with type if the type exists + if (!t.isNull()) + { + // if we decide later to support annotations for function types, this will + // update to separate t into ( argument types, return type ) + expr = getOverloadedConstantForType(name, t); + if (expr.isNull()) + { + parseError("Cannot get overloaded constant for type ascription."); + } + } + else + { + parseError("Overloaded constants must be type cast."); + } + } + // now, post-process the expression + Assert(!expr.isNull()); + api::Sort te = expr.getSort(); + if (te.isConstructor() && te.getConstructorArity() == 0) + { + // nullary constructors have APPLY_CONSTRUCTOR kind with no children + expr = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, expr); + } + return expr; +} + +bool ParserState::getTesterName(api::Term cons, std::string& name) +{ + return false; +} + +api::Kind ParserState::getKindForFunction(api::Term fun) +{ + api::Sort t = fun.getSort(); + if (t.isFunction()) + { + return api::APPLY_UF; + } + else if (t.isConstructor()) + { + return api::APPLY_CONSTRUCTOR; + } + else if (t.isSelector()) + { + return api::APPLY_SELECTOR; + } + else if (t.isTester()) + { + return api::APPLY_TESTER; + } + else if (t.isUpdater()) + { + return api::APPLY_UPDATER; + } + return api::UNDEFINED_KIND; +} + +api::Sort ParserState::getSort(const std::string& name) +{ + checkDeclaration(name, CHECK_DECLARED, SYM_SORT); + Assert(isDeclared(name, SYM_SORT)); + api::Sort t = d_symtab->lookupType(name); + return t; +} + +api::Sort ParserState::getSort(const std::string& name, + const std::vector<api::Sort>& params) +{ + checkDeclaration(name, CHECK_DECLARED, SYM_SORT); + Assert(isDeclared(name, SYM_SORT)); + api::Sort t = d_symtab->lookupType(name, params); + return t; +} + +size_t ParserState::getArity(const std::string& sort_name) +{ + checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); + Assert(isDeclared(sort_name, SYM_SORT)); + return d_symtab->lookupArity(sort_name); +} + +bool ParserState::isDeclared(const std::string& name, SymbolType type) +{ + switch (type) + { + case SYM_VARIABLE: return d_symtab->isBound(name); + case SYM_SORT: return d_symtab->isBoundType(name); + } + Assert(false); // Unhandled(type); + return false; +} + +void ParserState::checkDeclaration(const std::string& varName, + DeclarationCheck check, + SymbolType type, + std::string notes) +{ + if (!d_checksEnabled) + { + return; + } + + switch (check) + { + case CHECK_DECLARED: + if (!isDeclared(varName, type)) + { + parseError("Symbol '" + varName + "' not declared as a " + + (type == SYM_VARIABLE ? "variable" : "type") + + (notes.size() == 0 ? notes : "\n" + notes)); + } + break; + + case CHECK_UNDECLARED: + if (isDeclared(varName, type)) + { + parseError("Symbol '" + varName + "' previously declared as a " + + (type == SYM_VARIABLE ? "variable" : "type") + + (notes.size() == 0 ? notes : "\n" + notes)); + } + break; + + case CHECK_NONE: break; + + default: Assert(false); // Unhandled(check); + } +} + +void ParserState::checkFunctionLike(api::Term fun) +{ + if (d_checksEnabled && !isFunctionLike(fun)) + { + stringstream ss; + ss << "Expecting function-like symbol, found '"; + ss << fun; + ss << "'"; + parseError(ss.str()); + } +} + +api::Term ParserState::bindVar(const std::string& name, + const api::Sort& type, + bool levelZero, + bool doOverload) +{ + bool globalDecls = d_symman->getGlobalDeclarations(); + Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl; + api::Term expr = d_solver->mkConst(type, name); + defineVar(name, expr, globalDecls || levelZero, doOverload); + return expr; +} + +std::vector<api::Term> ParserState::bindVars( + const std::vector<std::string> names, + const api::Sort& type, + bool levelZero, + bool doOverload) +{ + std::vector<api::Term> vars; + for (unsigned i = 0; i < names.size(); ++i) + { + vars.push_back(bindVar(names[i], type, levelZero, doOverload)); + } + return vars; +} + +api::Term ParserState::bindBoundVar(const std::string& name, + const api::Sort& type) +{ + Debug("parser") << "bindBoundVar(" << name << ", " << type << ")" + << std::endl; + api::Term expr = d_solver->mkVar(type, name); + defineVar(name, expr); + return expr; +} + +std::vector<api::Term> ParserState::bindBoundVars( + const std::vector<std::string> names, const api::Sort& type) +{ + std::vector<api::Term> vars; + for (unsigned i = 0; i < names.size(); ++i) + { + vars.push_back(bindBoundVar(names[i], type)); + } + return vars; +} + +std::vector<api::Term> ParserState::bindBoundVars( + std::vector<std::pair<std::string, api::Sort> >& sortedVarNames) +{ + std::vector<api::Term> vars; + for (std::pair<std::string, api::Sort>& i : sortedVarNames) + { + vars.push_back(bindBoundVar(i.first, i.second)); + } + return vars; +} + +void ParserState::defineVar(const std::string& name, + const api::Term& val, + bool levelZero, + bool doOverload) +{ + Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl; + if (!d_symtab->bind(name, val, levelZero, doOverload)) + { + std::stringstream ss; + ss << "Cannot bind " << name << " to symbol of type " << val.getSort(); + ss << ", maybe the symbol has already been defined?"; + parseError(ss.str()); + } + Assert(isDeclared(name)); +} + +void ParserState::defineType(const std::string& name, + const api::Sort& type, + bool levelZero, + bool skipExisting) +{ + if (skipExisting && isDeclared(name, SYM_SORT)) + { + Assert(d_symtab->lookupType(name) == type); + return; + } + d_symtab->bindType(name, type, levelZero); + Assert(isDeclared(name, SYM_SORT)); +} + +void ParserState::defineType(const std::string& name, + const std::vector<api::Sort>& params, + const api::Sort& type, + bool levelZero) +{ + d_symtab->bindType(name, params, type, levelZero); + Assert(isDeclared(name, SYM_SORT)); +} + +void ParserState::defineParameterizedType(const std::string& name, + const std::vector<api::Sort>& params, + const api::Sort& type) +{ + if (Debug.isOn("parser")) + { + Debug("parser") << "defineParameterizedType(" << name << ", " + << params.size() << ", ["; + if (params.size() > 0) + { + copy(params.begin(), + params.end() - 1, + ostream_iterator<api::Sort>(Debug("parser"), ", ")); + Debug("parser") << params.back(); + } + Debug("parser") << "], " << type << ")" << std::endl; + } + defineType(name, params, type); +} + +api::Sort ParserState::mkSort(const std::string& name) +{ + Debug("parser") << "newSort(" << name << ")" << std::endl; + bool globalDecls = d_symman->getGlobalDeclarations(); + api::Sort type = d_solver->mkUninterpretedSort(name); + defineType(name, type, globalDecls); + return type; +} + +api::Sort ParserState::mkSortConstructor(const std::string& name, size_t arity) +{ + Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" + << std::endl; + bool globalDecls = d_symman->getGlobalDeclarations(); + api::Sort type = d_solver->mkSortConstructorSort(name, arity); + defineType(name, vector<api::Sort>(arity), type, globalDecls); + return type; +} + +api::Sort ParserState::mkUnresolvedType(const std::string& name) +{ + api::Sort unresolved = d_solver->mkUninterpretedSort(name); + defineType(name, unresolved); + d_unresolved.insert(unresolved); + return unresolved; +} + +api::Sort ParserState::mkUnresolvedTypeConstructor(const std::string& name, + size_t arity) +{ + api::Sort unresolved = d_solver->mkSortConstructorSort(name, arity); + defineType(name, vector<api::Sort>(arity), unresolved); + d_unresolved.insert(unresolved); + return unresolved; +} + +api::Sort ParserState::mkUnresolvedTypeConstructor( + const std::string& name, const std::vector<api::Sort>& params) +{ + Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() + << ")" << std::endl; + api::Sort unresolved = d_solver->mkSortConstructorSort(name, params.size()); + defineType(name, params, unresolved); + api::Sort t = getSort(name, params); + d_unresolved.insert(unresolved); + return unresolved; +} + +api::Sort ParserState::mkUnresolvedType(const std::string& name, size_t arity) +{ + if (arity == 0) + { + return mkUnresolvedType(name); + } + return mkUnresolvedTypeConstructor(name, arity); +} + +bool ParserState::isUnresolvedType(const std::string& name) +{ + if (!isDeclared(name, SYM_SORT)) + { + return false; + } + return d_unresolved.find(getSort(name)) != d_unresolved.end(); +} + +std::vector<api::Sort> ParserState::bindMutualDatatypeTypes( + std::vector<api::DatatypeDecl>& datatypes, bool doOverload) +{ + try + { + std::vector<api::Sort> types = + d_solver->mkDatatypeSorts(datatypes, d_unresolved); + + Assert(datatypes.size() == types.size()); + bool globalDecls = d_symman->getGlobalDeclarations(); + + for (unsigned i = 0; i < datatypes.size(); ++i) + { + api::Sort t = types[i]; + const api::Datatype& dt = t.getDatatype(); + const std::string& name = dt.getName(); + Debug("parser-idt") << "define " << name << " as " << t << std::endl; + if (isDeclared(name, SYM_SORT)) + { + throw ParserException(name + " already declared"); + } + if (t.isParametricDatatype()) + { + std::vector<api::Sort> paramTypes = t.getDatatypeParamSorts(); + defineType(name, paramTypes, t, globalDecls); + } + else + { + defineType(name, t, globalDecls); + } + std::unordered_set<std::string> consNames; + std::unordered_set<std::string> selNames; + for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) + { + const api::DatatypeConstructor& ctor = dt[j]; + api::Term constructor = ctor.getConstructorTerm(); + Debug("parser-idt") << "+ define " << constructor << std::endl; + string constructorName = ctor.getName(); + if (consNames.find(constructorName) == consNames.end()) + { + if (!doOverload) + { + checkDeclaration(constructorName, CHECK_UNDECLARED); + } + defineVar(constructorName, constructor, globalDecls, doOverload); + consNames.insert(constructorName); + } + else + { + throw ParserException(constructorName + + " already declared in this datatype"); + } + std::string testerName; + if (getTesterName(constructor, testerName)) + { + api::Term tester = ctor.getTesterTerm(); + Debug("parser-idt") << "+ define " << testerName << std::endl; + if (!doOverload) + { + checkDeclaration(testerName, CHECK_UNDECLARED); + } + defineVar(testerName, tester, globalDecls, doOverload); + } + for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++) + { + const api::DatatypeSelector& sel = ctor[k]; + api::Term selector = sel.getSelectorTerm(); + Debug("parser-idt") << "+++ define " << selector << std::endl; + string selectorName = sel.getName(); + if (selNames.find(selectorName) == selNames.end()) + { + if (!doOverload) + { + checkDeclaration(selectorName, CHECK_UNDECLARED); + } + defineVar(selectorName, selector, globalDecls, doOverload); + selNames.insert(selectorName); + } + else + { + throw ParserException(selectorName + + " already declared in this datatype"); + } + } + } + } + + // These are no longer used, and the ExprManager would have + // complained of a bad substitution if anything is left unresolved. + // Clear out the set. + d_unresolved.clear(); + + // throw exception if any datatype is not well-founded + for (unsigned i = 0; i < datatypes.size(); ++i) + { + const api::Datatype& dt = types[i].getDatatype(); + if (!dt.isCodatatype() && !dt.isWellFounded()) + { + throw ParserException(dt.getName() + " is not well-founded"); + } + } + return types; + } + catch (IllegalArgumentException& ie) + { + throw ParserException(ie.getMessage()); + } +} + +api::Sort ParserState::mkFlatFunctionType(std::vector<api::Sort>& sorts, + api::Sort range, + std::vector<api::Term>& flattenVars) +{ + if (range.isFunction()) + { + std::vector<api::Sort> domainTypes = range.getFunctionDomainSorts(); + for (unsigned i = 0, size = domainTypes.size(); i < size; i++) + { + sorts.push_back(domainTypes[i]); + // the introduced variable is internal (not parsable) + std::stringstream ss; + ss << "__flatten_var_" << i; + api::Term v = d_solver->mkVar(domainTypes[i], ss.str()); + flattenVars.push_back(v); + } + range = range.getFunctionCodomainSort(); + } + if (sorts.empty()) + { + return range; + } + return d_solver->mkFunctionSort(sorts, range); +} + +api::Sort ParserState::mkFlatFunctionType(std::vector<api::Sort>& sorts, + api::Sort range) +{ + if (sorts.empty()) + { + // no difference + return range; + } + if (Debug.isOn("parser")) + { + Debug("parser") << "mkFlatFunctionType: range " << range << " and domains "; + for (api::Sort t : sorts) + { + Debug("parser") << " " << t; + } + Debug("parser") << "\n"; + } + while (range.isFunction()) + { + std::vector<api::Sort> domainTypes = range.getFunctionDomainSorts(); + sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end()); + range = range.getFunctionCodomainSort(); + } + return d_solver->mkFunctionSort(sorts, range); +} + +api::Term ParserState::mkHoApply(api::Term expr, + const std::vector<api::Term>& args) +{ + for (unsigned i = 0; i < args.size(); i++) + { + expr = d_solver->mkTerm(api::HO_APPLY, expr, args[i]); + } + return expr; +} + +api::Term ParserState::applyTypeAscription(api::Term t, api::Sort s) +{ + api::Kind k = t.getKind(); + if (k == api::EMPTYSET) + { + t = d_solver->mkEmptySet(s); + } + else if (k == api::EMPTYBAG) + { + t = d_solver->mkEmptyBag(s); + } + else if (k == api::CONST_SEQUENCE) + { + if (!s.isSequence()) + { + std::stringstream ss; + ss << "Type ascription on empty sequence must be a sequence, got " << s; + parseError(ss.str()); + } + if (!t.getConstSequenceElements().empty()) + { + std::stringstream ss; + ss << "Cannot apply a type ascription to a non-empty sequence"; + parseError(ss.str()); + } + t = d_solver->mkEmptySequence(s.getSequenceElementSort()); + } + else if (k == api::UNIVERSE_SET) + { + t = d_solver->mkUniverseSet(s); + } + else if (k == api::SEP_NIL) + { + t = d_solver->mkSepNil(s); + } + else if (k == api::APPLY_CONSTRUCTOR) + { + std::vector<api::Term> children(t.begin(), t.end()); + // apply type ascription to the operator and reconstruct + children[0] = applyTypeAscription(children[0], s); + t = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, children); + } + // !!! temporary until datatypes are refactored in the new API + api::Sort etype = t.getSort(); + if (etype.isConstructor()) + { + // Type ascriptions only have an effect on the node structure if this is a + // parametric datatype. + if (s.isParametricDatatype()) + { + // get the datatype that t belongs to + api::Sort etyped = etype.getConstructorCodomainSort(); + api::Datatype d = etyped.getDatatype(); + // lookup by name + api::DatatypeConstructor dc = d.getConstructor(t.toString()); + // ask the constructor for the specialized constructor term + t = dc.getSpecializedConstructorTerm(s); + } + // the type of t does not match the sort s by design (constructor type + // vs datatype type), thus we use an alternative check here. + if (t.getSort().getConstructorCodomainSort() != s) + { + std::stringstream ss; + ss << "Type ascription on constructor not satisfied, term " << t + << " expected sort " << s << " but has sort " + << t.getSort().getConstructorCodomainSort(); + parseError(ss.str()); + } + return t; + } + // otherwise, nothing to do + // check that the type is correct + if (t.getSort() != s) + { + std::stringstream ss; + ss << "Type ascription not satisfied, term " << t << " expected sort " << s + << " but has sort " << t.getSort(); + parseError(ss.str()); + } + return t; +} + +void ParserState::addOperator(api::Kind kind) { d_logicOperators.insert(kind); } + +bool ParserState::hasCommand() { return !d_commandQueue.empty(); } + +void ParserState::preemptCommand(Command* cmd) +{ + d_commandQueue.push_back(cmd); +} + +Command* ParserState::getNextCommand() +{ + Assert(!d_commandQueue.empty()); + Command* cmd = d_commandQueue.front(); + d_commandQueue.pop_front(); + return cmd; +} + +/* Returns true if name is bound to a boolean variable. */ +bool ParserState::isBoolean(const std::string& name) +{ + api::Term expr = getVariable(name); + return !expr.isNull() && expr.getSort().isBoolean(); +} + +bool ParserState::isFunctionLike(api::Term fun) +{ + if (fun.isNull()) + { + return false; + } + api::Sort type = fun.getSort(); + return type.isFunction() || type.isConstructor() || type.isTester() + || type.isSelector(); +} + +/* Returns true if name is bound to a function returning boolean. */ +bool ParserState::isPredicate(const std::string& name) +{ + api::Term expr = getVariable(name); + return !expr.isNull() && expr.getSort().isPredicate(); +} + +void ParserState::attributeNotSupported(const std::string& attr) +{ + if (d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) + { + stringstream ss; + ss << "warning: Attribute '" << attr + << "' not supported (ignoring this and all following uses)"; + d_input->warning(ss.str()); + d_attributesWarnedAbout.insert(attr); + } +} + +size_t ParserState::scopeLevel() const { return d_symman->scopeLevel(); } + +void ParserState::pushScope(bool isUserContext) +{ + d_symman->pushScope(isUserContext); +} + +void ParserState::popScope() { d_symman->popScope(); } + +void ParserState::reset() {} + +SymbolManager* ParserState::getSymbolManager() { return d_symman; } + +api::Term ParserState::mkStringConstant(const std::string& s) +{ + if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage())) + { + return d_solver->mkString(s, true); + } + // otherwise, we must process ad-hoc escape sequences + std::vector<unsigned> str = processAdHocStringEsc(s); + return d_solver->mkString(str); +} + +std::vector<unsigned> ParserState::processAdHocStringEsc(const std::string& s) +{ + std::wstring ws; + { + std::setlocale(LC_ALL, "en_US.utf8"); + std::mbtowc(nullptr, nullptr, 0); + const char* end = s.data() + s.size(); + const char* ptr = s.data(); + for (wchar_t c; ptr != end;) + { + int res = std::mbtowc(&c, ptr, end - ptr); + if (res == -1) + { + std::cerr << "Invalid escape sequence in " << s << std::endl; + break; + } + else if (res == 0) + { + break; + } + else + { + ws += c; + ptr += res; + } + } + } + + std::vector<unsigned> str; + unsigned i = 0; + while (i < ws.size()) + { + // get the current character + if (ws[i] != '\\') + { + // don't worry about printable here + str.push_back(static_cast<unsigned>(ws[i])); + ++i; + continue; + } + // slash is always escaped + ++i; + if (i >= ws.size()) + { + // slash cannot be the last character if we are parsing escape sequences + std::stringstream serr; + serr << "Escape sequence at the end of string: \"" << s + << "\" should be handled by lexer"; + parseError(serr.str()); + } + switch (ws[i]) + { + case 'n': + { + str.push_back(static_cast<unsigned>('\n')); + i++; + } + break; + case 't': + { + str.push_back(static_cast<unsigned>('\t')); + i++; + } + break; + case 'v': + { + str.push_back(static_cast<unsigned>('\v')); + i++; + } + break; + case 'b': + { + str.push_back(static_cast<unsigned>('\b')); + i++; + } + break; + case 'r': + { + str.push_back(static_cast<unsigned>('\r')); + i++; + } + break; + case 'f': + { + str.push_back(static_cast<unsigned>('\f')); + i++; + } + break; + case 'a': + { + str.push_back(static_cast<unsigned>('\a')); + i++; + } + break; + case '\\': + { + str.push_back(static_cast<unsigned>('\\')); + i++; + } + break; + case 'x': + { + bool isValid = false; + if (i + 2 < ws.size()) + { + if (std::isxdigit(ws[i + 1]) && std::isxdigit(ws[i + 2])) + { + std::wstringstream shex; + shex << ws[i + 1] << ws[i + 2]; + unsigned val; + shex >> std::hex >> val; + str.push_back(val); + i += 3; + isValid = true; + } + } + if (!isValid) + { + std::stringstream serr; + serr << "Illegal String Literal: \"" << s + << "\", must have two digits after \\x"; + parseError(serr.str()); + } + } + break; + default: + { + if (std::isdigit(ws[i])) + { + // octal escape sequences TODO : revisit (issue #1251). + unsigned num = static_cast<unsigned>(ws[i]) - 48; + bool flag = num < 4; + if (i + 1 < ws.size() && num < 8 && std::isdigit(ws[i + 1]) + && ws[i + 1] < '8') + { + num = num * 8 + static_cast<unsigned>(ws[i + 1]) - 48; + if (flag && i + 2 < ws.size() && std::isdigit(ws[i + 2]) + && ws[i + 2] < '8') + { + num = num * 8 + static_cast<unsigned>(ws[i + 2]) - 48; + str.push_back(num); + i += 3; + } + else + { + str.push_back(num); + i += 2; + } + } + else + { + str.push_back(num); + i++; + } + } + } + } + } + return str; +} + +ParserState::ParserState(api::Solver* solver, + SymbolManager* sm, + InputLanguage lang, + bool strictMode, + bool parseOnly) + : d_solver(solver), + d_symman(sm), + d_lang(lang), + d_symtab(sm->getSymbolTable()), + d_assertionLevel(0), + d_anonymousFunctionCount(0), + d_done(true), + d_checksEnabled(true), + d_strictMode(strictMode), + d_parseOnly(parseOnly), + d_canIncludeFile(true), + d_logicIsForced(false), + d_forcedLogic() +{ +} + +api::Term ParserState::getSymbol(const std::string& name, SymbolType type) +{ + checkDeclaration(name, CHECK_DECLARED, type); + Assert(isDeclared(name, type)); + Assert(type == SYM_VARIABLE); + // Functions share var namespace + return d_symtab->lookup(name); +} + +} // namespace parser +} // namespace cvc5 diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h new file mode 100644 index 000000000..2970f11cb --- /dev/null +++ b/src/parser/parser_state.h @@ -0,0 +1,775 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Generic interface for the state of a parser. + */ + +#include "cvc5parser_public.h" + +#ifndef CVC5__PARSER__PARSER_STATE_H +#define CVC5__PARSER__PARSER_STATE_H + +#include <list> +#include <memory> +#include <set> +#include <string> + +#include "api/cpp/cvc5.h" +#include "cvc5_export.h" +#include "expr/kind.h" +#include "expr/symbol_manager.h" +#include "expr/symbol_table.h" +#include "parser/input.h" +#include "parser/parse_op.h" +#include "parser/parser_exception.h" +#include "util/unsafe_interrupt_exception.h" + +namespace cvc5 { + +// Forward declarations +class Command; +class ResourceManager; + +namespace parser { + +class Input; + +/** Types of checks for the symbols */ +enum DeclarationCheck { + /** Enforce that the symbol has been declared */ + CHECK_DECLARED, + /** Enforce that the symbol has not been declared */ + 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); +inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) { + switch(check) { + case CHECK_NONE: + return out << "CHECK_NONE"; + case CHECK_DECLARED: + return out << "CHECK_DECLARED"; + case CHECK_UNDECLARED: + return out << "CHECK_UNDECLARED"; + default: + return out << "DeclarationCheck!UNKNOWN"; + } +} + +/** + * Types of symbols. Used to define namespaces. + */ +enum SymbolType { + /** Variables */ + 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); +inline std::ostream& operator<<(std::ostream& out, SymbolType type) { + switch(type) { + case SYM_VARIABLE: + return out << "SYM_VARIABLE"; + case SYM_SORT: + return out << "SYM_SORT"; + default: + return out << "SymbolType!UNKNOWN"; + } +} + +/** + * This class encapsulates all of the state of a parser, including the + * name of the file, line number and column information, and in-scope + * declarations. + */ +class ParserState +{ + friend class ParserBuilder; + + public: + virtual ~ParserState(); + + /** Get the associated solver. */ + api::Solver* getSolver() const; + + /** Get the associated input. */ + Input* getInput() const { return d_input; } + + /** Set the associated input. */ + void setInput(Input* input) { d_input = input; } + + /** Get unresolved sorts */ + inline std::set<api::Sort>& getUnresolvedSorts() { return d_unresolved; } + + /** + * Check if we are done -- either the end of input has been reached, or some + * error has been encountered. + * @return true if parser is done + */ + inline bool done() const { + return d_done; + } + + /** Sets the done flag */ + inline void setDone(bool done = true) { + d_done = done; + } + + /** Enable semantic checks during parsing. */ + void enableChecks() { d_checksEnabled = true; } + + /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ + void disableChecks() { d_checksEnabled = false; } + + /** Enable strict parsing, according to the language standards. */ + void enableStrictMode() { d_strictMode = true; } + + /** Disable strict parsing. Allows certain syntactic infelicities to + pass without comment. */ + void disableStrictMode() { d_strictMode = false; } + + bool strictModeEnabled() { return d_strictMode; } + + void allowIncludeFile() { d_canIncludeFile = true; } + void disallowIncludeFile() { d_canIncludeFile = false; } + bool canIncludeFile() const { return d_canIncludeFile; } + + /** Expose the functionality from SMT/SMT2 parsers, while making + implementation optional by returning false by default. */ + virtual bool logicIsSet() { return false; } + + virtual void forceLogic(const std::string& logic); + + const std::string& getForcedLogic() const { return d_forcedLogic; } + bool logicIsForced() const { return d_logicIsForced; } + + /** + * Gets the variable currently bound to name. + * + * @param name the name of the variable + * @return the variable expression + * Only returns a variable if its name is not overloaded, returns null otherwise. + */ + api::Term getVariable(const std::string& name); + + /** + * Gets the function currently bound to name. + * + * @param name the name of the variable + * @return the variable expression + * Only returns a function if its name is not overloaded, returns null otherwise. + */ + api::Term getFunction(const std::string& name); + + /** + * Returns the expression that name should be interpreted as, based on the current binding. + * + * The symbol name should be declared. + * This creates the expression that the string "name" should be interpreted as. + * Typically this corresponds to a variable, but it may also correspond to + * a nullary constructor or a defined function. + * Only returns an expression if its name is not overloaded, returns null otherwise. + */ + virtual api::Term getExpressionForName(const std::string& name); + + /** + * Returns the expression that name should be interpreted as, based on the current binding. + * + * This is the same as above but where the name has been type cast to t. + */ + virtual api::Term getExpressionForNameAndType(const std::string& name, + api::Sort t); + + /** + * If this method returns true, then name is updated with the tester name + * for constructor cons. + * + * In detail, notice that (user-defined) datatypes associate a unary predicate + * for each constructor, called its "tester". This symbol is automatically + * defined when a datatype is defined. The tester name for a constructor + * (e.g. "cons") depends on the language: + * - In smt versions < 2.6, the (non-standard) syntax is "is-cons", + * - In smt versions >= 2.6, the indexed symbol "(_ is cons)" is used. Thus, + * no tester symbol is necessary, since "is" is a builtin symbol. We still use + * the above syntax if strict mode is disabled. + * - In cvc, the syntax for testers is "is_cons". + */ + virtual bool getTesterName(api::Term cons, std::string& name); + + /** + * Returns the kind that should be used for applications of expression fun. + * This is a generalization of ExprManager::operatorToKind that also + * handles variables whose types are "function-like", i.e. where + * checkFunctionLike(fun) returns true. + * + * For examples of the latter, this function returns + * APPLY_UF if fun has function type, + * APPLY_CONSTRUCTOR if fun has constructor type. + */ + api::Kind getKindForFunction(api::Term fun); + + /** + * Returns a sort, given a name. + * @param sort_name the name to look up + */ + api::Sort getSort(const std::string& sort_name); + + /** + * Returns a (parameterized) sort, given a name and args. + */ + api::Sort getSort(const std::string& sort_name, + const std::vector<api::Sort>& params); + + /** + * Returns arity of a (parameterized) sort, given a name and args. + */ + size_t getArity(const std::string& sort_name); + + /** + * Checks if a symbol has been declared. + * @param name the symbol name + * @param type the symbol type + * @return true iff the symbol has been declared with the given type + */ + bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE); + + /** + * Checks if the declaration policy we want to enforce holds + * for the given symbol. + * @param name the symbol to check + * @param check the kind of check to perform + * @param type the type of the symbol + * @param notes notes to add to a parse error (if one is generated) + * @throws ParserException if checks are enabled and the check fails + */ + void checkDeclaration(const std::string& name, + DeclarationCheck check, + SymbolType type = SYM_VARIABLE, + std::string notes = ""); + + /** + * Checks whether the given expression is function-like, i.e. + * it expects arguments. This is checked by looking at the type + * of fun. Examples of function types are function, constructor, + * selector, tester. + * @param fun the expression to check + * @throws ParserException if checks are enabled and fun is not + * a function + */ + void checkFunctionLike(api::Term fun); + + /** Create a new cvc5 variable expression of the given type. + * + * It is inserted at context level zero in the symbol table if levelZero is + * true, or if we are using global declarations. + * + * If a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the + * new expression. + */ + api::Term bindVar(const std::string& name, + const api::Sort& type, + bool levelZero = false, + bool doOverload = false); + + /** + * Create a set of new cvc5 variable expressions of the given type. + * + * It is inserted at context level zero in the symbol table if levelZero is + * true, or if we are using global declarations. + * + * For each name, if a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the + * new expression. + */ + std::vector<api::Term> bindVars(const std::vector<std::string> names, + const api::Sort& type, + bool levelZero = false, + bool doOverload = false); + + /** + * Create a new cvc5 bound variable expression of the given type. This binds + * the symbol name to that variable in the current scope. + */ + api::Term bindBoundVar(const std::string& name, const api::Sort& type); + /** + * Create a new cvc5 bound variable expressions of the given names and types. + * Like the method above, this binds these names to those variables in the + * current scope. + */ + std::vector<api::Term> bindBoundVars( + std::vector<std::pair<std::string, api::Sort> >& sortedVarNames); + + /** + * Create a set of new cvc5 bound variable expressions of the given type. + * + * For each name, if a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the + * new expression. + */ + std::vector<api::Term> bindBoundVars(const std::vector<std::string> names, + const api::Sort& type); + + /** Create a new variable definition (e.g., from a let binding). + * levelZero is set if the binding must be done at level 0. + * If a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the new expression. + */ + void defineVar(const std::string& name, + const api::Term& val, + bool levelZero = false, + bool doOverload = false); + + /** + * Create a new type definition. + * + * @param name The name of the type + * @param type The type that should be associated with the name + * @param levelZero If true, the type definition is considered global and + * cannot be removed by popping the user context + * @param skipExisting If true, the type definition is ignored if the same + * symbol has already been defined. It is assumed that + * the definition is the exact same as the existing one. + */ + void defineType(const std::string& name, + const api::Sort& type, + bool levelZero = false, + bool skipExisting = false); + + /** + * Create a new (parameterized) type definition. + * + * @param name The name of the type + * @param params The type parameters + * @param type The type that should be associated with the name + * @param levelZero If true, the type definition is considered global and + * cannot be removed by poppoing the user context + */ + void defineType(const std::string& name, + const std::vector<api::Sort>& params, + const api::Sort& type, + bool levelZero = false); + + /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ + void defineParameterizedType(const std::string& name, + const std::vector<api::Sort>& params, + const api::Sort& type); + + /** + * Creates a new sort with the given name. + */ + api::Sort mkSort(const std::string& name); + + /** + * Creates a new sort constructor with the given name and arity. + */ + api::Sort mkSortConstructor(const std::string& name, size_t arity); + + /** + * Creates a new "unresolved type," used only during parsing. + */ + api::Sort mkUnresolvedType(const std::string& name); + + /** + * Creates a new unresolved (parameterized) type constructor of the given + * arity. + */ + api::Sort mkUnresolvedTypeConstructor(const std::string& name, size_t arity); + /** + * Creates a new unresolved (parameterized) type constructor given the type + * parameters. + */ + api::Sort mkUnresolvedTypeConstructor(const std::string& name, + const std::vector<api::Sort>& params); + + /** + * Creates a new unresolved (parameterized) type constructor of the given + * arity. Calls either mkUnresolvedType or mkUnresolvedTypeConstructor + * depending on the arity. + */ + api::Sort mkUnresolvedType(const std::string& name, size_t arity); + + /** + * Returns true IFF name is an unresolved type. + */ + bool isUnresolvedType(const std::string& name); + + /** + * Creates and binds sorts of a list of mutually-recursive datatype + * declarations. + * + * For each symbol defined by the datatype, if a symbol with name already + * exists, then if doOverload is true, we create overloaded operators. Else, if + * doOverload is false, the existing expression is shadowed by the new + * expression. + */ + std::vector<api::Sort> bindMutualDatatypeTypes( + std::vector<api::DatatypeDecl>& datatypes, bool doOverload = false); + + /** make flat function type + * + * Returns the "flat" function type corresponding to the function taking + * argument types "sorts" and range type "range". A flat function type is + * one whose range is not a function. Notice that if sorts is empty and range + * is not a function, then this function returns range itself. + * + * If range is a function type, we add its function argument sorts to sorts + * and consider its function range as the new range. For each sort S added + * to sorts in this process, we add a new bound variable of sort S to + * flattenVars. + * + * For example: + * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ): + * - returns the the function type (-> Int (-> Real Real) Int Bool) + * - updates sorts to { Int, (-> Real Real), Int }, + * - updates flattenVars to { x }, where x is bound variable of type Int. + * + * Notice that this method performs only one level of flattening, for example, + * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}): + * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool)) + * - updates sorts to { Int, (-> Real Real), Int }, + * - updates flattenVars to { x }, where x is bound variable of type Int. + * + * This method is required so that we do not return functions + * that have function return type (these give an unhandled exception + * in the ExprManager). For examples of the equivalence between function + * definitions in the proposed higher-order extension of the smt2 language, + * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf. + * + * The argument flattenVars is needed in the case of defined functions + * with function return type. These have implicit arguments, for instance: + * (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x))) + * is equivalent to the command: + * (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z)) + * where @ is (higher-order) application. In this example, z is added to + * flattenVars. + */ + api::Sort mkFlatFunctionType(std::vector<api::Sort>& sorts, + api::Sort range, + std::vector<api::Term>& flattenVars); + + /** make flat function type + * + * Same as above, but does not take argument flattenVars. + * This is used when the arguments of the function are not important (for + * instance, if we are only using this type in a declare-fun). + */ + api::Sort mkFlatFunctionType(std::vector<api::Sort>& sorts, api::Sort range); + + /** make higher-order apply + * + * This returns the left-associative curried application of (function) expr to + * the arguments in args. + * + * For example, mkHoApply( f, { a, b }, 0 ) returns + * (HO_APPLY (HO_APPLY f a) b) + * + * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where + * args[i].getType() = Ti + * for each i where 0 <= i < args.size(). If expr is not of this + * type, the expression returned by this method will not be well typed. + */ + api::Term mkHoApply(api::Term expr, const std::vector<api::Term>& args); + + /** Apply type ascription + * + * Return term t with a type ascription applied to it. This is used for + * syntax like (as t T) in smt2 and t::T in the CVC language. This includes: + * - (as emptyset (Set T)) + * - (as emptybag (Bag T)) + * - (as univset (Set T)) + * - (as sep.nil T) + * - (cons T) + * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor. + * + * The term to ascribe t is a term whose kind and children (but not type) + * are equivalent to that of the term returned by this method. + * + * Notice that method is not necessarily a cast. In actuality, the above terms + * should be understood as symbols indexed by types. However, SMT-LIB does not + * permit types as indices, so we must use, e.g. (as emptyset (Set T)) + * instead of (_ emptyset (Set T)). + * + * @param t The term to ascribe a type + * @param s The sort to ascribe + * @return Term t with sort s ascribed. + */ + api::Term applyTypeAscription(api::Term t, api::Sort s); + + /** + * Add an operator to the current legal set. + * + * @param kind the built-in operator to add + */ + void addOperator(api::Kind kind); + + /** Is there a command in the queue? */ + bool hasCommand(); + + /** + * Preempt the next returned command with other ones; used to + * support the :named attribute in SMT-LIBv2, which implicitly + * inserts a new command before the current one. Also used in TPTP + * because function and predicate symbols are implicitly declared. + */ + void preemptCommand(Command* cmd); + + /** Get the next command from the queue. */ + Command* getNextCommand(); + + /** Is the symbol bound to a boolean variable? */ + bool isBoolean(const std::string& name); + + /** Is fun a function (or function-like thing)? + * Currently this means its type is either a function, constructor, tester, or selector. + */ + bool isFunctionLike(api::Term fun); + + /** Is the symbol bound to a predicate? */ + bool isPredicate(const std::string& name); + + /** Issue a warning to the user. */ + void warning(const std::string& msg) { d_input->warning(msg); } + /** Issue a warning to the user, but only once per attribute. */ + void attributeNotSupported(const std::string& attr); + + /** Raise a parse error with the given message. */ + inline void parseError(const std::string& msg) { d_input->parseError(msg); } + /** Unexpectedly encountered an EOF */ + inline void unexpectedEOF(const std::string& msg) + { + d_input->parseError(msg, true); + } + + /** + * If we are parsing only, don't raise an exception; if we are not, + * raise a parse error with the given message. There is no actual + * parse error, everything is as expected, but we cannot create the + * Expr, Type, or other requested thing yet due to internal + * limitations. Even though it's not a parse error, we throw a + * parse error so that the input line and column information is + * available. + * + * Think quantifiers. We don't have a TheoryQuantifiers yet, so we + * have no kind::FORALL or kind::EXISTS. But we might want to + * support parsing quantifiers (just not doing anything with them). + * So this mechanism gives you a way to do it with --parse-only. + */ + inline void unimplementedFeature(const std::string& msg) + { + if(!d_parseOnly) { + parseError("Unimplemented feature: " + msg); + } + } + + /** + * Gets the current declaration level. + */ + size_t scopeLevel() const; + + /** + * Pushes a scope. All subsequent symbol declarations made are only valid in + * this scope, i.e. they are deleted on the next call to popScope. + * + * The argument isUserContext is true, when we are pushing a user context + * e.g. via the smt2 command (push n). This may also include one initial + * pushScope when the parser is initialized. User-context pushes and pops + * have an impact on both expression names and the symbol table, whereas + * other pushes and pops only have an impact on the symbol table. + */ + void pushScope(bool isUserContext = false); + + void popScope(); + + virtual void reset(); + + /** Return the symbol manager used by this parser. */ + SymbolManager* getSymbolManager(); + + //------------------------ operator overloading + /** is this function overloaded? */ + bool isOverloadedFunction(api::Term fun) + { + return d_symtab->isOverloadedFunction(fun); + } + + /** Get overloaded constant for type. + * If possible, it returns a defined symbol with name + * that has type t. Otherwise returns null expression. + */ + api::Term getOverloadedConstantForType(const std::string& name, api::Sort t) + { + return d_symtab->getOverloadedConstantForType(name, t); + } + + /** + * If possible, returns a defined function for a name + * and a vector of expected argument types. Otherwise returns + * null expression. + */ + api::Term getOverloadedFunctionForTypes(const std::string& name, + std::vector<api::Sort>& argTypes) + { + return d_symtab->getOverloadedFunctionForTypes(name, argTypes); + } + //------------------------ end operator overloading + /** + * Make string constant + * + * This makes the string constant based on the string s. This may involve + * processing ad-hoc escape sequences (if the language is not + * SMT-LIB 2.6 or higher), or otherwise calling the solver to construct + * the string. + */ + api::Term mkStringConstant(const std::string& s); + + /** ad-hoc string escaping + * + * Returns the (internal) vector of code points corresponding to processing + * the escape sequences in string s. This is to support string inputs that + * do no comply with the SMT-LIB standard. + * + * This method handles escape sequences, including \n, \t, \v, \b, \r, \f, \a, + * \\, \x[N] and octal escape sequences of the form \[c1]([c2]([c3])?)? where + * c1, c2, c3 are digits from 0 to 7. + */ + std::vector<unsigned> processAdHocStringEsc(const std::string& s); + + protected: + /** + * Create a parser state. + * + * @attention The parser takes "ownership" of the given + * input and will delete it on destruction. + * + * @param solver solver API object + * @param symm reference to the symbol manager + * @param input the parser input + * @param strictMode whether to incorporate strict(er) compliance checks + * @param parseOnly whether we are parsing only (and therefore certain checks + * need not be performed, like those about unimplemented features, @see + * unimplementedFeature()) + */ + ParserState(api::Solver* solver, + SymbolManager* sm, + InputLanguage lang, + bool strictMode = false, + bool parseOnly = false); + + /** The API Solver object. */ + api::Solver* d_solver; + + private: + /** Lookup a symbol in the given namespace (as specified by the type). + * Only returns a symbol if it is not overloaded, returns null otherwise. + */ + api::Term getSymbol(const std::string& var_name, SymbolType type); + + /** The input that we're parsing. */ + Input* d_input; + + /** + * Reference to the symbol manager, which manages the symbol table used by + * this parser. + */ + SymbolManager* d_symman; + + /** The language that we are parsing. */ + InputLanguage d_lang; + + /** + * This current symbol table used by this parser, from symbol manager. + */ + SymbolTable* d_symtab; + + /** + * The level of the assertions in the declaration scope. Things declared + * after this level are bindings from e.g. a let, a quantifier, or a + * lambda. + */ + size_t d_assertionLevel; + + /** How many anonymous functions we've created. */ + size_t d_anonymousFunctionCount; + + /** Are we done */ + bool d_done; + + /** Are semantic checks enabled during parsing? */ + bool d_checksEnabled; + + /** Are we parsing in strict mode? */ + bool d_strictMode; + + /** Are we only parsing? */ + bool d_parseOnly; + + /** + * Can we include files? (Set to false for security purposes in + * e.g. the online version.) + */ + bool d_canIncludeFile; + + /** + * Whether the logic has been forced with --force-logic. + */ + bool d_logicIsForced; + + /** + * The logic, if d_logicIsForced == true. + */ + std::string d_forcedLogic; + + /** The set of operators available in the current logic. */ + std::set<api::Kind> d_logicOperators; + + /** The set of attributes already warned about. */ + std::set<std::string> d_attributesWarnedAbout; + + /** + * The current set of unresolved types. We can get by with this NOT + * being on the scope, because we can only have one DATATYPE + * definition going on at one time. This is a bit hackish; we + * depend on mkMutualDatatypeTypes() to check everything and clear + * this out. + */ + std::set<api::Sort> d_unresolved; + + /** + * "Preemption commands": extra commands implied by subterms that + * should be issued before the currently-being-parsed command is + * issued. Used to support SMT-LIBv2 ":named" attribute on terms. + * + * Owns the memory of the Commands in the queue. + */ + std::list<Command*> d_commandQueue; +}; + +} // namespace parser +} // namespace cvc5 + +#endif /* CVC5__PARSER__PARSER_STATE_H */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 13bdad998..4a907e93e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -34,7 +34,7 @@ Smt2::Smt2(api::Solver* solver, InputLanguage lang, bool strictMode, bool parseOnly) - : Parser(solver, sm, lang, strictMode, parseOnly), + : ParserState(solver, sm, lang, strictMode, parseOnly), d_logicSet(false), d_seenSetLogic(false) { @@ -46,7 +46,7 @@ void Smt2::addArithmeticOperators() { addOperator(api::PLUS, "+"); addOperator(api::MINUS, "-"); // api::MINUS is converted to api::UMINUS if there is only a single operand - Parser::addOperator(api::UMINUS); + ParserState::addOperator(api::UMINUS); addOperator(api::MULT, "*"); addOperator(api::LT, "<"); addOperator(api::LEQ, "<="); @@ -129,13 +129,13 @@ void Smt2::addBitvectorOperators() { void Smt2::addDatatypesOperators() { - Parser::addOperator(api::APPLY_CONSTRUCTOR); - Parser::addOperator(api::APPLY_TESTER); - Parser::addOperator(api::APPLY_SELECTOR); + ParserState::addOperator(api::APPLY_CONSTRUCTOR); + ParserState::addOperator(api::APPLY_TESTER); + ParserState::addOperator(api::APPLY_SELECTOR); if (!strictModeEnabled()) { - Parser::addOperator(api::APPLY_UPDATER); + ParserState::addOperator(api::APPLY_UPDATER); addOperator(api::DT_SIZE, "dt.size"); } } @@ -262,10 +262,10 @@ void Smt2::addSepOperators() { addOperator(api::SEP_PTO, "pto"); addOperator(api::SEP_WAND, "wand"); addOperator(api::SEP_EMP, "emp"); - Parser::addOperator(api::SEP_STAR); - Parser::addOperator(api::SEP_PTO); - Parser::addOperator(api::SEP_WAND); - Parser::addOperator(api::SEP_EMP); + ParserState::addOperator(api::SEP_STAR); + ParserState::addOperator(api::SEP_PTO); + ParserState::addOperator(api::SEP_WAND); + ParserState::addOperator(api::SEP_EMP); } void Smt2::addCoreSymbols() @@ -287,7 +287,7 @@ void Smt2::addOperator(api::Kind kind, const std::string& name) { Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )" << std::endl; - Parser::addOperator(kind); + ParserState::addOperator(kind); operatorKindMap[name] = kind; } @@ -295,7 +295,7 @@ void Smt2::addIndexedOperator(api::Kind tKind, api::Kind opKind, const std::string& name) { - Parser::addOperator(tKind); + ParserState::addOperator(tKind); d_indexedOpKindMap[name] = opKind; } @@ -330,7 +330,7 @@ api::Term Smt2::getExpressionForNameAndType(const std::string& name, { return mkAbstractValue(name); } - return Parser::getExpressionForNameAndType(name, t); + return ParserState::getExpressionForNameAndType(name, t); } bool Smt2::getTesterName(api::Term cons, std::string& name) @@ -518,7 +518,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addCoreSymbols(); if(d_logic.isTheoryEnabled(theory::THEORY_UF)) { - Parser::addOperator(api::APPLY_UF); + ParserState::addOperator(api::APPLY_UF); if (!strictModeEnabled() && d_logic.hasCardinalityConstraints()) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index bc4ca1173..19191b4f7 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -26,7 +26,7 @@ #include "api/cpp/cvc5.h" #include "parser/parse_op.h" -#include "parser/parser.h" +#include "parser/parser_state.h" #include "theory/logic_info.h" namespace cvc5 { @@ -39,9 +39,9 @@ class Solver; namespace parser { -class Smt2 : public Parser +class Smt2 : public ParserState { - friend class ParserBuilder; + friend class Parser; private: /** Has the logic been set (either by forcing it or a set-logic command)? */ @@ -152,9 +152,9 @@ class Smt2 : public Parser * * This function will create a bind a new function term to name fname. * The type of this function is - * Parser::mkFlatFunctionType(sorts,t,flattenVars), + * ParserState::mkFlatFunctionType(sorts,t,flattenVars), * where sorts are the types in the second components of sortedVarNames. - * As descibed in Parser::mkFlatFunctionType, new bound variables may be + * As descibed in ParserState::mkFlatFunctionType, new bound variables may be * added to flattenVars in this function if the function is given a function * range type. */ @@ -166,7 +166,7 @@ class Smt2 : public Parser /** Push scope for define-fun-rec * - * This calls Parser::pushScope() and sets up + * This calls ParserState::pushScope() and sets up * initial information for reading a body of a function definition * in the define-fun-rec and define-funs-rec command. * The input parameters func/flattenVars are the result @@ -177,7 +177,7 @@ class Smt2 : public Parser * flattenVars : the implicit variables introduced when defining func. * * This function: - * (1) Calls Parser::pushScope(). + * (1) Calls ParserState::pushScope(). * (2) Computes the bound variable list for the quantified formula * that defined this definition and stores it in bvs. */ @@ -317,10 +317,10 @@ class Smt2 : public Parser std::stringstream ss; ss << notes << "You may have intended to apply unary minus: `(- " << name.substr(1) << ")'\n"; - this->Parser::checkDeclaration(name, check, type, ss.str()); + this->ParserState::checkDeclaration(name, check, type, ss.str()); return; } - this->Parser::checkDeclaration(name, check, type, notes); + this->ParserState::checkDeclaration(name, check, type, notes); } /** * Notify that expression expr was given name std::string via a :named diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 5f0e7f7e8..9189f4084 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -37,7 +37,7 @@ Tptp::Tptp(api::Solver* solver, InputLanguage lang, bool strictMode, bool parseOnly) - : Parser(solver, sm, lang, strictMode, parseOnly), + : ParserState(solver, sm, lang, strictMode, parseOnly), d_cnf(false), d_fof(false) { @@ -441,7 +441,7 @@ api::Term Tptp::mkDecimal( void Tptp::forceLogic(const std::string& logic) { - Parser::forceLogic(logic); + ParserState::forceLogic(logic); preemptCommand(new SetBenchmarkLogicCommand(logic)); } diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 78cd11054..45ad9ce1e 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -24,7 +24,7 @@ #include "api/cpp/cvc5.h" #include "parser/parse_op.h" -#include "parser/parser.h" +#include "parser/parser_state.h" #include "util/hash.h" namespace cvc5 { @@ -37,9 +37,10 @@ class Solver; namespace parser { -class Tptp : public Parser { +class Tptp : public ParserState { private: - friend class ParserBuilder; + friend class Parser; + public: bool cnf() const { return d_cnf; } void setCnf(bool cnf) { d_cnf = cnf; } |