projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
ba7dd53
)
Add support for set-logic ALL, fix compiler error in GCC 6.1
author
Clark Barrett
<barrett@cs.stanford.edu>
Fri, 18 Nov 2016 23:01:59 +0000
(15:01 -0800)
committer
Clark Barrett
<barrett@cs.stanford.edu>
Fri, 18 Nov 2016 23:01:59 +0000
(15:01 -0800)
src/main/command_executor.cpp
patch
|
blob
|
history
src/parser/smt1/smt1.cpp
patch
|
blob
|
history
src/parser/smt2/Smt2.g
patch
|
blob
|
history
src/parser/smt2/smt2.cpp
patch
|
blob
|
history
src/smt/smt_engine.cpp
patch
|
blob
|
history
src/theory/logic_info.cpp
patch
|
blob
|
history
src/theory/strings/theory_strings.cpp
patch
|
blob
|
history
diff --git
a/src/main/command_executor.cpp
b/src/main/command_executor.cpp
index f9055f56cd131733578be1aa86620568ae656089..64025fc0468c4f115d4c47163cf0f1e997e6c71b 100644
(file)
--- a/
src/main/command_executor.cpp
+++ b/
src/main/command_executor.cpp
@@
-254,7
+254,7
@@
void CommandExecutor::printStatsFilterZeros(std::ostream& out,
std::getline(iss, statValue, '\n');
double curFloat;
std::getline(iss, statValue, '\n');
double curFloat;
- bool isFloat = (std::istringstream(statValue) >> curFloat);
+ bool isFloat =
static_cast<bool>
(std::istringstream(statValue) >> curFloat);
if( (isFloat && curFloat == 0) ||
statValue == " \"0\"" ||
if( (isFloat && curFloat == 0) ||
statValue == " \"0\"" ||
diff --git
a/src/parser/smt1/smt1.cpp
b/src/parser/smt1/smt1.cpp
index 50f62009acfc4c36c1a22d172943a0dc078b27be..015129f100bfe8f478f381c2c886c8b0c11c468f 100644
(file)
--- a/
src/parser/smt1/smt1.cpp
+++ b/
src/parser/smt1/smt1.cpp
@@
-62,6
+62,8
@@
std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne
logicMap["UFLRA"] = UFLRA;
logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
logicMap["UFLRA"] = UFLRA;
logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
+ logicMap["QF_ALL"] = QF_ALL_SUPPORTED;
+ logicMap["ALL"] = ALL_SUPPORTED;
return logicMap;
}
return logicMap;
}
diff --git
a/src/parser/smt2/Smt2.g
b/src/parser/smt2/Smt2.g
index 27c5a62bd22f2bfc93eec43b517574d7427c743d..ff34fd9a3ed2888685bb6372aba69b236b91ca53 100644
(file)
--- a/
src/parser/smt2/Smt2.g
+++ b/
src/parser/smt2/Smt2.g
@@
-272,7
+272,7
@@
command [CVC4::PtrCloser<CVC4::Command>* cmd]
}
PARSER_STATE->setLogic(name);
if( PARSER_STATE->sygus() ){
}
PARSER_STATE->setLogic(name);
if( PARSER_STATE->sygus() ){
- cmd->reset(new SetBenchmarkLogicCommand("ALL
_SUPPORTED
"));
+ cmd->reset(new SetBenchmarkLogicCommand("ALL"));
}else{
cmd->reset(new SetBenchmarkLogicCommand(name));
}
}else{
cmd->reset(new SetBenchmarkLogicCommand(name));
}
diff --git
a/src/parser/smt2/smt2.cpp
b/src/parser/smt2/smt2.cpp
index 8db344f929b7bcccbe32dbc6deca535204d2b240..2e2481a6e0af3b2591015926a0d5ca63039eb641 100644
(file)
--- a/
src/parser/smt2/smt2.cpp
+++ b/
src/parser/smt2/smt2.cpp
@@
-370,7
+370,7
@@
void Smt2::setLogic(std::string name) {
name = "UFSLIA";
} else if(name == "SAT") {
name = "UF";
name = "UFSLIA";
} else if(name == "SAT") {
name = "UF";
- } else if(name == "ALL_SUPPORTED") {
+ } else if(name == "ALL
" || name == "ALL
_SUPPORTED") {
//no change
} else {
std::stringstream ss;
//no change
} else {
std::stringstream ss;
@@
-456,14
+456,14
@@
void Smt2::checkThatLogicIsSet() {
setLogic("LIA");
} else {
warning("No set-logic command was given before this point.");
setLogic("LIA");
} else {
warning("No set-logic command was given before this point.");
- warning("CVC4 will
assume the non-standard ALL_SUPPORTED logic
.");
+ warning("CVC4 will
make all theories available
.");
warning("Consider setting a stricter logic for (likely) better performance.");
warning("Consider setting a stricter logic for (likely) better performance.");
- warning("To suppress this warning in the future use (set-logic ALL
_SUPPORTED
).");
+ warning("To suppress this warning in the future use (set-logic ALL).");
- setLogic("ALL
_SUPPORTED
");
+ setLogic("ALL");
}
}
- Command* c = new SetBenchmarkLogicCommand("ALL
_SUPPORTED
");
+ Command* c = new SetBenchmarkLogicCommand("ALL");
c->setMuted(true);
preemptCommand(c);
}
c->setMuted(true);
preemptCommand(c);
}
diff --git
a/src/smt/smt_engine.cpp
b/src/smt/smt_engine.cpp
index 38347508cabc7860e9eda2b6bfbec6bbda39dba6..5fc96aa6ea50e199bf4e226087c32706b3f97989 100644
(file)
--- a/
src/smt/smt_engine.cpp
+++ b/
src/smt/smt_engine.cpp
@@
-1645,7
+1645,7
@@
void SmtEngine::setDefaults() {
// Set decision mode based on logic (if not set by user)
if(!options::decisionMode.wasSetByUser()) {
decision::DecisionMode decMode =
// Set decision mode based on logic (if not set by user)
if(!options::decisionMode.wasSetByUser()) {
decision::DecisionMode decMode =
- // ALL
_SUPPORTED
+ // ALL
d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION :
( // QF_BV
(not d_logic.isQuantified() &&
d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION :
( // QF_BV
(not d_logic.isQuantified() &&
@@
-1676,7
+1676,7
@@
void SmtEngine::setDefaults() {
);
bool stoponly =
);
bool stoponly =
- // ALL
_SUPPORTED
+ // ALL
d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
( // QF_AUFLIA
(not d_logic.isQuantified() &&
d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
( // QF_AUFLIA
(not d_logic.isQuantified() &&
diff --git
a/src/theory/logic_info.cpp
b/src/theory/logic_info.cpp
index 6ac1c5e32ec7fb3d42c4daa6e2fdbcf1568f958e..0e4ccf0f73ce67722349395ee48f99b7b6ef6638 100644
(file)
--- a/
src/theory/logic_info.cpp
+++ b/
src/theory/logic_info.cpp
@@
-242,9
+242,9
@@
std::string LogicInfo::getLogicString() const {
qf_all_supported.disableQuantifiers();
qf_all_supported.lock();
if(hasEverything()) {
qf_all_supported.disableQuantifiers();
qf_all_supported.lock();
if(hasEverything()) {
- d_logicString = "ALL
_SUPPORTED
";
+ d_logicString = "ALL";
} else if(*this == qf_all_supported) {
} else if(*this == qf_all_supported) {
- d_logicString = "QF_ALL
_SUPPORTED
";
+ d_logicString = "QF_ALL";
} else {
size_t seen = 0; // make sure we support all the active theories
} else {
size_t seen = 0; // make sure we support all the active theories
@@
-341,11
+341,21
@@
void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
enableEverything();
disableQuantifiers();
p += 16;
enableEverything();
disableQuantifiers();
p += 16;
+ } else if(!strcmp(p, "QF_ALL")) {
+ // the "all theories included" logic, no quantifiers
+ enableEverything();
+ disableQuantifiers();
+ p += 6;
} else if(!strcmp(p, "ALL_SUPPORTED")) {
// the "all theories included" logic, with quantifiers
enableEverything();
enableQuantifiers();
p += 13;
} else if(!strcmp(p, "ALL_SUPPORTED")) {
// the "all theories included" logic, with quantifiers
enableEverything();
enableQuantifiers();
p += 13;
+ } else if(!strcmp(p, "ALL")) {
+ // the "all theories included" logic, with quantifiers
+ enableEverything();
+ enableQuantifiers();
+ p += 3;
} else {
if(!strncmp(p, "QF_", 3)) {
disableQuantifiers();
} else {
if(!strncmp(p, "QF_", 3)) {
disableQuantifiers();
diff --git
a/src/theory/strings/theory_strings.cpp
b/src/theory/strings/theory_strings.cpp
index 26e6908daf7b9efdbb8ba2ecf7039ede4c7cd9b1..8b44b5cac9b224e82afbe8041e642d5b7c57adef 100644
(file)
--- a/
src/theory/strings/theory_strings.cpp
+++ b/
src/theory/strings/theory_strings.cpp
@@
-646,12
+646,6
@@
void TheoryStrings::check(Effort e) {
bool polarity;
TNode atom;
bool polarity;
TNode atom;
- /*if(getLogicInfo().hasEverything()) {
- WarningOnce() << "WARNING: strings not supported in default configuration (ALL_SUPPORTED).\n"
- << "To suppress this warning in the future use proper logic symbol, e.g. (set-logic QF_S)." << std::endl;
- }
- }*/
-
if( !done() && !hasTerm( d_emptyString ) ) {
preRegisterTerm( d_emptyString );
}
if( !done() && !hasTerm( d_emptyString ) ) {
preRegisterTerm( d_emptyString );
}