summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp52
-rw-r--r--src/options/options.h3
-rw-r--r--src/options/options_handler.cpp4
-rw-r--r--src/options/options_handler.h3
-rw-r--r--src/options/options_template.cpp8
-rw-r--r--src/options/parser_options.toml9
-rw-r--r--src/options/smt_options.toml10
-rw-r--r--src/parser/CMakeLists.txt2
-rw-r--r--src/parser/cvc/cvc.cpp29
-rw-r--r--src/parser/cvc/cvc.h50
-rw-r--r--src/parser/parser.h7
-rw-r--r--src/parser/parser_builder.cpp3
-rw-r--r--src/parser/smt2/Smt2.g15
-rw-r--r--src/parser/smt2/smt2.cpp80
-rw-r--r--src/parser/smt2/smt2.h10
-rw-r--r--src/parser/tptp/tptp.cpp6
-rw-r--r--src/parser/tptp/tptp.h2
-rw-r--r--src/smt/smt_engine.cpp52
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")
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback