diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/cvc_input.h | 1 | ||||
-rw-r--r-- | src/parser/parser.cpp | 53 | ||||
-rw-r--r-- | src/parser/parser.h | 220 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 76 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 27 | ||||
-rw-r--r-- | src/parser/smt1/smt1.cpp | 10 | ||||
-rw-r--r-- | src/parser/smt1/smt1.h | 11 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 10 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 9 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 9 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 9 |
11 files changed, 237 insertions, 198 deletions
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 4da6dbb81..d9a065fd5 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -29,7 +29,6 @@ namespace CVC4 { class Command; class Expr; -class ExprManager; namespace parser { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 47124a589..182abb89b 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -25,6 +25,7 @@ #include <sstream> #include <unordered_set> +#include "api/cvc4cpp.h" #include "base/output.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" @@ -42,10 +43,12 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, +Parser::Parser(api::Solver* solver, + Input* input, + bool strictMode, bool parseOnly) - : d_exprManager(exprManager), - d_resourceManager(d_exprManager->getResourceManager()), + : d_solver(solver), + d_resourceManager(d_solver->getExprManager()->getResourceManager()), d_input(input), d_symtabAllocated(), d_symtab(&d_symtabAllocated), @@ -58,7 +61,8 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, d_parseOnly(parseOnly), d_canIncludeFile(true), d_logicIsForced(false), - d_forcedLogic() { + d_forcedLogic() +{ d_input->setParser(*this); } @@ -72,6 +76,11 @@ Parser::~Parser() { delete d_input; } +ExprManager* Parser::getExprManager() const +{ + return d_solver->getExprManager(); +} + Expr Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); assert(isDeclared(name, type)); @@ -120,12 +129,12 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { if(isDefinedFunction(expr)) { // defined functions/constants are wrapped in an APPLY so that they are // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions - expr = d_exprManager->mkExpr(CVC4::kind::APPLY, expr); + expr = getExprManager()->mkExpr(CVC4::kind::APPLY, expr); }else{ Type te = expr.getType(); if(te.isConstructor() && ConstructorType(te).getArity() == 0) { // nullary constructors have APPLY_CONSTRUCTOR kind with no children - expr = d_exprManager->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); + expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); } } return expr; @@ -210,14 +219,14 @@ Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags, bo flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(name, type, flags); + Expr expr = getExprManager()->mkVar(name, type, flags); defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); return expr; } Expr Parser::mkBoundVar(const std::string& name, const Type& type) { Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = d_exprManager->mkBoundVar(name, type); + Expr expr = getExprManager()->mkBoundVar(name, type); defineVar(name, expr, false); return expr; } @@ -228,7 +237,7 @@ Expr Parser::mkFunction(const std::string& name, const Type& type, flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(name, type, flags); + Expr expr = getExprManager()->mkVar(name, type, flags); defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); return expr; } @@ -240,7 +249,7 @@ Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, } stringstream name; name << prefix << "_anon_" << ++d_anonymousFunctionCount; - return d_exprManager->mkVar(name.str(), type, flags); + return getExprManager()->mkVar(name.str(), type, flags); } std::vector<Expr> Parser::mkVars(const std::vector<std::string> names, @@ -318,7 +327,7 @@ SortType Parser::mkSort(const std::string& name, uint32_t flags) { flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "newSort(" << name << ")" << std::endl; - Type type = d_exprManager->mkSort(name, flags); + Type type = getExprManager()->mkSort(name, flags); defineType(name, type); return type; } @@ -330,7 +339,7 @@ SortConstructorType Parser::mkSortConstructor(const std::string& name, Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; SortConstructorType type = - d_exprManager->mkSortConstructor(name, arity, flags); + getExprManager()->mkSortConstructor(name, arity, flags); defineType(name, vector<Type>(arity), type); return type; } @@ -353,7 +362,7 @@ SortConstructorType Parser::mkUnresolvedTypeConstructor( const std::string& name, const std::vector<Type>& params) { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - SortConstructorType unresolved = d_exprManager->mkSortConstructor( + SortConstructorType unresolved = getExprManager()->mkSortConstructor( name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); defineType(name, params, unresolved); Type t = getSort(name, params); @@ -372,7 +381,7 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes( std::vector<Datatype>& datatypes, bool doOverload) { try { std::vector<DatatypeType> types = - d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); + getExprManager()->mkMutualDatatypeTypes(datatypes, d_unresolved); assert(datatypes.size() == types.size()); @@ -467,7 +476,7 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, // the introduced variable is internal (not parsable) std::stringstream ss; ss << "__flatten_var_" << i; - Expr v = d_exprManager->mkBoundVar(ss.str(), domainTypes[i]); + Expr v = getExprManager()->mkBoundVar(ss.str(), domainTypes[i]); flattenVars.push_back(v); } range = static_cast<FunctionType>(range).getRangeType(); @@ -476,7 +485,7 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, { return range; } - return d_exprManager->mkFunctionType(sorts, range); + return getExprManager()->mkFunctionType(sorts, range); } Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range) @@ -493,14 +502,14 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range) sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end()); range = static_cast<FunctionType>(range).getRangeType(); } - return d_exprManager->mkFunctionType(sorts, range); + return getExprManager()->mkFunctionType(sorts, range); } Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex) { for (unsigned i = startIndex; i < args.size(); i++) { - expr = d_exprManager->mkExpr(HO_APPLY, expr, args[i]); + expr = getExprManager()->mkExpr(HO_APPLY, expr, args[i]); } return expr; } @@ -573,8 +582,8 @@ void Parser::checkArity(Kind kind, unsigned numArgs) return; } - unsigned min = d_exprManager->minArity(kind); - unsigned max = d_exprManager->maxArity(kind); + unsigned min = getExprManager()->minArity(kind); + unsigned max = getExprManager()->maxArity(kind); if (numArgs < min || numArgs > max) { stringstream ss; @@ -630,7 +639,7 @@ Command* Parser::nextCommand() dynamic_cast<QuitCommand*>(cmd) == NULL) { // don't count set-option commands as to not get stuck in an infinite // loop of resourcing out - const Options& options = d_exprManager->getOptions(); + const Options& options = getExprManager()->getOptions(); d_resourceManager->spendResource(options.getParseStep()); } return cmd; @@ -639,7 +648,7 @@ Command* Parser::nextCommand() Expr Parser::nextExpression() { Debug("parser") << "nextExpression()" << std::endl; - const Options& options = d_exprManager->getOptions(); + const Options& options = getExprManager()->getOptions(); d_resourceManager->spendResource(options.getParseStep()); Expr result; if (!done()) { diff --git a/src/parser/parser.h b/src/parser/parser.h index 78cbcaafb..b0519691c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -24,23 +24,25 @@ #include <list> #include <cassert> -#include "parser/input.h" -#include "parser/parser_exception.h" #include "expr/expr.h" -#include "expr/symbol_table.h" -#include "expr/kind.h" #include "expr/expr_stream.h" +#include "expr/kind.h" +#include "expr/symbol_table.h" +#include "parser/input.h" +#include "parser/parser_exception.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { // Forward declarations class BooleanType; -class ExprManager; class Command; class FunctionType; class Type; class ResourceManager; +namespace api { +class Solver; +} //for sygus gterm two-pass parsing class CVC4_PUBLIC SygusGTerm { @@ -135,135 +137,137 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) { class CVC4_PUBLIC Parser { friend class ParserBuilder; private: - /** The expression manager */ - ExprManager *d_exprManager; - /** The resource manager associated with this expr manager */ - ResourceManager *d_resourceManager; + /** The API Solver object. */ + api::Solver* d_solver; - /** The input that we're parsing. */ - Input *d_input; + /** The resource manager associated with this expr manager */ + ResourceManager* d_resourceManager; - /** - * The declaration scope that is "owned" by this parser. May or - * may not be the current declaration scope in use. - */ - SymbolTable d_symtabAllocated; + /** The input that we're parsing. */ + Input* d_input; - /** - * This current symbol table used by this parser. Initially points - * to d_symtabAllocated, but can be changed (making this parser - * delegate its definitions and lookups to another parser). - * See useDeclarationsFrom(). - */ - SymbolTable* d_symtab; + /** + * The declaration scope that is "owned" by this parser. May or + * may not be the current declaration scope in use. + */ + SymbolTable d_symtabAllocated; - /** - * 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; + /** + * This current symbol table used by this parser. Initially points + * to d_symtabAllocated, but can be changed (making this parser + * delegate its definitions and lookups to another parser). + * See useDeclarationsFrom(). + */ + SymbolTable* d_symtab; - /** - * Whether we're in global declarations mode (all definitions and - * declarations are global). - */ - bool d_globalDeclarations; + /** + * 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; - /** - * Maintains a list of reserved symbols at the assertion level that might - * not occur in our symbol table. This is necessary to e.g. support the - * proper behavior of the :named annotation in SMT-LIBv2 when used under - * a let or a quantifier, since inside a let/quant body the declaration - * scope is that of the let/quant body, but the defined name should be - * reserved at the assertion level. - */ - std::set<std::string> d_reservedSymbols; + /** + * Whether we're in global declarations mode (all definitions and + * declarations are global). + */ + bool d_globalDeclarations; + + /** + * Maintains a list of reserved symbols at the assertion level that might + * not occur in our symbol table. This is necessary to e.g. support the + * proper behavior of the :named annotation in SMT-LIBv2 when used under + * a let or a quantifier, since inside a let/quant body the declaration + * scope is that of the let/quant body, but the defined name should be + * reserved at the assertion level. + */ + std::set<std::string> d_reservedSymbols; - /** How many anonymous functions we've created. */ - size_t d_anonymousFunctionCount; + /** How many anonymous functions we've created. */ + size_t d_anonymousFunctionCount; - /** Are we done */ - bool d_done; + /** Are we done */ + bool d_done; - /** Are semantic checks enabled during parsing? */ - bool d_checksEnabled; + /** Are semantic checks enabled during parsing? */ + bool d_checksEnabled; - /** Are we parsing in strict mode? */ - bool d_strictMode; + /** Are we parsing in strict mode? */ + bool d_strictMode; - /** Are we only parsing? */ - bool d_parseOnly; + /** 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; + /** + * Can we include files? (Set to false for security purposes in + * e.g. the online version.) + */ + bool d_canIncludeFile; - /** - * The logic, if d_logicIsForced == true. - */ - std::string d_forcedLogic; + /** + * Whether the logic has been forced with --force-logic. + */ + bool d_logicIsForced; - /** The set of operators available in the current logic. */ - std::set<Kind> d_logicOperators; + /** + * The logic, if d_logicIsForced == true. + */ + std::string d_forcedLogic; - /** The set of attributes already warned about. */ - std::set<std::string> d_attributesWarnedAbout; + /** The set of operators available in the current logic. */ + std::set<Kind> d_logicOperators; - /** - * 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<Type> d_unresolved; + /** The set of attributes already warned about. */ + std::set<std::string> d_attributesWarnedAbout; - /** - * "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; + /** + * 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<Type> 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. - */ - Expr getSymbol(const std::string& var_name, SymbolType type); + /** Lookup a symbol in the given namespace (as specified by the type). + * Only returns a symbol if it is not overloaded, returns null otherwise. + */ + Expr getSymbol(const std::string& var_name, SymbolType type); protected: - /** - * Create a parser state. - * - * @attention The parser takes "ownership" of the given - * input and will delete it on destruction. - * - * @param exprManager the expression manager to use when creating expressions - * @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()) - */ - Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + /** + * Create a parser state. + * + * @attention The parser takes "ownership" of the given + * input and will delete it on destruction. + * + * @param the solver API object + * @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()) + */ + Parser(api::Solver* solver, + Input* input, + bool strictMode = false, + bool parseOnly = false); public: virtual ~Parser(); /** Get the associated <code>ExprManager</code>. */ - inline ExprManager* getExprManager() const { - return d_exprManager; - } + ExprManager* getExprManager() const; /** Get the associated input. */ inline Input* getInput() const { diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 4505c4f86..95a3a7840 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -2,7 +2,7 @@ /*! \file parser_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -21,10 +21,11 @@ #include <string> +#include "api/cvc4cpp.h" #include "expr/expr_manager.h" +#include "options/options.h" #include "parser/input.h" #include "parser/parser.h" -#include "options/options.h" #include "smt1/smt1.h" #include "smt2/smt2.h" #include "tptp/tptp.h" @@ -32,29 +33,28 @@ namespace CVC4 { namespace parser { -ParserBuilder::ParserBuilder(ExprManager* exprManager, - const std::string& filename) : - d_filename(filename), - d_exprManager(exprManager) { - init(exprManager, filename); +ParserBuilder::ParserBuilder(api::Solver* solver, const std::string& filename) + : d_filename(filename), d_solver(solver) +{ + init(solver, filename); } -ParserBuilder::ParserBuilder(ExprManager* exprManager, +ParserBuilder::ParserBuilder(api::Solver* solver, const std::string& filename, - const Options& options) : - d_filename(filename), - d_exprManager(exprManager) { - init(exprManager, filename); + const Options& options) + : d_filename(filename), d_solver(solver) +{ + init(solver, filename); withOptions(options); } -void ParserBuilder::init(ExprManager* exprManager, - const std::string& filename) { +void ParserBuilder::init(api::Solver* solver, const std::string& filename) +{ d_inputType = FILE_INPUT; d_lang = language::input::LANG_AUTO; d_filename = filename; d_streamInput = NULL; - d_exprManager = exprManager; + d_solver = solver; d_checksEnabled = true; d_strictMode = false; d_canIncludeFile = true; @@ -87,26 +87,27 @@ Parser* ParserBuilder::build() assert(input != NULL); Parser* parser = NULL; - switch(d_lang) { - case language::input::LANG_SMTLIB_V1: - parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly); - break; - case language::input::LANG_SYGUS: - parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); - break; - case language::input::LANG_TPTP: - parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly); - break; - default: - if (language::isInputLang_smt2(d_lang)) - { - parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); - } - else - { - parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); - } - break; + switch (d_lang) + { + case language::input::LANG_SMTLIB_V1: + parser = new Smt1(d_solver, input, d_strictMode, d_parseOnly); + break; + case language::input::LANG_SYGUS: + parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly); + break; + case language::input::LANG_TPTP: + parser = new Tptp(d_solver, input, d_strictMode, d_parseOnly); + break; + default: + if (language::isInputLang_smt2(d_lang)) + { + parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly); + } + else + { + parser = new Parser(d_solver, input, d_strictMode, d_parseOnly); + } + break; } if( d_checksEnabled ) { @@ -133,8 +134,9 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withExprManager(ExprManager* exprManager) { - d_exprManager = exprManager; +ParserBuilder& ParserBuilder::withSolver(api::Solver* solver) +{ + d_solver = solver; return *this; } diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index c4c75aae5..3e14d715a 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -2,7 +2,7 @@ /*! \file parser_builder.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -26,9 +26,12 @@ namespace CVC4 { -class ExprManager; class Options; +namespace api { +class Solver; +} + namespace parser { class Parser; @@ -61,8 +64,8 @@ class CVC4_PUBLIC ParserBuilder { /** The stream input, if any. */ std::istream* d_streamInput; - /** The expression manager */ - ExprManager* d_exprManager; + /** The API Solver object. */ + api::Solver* d_solver; /** Should semantic checks be enabled during parsing? */ bool d_checksEnabled; @@ -86,14 +89,14 @@ class CVC4_PUBLIC ParserBuilder { std::string d_forcedLogic; /** Initialize this parser builder */ - void init(ExprManager* exprManager, const std::string& filename); - -public: + void init(api::Solver* solver, const std::string& filename); - /** Create a parser builder using the given ExprManager and filename. */ - ParserBuilder(ExprManager* exprManager, const std::string& filename); + public: + /** Create a parser builder using the given Solver and filename. */ + ParserBuilder(api::Solver* solver, const std::string& filename); - ParserBuilder(ExprManager* exprManager, const std::string& filename, + ParserBuilder(api::Solver* solver, + const std::string& filename, const Options& options); /** Build the parser, using the current settings. */ @@ -102,8 +105,8 @@ public: /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); - /** Set the ExprManager to use with the parser. */ - ParserBuilder& withExprManager(ExprManager* exprManager); + /** Set the Solver to use with the parser. */ + ParserBuilder& withSolver(api::Solver* solver); /** Set the parser to read a file for its input. (Default) */ ParserBuilder& withFileInput(); diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 87da44c0e..544c6e85c 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -14,9 +14,10 @@ #include "parser/smt1/smt1.h" +#include "api/cvc4cpp.h" #include "expr/type.h" -#include "smt/command.h" #include "parser/parser.h" +#include "smt/command.h" namespace CVC4 { namespace parser { @@ -70,9 +71,9 @@ Smt1::Logic Smt1::toLogic(const std::string& name) { return logicMap[name]; } -Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, - bool parseOnly) - : Parser(exprManager, input, strictMode, parseOnly), d_logic(UNSET) { +Smt1::Smt1(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) + : Parser(solver, input, strictMode, parseOnly), d_logic(UNSET) +{ // Boolean symbols are always defined addOperator(kind::AND); addOperator(kind::EQUAL); @@ -81,7 +82,6 @@ Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, addOperator(kind::NOT); addOperator(kind::OR); addOperator(kind::XOR); - } void Smt1::addArithmeticOperators() { diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index 42b6a4157..fe177d21e 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -2,7 +2,7 @@ /*! \file smt1.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -26,6 +26,10 @@ namespace CVC4 { class SExpr; +namespace api { +class Solver; +} + namespace parser { class Smt1 : public Parser { @@ -93,7 +97,10 @@ private: Logic d_logic; protected: - Smt1(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + Smt1(api::Solver* solver, + Input* input, + bool strictMode = false, + bool parseOnly = false); public: /** diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a0cc750b3..0a93beb2e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -15,6 +15,7 @@ **/ #include "parser/smt2/smt2.h" +#include "api/cvc4cpp.h" #include "expr/type.h" #include "options/options.h" #include "parser/antlr_input.h" @@ -34,10 +35,11 @@ namespace CVC4 { namespace parser { -Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : - Parser(exprManager,input,strictMode,parseOnly), - d_logicSet(false) { - if( !strictModeEnabled() ) { +Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) + : Parser(solver, input, strictMode, parseOnly), d_logicSet(false) +{ + if (!strictModeEnabled()) + { addTheory(Smt2::THEORY_CORE); } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c9b224d39..64a957402 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -34,6 +34,10 @@ namespace CVC4 { class SExpr; +namespace api { +class Solver; +} + namespace parser { class Smt2 : public Parser { @@ -69,7 +73,10 @@ private: std::map< Expr, bool > d_sygusVarPrimed; protected: - Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + Smt2(api::Solver* solver, + Input* input, + bool strictMode = false, + bool parseOnly = false); public: /** diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 0228fdeff..ee313a202 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -20,6 +20,7 @@ #include <algorithm> #include <set> +#include "api/cvc4cpp.h" #include "expr/type.h" #include "parser/parser.h" @@ -30,11 +31,9 @@ namespace CVC4 { namespace parser { -Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, - bool parseOnly) - : Parser(exprManager, input, strictMode, parseOnly), - d_cnf(false), - d_fof(false) { +Tptp::Tptp(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) + : Parser(solver, input, strictMode, parseOnly), d_cnf(false), d_fof(false) +{ addTheory(Tptp::THEORY_CORE); /* Try to find TPTP dir */ diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 3ce9668e0..eb5532247 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -30,6 +30,11 @@ #include "util/hash.h" namespace CVC4 { + +namespace api { +class Solver; +} + namespace parser { class Tptp : public Parser { @@ -81,7 +86,9 @@ class Tptp : public Parser { bool hasConjecture() const { return d_hasConjecture; } protected: - Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, + Tptp(api::Solver* solver, + Input* input, + bool strictMode = false, bool parseOnly = false); public: |