summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp25
-rw-r--r--src/main/driver_unified.cpp6
-rw-r--r--src/parser/cvc/Cvc.g45
-rw-r--r--src/parser/parser.h1
-rw-r--r--src/parser/smt2/Smt2.g69
-rw-r--r--src/parser/smt2/smt2.cpp8
-rw-r--r--src/parser/smt2/smt2.h4
-rw-r--r--src/parser/tptp/Tptp.g2
-rw-r--r--src/smt/command.cpp82
-rw-r--r--src/smt/command.h23
-rw-r--r--src/smt/smt_engine.cpp10
11 files changed, 140 insertions, 135 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 5eabcfe62..748a1ce06 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -354,6 +354,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
{CVC4::Kind::DISTINCT, DISTINCT},
{CVC4::Kind::VARIABLE, CONSTANT},
{CVC4::Kind::BOUND_VARIABLE, VARIABLE},
+ {CVC4::Kind::SEXPR, SEXPR},
{CVC4::Kind::LAMBDA, LAMBDA},
{CVC4::Kind::WITNESS, WITNESS},
/* Boolean --------------------------------------------------------- */
@@ -822,6 +823,14 @@ class CVC4ApiRecoverableExceptionStream
<< "Invalid argument '" << arg << "' for '" << #arg \
<< "', expected "
+#define CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg) \
+ CVC4_PREDICT_TRUE(cond) \
+ ? (void)0 \
+ : OstreamVoider() \
+ & CVC4ApiRecoverableExceptionStream().ostream() \
+ << "Invalid argument '" << arg << "' for '" << #arg \
+ << "', expected "
+
#define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \
CVC4_PREDICT_TRUE(cond) \
? (void)0 \
@@ -842,6 +851,10 @@ class CVC4ApiRecoverableExceptionStream
{
#define CVC4_API_SOLVER_TRY_CATCH_END \
} \
+ catch (const UnrecognizedOptionException& e) \
+ { \
+ throw CVC4ApiRecoverableException(e.getMessage()); \
+ } \
catch (const CVC4::RecoverableModalException& e) \
{ \
throw CVC4ApiRecoverableException(e.getMessage()); \
@@ -5083,7 +5096,7 @@ std::vector<Term> Solver::getAssertions(void) const
std::string Solver::getInfo(const std::string& flag) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag))
+ CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag))
<< "Unrecognized flag for getInfo.";
return d_smtEngine->getInfo(flag).toString();
@@ -5415,7 +5428,7 @@ void Solver::resetAssertions(void) const
void Solver::setInfo(const std::string& keyword, const std::string& value) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4_API_ARG_CHECK_EXPECTED(
+ CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(
keyword == "source" || keyword == "category" || keyword == "difficulty"
|| keyword == "filename" || keyword == "license" || keyword == "name"
|| keyword == "notes" || keyword == "smt-lib-version"
@@ -5423,10 +5436,10 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const
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)
+ CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(
+ keyword != "smt-lib-version" || value == "2" || value == "2.0"
+ || value == "2.5" || value == "2.6",
+ value)
<< "'2.0', '2.5', '2.6'";
CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat"
|| value == "unsat" || value == "unknown",
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 673c5ddd9..ab2c8a218 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -209,7 +209,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
"--tear-down-incremental doesn't work in interactive mode");
}
if(!opts.wasSetByUserIncrementalSolving()) {
- cmd.reset(new SetOptionCommand("incremental", SExpr(true)));
+ cmd.reset(new SetOptionCommand("incremental", "true"));
cmd->setMuted(true);
pExecutor->doCommand(cmd);
}
@@ -246,7 +246,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
// For tear-down-incremental values greater than 1, need incremental
// on too.
- cmd.reset(new SetOptionCommand("incremental", SExpr(true)));
+ cmd.reset(new SetOptionCommand("incremental", "true"));
cmd->setMuted(true);
pExecutor->doCommand(cmd);
// if(opts.wasSetByUserIncrementalSolving()) {
@@ -410,7 +410,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
}
} else {
if(!opts.wasSetByUserIncrementalSolving()) {
- cmd.reset(new SetOptionCommand("incremental", SExpr(false)));
+ cmd.reset(new SetOptionCommand("incremental", "false"));
cmd->setMuted(true);
pExecutor->doCommand(cmd);
}
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 91c7d0ded..30edf86cd 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -686,7 +686,7 @@ options { backtrack = true; }
mainCommand[std::unique_ptr<CVC4::Command>* cmd]
@init {
api::Term f;
- SExpr sexpr;
+ api::Term sexpr;
std::string id;
api::Sort t;
std::vector<CVC4::api::DatatypeDecl> dts;
@@ -715,14 +715,14 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
( symbolicExpr[sexpr]
{ if(s == "logic") {
- cmd->reset(new SetBenchmarkLogicCommand(sexpr.getValue()));
+ cmd->reset(new SetBenchmarkLogicCommand(sexprToString(sexpr)));
} else {
- cmd->reset(new SetOptionCommand(s, sexpr));
+ cmd->reset(new SetOptionCommand(s, sexprToString(sexpr)));
}
}
- | TRUE_TOK { cmd->reset(new SetOptionCommand(s, SExpr("true"))); }
- | FALSE_TOK { cmd->reset(new SetOptionCommand(s, SExpr("false"))); }
- | { cmd->reset(new SetOptionCommand(s, SExpr("true"))); }
+ | TRUE_TOK { cmd->reset(new SetOptionCommand(s, "true")); }
+ | FALSE_TOK { cmd->reset(new SetOptionCommand(s, "false")); }
+ | { cmd->reset(new SetOptionCommand(s, "true")); }
)
/* push / pop */
@@ -832,8 +832,8 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
{ UNSUPPORTED("CALL command"); }
| ECHO_TOK
- ( simpleSymbolicExpr[sexpr]
- { cmd->reset(new EchoCommand(sexpr.getValue())); }
+ ( simpleSymbolicExpr[s]
+ { cmd->reset(new EchoCommand(s)); }
| { cmd->reset(new EchoCommand()); }
)
@@ -939,34 +939,31 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
| toplevelDeclaration[cmd]
;
-simpleSymbolicExpr[CVC4::SExpr& sexpr]
-@declarations {
- std::string s;
- CVC4::Rational r;
-}
+simpleSymbolicExpr[std::string& s]
: INTEGER_LITERAL
- { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
+ { s = AntlrInput::tokenText($INTEGER_LITERAL); }
| MINUS_TOK INTEGER_LITERAL
- { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
+ { s = std::to_string(MINUS_TOK) + AntlrInput::tokenText($INTEGER_LITERAL); }
| DECIMAL_LITERAL
- { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
+ { s = AntlrInput::tokenText($DECIMAL_LITERAL); }
| HEX_LITERAL
- { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); }
+ { s = AntlrInput::tokenText($HEX_LITERAL); }
| BINARY_LITERAL
- { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); }
+ { s = AntlrInput::tokenText($BINARY_LITERAL); }
| str[s]
- { sexpr = SExpr(s); }
| IDENTIFIER
- { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); }
+ { s = AntlrInput::tokenText($IDENTIFIER); }
;
-symbolicExpr[CVC4::SExpr& sexpr]
+symbolicExpr[CVC4::api::Term& sexpr]
@declarations {
- std::vector<SExpr> children;
+ std::string s;
+ std::vector<api::Term> children;
}
- : simpleSymbolicExpr[sexpr]
+ : simpleSymbolicExpr[s]
+ { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); }
| LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN
- { sexpr = SExpr(children); }
+ { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); }
;
/**
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 96a16b31f..686a0d147 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -803,7 +803,6 @@ public:
*/
api::Term mkStringConstant(const std::string& s);
- private:
/** ad-hoc string escaping
*
* Returns the (internal) vector of code points corresponding to processing
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 88035dba4..6eb3d8061 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -722,29 +722,27 @@ sygusGrammar[CVC4::api::Grammar*& ret,
setInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
@declarations {
std::string name;
- SExpr sexpr;
+ api::Term sexpr;
}
: KEYWORD symbolicExpr[sexpr]
{ name = AntlrInput::tokenText($KEYWORD);
- PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
- cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr));
+ cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr)));
}
;
setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
@init {
std::string name;
- SExpr sexpr;
+ api::Term sexpr;
}
: keyword[name] symbolicExpr[sexpr]
- { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
- cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr));
+ { cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr)));
// Ugly that this changes the state of the parser; but
// global-declarations affects parsing, so we can't hold off
// on this until some SmtEngine eventually (if ever) executes it.
if(name == ":global-declarations")
{
- SYM_MAN->setGlobalDeclarations(sexpr.getValue() == "true");
+ SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true");
}
}
;
@@ -755,7 +753,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
std::string fname;
CVC4::api::Term expr, expr2;
std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
- SExpr sexpr;
+ std::string s;
CVC4::api::Sort t;
CVC4::api::Term func;
std::vector<CVC4::api::Term> bvs;
@@ -786,8 +784,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
/* echo */
| ECHO_TOK
- ( simpleSymbolicExpr[sexpr]
- { cmd->reset(new EchoCommand(sexpr.toString())); }
+ ( simpleSymbolicExpr[s]
+ { cmd->reset(new EchoCommand(s)); }
| { cmd->reset(new EchoCommand()); }
)
@@ -1246,30 +1244,17 @@ datatypesDef[bool isCo,
}
;
-simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
-@declarations {
- CVC4::Kind k;
- std::string s;
- std::vector<unsigned int> s_vec;
-}
+simpleSymbolicExprNoKeyword[std::string& s]
: INTEGER_LITERAL
- { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
+ { s = AntlrInput::tokenText($INTEGER_LITERAL); }
| DECIMAL_LITERAL
- { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
+ { s = AntlrInput::tokenText($DECIMAL_LITERAL); }
| HEX_LITERAL
- { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
- std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
- sexpr = SExpr(Integer(hexString, 16));
- }
+ { s = AntlrInput::tokenText($HEX_LITERAL); }
| BINARY_LITERAL
- { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
- std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
- sexpr = SExpr(Integer(binString, 2));
- }
+ { s = AntlrInput::tokenText($BINARY_LITERAL); }
| str[s,false]
- { sexpr = SExpr(s); }
| symbol[s,CHECK_NONE,SYM_SORT]
- { sexpr = SExpr(SExpr::Keyword(s)); }
| tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
| DECLARE_SORT_TOK
| DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
@@ -1279,7 +1264,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
| RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
| GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
| DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK)
- { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
+ { s = AntlrInput::tokenText($tok); }
;
keyword[std::string& s]
@@ -1287,20 +1272,21 @@ keyword[std::string& s]
{ s = AntlrInput::tokenText($KEYWORD); }
;
-simpleSymbolicExpr[CVC4::SExpr& sexpr]
- : simpleSymbolicExprNoKeyword[sexpr]
- | KEYWORD
- { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
+simpleSymbolicExpr[std::string& s]
+ : simpleSymbolicExprNoKeyword[s]
+ | KEYWORD { s = AntlrInput::tokenText($KEYWORD); }
;
-symbolicExpr[CVC4::SExpr& sexpr]
+symbolicExpr[CVC4::api::Term& sexpr]
@declarations {
- std::vector<SExpr> children;
+ std::string s;
+ std::vector<api::Term> children;
}
- : simpleSymbolicExpr[sexpr]
+ : simpleSymbolicExpr[s]
+ { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); }
| LPAREN_TOK
( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
- { sexpr = SExpr(children); }
+ { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); }
;
/**
@@ -1781,13 +1767,14 @@ termAtomic[CVC4::api::Term& atomTerm]
*/
attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
@init {
- SExpr sexpr;
+ api::Term sexpr;
+ std::string s;
CVC4::api::Term patexpr;
std::vector<CVC4::api::Term> patexprs;
CVC4::api::Term e2;
bool hasValue = false;
}
- : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
+ : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )?
{
attr = AntlrInput::tokenText($KEYWORD);
PARSER_STATE->attributeNotSupported(attr);
@@ -1824,7 +1811,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
| tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr]
{
api::Sort boolType = SOLVER->getBooleanSort();
- api::Term avar = SOLVER->mkConst(boolType, sexpr.toString());
+ api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr));
attr = std::string(":qid");
retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
Command* c = new SetUserAttributeCommand("qid", avar);
@@ -1835,7 +1822,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
{
attr = std::string(":named");
// notify that expression was given a name
- PARSER_STATE->notifyNamedExpression(expr, sexpr.getValue());
+ PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr));
}
;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b9279fcb0..17f5661b4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -750,14 +750,6 @@ bool Smt2::sygus_v2() const
return getLanguage() == language::input::LANG_SYGUS_V2;
}
-void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
- // TODO: ???
-}
-
-void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
- // TODO: ???
-}
-
void Smt2::checkThatLogicIsSet()
{
if (!logicIsSet())
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index fd08ab241..654ff9fbf 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -261,10 +261,6 @@ class Smt2 : public Parser
*/
bool escapeDupDblQuote() const { return v2_5() || sygus(); }
- void setInfo(const std::string& flag, const SExpr& sexpr);
-
- void setOption(const std::string& flag, const SExpr& sexpr);
-
void checkThatLogicIsSet();
/**
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 447a867c8..6b66b5422 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -259,7 +259,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
if(filename.substr(filename.length() - 2) == ".p") {
filename = filename.substr(0, filename.length() - 2);
}
- seq->addCommand(new SetInfoCommand("filename", SExpr(filename)));
+ seq->addCommand(new SetInfoCommand("filename", filename));
if(PARSER_STATE->hasConjecture()) {
seq->addCommand(new QueryCommand(SOLVER->mkFalse()));
} else {
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 432910cd3..14b9ed0aa 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -45,6 +45,43 @@ using namespace std;
namespace CVC4 {
+std::string sexprToString(api::Term sexpr)
+{
+ // if sexpr is a spec constant and not a string, return the result of calling
+ // Term::toString
+ if (sexpr.getKind() == api::CONST_BOOLEAN
+ || sexpr.getKind() == api::CONST_FLOATINGPOINT
+ || sexpr.getKind() == api::CONST_RATIONAL)
+ {
+ return sexpr.toString();
+ }
+
+ // if sexpr is a constant string, return the result of calling Term::toString.
+ // However, strip the surrounding quotes
+ if (sexpr.getKind() == api::CONST_STRING)
+ {
+ return sexpr.toString().substr(1, sexpr.toString().length() - 2);
+ }
+
+ // if sexpr is not a spec constant, make sure it is an array of sub-sexprs
+ Assert(sexpr.getKind() == api::SEXPR);
+
+ std::stringstream ss;
+ auto it = sexpr.begin();
+
+ // recursively print the sub-sexprs
+ ss << '(' << sexprToString(*it);
+ ++it;
+ while (it != sexpr.end())
+ {
+ ss << ' ' << sexprToString(*it);
+ ++it;
+ }
+ ss << ')';
+
+ return ss.str();
+}
+
const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
const CommandInterrupted* CommandInterrupted::s_instance =
@@ -137,11 +174,6 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
-Command::Command(const api::Solver* solver)
- : d_commandStatus(nullptr), d_muted(false)
-{
-}
-
Command::Command(const Command& cmd)
{
d_commandStatus =
@@ -1811,7 +1843,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm)
solver->blockModelValues(d_terms);
d_commandStatus = CommandSuccess::instance();
}
- catch (RecoverableModalException& e)
+ catch (api::CVC4ApiRecoverableException& e)
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
@@ -2520,21 +2552,21 @@ void SetBenchmarkLogicCommand::toStream(std::ostream& out,
/* class SetInfoCommand */
/* -------------------------------------------------------------------------- */
-SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
+SetInfoCommand::SetInfoCommand(std::string flag, const std::string& sexpr)
: d_flag(flag), d_sexpr(sexpr)
{
}
std::string SetInfoCommand::getFlag() const { return d_flag; }
-SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
+const std::string& SetInfoCommand::getSExpr() const { return d_sexpr; }
void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
- solver->getSmtEngine()->setInfo(d_flag, d_sexpr);
+ solver->setInfo(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
}
- catch (UnrecognizedOptionException&)
+ catch (api::CVC4ApiRecoverableException&)
{
// As per SMT-LIB spec, silently accept unknown set-info keys
d_commandStatus = CommandSuccess::instance();
@@ -2570,23 +2602,13 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
- vector<SExpr> v;
- v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
- v.emplace_back(solver->getSmtEngine()->getInfo(d_flag));
- stringstream ss;
- if (d_flag == "all-options" || d_flag == "all-statistics")
- {
- ss << PrettySExprs(true);
- }
- ss << SExpr(v);
- d_result = ss.str();
+ std::vector<api::Term> v;
+ v.push_back(solver->mkString(":" + d_flag));
+ v.push_back(solver->mkString(solver->getInfo(d_flag)));
+ d_result = sexprToString(solver->mkTerm(api::SEXPR, v));
d_commandStatus = CommandSuccess::instance();
}
- catch (UnrecognizedOptionException&)
- {
- d_commandStatus = new CommandUnsupported();
- }
- catch (RecoverableModalException& e)
+ catch (api::CVC4ApiRecoverableException& e)
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
@@ -2630,21 +2652,21 @@ void GetInfoCommand::toStream(std::ostream& out,
/* class SetOptionCommand */
/* -------------------------------------------------------------------------- */
-SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
+SetOptionCommand::SetOptionCommand(std::string flag, const std::string& sexpr)
: d_flag(flag), d_sexpr(sexpr)
{
}
std::string SetOptionCommand::getFlag() const { return d_flag; }
-SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
+const std::string& SetOptionCommand::getSExpr() const { return d_sexpr; }
void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
- solver->getSmtEngine()->setOption(d_flag, d_sexpr);
+ solver->setOption(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
}
- catch (UnrecognizedOptionException&)
+ catch (api::CVC4ApiRecoverableException&)
{
d_commandStatus = new CommandUnsupported();
}
@@ -2682,7 +2704,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
d_result = solver->getOption(d_flag);
d_commandStatus = CommandSuccess::instance();
}
- catch (UnrecognizedOptionException&)
+ catch (api::CVC4ApiRecoverableException&)
{
d_commandStatus = new CommandUnsupported();
}
diff --git a/src/smt/command.h b/src/smt/command.h
index b9c1b7d73..bfe5e737a 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -49,6 +49,16 @@ namespace smt {
class Model;
}
+/**
+ * Convert a symbolic expression to string. This method differs from
+ * Term::toString in that it does not surround constant strings with double
+ * quote symbols.
+ *
+ * @param sexpr the symbolic expression to convert
+ * @return the symbolic expression as string
+ */
+std::string sexprToString(api::Term sexpr);
+
std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_PUBLIC;
@@ -196,7 +206,6 @@ class CVC4_PUBLIC Command
typedef CommandPrintSuccess printsuccess;
Command();
- Command(const api::Solver* solver);
Command(const Command& cmd);
virtual ~Command();
@@ -1283,13 +1292,13 @@ class CVC4_PUBLIC SetInfoCommand : public Command
{
protected:
std::string d_flag;
- SExpr d_sexpr;
+ std::string d_sexpr;
public:
- SetInfoCommand(std::string flag, const SExpr& sexpr);
+ SetInfoCommand(std::string flag, const std::string& sexpr);
std::string getFlag() const;
- SExpr getSExpr() const;
+ const std::string& getSExpr() const;
void invoke(api::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
@@ -1328,13 +1337,13 @@ class CVC4_PUBLIC SetOptionCommand : public Command
{
protected:
std::string d_flag;
- SExpr d_sexpr;
+ std::string d_sexpr;
public:
- SetOptionCommand(std::string flag, const SExpr& sexpr);
+ SetOptionCommand(std::string flag, const std::string& sexpr);
std::string getFlag() const;
- SExpr getSExpr() const;
+ const std::string& getSExpr() const;
void invoke(api::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0f40db530..722f6a080 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -468,11 +468,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
value.getValue() == "2.6" ) {
ilang = language::input::LANG_SMTLIB_V2_6;
}
- else
- {
- Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
- throw UnrecognizedOptionException();
- }
options::inputLanguage.set(ilang);
// also update the output language
if (!options::outputLanguage.wasSetByUser())
@@ -497,7 +492,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
d_state->notifyExpectedStatus(s);
return;
}
- throw UnrecognizedOptionException();
}
bool SmtEngine::isValidGetInfoFlag(const std::string& key) const
@@ -517,10 +511,6 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
SmtScope smts(this);
Trace("smt") << "SMT getInfo(" << key << ")" << endl;
- if (!isValidGetInfoFlag(key))
- {
- throw UnrecognizedOptionException();
- }
if (key == "all-statistics")
{
vector<SExpr> stats;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback