*/
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);
}
/** 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;
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{
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.
Options::Options()
: d_holder(new options::OptionsHolder())
, d_handler(new options::OptionsHandler(this))
- , d_forceLogicListeners()
, d_beforeSearchListeners()
, d_tlimitListeners()
, d_tlimitPerListeners()
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)
{
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"
read_only = true
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"
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
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; }
#include <string>
#include "api/cvc4cpp.h"
+#include "cvc/cvc.h"
#include "expr/expr_manager.h"
#include "options/options.h"
#include "parser/input.h"
}
else
{
- parser = new Parser(d_solver, input, d_strictMode, d_parseOnly);
+ parser = new Cvc(d_solver, input, d_strictMode, d_parseOnly);
}
break;
}
}
: /* 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]
}
: 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));
}
#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>
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())
{
}
}
-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)
}
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
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: ???
// 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);
}
}
}
#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"
};
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;
/**
* 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.
}
}
+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);
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();
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) {}
* This list contains:
* softResourceOut
* hardResourceOut
- * setForceLogic
* beforeSearchListener
* UseTheoryListListener
*
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.
}
}
- 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(
"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");
}
}
}
- // 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")
regress0/bv/divtest_2_5.smt2
regress0/bv/divtest_2_6.smt2
regress0/bv/eager-inc-cryptominisat.smt2
+ regress0/bv/eager-force-logic.smt2
regress0/bv/fuzz01.smt
regress0/bv/fuzz02.delta01.smt
regress0/bv/fuzz02.smt
regress0/parser/bv_arity_smt2.6.smt2
regress0/parser/constraint.smt2
regress0/parser/declarefun-emptyset-uf.smt2
+ regress0/parser/force_logic_set_logic.smt2
regress0/parser/shadow_fun_symbol_all.smt2
regress0/parser/shadow_fun_symbol_nirat.smt2
regress0/parser/strings20.smt2
--- /dev/null
+; COMMAND-LINE: --bitblast=eager --force-logic="QF_BV"
+; EXPECT: sat
+(set-option :produce-models true)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+(declare-fun c () (_ BitVec 16))
+
+(assert (bvult a (bvadd b c)))
+(check-sat)
--- /dev/null
+; This regression ensures that we detect repeated set-logic commands even when
+; --force-logic is used.
+
+; COMMAND-LINE: --force-logic="QF_BV"
+; SCRUBBER: grep -o "Only one set-logic is allowed."
+; EXPECT: Only one set-logic is allowed.
+; EXIT: 1
+(set-logic QF_BV)
+(set-logic QF_BV)
void SolverBlack::testSetInfo()
{
- TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4-logic", "QF_BV"));
- TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4_logic", "QF_BV"));
TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->setInfo("cvc2-logic", "QF_BV"), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "asdf"), CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unsat"));
TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unknown"));
TS_ASSERT_THROWS(d_solver->setInfo("status", "asdf"), CVC4ApiException&);
-
- d_solver->assertFormula(d_solver->mkTrue());
- TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "QF_BV"), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->setInfo("cvc4_logic", "QF_BV"), CVC4ApiException&);
}
void SolverBlack::testSetLogic()
projects / cvc5.git / commitdiff