diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 52 | ||||
-rw-r--r-- | src/options/options.h | 3 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 4 | ||||
-rw-r--r-- | src/options/options_handler.h | 3 | ||||
-rw-r--r-- | src/options/options_template.cpp | 8 | ||||
-rw-r--r-- | src/options/parser_options.toml | 9 | ||||
-rw-r--r-- | src/options/smt_options.toml | 10 | ||||
-rw-r--r-- | src/parser/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/parser/cvc/cvc.cpp | 29 | ||||
-rw-r--r-- | src/parser/cvc/cvc.h | 50 | ||||
-rw-r--r-- | src/parser/parser.h | 7 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 3 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 15 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 80 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 10 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 6 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 52 |
18 files changed, 200 insertions, 145 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ab34e62b4..7750823d3 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3389,41 +3389,23 @@ void Solver::setLogicHelper(const std::string& logic) const */ void Solver::setInfo(const std::string& keyword, const std::string& value) const { - bool is_cvc4_keyword = false; - - /* Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") */ - if (keyword.length() > 5) - { - std::string prefix = keyword.substr(0, 5); - if (prefix == "cvc4-" || prefix == "cvc4_") - { - is_cvc4_keyword = true; - std::string cvc4key = keyword.substr(5); - CVC4_API_ARG_CHECK_EXPECTED(cvc4key == "logic", keyword) - << "keyword 'cvc4-logic'"; - setLogicHelper(value); - } - } - if (!is_cvc4_keyword) - { - CVC4_API_ARG_CHECK_EXPECTED( - keyword == "source" || keyword == "category" || keyword == "difficulty" - || keyword == "filename" || keyword == "license" - || keyword == "name" || keyword == "notes" - || keyword == "smt-lib-version" || keyword == "status", - keyword) - << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " - "'notes', 'smt-lib-version' or 'status'"; - CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2" - || value == "2.0" || value == "2.5" - || value == "2.6" || value == "2.6.1", - value) - << "'2.0', '2.5', '2.6' or '2.6.1'"; - CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat" - || value == "unsat" || value == "unknown", - value) - << "'sat', 'unsat' or 'unknown'"; - } + CVC4_API_ARG_CHECK_EXPECTED( + keyword == "source" || keyword == "category" || keyword == "difficulty" + || keyword == "filename" || keyword == "license" || keyword == "name" + || keyword == "notes" || keyword == "smt-lib-version" + || keyword == "status", + keyword) + << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " + "'notes', 'smt-lib-version' or 'status'"; + CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2" + || value == "2.0" || value == "2.5" + || value == "2.6" || value == "2.6.1", + value) + << "'2.0', '2.5', '2.6' or '2.6.1'"; + CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat" + || value == "unsat" || value == "unknown", + value) + << "'sat', 'unsat' or 'unknown'"; d_smtEngine->setInfo(keyword, value); } diff --git a/src/options/options.h b/src/options/options.h index 3f2d72b7e..1fc7ed51a 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -52,9 +52,6 @@ class CVC4_PUBLIC Options { /** The current Options in effect */ static thread_local Options* s_current; - /** Listeners for options::forceLogicString being set. */ - ListenerCollection d_forceLogicListeners; - /** Listeners for notifyBeforeSearch. */ ListenerCollection d_beforeSearchListeners; diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 5e98f8f5a..b145da639 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -74,10 +74,6 @@ void throwLazyBBUnsupported(theory::bv::SatSolverMode m) OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } -void OptionsHandler::notifyForceLogic(const std::string& option){ - d_options->d_forceLogicListeners.notify(); -} - void OptionsHandler::notifyBeforeSearch(const std::string& option) { try{ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 06f7ab6e4..7ae461fd8 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -174,9 +174,6 @@ public: decision::DecisionWeightInternal stringToDecisionWeightInternal( std::string option, std::string optarg); - /* smt/options_handlers.h */ - void notifyForceLogic(const std::string& option); - /** * Throws a ModalException if this option is being set after final * initialization. diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 1f7ba05fc..f67493f87 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -231,7 +231,6 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h Options::Options() : d_holder(new options::OptionsHolder()) , d_handler(new options::OptionsHandler(this)) - , d_forceLogicListeners() , d_beforeSearchListeners() , d_tlimitListeners() , d_tlimitPerListeners() @@ -283,13 +282,6 @@ ListenerCollection::Registration* Options::registerAndNotify( return registration; } -ListenerCollection::Registration* Options::registerForceLogicListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::forceLogicString); - return registerAndNotify(d_forceLogicListeners, listener, notify); -} - ListenerCollection::Registration* Options::registerBeforeSearchListener( Listener* listener) { diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 988bcb6eb..71074d420 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -65,3 +65,12 @@ header = "options/parser_options.h" category = "undocumented" long = "no-include-file" links = ["--no-filesystem-access"] + +[[option]] + name = "forceLogicString" + smt_name = "force-logic" + category = "expert" + long = "force-logic=LOGIC" + type = "std::string" + read_only = true + help = "set the logic, and override all further user attempts to change it" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index e0041774a..72dfdd7f8 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -23,16 +23,6 @@ header = "options/smt_options.h" help = "all dumping goes to FILE (instead of stdout)" [[option]] - name = "forceLogicString" - smt_name = "force-logic" - category = "expert" - long = "force-logic=LOGIC" - type = "std::string" - notifies = ["notifyForceLogic"] - read_only = true - help = "set the logic, and override all further user attempts to change it" - -[[option]] name = "simplificationMode" smt_name = "simplification-mode" category = "regular" diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index d79d7b22c..03e194b90 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -22,6 +22,8 @@ set(libcvc4parser_src_files bounded_token_buffer.h bounded_token_factory.cpp bounded_token_factory.h + cvc/cvc.cpp + cvc/cvc.h cvc/cvc_input.cpp cvc/cvc_input.h input.cpp diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp new file mode 100644 index 000000000..9b7e1f403 --- /dev/null +++ b/src/parser/cvc/cvc.cpp @@ -0,0 +1,29 @@ +/********************* */ +/*! \file cvc.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief The parser class for the CVC language. + ** + ** The parser class for the CVC language. + **/ + +#include "parser/cvc/cvc.h" + +namespace CVC4 { +namespace parser { + +void Cvc::forceLogic(const std::string& logic) +{ + Parser::forceLogic(logic); + preemptCommand(new SetBenchmarkLogicCommand(logic)); +} + +} // namespace parser +} // namespace CVC4 diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h new file mode 100644 index 000000000..feb962a09 --- /dev/null +++ b/src/parser/cvc/cvc.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file cvc.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief The parser class for the CVC language. + ** + ** The parser class for the CVC language. + **/ + +#include "cvc4parser_private.h" + +#ifndef CVC4__PARSER__CVC_H +#define CVC4__PARSER__CVC_H + +#include "api/cvc4cpp.h" +#include "parser/parser.h" +#include "smt/command.h" + +namespace CVC4 { + +namespace parser { + +class Cvc : public Parser +{ + friend class ParserBuilder; + + public: + void forceLogic(const std::string& logic) override; + + protected: + Cvc(api::Solver* solver, + Input* input, + bool strictMode = false, + bool parseOnly = false) + : Parser(solver, input, strictMode, parseOnly) + { + } +}; + +} // namespace parser +} // namespace CVC4 + +#endif /* CVC4__PARSER__CVC_H */ diff --git a/src/parser/parser.h b/src/parser/parser.h index fcc37d5d3..8f9cc425a 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -322,7 +322,12 @@ public: implementation optional by returning false by default. */ virtual bool logicIsSet() { return false; } - void forceLogic(const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced = true; d_forcedLogic = logic; } + virtual void forceLogic(const std::string& logic) + { + assert(!d_logicIsForced); + d_logicIsForced = true; + d_forcedLogic = logic; + } const std::string& getForcedLogic() const { return d_forcedLogic; } bool logicIsForced() const { return d_logicIsForced; } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 57b63cc0f..f0e6ad284 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -22,6 +22,7 @@ #include <string> #include "api/cvc4cpp.h" +#include "cvc/cvc.h" #include "expr/expr_manager.h" #include "options/options.h" #include "parser/input.h" @@ -105,7 +106,7 @@ Parser* ParserBuilder::build() } else { - parser = new Parser(d_solver, input, d_strictMode, d_parseOnly); + parser = new Cvc(d_solver, input, d_strictMode, d_parseOnly); } break; } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4a30841e6..b49b62604 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -269,16 +269,8 @@ command [std::unique_ptr<CVC4::Command>* cmd] } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] - { Debug("parser") << "set logic: '" << name << "'" << std::endl; - if( PARSER_STATE->logicIsSet() ) { - PARSER_STATE->parseError("Only one set-logic is allowed."); - } - PARSER_STATE->setLogic(name); - if( PARSER_STATE->sygus() ){ - cmd->reset(new SetBenchmarkLogicCommand(PARSER_STATE->getLogic().getLogicString())); - }else{ - cmd->reset(new SetBenchmarkLogicCommand(name)); - } + { + cmd->reset(PARSER_STATE->setLogic(name)); } | /* set-info */ SET_INFO_TOK metaInfoInternal[cmd] @@ -1029,9 +1021,6 @@ metaInfoInternal[std::unique_ptr<CVC4::Command>* cmd] } : KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - if(name == ":cvc4-logic" || name == ":cvc4_logic") { - PARSER_STATE->setLogic(sexpr.getValue()); - } PARSER_STATE->setInfo(name.c_str() + 1, sexpr); cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr)); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 12b43f346..c072c535f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -22,7 +22,6 @@ #include "parser/smt1/smt1.h" #include "parser/smt2/smt2_input.h" #include "printer/sygus_print_callback.h" -#include "smt/command.h" #include "util/bitvector.h" #include <algorithm> @@ -35,7 +34,9 @@ namespace CVC4 { namespace parser { Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) - : Parser(solver, input, strictMode, parseOnly), d_logicSet(false) + : Parser(solver, input, strictMode, parseOnly), + d_logicSet(false), + d_seenSetLogic(false) { if (!strictModeEnabled()) { @@ -626,7 +627,22 @@ void Smt2::resetAssertions() { } } -void Smt2::setLogic(std::string name) { +Command* Smt2::setLogic(std::string name, bool fromCommand) +{ + if (fromCommand) + { + if (d_seenSetLogic) + { + parseError("Only one set-logic is allowed."); + } + d_seenSetLogic = true; + + if (logicIsForced()) + { + // If the logic is forced, we ignore all set-logic requests from commands. + return new EmptyCommand(); + } + } if(sygus()) { // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2) @@ -638,11 +654,7 @@ void Smt2::setLogic(std::string name) { } d_logicSet = true; - if(logicIsForced()) { - d_logic = getForcedLogic(); - } else { - d_logic = name; - } + d_logic = name; // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and // higher-order @@ -718,8 +730,16 @@ void Smt2::setLogic(std::string name) { if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) { addTheory(THEORY_SEP); } - -}/* Smt2::setLogic() */ + + if (sygus()) + { + return new SetBenchmarkLogicCommand(d_logic.getLogicString()); + } + else + { + return new SetBenchmarkLogicCommand(name); + } +} /* Smt2::setLogic() */ void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { // TODO: ??? @@ -729,21 +749,33 @@ void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { // TODO: ??? } -void Smt2::checkThatLogicIsSet() { - if( ! logicIsSet() ) { - if(strictModeEnabled()) { +void Smt2::checkThatLogicIsSet() +{ + if (!logicIsSet()) + { + if (strictModeEnabled()) + { parseError("set-logic must appear before this point."); - } else { - warning("No set-logic command was given before this point."); - warning("CVC4 will make all theories available."); - warning("Consider setting a stricter logic for (likely) better performance."); - warning("To suppress this warning in the future use (set-logic ALL)."); - - setLogic("ALL"); - - Command* c = new SetBenchmarkLogicCommand("ALL"); - c->setMuted(true); - preemptCommand(c); + } + else + { + Command* cmd = nullptr; + if (logicIsForced()) + { + cmd = setLogic(getForcedLogic(), false); + } + else + { + warning("No set-logic command was given before this point."); + warning("CVC4 will make all theories available."); + warning( + "Consider setting a stricter logic for (likely) better " + "performance."); + warning("To suppress this warning in the future use (set-logic ALL)."); + + cmd = setLogic("ALL", false); + } + preemptCommand(cmd); } } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index d4d310b89..2ac796166 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -28,6 +28,7 @@ #include "api/cvc4cpp.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" +#include "smt/command.h" #include "theory/logic_info.h" #include "util/abstract_value.h" @@ -65,7 +66,11 @@ class Smt2 : public Parser }; private: + /** Has the logic been set (either by forcing it or a set-logic command)? */ bool d_logicSet; + /** Have we seen a set-logic command yet? */ + bool d_seenSetLogic; + LogicInfo d_logic; std::unordered_map<std::string, Kind> operatorKindMap; /** @@ -197,8 +202,11 @@ class Smt2 : public Parser * theory symbols. * * @param name the name of the logic (e.g., QF_UF, AUFLIA) + * @param fromCommand should be set to true if the request originates from a + * set-logic command and false otherwise + * @return the command corresponding to setting the logic */ - void setLogic(std::string name); + Command* setLogic(std::string name, bool fromCommand = true); /** * Get the logic. diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index fd593c68b..c4efe5e09 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -214,6 +214,12 @@ void Tptp::checkLetBinding(const std::vector<Expr>& bvlist, Expr lhs, Expr rhs, } } +void Tptp::forceLogic(const std::string& logic) +{ + Parser::forceLogic(logic); + preemptCommand(new SetBenchmarkLogicCommand(logic)); +} + void Tptp::addFreeVar(Expr var) { assert(cnf()); d_freeVar.push_back(var); diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 082b905df..605748d88 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -47,6 +47,8 @@ class Tptp : public Parser { bool fof() const { return d_fof; } void setFof(bool fof) { d_fof = fof; } + void forceLogic(const std::string& logic) override; + void addFreeVar(Expr var); std::vector< Expr > getFreeVar(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2b81b3835..5cf690147 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -285,18 +285,6 @@ class HardResourceOutListener : public Listener { SmtEngine* d_smt; }; /* class HardResourceOutListener */ -class SetLogicListener : public Listener { - public: - SetLogicListener(SmtEngine& smt) : d_smt(&smt) {} - void notify() override - { - LogicInfo inOptions(options::forceLogicString()); - d_smt->setLogic(inOptions); - } - private: - SmtEngine* d_smt; -}; /* class SetLogicListener */ - class BeforeSearchListener : public Listener { public: BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {} @@ -452,7 +440,6 @@ class SmtEnginePrivate : public NodeManagerListener { * This list contains: * softResourceOut * hardResourceOut - * setForceLogic * beforeSearchListener * UseTheoryListListener * @@ -600,9 +587,6 @@ class SmtEnginePrivate : public NodeManagerListener { try { Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - d_listenerRegistrations->add( - nodeManagerOptions.registerForceLogicListener( - new SetLogicListener(d_smt), true)); // Multiple options reuse BeforeSearchListener so registration requires an // extra bit of care. @@ -1209,9 +1193,8 @@ void SmtEngine::setDefaults() { } } - if(options::forceLogicString.wasSetByUser()) { - d_logic = LogicInfo(options::forceLogicString()); - }else if (options::solveIntAsBV() > 0) { + if (options::solveIntAsBV() > 0) + { if (!(d_logic <= LogicInfo("QF_NIA"))) { throw OptionException( @@ -1219,11 +1202,15 @@ void SmtEngine::setDefaults() { "QF_LIA, QF_IDL)"); } d_logic = LogicInfo("QF_BV"); - }else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt()) { + } + else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt()) + { d_logic = LogicInfo("QF_NIA"); - } else if ((d_logic.getLogicString() == "QF_UFBV" || - d_logic.getLogicString() == "QF_ABV") && - options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + } + else if ((d_logic.getLogicString() == "QF_UFBV" + || d_logic.getLogicString() == "QF_ABV") + && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + { d_logic = LogicInfo("QF_BV"); } @@ -2346,25 +2333,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } } - // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") - if(key.length() > 5) { - string prefix = key.substr(0, 5); - if(prefix == "cvc4-" || prefix == "cvc4_") { - string cvc4key = key.substr(5); - if(cvc4key == "logic") { - if(! value.isAtom()) { - throw OptionException("argument to (set-info :cvc4-logic ..) must be a string"); - } - SmtScope smts(this); - d_logic = value.getValue(); - setLogicInternal(); - return; - } else { - throw UnrecognizedOptionException(); - } - } - } - // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...) if (key == "source" || key == "category" || key == "difficulty" || key == "notes" || key == "name" || key == "license") |