summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp10
-rw-r--r--src/api/cvc4cpp.h2
-rw-r--r--src/main/command_executor.cpp46
-rw-r--r--src/main/command_executor.h6
-rw-r--r--src/main/driver_unified.cpp4
-rw-r--r--src/main/interactive_shell.cpp56
-rw-r--r--src/parser/cvc/Cvc.g24
-rw-r--r--src/parser/smt2/Smt2.g111
-rw-r--r--src/parser/smt2/smt2.cpp11
-rw-r--r--src/parser/tptp/Tptp.g24
-rw-r--r--src/parser/tptp/tptp.cpp19
-rw-r--r--src/smt/command.cpp1066
-rw-r--r--src/smt/command.h495
-rw-r--r--src/smt/smt_engine.h2
-rw-r--r--test/api/smt2_compliance.cpp2
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress0/smtlib/get-unsat-assumptions.smt21
17 files changed, 660 insertions, 1222 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 401f62cae..125e33ba5 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -5708,6 +5708,16 @@ std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts)
return types;
}
+std::vector<TypeNode> sortVectorToTypeNodes(const std::vector<Sort>& sorts)
+{
+ std::vector<TypeNode> typeNodes;
+ for (const Sort& sort : sorts)
+ {
+ typeNodes.push_back(TypeNode::fromType(sort.getType()));
+ }
+ return typeNodes;
+}
+
std::set<Type> sortSetToTypes(const std::set<Sort>& sorts)
{
std::set<Type> types;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index c66113f31..841a8ee8a 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -50,6 +50,7 @@ class NodeManager;
class SmtEngine;
class SynthFunCommand;
class Type;
+class TypeNode;
class Options;
class Random;
class Result;
@@ -3413,6 +3414,7 @@ class CVC4_PUBLIC Solver
std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
std::vector<Node> termVectorToNodes(const std::vector<Term>& terms);
std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts);
+std::vector<TypeNode> sortVectorToTypeNodes(const std::vector<Sort>& sorts);
std::set<Type> sortSetToTypes(const std::set<Sort>& sorts);
std::vector<Term> exprVectorToTerms(const Solver* slv,
const std::vector<Expr>& terms);
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index caae54e7a..c91b0455c 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -118,12 +118,12 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
{
bool status = true;
if(d_options.getVerbosity() >= -1) {
- status = smtEngineInvoke(d_smtEngine, cmd, d_options.getOut());
+ status = solverInvoke(d_solver.get(), cmd, d_options.getOut());
} else {
- status = smtEngineInvoke(d_smtEngine, cmd, nullptr);
+ status = solverInvoke(d_solver.get(), cmd, nullptr);
}
- Result res;
+ api::Result res;
const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
if(cs != nullptr) {
d_result = res = cs->getResult();
@@ -149,34 +149,34 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
if (status) {
std::vector<std::unique_ptr<Command> > getterCommands;
if (d_options.getDumpModels()
- && (res.asSatisfiabilityResult() == Result::SAT
- || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE)))
+ && (res.isSat()
+ || (res.isSatUnknown()
+ && res.getResult().whyUnknown() == Result::INCOMPLETE)))
{
getterCommands.emplace_back(new GetModelCommand());
}
- if (d_options.getDumpProofs()
- && res.asSatisfiabilityResult() == Result::UNSAT)
+ if (d_options.getDumpProofs() && res.isUnsat())
{
getterCommands.emplace_back(new GetProofCommand());
}
if (d_options.getDumpInstantiations()
&& ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
- && (res.asSatisfiabilityResult() == Result::SAT
- || (res.isUnknown()
- && res.whyUnknown() == Result::INCOMPLETE)))
- || res.asSatisfiabilityResult() == Result::UNSAT))
+ && (res.isSat()
+ || (res.isSatUnknown()
+ && res.getResult().whyUnknown() == Result::INCOMPLETE)))
+ || res.isUnsat()))
{
getterCommands.emplace_back(new GetInstantiationsCommand());
}
- if (d_options.getDumpSynth() &&
- res.asSatisfiabilityResult() == Result::UNSAT) {
+ if (d_options.getDumpSynth() && res.isUnsat())
+ {
getterCommands.emplace_back(new GetSynthSolutionCommand());
}
- if (d_options.getDumpUnsatCores() &&
- res.asSatisfiabilityResult() == Result::UNSAT) {
+ if (d_options.getDumpUnsatCores() && res.isUnsat())
+ {
getterCommands.emplace_back(new GetUnsatCoreCommand());
}
@@ -197,17 +197,21 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
return status;
}
-bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
+bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out)
{
- if(out == NULL) {
- cmd->invoke(smt);
- } else {
- cmd->invoke(smt, *out);
+ if (out == NULL)
+ {
+ cmd->invoke(solver);
+ }
+ else
+ {
+ cmd->invoke(solver, *out);
}
// ignore the error if the command-verbosity is 0 for this command
std::string commandName =
std::string("command-verbosity:") + cmd->getCommandName();
- if(smt->getOption(commandName).getIntegerValue() == 0) {
+ if (solver->getOption(commandName) == "0")
+ {
return true;
}
return !cmd->fail();
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 92b0cd166..d7899020e 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -44,7 +44,7 @@ class CommandExecutor
SmtEngine* d_smtEngine;
Options& d_options;
StatisticsRegistry d_stats;
- Result d_result;
+ api::Result d_result;
public:
CommandExecutor(Options& options);
@@ -67,7 +67,7 @@ class CommandExecutor
/** Get a pointer to the solver object owned by this CommandExecutor. */
api::Solver* getSolver() { return d_solver.get(); }
- Result getResult() const { return d_result; }
+ api::Result getResult() const { return d_result; }
void reset();
StatisticsRegistry& getStatisticsRegistry() {
@@ -101,7 +101,7 @@ private:
}; /* class CommandExecutor */
-bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out);
+bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out);
}/* CVC4::main namespace */
}/* CVC4 namespace */
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 43529278b..9fff51b93 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -450,7 +450,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
}
}
- Result result;
+ api::Result result;
if(status) {
result = pExecutor->getResult();
returnValue = 0;
@@ -467,7 +467,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
_exit(returnValue);
#endif /* CVC4_COMPETITION_MODE */
- ReferenceStat< Result > s_statSatResult("sat/unsat", result);
+ ReferenceStat<api::Result> s_statSatResult("sat/unsat", result);
RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(),
&s_statSatResult);
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 121513856..b798d03ee 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -309,34 +309,56 @@ restart:
CommandSequence *cmd_seq = new CommandSequence();
Command *cmd;
- try {
- while( (cmd = d_parser->nextCommand()) ) {
+ try
+ {
+ while ((cmd = d_parser->nextCommand()))
+ {
cmd_seq->addCommand(cmd);
- if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+ if (dynamic_cast<QuitCommand*>(cmd) != NULL)
+ {
d_quit = true;
break;
- } else {
+ }
+ else
+ {
#if HAVE_LIBEDITLINE
- if(dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) {
- s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
- } else if(dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) {
- s_declarations.insert(dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
- } else if(dynamic_cast<DeclareTypeCommand*>(cmd) != NULL) {
- s_declarations.insert(dynamic_cast<DeclareTypeCommand*>(cmd)->getSymbol());
- } else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) {
- s_declarations.insert(dynamic_cast<DefineTypeCommand*>(cmd)->getSymbol());
+ if (dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL)
+ {
+ s_declarations.insert(
+ dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
+ }
+ else if (dynamic_cast<DefineFunctionCommand*>(cmd) != NULL)
+ {
+ s_declarations.insert(
+ dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
+ }
+ else if (dynamic_cast<DeclareSortCommand*>(cmd) != NULL)
+ {
+ s_declarations.insert(
+ dynamic_cast<DeclareSortCommand*>(cmd)->getSymbol());
+ }
+ else if (dynamic_cast<DefineSortCommand*>(cmd) != NULL)
+ {
+ s_declarations.insert(
+ dynamic_cast<DefineSortCommand*>(cmd)->getSymbol());
}
#endif /* HAVE_LIBEDITLINE */
}
}
- } catch(ParserEndOfFileException& pe) {
+ }
+ catch (ParserEndOfFileException& pe)
+ {
line += "\n";
goto restart;
- } catch(ParserException& pe) {
+ }
+ catch (ParserException& pe)
+ {
if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
{
d_out << "(error \"" << pe << "\")" << endl;
- } else {
+ }
+ else
+ {
d_out << pe << endl;
}
// We can't really clear out the sequence and abort the current line,
@@ -350,8 +372,8 @@ restart:
// FIXME: does that mean e.g. that a pushed LET scope might not yet have
// been popped?!
//
- //delete cmd_seq;
- //cmd_seq = new CommandSequence();
+ // delete cmd_seq;
+ // cmd_seq = new CommandSequence();
}
return cmd_seq;
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index d1aaa3d15..5f959c660 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -704,13 +704,12 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
bool formCommaFlag = true;
}
/* our bread & butter */
- : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f.getExpr())); }
+ : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f)); }
- | QUERY_TOK formula[f] { cmd->reset(new QueryCommand(f.getExpr())); }
+ | QUERY_TOK formula[f] { cmd->reset(new QueryCommand(f)); }
| CHECKSAT_TOK formula[f]?
{
- cmd->reset(f.isNull() ? new CheckSatCommand()
- : new CheckSatCommand(f.getExpr()));
+ cmd->reset(f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f));
}
/* options */
| OPTION_TOK
@@ -764,7 +763,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
END_TOK
{ PARSER_STATE->popScope();
cmd->reset(new DatatypeDeclarationCommand(
- api::sortVectorToTypes(PARSER_STATE->bindMutualDatatypeTypes(dts))));
+ PARSER_STATE->bindMutualDatatypeTypes(dts)));
}
| CONTEXT_TOK
@@ -789,7 +788,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
{ UNSUPPORTED("GET_OP command"); }
| GET_VALUE_TOK formula[f]
- { cmd->reset(new GetValueCommand(f.getExpr())); }
+ { cmd->reset(new GetValueCommand(f)); }
| SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON
type[t,CHECK_DECLARED] EQUAL_TOK formula[f] LBRACKET
@@ -823,7 +822,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
)
| TRANSFORM_TOK formula[f]
- { cmd->reset(new SimplifyCommand(f.getExpr())); }
+ { cmd->reset(new SimplifyCommand(f)); }
| PRINT_TOK formula[f]
{ UNSUPPORTED("PRINT command"); }
@@ -936,8 +935,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
PARSER_STATE->parseError("Type mismatch in definition");
}
}
- cmd->reset(
- new DefineFunctionRecCommand(SOLVER, funcs, formals, formulas, true));
+ cmd->reset(new DefineFunctionRecCommand(funcs, formals, formulas, true));
}
| toplevelDeclaration[cmd]
;
@@ -1059,7 +1057,7 @@ declareTypes[std::unique_ptr<CVC4::Command>* cmd,
// behavior here.
PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT);
api::Sort sort = PARSER_STATE->mkSort(*i);
- Command* decl = new DeclareTypeCommand(*i, 0, sort.getType());
+ Command* decl = new DeclareSortCommand(*i, 0, sort);
seq->addCommand(decl);
}
cmd->reset(seq.release());
@@ -1125,8 +1123,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
if(topLevel) {
api::Term func =
PARSER_STATE->bindVar(*i, t, ExprManager::VAR_FLAG_GLOBAL);
- Command* decl =
- new DeclareFunctionCommand(*i, func.getExpr(), t.getType());
+ Command* decl = new DeclareFunctionCommand(*i, func, t);
seq->addCommand(decl);
} else {
PARSER_STATE->bindBoundVar(*i, t);
@@ -1156,8 +1153,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
api::Sort(SOLVER, t.getType()),
ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
PARSER_STATE->defineVar(*i, f);
- Command* decl =
- new DefineFunctionCommand(*i, func.getExpr(), f.getExpr(), true);
+ Command* decl = new DefineFunctionCommand(*i, func, f, true);
seq->addCommand(decl);
}
}
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 65f72eb28..232723fc0 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -263,10 +263,10 @@ command [std::unique_ptr<CVC4::Command>* cmd]
unsigned arity = AntlrInput::tokenToUnsigned(n);
if(arity == 0) {
api::Sort type = PARSER_STATE->mkSort(name);
- cmd->reset(new DeclareTypeCommand(name, 0, type.getType()));
+ cmd->reset(new DeclareSortCommand(name, 0, type));
} else {
api::Sort type = PARSER_STATE->mkSortConstructor(name, arity);
- cmd->reset(new DeclareTypeCommand(name, arity, type.getType()));
+ cmd->reset(new DeclareSortCommand(name, arity, type));
}
}
| /* sort definition */
@@ -287,8 +287,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
// Do NOT call mkSort, since that creates a new sort!
// This name is not its own distinct sort, it's an alias.
PARSER_STATE->defineParameterizedType(name, sorts, t);
- cmd->reset(new DefineTypeCommand(
- name, api::sortVectorToTypes(sorts), t.getType()));
+ cmd->reset(new DefineSortCommand(name, sorts, t));
}
| /* function declaration */
DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -314,8 +313,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
{
api::Term func =
PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
- cmd->reset(
- new DeclareFunctionCommand(name, func.getExpr(), t.getType()));
+ cmd->reset(new DeclareFunctionCommand(name, func, t));
}
}
| /* function definition */
@@ -334,8 +332,9 @@ command [std::unique_ptr<CVC4::Command>* cmd]
++i) {
sorts.push_back((*i).second);
}
- t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
}
+
+ t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
PARSER_STATE->pushScope(true);
terms = PARSER_STATE->bindBoundVars(sortedVarNames);
}
@@ -354,19 +353,15 @@ command [std::unique_ptr<CVC4::Command>* cmd]
// we allow overloading for function definitions
api::Term func = PARSER_STATE->bindVar(name, t,
ExprManager::VAR_FLAG_DEFINED, true);
- cmd->reset(
- new DefineFunctionCommand(name,
- func.getExpr(),
- api::termVectorToExprs(terms),
- expr.getExpr(),
- PARSER_STATE->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionCommand(
+ name, func, terms, expr, PARSER_STATE->getGlobalDeclarations()));
}
| DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
| DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
| /* value query */
GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( LPAREN_TOK termList[terms,expr] RPAREN_TOK
- { cmd->reset(new GetValueCommand(api::termVectorToExprs(terms))); }
+ { cmd->reset(new GetValueCommand(terms)); }
| ~LPAREN_TOK
{ PARSER_STATE->parseError("The get-value command expects a list of "
"terms. Perhaps you forgot a pair of "
@@ -381,13 +376,13 @@ command [std::unique_ptr<CVC4::Command>* cmd]
{ PARSER_STATE->clearLastNamedTerm(); }
term[expr, expr2]
{ bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
- cmd->reset(new AssertCommand(expr.getExpr(), inUnsatCore));
+ cmd->reset(new AssertCommand(expr, inUnsatCore));
if(inUnsatCore) {
// set the expression name, if there was a named term
std::pair<api::Term, std::string> namedTerm =
PARSER_STATE->lastNamedTerm();
- Command* csen = new SetExpressionNameCommand(namedTerm.first.getExpr(),
- namedTerm.second);
+ Command* csen =
+ new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
csen->setMuted(true);
PARSER_STATE->preemptCommand(csen);
}
@@ -407,12 +402,12 @@ command [std::unique_ptr<CVC4::Command>* cmd]
}
| { expr = api::Term(); }
)
- { cmd->reset(new CheckSatCommand(expr.getExpr())); }
+ { cmd->reset(new CheckSatCommand(expr)); }
| /* check-sat-assuming */
CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( LPAREN_TOK termList[terms,expr] RPAREN_TOK
{
- cmd->reset(new CheckSatAssumingCommand(api::termVectorToExprs(terms)));
+ cmd->reset(new CheckSatAssumingCommand(terms));
}
| ~LPAREN_TOK
{ PARSER_STATE->parseError("The check-sat-assuming command expects a "
@@ -558,7 +553,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
sortSymbol[t,CHECK_DECLARED]
{
api::Term var = PARSER_STATE->bindBoundVar(name, t);
- cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType()));
+ cmd.reset(new DeclareSygusVarCommand(name, var, t));
}
| /* synth-fun */
( SYNTH_FUN_TOK { isInv = false; }
@@ -590,7 +585,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
}
term[expr, expr2]
{ Debug("parser-sygus") << "...read constraint " << expr << std::endl;
- cmd.reset(new SygusConstraintCommand(expr.getExpr()));
+ cmd.reset(new SygusConstraintCommand(expr));
}
| /* inv-constraint */
INV_CONSTRAINT_TOK
@@ -788,7 +783,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
{ // allow overloading here
api::Term c =
PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
- cmd->reset(new DeclareFunctionCommand(name, c.getExpr(), t.getType())); }
+ cmd->reset(new DeclareFunctionCommand(name, c, t)); }
/* get model */
| GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -831,7 +826,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
expr = PARSER_STATE->mkHoApply( expr, flattenVars );
}
cmd->reset(new DefineFunctionRecCommand(
- SOLVER, func, bvs, expr, PARSER_STATE->getGlobalDeclarations()));
+ func, bvs, expr, PARSER_STATE->getGlobalDeclarations()));
}
| DEFINE_FUNS_REC_TOK
{ PARSER_STATE->checkThatLogicIsSet();}
@@ -894,12 +889,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
"Number of functions defined does not match number listed in "
"define-funs-rec"));
}
- cmd->reset(
- new DefineFunctionRecCommand(SOLVER,
- funcs,
- formals,
- func_defs,
- PARSER_STATE->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionRecCommand(
+ funcs, formals, func_defs, PARSER_STATE->getGlobalDeclarations()));
}
;
@@ -935,7 +926,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
{ PARSER_STATE->checkUserSymbol(name);
api::Sort type = PARSER_STATE->mkSort(name);
- seq->addCommand(new DeclareTypeCommand(name, 0, type.getType()));
+ seq->addCommand(new DeclareSortCommand(name, 0, type));
}
)+
RPAREN_TOK
@@ -960,8 +951,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
// allow overloading
api::Term func =
PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true);
- seq->addCommand(
- new DeclareFunctionCommand(name, func.getExpr(), tt.getType()));
+ seq->addCommand(new DeclareFunctionCommand(name, func, tt));
sorts.clear();
}
)+
@@ -981,8 +971,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
// allow overloading
api::Term func =
PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
- seq->addCommand(
- new DeclareFunctionCommand(name, func.getExpr(), t.getType()));
+ seq->addCommand(new DeclareFunctionCommand(name, func, t));
sorts.clear();
}
)+
@@ -997,11 +986,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
{
api::Term func = PARSER_STATE->bindVar(name, e.getSort(),
ExprManager::VAR_FLAG_DEFINED);
- cmd->reset(
- new DefineFunctionCommand(name,
- func.getExpr(),
- e.getExpr(),
- PARSER_STATE->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionCommand(
+ name, func, e, PARSER_STATE->getGlobalDeclarations()));
}
| // (define (f (v U) ...) t)
LPAREN_TOK
@@ -1031,12 +1017,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
}
api::Term func = PARSER_STATE->bindVar(name, tt,
ExprManager::VAR_FLAG_DEFINED);
- cmd->reset(
- new DefineFunctionCommand(name,
- func.getExpr(),
- api::termVectorToExprs(terms),
- e.getExpr(),
- PARSER_STATE->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionCommand(
+ name, func, terms, e, PARSER_STATE->getGlobalDeclarations()));
}
)
| // (define-const x U t)
@@ -1057,23 +1039,19 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
// permitted)
api::Term func = PARSER_STATE->bindVar(name, t,
ExprManager::VAR_FLAG_DEFINED);
- cmd->reset(
- new DefineFunctionCommand(name,
- func.getExpr(),
- api::termVectorToExprs(terms),
- e.getExpr(),
- PARSER_STATE->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionCommand(
+ name, func, terms, e, PARSER_STATE->getGlobalDeclarations()));
}
| SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[e,e2]
- { cmd->reset(new SimplifyCommand(e.getExpr())); }
+ { cmd->reset(new SimplifyCommand(e)); }
| GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[e,e2]
- { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), true)); }
+ { cmd->reset(new GetQuantifierEliminationCommand(e, true)); }
| GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[e,e2]
- { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), false)); }
+ { cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
| GET_ABDUCT_TOK {
PARSER_STATE->checkThatLogicIsSet();
}
@@ -1083,7 +1061,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
sygusGrammar[g, terms, name]
)?
{
- cmd->reset(new GetAbductCommand(SOLVER, name, e, g));
+ cmd->reset(new GetAbductCommand(name, e, g));
}
| GET_INTERPOL_TOK {
PARSER_STATE->checkThatLogicIsSet();
@@ -1094,7 +1072,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
sygusGrammar[g, terms, name]
)?
{
- cmd->reset(new GetInterpolCommand(SOLVER, name, e, g));
+ cmd->reset(new GetInterpolCommand(name, e, g));
}
| DECLARE_HEAP LPAREN_TOK
sortSymbol[t, CHECK_DECLARED]
@@ -1107,7 +1085,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
| BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( LPAREN_TOK termList[terms,e] RPAREN_TOK
- { cmd->reset(new BlockModelValuesCommand(api::termVectorToExprs(terms))); }
+ { cmd->reset(new BlockModelValuesCommand(terms)); }
| ~LPAREN_TOK
{ PARSER_STATE->parseError("The block-model-value command expects a list "
"of terms. Perhaps you forgot a pair of "
@@ -1138,8 +1116,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
{ PARSER_STATE->popScope();
cmd->reset(new DatatypeDeclarationCommand(
- api::sortVectorToTypes(
- PARSER_STATE->bindMutualDatatypeTypes(dts, true))));
+ PARSER_STATE->bindMutualDatatypeTypes(dts, true)));
}
;
@@ -1271,8 +1248,7 @@ datatypesDef[bool isCo,
}
PARSER_STATE->popScope();
cmd->reset(new DatatypeDeclarationCommand(
- api::sortVectorToTypes(
- PARSER_STATE->bindMutualDatatypeTypes(dts, true))));
+ PARSER_STATE->bindMutualDatatypeTypes(dts, true)));
}
;
@@ -1847,8 +1823,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
api::Sort boolType = SOLVER->getBooleanSort();
api::Term avar = PARSER_STATE->bindVar(attr_name, boolType);
retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
- Command* c = new SetUserAttributeCommand(
- attr_name, avar.getExpr(), api::termVectorToExprs(values));
+ Command* c = new SetUserAttributeCommand(attr_name, avar, values);
c->setMuted(true);
PARSER_STATE->preemptCommand(c);
}
@@ -1858,7 +1833,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
api::Term avar = SOLVER->mkConst(boolType, sexpr.toString());
attr = std::string(":qid");
retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
- Command* c = new SetUserAttributeCommand("qid", avar.getExpr());
+ Command* c = new SetUserAttributeCommand("qid", avar);
c->setMuted(true);
PARSER_STATE->preemptCommand(c);
}
@@ -1868,8 +1843,12 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr);
std::string name = sexpr.getValue();
// bind name to expr with define-fun
- Command* c = new DefineNamedFunctionCommand(
- name, func.getExpr(), std::vector<Expr>(), expr.getExpr(), PARSER_STATE->getGlobalDeclarations());
+ Command* c =
+ new DefineNamedFunctionCommand(name,
+ func,
+ std::vector<api::Term>(),
+ expr,
+ PARSER_STATE->getGlobalDeclarations());
c->setMuted(true);
PARSER_STATE->preemptCommand(c);
}
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 387117335..e7bb8795c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -525,8 +525,8 @@ std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar)
{
Debug("parser-sygus") << "...read synth fun " << d_id << std::endl;
d_smt2->popScope();
- return std::unique_ptr<Command>(new SynthFunCommand(
- d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar));
+ return std::unique_ptr<Command>(
+ new SynthFunCommand(d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar));
}
std::unique_ptr<Command> Smt2::invConstraint(
@@ -556,8 +556,7 @@ std::unique_ptr<Command> Smt2::invConstraint(
terms.push_back(getVariable(name));
}
- return std::unique_ptr<Command>(
- new SygusInvConstraintCommand(api::termVectorToExprs(terms)));
+ return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms));
}
Command* Smt2::setLogic(std::string name, bool fromCommand)
@@ -776,8 +775,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
const std::vector<api::Term>& ntSymbols)
{
- d_allocGrammars.emplace_back(new api::Grammar(
- std::move(d_solver->mkSygusGrammar(boundVars, ntSymbols))));
+ d_allocGrammars.emplace_back(
+ new api::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols)));
return d_allocGrammars.back().get();
}
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 050a23320..b99376685 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -161,10 +161,10 @@ parseCommand returns [CVC4::Command* cmd = NULL]
}
(COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
{
- CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
+ CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr);
if( !aexpr.isNull() ){
// set the expression name (e.g. used with unsat core printing)
- Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
+ Command* csen = new SetExpressionNameCommand(aexpr, name);
csen->setMuted(true);
PARSER_STATE->preemptCommand(csen);
}
@@ -178,7 +178,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
if( !aexpr.isNull() ){
// set the expression name (e.g. used with unsat core printing)
- Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
+ Command* csen = new SetExpressionNameCommand(aexpr, name);
csen->setMuted(true);
PARSER_STATE->preemptCommand(csen);
}
@@ -194,7 +194,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
if( !aexpr.isNull() ){
// set the expression name (e.g. used with unsat core printing)
- Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
+ Command* csen = new SetExpressionNameCommand(aexpr, name);
csen->setMuted(true);
PARSER_STATE->preemptCommand(csen);
}
@@ -219,7 +219,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
if (!aexpr.isNull())
{
// set the expression name (e.g. used with unsat core printing)
- Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name);
+ Command* csen = new SetExpressionNameCommand(aexpr, name);
csen->setMuted(true);
PARSER_STATE->preemptCommand(csen);
}
@@ -255,7 +255,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
CVC4::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants();
if( !aexpr.isNull() )
{
- seq->addCommand(new AssertCommand(aexpr.getExpr(), false));
+ seq->addCommand(new AssertCommand(aexpr, false));
}
std::string filename = PARSER_STATE->getInput()->getInputStreamName();
@@ -268,7 +268,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
}
seq->addCommand(new SetInfoCommand("filename", SExpr(filename)));
if(PARSER_STATE->hasConjecture()) {
- seq->addCommand(new QueryCommand(SOLVER->mkFalse().getExpr()));
+ seq->addCommand(new QueryCommand(SOLVER->mkFalse()));
} else {
seq->addCommand(new CheckSatCommand());
}
@@ -967,7 +967,7 @@ thfAtomTyping[CVC4::Command*& cmd]
{
// as yet, it's undeclared
api::Sort atype = PARSER_STATE->mkSort(name);
- cmd = new DeclareTypeCommand(name, 0, atype.getType());
+ cmd = new DeclareSortCommand(name, 0, atype);
}
}
| parseThfType[type]
@@ -1007,8 +1007,7 @@ thfAtomTyping[CVC4::Command*& cmd]
{
freshExpr = PARSER_STATE->bindVar(name, type);
}
- cmd = new DeclareFunctionCommand(
- name, freshExpr.getExpr(), type.getType());
+ cmd = new DeclareFunctionCommand(name, freshExpr, type);
}
}
)
@@ -1320,7 +1319,7 @@ tffTypedAtom[CVC4::Command*& cmd]
} else {
// as yet, it's undeclared
api::Sort atype = PARSER_STATE->mkSort(name);
- cmd = new DeclareTypeCommand(name, 0, atype.getType());
+ cmd = new DeclareSortCommand(name, 0, atype);
}
}
| parseType[type]
@@ -1339,8 +1338,7 @@ tffTypedAtom[CVC4::Command*& cmd]
} else {
// as yet, it's undeclared
CVC4::api::Term aexpr = PARSER_STATE->bindVar(name, type);
- cmd =
- new DeclareFunctionCommand(name, aexpr.getExpr(), type.getType());
+ cmd = new DeclareFunctionCommand(name, aexpr, type);
}
}
)
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 8f75cf8d3..066970fe3 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -76,8 +76,7 @@ void Tptp::addTheory(Theory theory) {
{
std::string d_unsorted_name = "$$unsorted";
d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name);
- preemptCommand(
- new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted.getType()));
+ preemptCommand(new DeclareSortCommand(d_unsorted_name, 0, d_unsorted));
}
// propositionnal
defineType("Bool", d_solver->getBooleanSort());
@@ -243,8 +242,7 @@ api::Term Tptp::parseOpToExpr(ParseOp& p)
api::Sort t =
p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
expr = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
- preemptCommand(
- new DeclareFunctionCommand(p.d_name, expr.getExpr(), t.getType()));
+ preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
}
return expr;
}
@@ -288,8 +286,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
t = d_solver->mkFunctionSort(sorts, t);
v = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
- preemptCommand(
- new DeclareFunctionCommand(p.d_name, v.getExpr(), t.getType()));
+ preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
}
// args might be rationals, in which case we need to create
// distinct constants of the "unsorted" sort to represent them
@@ -394,13 +391,11 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr)
// Conversion from rational to unsorted
t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted);
d_rtu_op = d_solver->mkConst(t, "$$rtu");
- preemptCommand(
- new DeclareFunctionCommand("$$rtu", d_rtu_op.getExpr(), t.getType()));
+ preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
// Conversion from unsorted to rational
t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort());
d_utr_op = d_solver->mkConst(t, "$$utr");
- preemptCommand(
- new DeclareFunctionCommand("$$utr", d_utr_op.getExpr(), t.getType()));
+ preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
}
// Add the inverse in order to show that over the elements that
// appear in the problem there is a bijection between unsorted and
@@ -410,7 +405,7 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr)
d_r_converted.insert(expr);
api::Term eq = d_solver->mkTerm(
api::EQUAL, expr, d_solver->mkTerm(api::APPLY_UF, d_utr_op, ret));
- preemptCommand(new AssertCommand(eq.getExpr()));
+ preemptCommand(new AssertCommand(eq));
}
return api::Term(ret);
}
@@ -506,7 +501,7 @@ Command* Tptp::makeAssertCommand(FormulaRole fr,
if( expr.isNull() ){
return new EmptyCommand("Untreated role for expression");
}else{
- return new AssertCommand(expr.getExpr(), inUnsatCore);
+ return new AssertCommand(expr, inUnsatCore);
}
}
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 6d236aa47..84bc5fc99 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -105,20 +105,6 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
}
}
-// !!! Temporary until commands are migrated to the new API !!!
-std::vector<TypeNode> typeVectorToTypeNodes(const std::vector<Type>& types)
-{
- std::vector<TypeNode> typeNodes;
- typeNodes.reserve(types.size());
-
- for (Type t : types)
- {
- typeNodes.push_back(TypeNode::fromType(t));
- }
-
- return typeNodes;
-}
-
/* -------------------------------------------------------------------------- */
/* class CommandPrintSuccess */
/* -------------------------------------------------------------------------- */
@@ -151,7 +137,7 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
Command::Command(const api::Solver* solver)
- : d_solver(solver), d_commandStatus(nullptr), d_muted(false)
+ : d_commandStatus(nullptr), d_muted(false)
{
}
@@ -189,15 +175,14 @@ bool Command::interrupted() const
&& dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
}
-void Command::invoke(SmtEngine* smtEngine, std::ostream& out)
+void Command::invoke(api::Solver* solver, std::ostream& out)
{
- invoke(smtEngine);
+ invoke(solver);
if (!(isMuted() && ok()))
{
- printResult(out,
- smtEngine->getOption("command-verbosity:" + getCommandName())
- .getIntegerValue()
- .toUnsignedInt());
+ printResult(
+ out,
+ std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
}
}
@@ -230,18 +215,12 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const
EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
std::string EmptyCommand::getName() const { return d_name; }
-void EmptyCommand::invoke(SmtEngine* smtEngine)
+void EmptyCommand::invoke(api::Solver* solver)
{
/* empty commands have no implementation */
d_commandStatus = CommandSuccess::instance();
}
-Command* EmptyCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new EmptyCommand(d_name);
-}
-
Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
std::string EmptyCommand::getCommandName() const { return "empty"; }
@@ -260,28 +239,21 @@ void EmptyCommand::toStream(std::ostream& out,
EchoCommand::EchoCommand(std::string output) : d_output(output) {}
std::string EchoCommand::getOutput() const { return d_output; }
-void EchoCommand::invoke(SmtEngine* smtEngine)
+void EchoCommand::invoke(api::Solver* solver)
{
/* we don't have an output stream here, nothing to do */
d_commandStatus = CommandSuccess::instance();
}
-void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out)
+void EchoCommand::invoke(api::Solver* solver, std::ostream& out)
{
out << d_output << std::endl;
Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
<< std::endl;
d_commandStatus = CommandSuccess::instance();
- printResult(out,
- smtEngine->getOption("command-verbosity:" + getCommandName())
- .getIntegerValue()
- .toUnsignedInt());
-}
-
-Command* EchoCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new EchoCommand(d_output);
+ printResult(
+ out,
+ std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
}
Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
@@ -300,17 +272,17 @@ void EchoCommand::toStream(std::ostream& out,
/* class AssertCommand */
/* -------------------------------------------------------------------------- */
-AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore)
- : d_expr(e), d_inUnsatCore(inUnsatCore)
+AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore)
+ : d_term(t), d_inUnsatCore(inUnsatCore)
{
}
-Expr AssertCommand::getExpr() const { return d_expr; }
-void AssertCommand::invoke(SmtEngine* smtEngine)
+api::Term AssertCommand::getTerm() const { return d_term; }
+void AssertCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->assertFormula(d_expr, d_inUnsatCore);
+ solver->getSmtEngine()->assertFormula(d_term.getExpr(), d_inUnsatCore);
d_commandStatus = CommandSuccess::instance();
}
catch (UnsafeInterruptException& e)
@@ -323,16 +295,9 @@ void AssertCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* AssertCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new AssertCommand(d_expr.exportTo(exprManager, variableMap),
- d_inUnsatCore);
-}
-
Command* AssertCommand::clone() const
{
- return new AssertCommand(d_expr, d_inUnsatCore);
+ return new AssertCommand(d_term, d_inUnsatCore);
}
std::string AssertCommand::getCommandName() const { return "assert"; }
@@ -343,18 +308,18 @@ void AssertCommand::toStream(std::ostream& out,
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdAssert(out, Node::fromExpr(d_expr));
+ Printer::getPrinter(language)->toStreamCmdAssert(out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
/* class PushCommand */
/* -------------------------------------------------------------------------- */
-void PushCommand::invoke(SmtEngine* smtEngine)
+void PushCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->push();
+ solver->push();
d_commandStatus = CommandSuccess::instance();
}
catch (UnsafeInterruptException& e)
@@ -367,12 +332,6 @@ void PushCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* PushCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new PushCommand();
-}
-
Command* PushCommand::clone() const { return new PushCommand(); }
std::string PushCommand::getCommandName() const { return "push"; }
@@ -389,11 +348,11 @@ void PushCommand::toStream(std::ostream& out,
/* class PopCommand */
/* -------------------------------------------------------------------------- */
-void PopCommand::invoke(SmtEngine* smtEngine)
+void PopCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->pop();
+ solver->pop();
d_commandStatus = CommandSuccess::instance();
}
catch (UnsafeInterruptException& e)
@@ -406,12 +365,6 @@ void PopCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* PopCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new PopCommand();
-}
-
Command* PopCommand::clone() const { return new PopCommand(); }
std::string PopCommand::getCommandName() const { return "pop"; }
@@ -428,18 +381,20 @@ void PopCommand::toStream(std::ostream& out,
/* class CheckSatCommand */
/* -------------------------------------------------------------------------- */
-CheckSatCommand::CheckSatCommand() : d_expr() {}
+CheckSatCommand::CheckSatCommand() : d_term() {}
-CheckSatCommand::CheckSatCommand(const Expr& expr) : d_expr(expr) {}
+CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {}
-Expr CheckSatCommand::getExpr() const { return d_expr; }
-void CheckSatCommand::invoke(SmtEngine* smtEngine)
+api::Term CheckSatCommand::getTerm() const { return d_term; }
+void CheckSatCommand::invoke(api::Solver* solver)
{
Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
<< std::endl;
try
{
- d_result = smtEngine->checkSat(d_expr);
+ d_result =
+ d_term.isNull() ? solver->checkSat() : solver->checkSatAssuming(d_term);
+
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -448,7 +403,7 @@ void CheckSatCommand::invoke(SmtEngine* smtEngine)
}
}
-Result CheckSatCommand::getResult() const { return d_result; }
+api::Result CheckSatCommand::getResult() const { return d_result; }
void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
if (!ok())
@@ -462,18 +417,9 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* CheckSatCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- CheckSatCommand* c =
- new CheckSatCommand(d_expr.exportTo(exprManager, variableMap));
- c->d_result = d_result;
- return c;
-}
-
Command* CheckSatCommand::clone() const
{
- CheckSatCommand* c = new CheckSatCommand(d_expr);
+ CheckSatCommand* c = new CheckSatCommand(d_term);
c->d_result = d_result;
return c;
}
@@ -486,33 +432,36 @@ void CheckSatCommand::toStream(std::ostream& out,
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdCheckSat(out,
- Node::fromExpr(d_expr));
+ Printer::getPrinter(language)->toStreamCmdCheckSat(out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
/* class CheckSatAssumingCommand */
/* -------------------------------------------------------------------------- */
-CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms({term}) {}
+CheckSatAssumingCommand::CheckSatAssumingCommand(api::Term term)
+ : d_terms({term})
+{
+}
-CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms)
+CheckSatAssumingCommand::CheckSatAssumingCommand(
+ const std::vector<api::Term>& terms)
: d_terms(terms)
{
}
-const std::vector<Expr>& CheckSatAssumingCommand::getTerms() const
+const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const
{
return d_terms;
}
-void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine)
+void CheckSatAssumingCommand::invoke(api::Solver* solver)
{
Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
<< " )~" << std::endl;
try
{
- d_result = smtEngine->checkSat(d_terms);
+ d_result = solver->checkSatAssuming(d_terms);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -521,7 +470,7 @@ void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine)
}
}
-Result CheckSatAssumingCommand::getResult() const
+api::Result CheckSatAssumingCommand::getResult() const
{
Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
return d_result;
@@ -540,19 +489,6 @@ void CheckSatAssumingCommand::printResult(std::ostream& out,
}
}
-Command* CheckSatAssumingCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- vector<Expr> exportedTerms;
- for (const Expr& e : d_terms)
- {
- exportedTerms.push_back(e.exportTo(exprManager, variableMap));
- }
- CheckSatAssumingCommand* c = new CheckSatAssumingCommand(exportedTerms);
- c->d_result = d_result;
- return c;
-}
-
Command* CheckSatAssumingCommand::clone() const
{
CheckSatAssumingCommand* c = new CheckSatAssumingCommand(d_terms);
@@ -571,30 +507,25 @@ void CheckSatAssumingCommand::toStream(std::ostream& out,
size_t dag,
OutputLanguage language) const
{
- std::vector<Node> nodes;
- nodes.reserve(d_terms.size());
- for (const Expr& e : d_terms)
- {
- nodes.push_back(Node::fromExpr(e));
- }
- Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(out, nodes);
+ Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(
+ out, api::termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
/* class QueryCommand */
/* -------------------------------------------------------------------------- */
-QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore)
- : d_expr(e), d_inUnsatCore(inUnsatCore)
+QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore)
+ : d_term(t), d_inUnsatCore(inUnsatCore)
{
}
-Expr QueryCommand::getExpr() const { return d_expr; }
-void QueryCommand::invoke(SmtEngine* smtEngine)
+api::Term QueryCommand::getTerm() const { return d_term; }
+void QueryCommand::invoke(api::Solver* solver)
{
try
{
- d_result = smtEngine->checkEntailed(d_expr);
+ d_result = solver->checkEntailed(d_term);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -603,7 +534,7 @@ void QueryCommand::invoke(SmtEngine* smtEngine)
}
}
-Result QueryCommand::getResult() const { return d_result; }
+api::Result QueryCommand::getResult() const { return d_result; }
void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
if (!ok())
@@ -616,18 +547,9 @@ void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* QueryCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap),
- d_inUnsatCore);
- c->d_result = d_result;
- return c;
-}
-
Command* QueryCommand::clone() const
{
- QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore);
+ QueryCommand* c = new QueryCommand(d_term, d_inUnsatCore);
c->d_result = d_result;
return c;
}
@@ -640,7 +562,7 @@ void QueryCommand::toStream(std::ostream& out,
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdQuery(out, d_expr);
+ Printer::getPrinter(language)->toStreamCmdQuery(out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
@@ -648,21 +570,21 @@ void QueryCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
- Expr var,
- Type t)
- : DeclarationDefinitionCommand(id), d_var(var), d_type(t)
+ api::Term var,
+ api::Sort sort)
+ : DeclarationDefinitionCommand(id), d_var(var), d_sort(sort)
{
}
-Expr DeclareSygusVarCommand::getVar() const { return d_var; }
-Type DeclareSygusVarCommand::getType() const { return d_type; }
+api::Term DeclareSygusVarCommand::getVar() const { return d_var; }
+api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; }
-void DeclareSygusVarCommand::invoke(SmtEngine* smtEngine)
+void DeclareSygusVarCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->declareSygusVar(
- d_symbol, Node::fromExpr(d_var), TypeNode::fromType(d_type));
+ solver->getSmtEngine()->declareSygusVar(
+ d_symbol, d_var.getNode(), TypeNode::fromType(d_sort.getType()));
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -671,17 +593,9 @@ void DeclareSygusVarCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* DeclareSygusVarCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new DeclareSygusVarCommand(d_symbol,
- d_var.exportTo(exprManager, variableMap),
- d_type.exportTo(exprManager, variableMap));
-}
-
Command* DeclareSygusVarCommand::clone() const
{
- return new DeclareSygusVarCommand(d_symbol, d_var, d_type);
+ return new DeclareSygusVarCommand(d_symbol, d_var, d_sort);
}
std::string DeclareSygusVarCommand::getCommandName() const
@@ -696,15 +610,14 @@ void DeclareSygusVarCommand::toStream(std::ostream& out,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdDeclareVar(
- out, Node::fromExpr(d_var), TypeNode::fromType(d_type));
+ out, d_var.getNode(), TypeNode::fromType(d_sort.getType()));
}
/* -------------------------------------------------------------------------- */
/* class SynthFunCommand */
/* -------------------------------------------------------------------------- */
-SynthFunCommand::SynthFunCommand(const api::Solver* solver,
- const std::string& id,
+SynthFunCommand::SynthFunCommand(const std::string& id,
api::Term fun,
const std::vector<api::Term>& vars,
api::Sort sort,
@@ -717,7 +630,6 @@ SynthFunCommand::SynthFunCommand(const api::Solver* solver,
d_isInv(isInv),
d_grammar(g)
{
- d_solver = solver;
}
api::Term SynthFunCommand::getFunction() const { return d_fun; }
@@ -732,7 +644,7 @@ bool SynthFunCommand::isInv() const { return d_isInv; }
const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
-void SynthFunCommand::invoke(SmtEngine* smtEngine)
+void SynthFunCommand::invoke(api::Solver* solver)
{
try
{
@@ -741,7 +653,7 @@ void SynthFunCommand::invoke(SmtEngine* smtEngine)
{
vns.push_back(Node::fromExpr(t.getExpr()));
}
- smtEngine->declareSynthFun(
+ solver->getSmtEngine()->declareSynthFun(
d_symbol,
Node::fromExpr(d_fun.getExpr()),
TypeNode::fromType(d_grammar == nullptr
@@ -757,16 +669,10 @@ void SynthFunCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* SynthFunCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- Unimplemented();
-}
-
Command* SynthFunCommand::clone() const
{
return new SynthFunCommand(
- d_solver, d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
+ d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
}
std::string SynthFunCommand::getCommandName() const
@@ -794,13 +700,15 @@ void SynthFunCommand::toStream(std::ostream& out,
/* class SygusConstraintCommand */
/* -------------------------------------------------------------------------- */
-SygusConstraintCommand::SygusConstraintCommand(const Expr& e) : d_expr(e) {}
+SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
+{
+}
-void SygusConstraintCommand::invoke(SmtEngine* smtEngine)
+void SygusConstraintCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->assertSygusConstraint(d_expr);
+ solver->addSygusConstraint(d_term);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -809,17 +717,11 @@ void SygusConstraintCommand::invoke(SmtEngine* smtEngine)
}
}
-Expr SygusConstraintCommand::getExpr() const { return d_expr; }
-
-Command* SygusConstraintCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new SygusConstraintCommand(d_expr.exportTo(exprManager, variableMap));
-}
+api::Term SygusConstraintCommand::getTerm() const { return d_term; }
Command* SygusConstraintCommand::clone() const
{
- return new SygusConstraintCommand(d_expr);
+ return new SygusConstraintCommand(d_term);
}
std::string SygusConstraintCommand::getCommandName() const
@@ -833,8 +735,7 @@ void SygusConstraintCommand::toStream(std::ostream& out,
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdConstraint(out,
- Node::fromExpr(d_expr));
+ Printer::getPrinter(language)->toStreamCmdConstraint(out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
@@ -842,24 +743,24 @@ void SygusConstraintCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
SygusInvConstraintCommand::SygusInvConstraintCommand(
- const std::vector<Expr>& predicates)
+ const std::vector<api::Term>& predicates)
: d_predicates(predicates)
{
}
-SygusInvConstraintCommand::SygusInvConstraintCommand(const Expr& inv,
- const Expr& pre,
- const Expr& trans,
- const Expr& post)
- : SygusInvConstraintCommand(std::vector<Expr>{inv, pre, trans, post})
+SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv,
+ const api::Term& pre,
+ const api::Term& trans,
+ const api::Term& post)
+ : SygusInvConstraintCommand(std::vector<api::Term>{inv, pre, trans, post})
{
}
-void SygusInvConstraintCommand::invoke(SmtEngine* smtEngine)
+void SygusInvConstraintCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->assertSygusInvConstraint(
+ solver->addSygusInvConstraint(
d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
d_commandStatus = CommandSuccess::instance();
}
@@ -869,17 +770,11 @@ void SygusInvConstraintCommand::invoke(SmtEngine* smtEngine)
}
}
-const std::vector<Expr>& SygusInvConstraintCommand::getPredicates() const
+const std::vector<api::Term>& SygusInvConstraintCommand::getPredicates() const
{
return d_predicates;
}
-Command* SygusInvConstraintCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- return new SygusInvConstraintCommand(d_predicates);
-}
-
Command* SygusInvConstraintCommand::clone() const
{
return new SygusInvConstraintCommand(d_predicates);
@@ -898,26 +793,25 @@ void SygusInvConstraintCommand::toStream(std::ostream& out,
{
Printer::getPrinter(language)->toStreamCmdInvConstraint(
out,
- Node::fromExpr(d_predicates[0]),
- Node::fromExpr(d_predicates[1]),
- Node::fromExpr(d_predicates[2]),
- Node::fromExpr(d_predicates[3]));
+ d_predicates[0].getNode(),
+ d_predicates[1].getNode(),
+ d_predicates[2].getNode(),
+ d_predicates[3].getNode());
}
/* -------------------------------------------------------------------------- */
/* class CheckSynthCommand */
/* -------------------------------------------------------------------------- */
-void CheckSynthCommand::invoke(SmtEngine* smtEngine)
+void CheckSynthCommand::invoke(api::Solver* solver)
{
try
{
- d_result = smtEngine->checkSynth();
+ d_result = solver->checkSynth();
d_commandStatus = CommandSuccess::instance();
- smt::SmtScope scope(smtEngine);
d_solution.clear();
// check whether we should print the status
- if (d_result.asSatisfiabilityResult() != Result::UNSAT
+ if (!d_result.isUnsat()
|| options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF
|| options::sygusOut() == options::SygusSolutionOutMode::STATUS)
{
@@ -931,7 +825,7 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine)
}
}
// check whether we should print the solution
- if (d_result.asSatisfiabilityResult() == Result::UNSAT
+ if (d_result.isUnsat()
&& options::sygusOut() != options::SygusSolutionOutMode::STATUS)
{
// printing a synthesis solution is a non-constant
@@ -939,7 +833,7 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine)
// (Figure 5 of Reynolds et al. CAV 2015).
// Hence, we must call here print solution here,
// instead of during printResult.
- smtEngine->printSynthSolution(d_solution);
+ solver->printSynthSolution(d_solution);
}
}
catch (exception& e)
@@ -948,7 +842,7 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine)
}
}
-Result CheckSynthCommand::getResult() const { return d_result; }
+api::Result CheckSynthCommand::getResult() const { return d_result; }
void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
if (!ok())
@@ -961,12 +855,6 @@ void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* CheckSynthCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new CheckSynthCommand();
-}
-
Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
@@ -984,11 +872,11 @@ void CheckSynthCommand::toStream(std::ostream& out,
/* class ResetCommand */
/* -------------------------------------------------------------------------- */
-void ResetCommand::invoke(SmtEngine* smtEngine)
+void ResetCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->reset();
+ solver->getSmtEngine()->reset();
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -997,12 +885,6 @@ void ResetCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* ResetCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new ResetCommand();
-}
-
Command* ResetCommand::clone() const { return new ResetCommand(); }
std::string ResetCommand::getCommandName() const { return "reset"; }
@@ -1019,11 +901,11 @@ void ResetCommand::toStream(std::ostream& out,
/* class ResetAssertionsCommand */
/* -------------------------------------------------------------------------- */
-void ResetAssertionsCommand::invoke(SmtEngine* smtEngine)
+void ResetAssertionsCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->resetAssertions();
+ solver->resetAssertions();
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -1032,12 +914,6 @@ void ResetAssertionsCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new ResetAssertionsCommand();
-}
-
Command* ResetAssertionsCommand::clone() const
{
return new ResetAssertionsCommand();
@@ -1061,18 +937,12 @@ void ResetAssertionsCommand::toStream(std::ostream& out,
/* class QuitCommand */
/* -------------------------------------------------------------------------- */
-void QuitCommand::invoke(SmtEngine* smtEngine)
+void QuitCommand::invoke(api::Solver* solver)
{
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
}
-Command* QuitCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new QuitCommand();
-}
-
Command* QuitCommand::clone() const { return new QuitCommand(); }
std::string QuitCommand::getCommandName() const { return "exit"; }
@@ -1091,18 +961,12 @@ void QuitCommand::toStream(std::ostream& out,
CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
std::string CommentCommand::getComment() const { return d_comment; }
-void CommentCommand::invoke(SmtEngine* smtEngine)
+void CommentCommand::invoke(api::Solver* solver)
{
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
}
-Command* CommentCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new CommentCommand(d_comment);
-}
-
Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
std::string CommentCommand::getCommandName() const { return "comment"; }
@@ -1134,11 +998,11 @@ void CommandSequence::addCommand(Command* cmd)
}
void CommandSequence::clear() { d_commandSequence.clear(); }
-void CommandSequence::invoke(SmtEngine* smtEngine)
+void CommandSequence::invoke(api::Solver* solver)
{
for (; d_index < d_commandSequence.size(); ++d_index)
{
- d_commandSequence[d_index]->invoke(smtEngine);
+ d_commandSequence[d_index]->invoke(solver);
if (!d_commandSequence[d_index]->ok())
{
// abort execution
@@ -1152,11 +1016,11 @@ void CommandSequence::invoke(SmtEngine* smtEngine)
d_commandStatus = CommandSuccess::instance();
}
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out)
+void CommandSequence::invoke(api::Solver* solver, std::ostream& out)
{
for (; d_index < d_commandSequence.size(); ++d_index)
{
- d_commandSequence[d_index]->invoke(smtEngine, out);
+ d_commandSequence[d_index]->invoke(solver, out);
if (!d_commandSequence[d_index]->ok())
{
// abort execution
@@ -1170,21 +1034,6 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out)
d_commandStatus = CommandSuccess::instance();
}
-Command* CommandSequence::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- CommandSequence* seq = new CommandSequence();
- for (iterator i = begin(); i != end(); ++i)
- {
- Command* cmd_to_export = *i;
- Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
- seq->addCommand(cmd);
- Debug("export") << "[export] so far converted: " << seq << endl;
- }
- seq->d_index = d_index;
- return seq;
-}
-
Command* CommandSequence::clone() const
{
CommandSequence* seq = new CommandSequence();
@@ -1259,18 +1108,18 @@ std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }
/* -------------------------------------------------------------------------- */
DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
- Expr func,
- Type t)
+ api::Term func,
+ api::Sort sort)
: DeclarationDefinitionCommand(id),
d_func(func),
- d_type(t),
+ d_sort(sort),
d_printInModel(true),
d_printInModelSetByUser(false)
{
}
-Expr DeclareFunctionCommand::getFunction() const { return d_func; }
-Type DeclareFunctionCommand::getType() const { return d_type; }
+api::Term DeclareFunctionCommand::getFunction() const { return d_func; }
+api::Sort DeclareFunctionCommand::getSort() const { return d_sort; }
bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; }
bool DeclareFunctionCommand::getPrintInModelSetByUser() const
{
@@ -1283,27 +1132,15 @@ void DeclareFunctionCommand::setPrintInModel(bool p)
d_printInModelSetByUser = true;
}
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine)
+void DeclareFunctionCommand::invoke(api::Solver* solver)
{
d_commandStatus = CommandSuccess::instance();
}
-Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- DeclareFunctionCommand* dfc =
- new DeclareFunctionCommand(d_symbol,
- d_func.exportTo(exprManager, variableMap),
- d_type.exportTo(exprManager, variableMap));
- dfc->d_printInModel = d_printInModel;
- dfc->d_printInModelSetByUser = d_printInModelSetByUser;
- return dfc;
-}
-
Command* DeclareFunctionCommand::clone() const
{
DeclareFunctionCommand* dfc =
- new DeclareFunctionCommand(d_symbol, d_func, d_type);
+ new DeclareFunctionCommand(d_symbol, d_func, d_sort);
dfc->d_printInModel = d_printInModel;
dfc->d_printInModelSetByUser = d_printInModelSetByUser;
return dfc;
@@ -1321,101 +1158,82 @@ void DeclareFunctionCommand::toStream(std::ostream& out,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdDeclareFunction(
- out, d_func.toString(), TypeNode::fromType(d_type));
+ out, d_func.toString(), TypeNode::fromType(d_sort.getType()));
}
/* -------------------------------------------------------------------------- */
-/* class DeclareTypeCommand */
+/* class DeclareSortCommand */
/* -------------------------------------------------------------------------- */
-DeclareTypeCommand::DeclareTypeCommand(const std::string& id,
+DeclareSortCommand::DeclareSortCommand(const std::string& id,
size_t arity,
- Type t)
- : DeclarationDefinitionCommand(id), d_arity(arity), d_type(t)
+ api::Sort sort)
+ : DeclarationDefinitionCommand(id), d_arity(arity), d_sort(sort)
{
}
-size_t DeclareTypeCommand::getArity() const { return d_arity; }
-Type DeclareTypeCommand::getType() const { return d_type; }
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine)
+size_t DeclareSortCommand::getArity() const { return d_arity; }
+api::Sort DeclareSortCommand::getSort() const { return d_sort; }
+void DeclareSortCommand::invoke(api::Solver* solver)
{
d_commandStatus = CommandSuccess::instance();
}
-Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new DeclareTypeCommand(
- d_symbol, d_arity, d_type.exportTo(exprManager, variableMap));
-}
-
-Command* DeclareTypeCommand::clone() const
+Command* DeclareSortCommand::clone() const
{
- return new DeclareTypeCommand(d_symbol, d_arity, d_type);
+ return new DeclareSortCommand(d_symbol, d_arity, d_sort);
}
-std::string DeclareTypeCommand::getCommandName() const
+std::string DeclareSortCommand::getCommandName() const
{
return "declare-sort";
}
-void DeclareTypeCommand::toStream(std::ostream& out,
+void DeclareSortCommand::toStream(std::ostream& out,
int toDepth,
bool types,
size_t dag,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdDeclareType(
- out, d_type.toString(), d_arity, TypeNode::fromType(d_type));
+ out, d_sort.toString(), d_arity, TypeNode::fromType(d_sort.getType()));
}
/* -------------------------------------------------------------------------- */
-/* class DefineTypeCommand */
+/* class DefineSortCommand */
/* -------------------------------------------------------------------------- */
-DefineTypeCommand::DefineTypeCommand(const std::string& id, Type t)
- : DeclarationDefinitionCommand(id), d_params(), d_type(t)
+DefineSortCommand::DefineSortCommand(const std::string& id, api::Sort sort)
+ : DeclarationDefinitionCommand(id), d_params(), d_sort(sort)
{
}
-DefineTypeCommand::DefineTypeCommand(const std::string& id,
- const std::vector<Type>& params,
- Type t)
- : DeclarationDefinitionCommand(id), d_params(params), d_type(t)
+DefineSortCommand::DefineSortCommand(const std::string& id,
+ const std::vector<api::Sort>& params,
+ api::Sort sort)
+ : DeclarationDefinitionCommand(id), d_params(params), d_sort(sort)
{
}
-const std::vector<Type>& DefineTypeCommand::getParameters() const
+const std::vector<api::Sort>& DefineSortCommand::getParameters() const
{
return d_params;
}
-Type DefineTypeCommand::getType() const { return d_type; }
-void DefineTypeCommand::invoke(SmtEngine* smtEngine)
+api::Sort DefineSortCommand::getSort() const { return d_sort; }
+void DefineSortCommand::invoke(api::Solver* solver)
{
d_commandStatus = CommandSuccess::instance();
}
-Command* DefineTypeCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- vector<Type> params;
- transform(d_params.begin(),
- d_params.end(),
- back_inserter(params),
- ExportTransformer(exprManager, variableMap));
- Type type = d_type.exportTo(exprManager, variableMap);
- return new DefineTypeCommand(d_symbol, params, type);
-}
-
-Command* DefineTypeCommand::clone() const
+Command* DefineSortCommand::clone() const
{
- return new DefineTypeCommand(d_symbol, d_params, d_type);
+ return new DefineSortCommand(d_symbol, d_params, d_sort);
}
-std::string DefineTypeCommand::getCommandName() const { return "define-sort"; }
+std::string DefineSortCommand::getCommandName() const { return "define-sort"; }
-void DefineTypeCommand::toStream(std::ostream& out,
+void DefineSortCommand::toStream(std::ostream& out,
int toDepth,
bool types,
size_t dag,
@@ -1424,8 +1242,8 @@ void DefineTypeCommand::toStream(std::ostream& out,
Printer::getPrinter(language)->toStreamCmdDefineType(
out,
d_symbol,
- typeVectorToTypeNodes(d_params),
- TypeNode::fromType(d_type));
+ api::sortVectorToTypeNodes(d_params),
+ TypeNode::fromType(d_sort.getType()));
}
/* -------------------------------------------------------------------------- */
@@ -1433,8 +1251,8 @@ void DefineTypeCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
- Expr func,
- Expr formula,
+ api::Term func,
+ api::Term formula,
bool global)
: DeclarationDefinitionCommand(id),
d_func(func),
@@ -1444,34 +1262,34 @@ DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
{
}
-DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
- Expr func,
- const std::vector<Expr>& formals,
- Expr formula,
- bool global)
+DefineFunctionCommand::DefineFunctionCommand(
+ const std::string& id,
+ api::Term func,
+ const std::vector<api::Term>& formals,
+ api::Term formula,
+ bool global)
: DeclarationDefinitionCommand(id),
d_func(func),
d_formals(formals),
d_formula(formula),
d_global(global)
-
{
}
-Expr DefineFunctionCommand::getFunction() const { return d_func; }
-const std::vector<Expr>& DefineFunctionCommand::getFormals() const
+api::Term DefineFunctionCommand::getFunction() const { return d_func; }
+const std::vector<api::Term>& DefineFunctionCommand::getFormals() const
{
return d_formals;
}
-Expr DefineFunctionCommand::getFormula() const { return d_formula; }
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine)
+api::Term DefineFunctionCommand::getFormula() const { return d_formula; }
+void DefineFunctionCommand::invoke(api::Solver* solver)
{
try
{
if (!d_func.isNull())
{
- smtEngine->defineFunction(d_func, d_formals, d_formula, d_global);
+ solver->defineFun(d_func, d_formals, d_formula, d_global);
}
d_commandStatus = CommandSuccess::instance();
}
@@ -1481,20 +1299,6 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* DefineFunctionCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- Expr func = d_func.exportTo(
- exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
- vector<Expr> formals;
- transform(d_formals.begin(),
- d_formals.end(),
- back_inserter(formals),
- ExportTransformer(exprManager, variableMap));
- Expr formula = d_formula.exportTo(exprManager, variableMap);
- return new DefineFunctionCommand(d_symbol, func, formals, formula, d_global);
-}
-
Command* DefineFunctionCommand::clone() const
{
return new DefineFunctionCommand(
@@ -1515,9 +1319,9 @@ void DefineFunctionCommand::toStream(std::ostream& out,
Printer::getPrinter(language)->toStreamCmdDefineFunction(
out,
d_func.toString(),
- exprVectorToNodes(d_formals),
- Node::fromExpr(d_func).getType().getRangeType(),
- Node::fromExpr(d_formula));
+ api::termVectorToNodes(d_formals),
+ d_func.getNode().getType().getRangeType(),
+ d_formula.getNode());
}
/* -------------------------------------------------------------------------- */
@@ -1525,39 +1329,26 @@ void DefineFunctionCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
DefineNamedFunctionCommand::DefineNamedFunctionCommand(
+
const std::string& id,
- Expr func,
- const std::vector<Expr>& formals,
- Expr formula,
+ api::Term func,
+ const std::vector<api::Term>& formals,
+ api::Term formula,
bool global)
: DefineFunctionCommand(id, func, formals, formula, global)
{
}
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine)
+void DefineNamedFunctionCommand::invoke(api::Solver* solver)
{
- this->DefineFunctionCommand::invoke(smtEngine);
- if (!d_func.isNull() && d_func.getType().isBoolean())
+ this->DefineFunctionCommand::invoke(solver);
+ if (!d_func.isNull() && d_func.getSort().isBoolean())
{
- smtEngine->addToAssignment(d_func);
+ solver->getSmtEngine()->addToAssignment(d_func.getExpr());
}
d_commandStatus = CommandSuccess::instance();
}
-Command* DefineNamedFunctionCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- Expr func = d_func.exportTo(exprManager, variableMap);
- vector<Expr> formals;
- transform(d_formals.begin(),
- d_formals.end(),
- back_inserter(formals),
- ExportTransformer(exprManager, variableMap));
- Expr formula = d_formula.exportTo(exprManager, variableMap);
- return new DefineNamedFunctionCommand(
- d_symbol, func, formals, formula, d_global);
-}
-
Command* DefineNamedFunctionCommand::clone() const
{
return new DefineNamedFunctionCommand(
@@ -1573,9 +1364,9 @@ void DefineNamedFunctionCommand::toStream(std::ostream& out,
Printer::getPrinter(language)->toStreamCmdDefineNamedFunction(
out,
d_func.toString(),
- exprVectorToNodes(d_formals),
- Node::fromExpr(d_func).getType().getRangeType(),
- Node::fromExpr(d_formula));
+ api::termVectorToNodes(d_formals),
+ TypeNode::fromType(d_func.getSort().getFunctionCodomainSort().getType()),
+ d_formula.getNode());
}
/* -------------------------------------------------------------------------- */
@@ -1583,12 +1374,12 @@ void DefineNamedFunctionCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
DefineFunctionRecCommand::DefineFunctionRecCommand(
- const api::Solver* solver,
+
api::Term func,
const std::vector<api::Term>& formals,
api::Term formula,
bool global)
- : Command(solver), d_global(global)
+ : d_global(global)
{
d_funcs.push_back(func);
d_formals.push_back(formals);
@@ -1596,16 +1387,12 @@ DefineFunctionRecCommand::DefineFunctionRecCommand(
}
DefineFunctionRecCommand::DefineFunctionRecCommand(
- const api::Solver* solver,
+
const std::vector<api::Term>& funcs,
const std::vector<std::vector<api::Term>>& formals,
const std::vector<api::Term>& formulas,
bool global)
- : Command(solver),
- d_funcs(funcs),
- d_formals(formals),
- d_formulas(formulas),
- d_global(global)
+ : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global)
{
}
@@ -1625,11 +1412,11 @@ const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
return d_formulas;
}
-void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine)
+void DefineFunctionRecCommand::invoke(api::Solver* solver)
{
try
{
- d_solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global);
+ solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -1638,16 +1425,9 @@ void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* DefineFunctionRecCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- Unimplemented();
-}
-
Command* DefineFunctionRecCommand::clone() const
{
- return new DefineFunctionRecCommand(
- d_solver, d_funcs, d_formals, d_formulas, d_global);
+ return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global);
}
std::string DefineFunctionRecCommand::getCommandName() const
@@ -1681,42 +1461,45 @@ void DefineFunctionRecCommand::toStream(std::ostream& out,
SetUserAttributeCommand::SetUserAttributeCommand(
const std::string& attr,
- Expr expr,
- const std::vector<Expr>& expr_values,
- const std::string& str_value)
- : d_attr(attr),
- d_expr(expr),
- d_expr_values(expr_values),
- d_str_value(str_value)
+ api::Term term,
+ const std::vector<api::Term>& termValues,
+ const std::string& strValue)
+ : d_attr(attr), d_term(term), d_termValues(termValues), d_strValue(strValue)
{
}
SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
- Expr expr)
- : SetUserAttributeCommand(attr, expr, {}, "")
+ api::Term term)
+ : SetUserAttributeCommand(attr, term, {}, "")
{
}
SetUserAttributeCommand::SetUserAttributeCommand(
- const std::string& attr, Expr expr, const std::vector<Expr>& values)
- : SetUserAttributeCommand(attr, expr, values, "")
+ const std::string& attr,
+ api::Term term,
+ const std::vector<api::Term>& values)
+ : SetUserAttributeCommand(attr, term, values, "")
{
}
SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
- Expr expr,
+ api::Term term,
const std::string& value)
- : SetUserAttributeCommand(attr, expr, {}, value)
+ : SetUserAttributeCommand(attr, term, {}, value)
{
}
-void SetUserAttributeCommand::invoke(SmtEngine* smtEngine)
+void SetUserAttributeCommand::invoke(api::Solver* solver)
{
try
{
- if (!d_expr.isNull())
+ if (!d_term.isNull())
{
- smtEngine->setUserAttribute(d_attr, d_expr, d_expr_values, d_str_value);
+ solver->getSmtEngine()->setUserAttribute(
+ d_attr,
+ d_term.getExpr(),
+ api::termVectorToExprs(d_termValues),
+ d_strValue);
}
d_commandStatus = CommandSuccess::instance();
}
@@ -1726,17 +1509,9 @@ void SetUserAttributeCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* SetUserAttributeCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- Expr expr = d_expr.exportTo(exprManager, variableMap);
- return new SetUserAttributeCommand(d_attr, expr, d_expr_values, d_str_value);
-}
-
Command* SetUserAttributeCommand::clone() const
{
- return new SetUserAttributeCommand(
- d_attr, d_expr, d_expr_values, d_str_value);
+ return new SetUserAttributeCommand(d_attr, d_term, d_termValues, d_strValue);
}
std::string SetUserAttributeCommand::getCommandName() const
@@ -1751,20 +1526,20 @@ void SetUserAttributeCommand::toStream(std::ostream& out,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdSetUserAttribute(
- out, d_attr, Node::fromExpr(d_expr));
+ out, d_attr, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
/* class SimplifyCommand */
/* -------------------------------------------------------------------------- */
-SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) {}
-Expr SimplifyCommand::getTerm() const { return d_term; }
-void SimplifyCommand::invoke(SmtEngine* smtEngine)
+SimplifyCommand::SimplifyCommand(api::Term term) : d_term(term) {}
+api::Term SimplifyCommand::getTerm() const { return d_term; }
+void SimplifyCommand::invoke(api::Solver* solver)
{
try
{
- d_result = smtEngine->simplify(Node::fromExpr(d_term)).toExpr();
+ d_result = solver->simplify(d_term);
d_commandStatus = CommandSuccess::instance();
}
catch (UnsafeInterruptException& e)
@@ -1777,7 +1552,7 @@ void SimplifyCommand::invoke(SmtEngine* smtEngine)
}
}
-Expr SimplifyCommand::getResult() const { return d_result; }
+api::Term SimplifyCommand::getResult() const { return d_result; }
void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
if (!ok())
@@ -1790,15 +1565,6 @@ void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* SimplifyCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- SimplifyCommand* c =
- new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
- c->d_result = d_result.exportTo(exprManager, variableMap);
- return c;
-}
-
Command* SimplifyCommand::clone() const
{
SimplifyCommand* c = new SimplifyCommand(d_term);
@@ -1814,23 +1580,26 @@ void SimplifyCommand::toStream(std::ostream& out,
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term);
+ Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
/* class ExpandDefinitionsCommand */
/* -------------------------------------------------------------------------- */
-ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {}
-Expr ExpandDefinitionsCommand::getTerm() const { return d_term; }
-void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine)
+ExpandDefinitionsCommand::ExpandDefinitionsCommand(api::Term term)
+ : d_term(term)
+{
+}
+api::Term ExpandDefinitionsCommand::getTerm() const { return d_term; }
+void ExpandDefinitionsCommand::invoke(api::Solver* solver)
{
- Node t = Node::fromExpr(d_term);
- d_result = smtEngine->expandDefinitions(t).toExpr();
+ Node t = d_term.getNode();
+ d_result = api::Term(solver, solver->getSmtEngine()->expandDefinitions(t));
d_commandStatus = CommandSuccess::instance();
}
-Expr ExpandDefinitionsCommand::getResult() const { return d_result; }
+api::Term ExpandDefinitionsCommand::getResult() const { return d_result; }
void ExpandDefinitionsCommand::printResult(std::ostream& out,
uint32_t verbosity) const
{
@@ -1844,15 +1613,6 @@ void ExpandDefinitionsCommand::printResult(std::ostream& out,
}
}
-Command* ExpandDefinitionsCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- ExpandDefinitionsCommand* c =
- new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
- c->d_result = d_result.exportTo(exprManager, variableMap);
- return c;
-}
-
Command* ExpandDefinitionsCommand::clone() const
{
ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
@@ -1871,45 +1631,51 @@ void ExpandDefinitionsCommand::toStream(std::ostream& out,
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdExpandDefinitions(
- out, Node::fromExpr(d_term));
+ Printer::getPrinter(language)->toStreamCmdExpandDefinitions(out,
+ d_term.getNode());
}
/* -------------------------------------------------------------------------- */
/* class GetValueCommand */
/* -------------------------------------------------------------------------- */
-GetValueCommand::GetValueCommand(Expr term) : d_terms()
+GetValueCommand::GetValueCommand(api::Term term) : d_terms()
{
d_terms.push_back(term);
}
-GetValueCommand::GetValueCommand(const std::vector<Expr>& terms)
+GetValueCommand::GetValueCommand(const std::vector<api::Term>& terms)
: d_terms(terms)
{
PrettyCheckArgument(
terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
}
-const std::vector<Expr>& GetValueCommand::getTerms() const { return d_terms; }
-void GetValueCommand::invoke(SmtEngine* smtEngine)
+const std::vector<api::Term>& GetValueCommand::getTerms() const
+{
+ return d_terms;
+}
+void GetValueCommand::invoke(api::Solver* solver)
{
try
{
- ExprManager* em = smtEngine->getExprManager();
- NodeManager* nm = NodeManager::fromExprManager(em);
- smt::SmtScope scope(smtEngine);
- vector<Expr> result = smtEngine->getValues(d_terms);
+ NodeManager* nm = solver->getNodeManager();
+ smt::SmtScope scope(solver->getSmtEngine());
+ std::vector<Node> result;
+ for (const Expr& e :
+ solver->getSmtEngine()->getValues(api::termVectorToExprs(d_terms)))
+ {
+ result.push_back(Node::fromExpr(e));
+ }
Assert(result.size() == d_terms.size());
for (int i = 0, size = d_terms.size(); i < size; i++)
{
- Expr e = d_terms[i];
- Node eNode = Node::fromExpr(e);
- Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
+ api::Term t = d_terms[i];
+ Node tNode = t.getNode();
Node request = options::expandDefinitions()
- ? smtEngine->expandDefinitions(eNode)
- : eNode;
- Node value = Node::fromExpr(result[i]);
+ ? solver->getSmtEngine()->expandDefinitions(tNode)
+ : tNode;
+ Node value = result[i];
if (value.getType().isInteger() && request.getType() == nm->realType())
{
// Need to wrap in division-by-one so that output printers know this
@@ -1917,9 +1683,9 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
// a rational. Necessary for SMT-LIB standards compliance.
value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
}
- result[i] = nm->mkNode(kind::SEXPR, request, value).toExpr();
+ result[i] = nm->mkNode(kind::SEXPR, request, value);
}
- d_result = em->mkExpr(kind::SEXPR, result);
+ d_result = api::Term(solver, nm->mkNode(kind::SEXPR, result));
d_commandStatus = CommandSuccess::instance();
}
catch (RecoverableModalException& e)
@@ -1936,7 +1702,7 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
}
}
-Expr GetValueCommand::getResult() const { return d_result; }
+api::Term GetValueCommand::getResult() const { return d_result; }
void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
if (!ok())
@@ -1950,21 +1716,6 @@ void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* GetValueCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- vector<Expr> exportedTerms;
- for (std::vector<Expr>::const_iterator i = d_terms.begin();
- i != d_terms.end();
- ++i)
- {
- exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
- }
- GetValueCommand* c = new GetValueCommand(exportedTerms);
- c->d_result = d_result.exportTo(exprManager, variableMap);
- return c;
-}
-
Command* GetValueCommand::clone() const
{
GetValueCommand* c = new GetValueCommand(d_terms);
@@ -1981,7 +1732,7 @@ void GetValueCommand::toStream(std::ostream& out,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdGetValue(
- out, exprVectorToNodes(d_terms));
+ out, api::termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
@@ -1989,11 +1740,12 @@ void GetValueCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetAssignmentCommand::GetAssignmentCommand() {}
-void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
+void GetAssignmentCommand::invoke(api::Solver* solver)
{
try
{
- std::vector<std::pair<Expr, Expr>> assignments = smtEngine->getAssignment();
+ std::vector<std::pair<Expr, Expr>> assignments =
+ solver->getSmtEngine()->getAssignment();
vector<SExpr> sexprs;
for (const auto& p : assignments)
{
@@ -2033,14 +1785,6 @@ void GetAssignmentCommand::printResult(std::ostream& out,
}
}
-Command* GetAssignmentCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- GetAssignmentCommand* c = new GetAssignmentCommand();
- c->d_result = d_result;
- return c;
-}
-
Command* GetAssignmentCommand::clone() const
{
GetAssignmentCommand* c = new GetAssignmentCommand();
@@ -2067,12 +1811,12 @@ void GetAssignmentCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
-void GetModelCommand::invoke(SmtEngine* smtEngine)
+void GetModelCommand::invoke(api::Solver* solver)
{
try
{
- d_result = smtEngine->getModel();
- d_smtEngine = smtEngine;
+ d_result = solver->getSmtEngine()->getModel();
+ d_smtEngine = solver->getSmtEngine();
d_commandStatus = CommandSuccess::instance();
}
catch (RecoverableModalException& e)
@@ -2107,15 +1851,6 @@ void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* GetModelCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- GetModelCommand* c = new GetModelCommand();
- c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
- return c;
-}
-
Command* GetModelCommand::clone() const
{
GetModelCommand* c = new GetModelCommand();
@@ -2140,11 +1875,11 @@ void GetModelCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
BlockModelCommand::BlockModelCommand() {}
-void BlockModelCommand::invoke(SmtEngine* smtEngine)
+void BlockModelCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->blockModel();
+ solver->getSmtEngine()->blockModel();
d_commandStatus = CommandSuccess::instance();
}
catch (RecoverableModalException& e)
@@ -2161,13 +1896,6 @@ void BlockModelCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* BlockModelCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- BlockModelCommand* c = new BlockModelCommand();
- return c;
-}
-
Command* BlockModelCommand::clone() const
{
BlockModelCommand* c = new BlockModelCommand();
@@ -2189,7 +1917,8 @@ void BlockModelCommand::toStream(std::ostream& out,
/* class BlockModelValuesCommand */
/* -------------------------------------------------------------------------- */
-BlockModelValuesCommand::BlockModelValuesCommand(const std::vector<Expr>& terms)
+BlockModelValuesCommand::BlockModelValuesCommand(
+ const std::vector<api::Term>& terms)
: d_terms(terms)
{
PrettyCheckArgument(terms.size() >= 1,
@@ -2197,15 +1926,15 @@ BlockModelValuesCommand::BlockModelValuesCommand(const std::vector<Expr>& terms)
"cannot block-model-values of an empty set of terms");
}
-const std::vector<Expr>& BlockModelValuesCommand::getTerms() const
+const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const
{
return d_terms;
}
-void BlockModelValuesCommand::invoke(SmtEngine* smtEngine)
+void BlockModelValuesCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->blockModelValues(d_terms);
+ solver->getSmtEngine()->blockModelValues(api::termVectorToExprs(d_terms));
d_commandStatus = CommandSuccess::instance();
}
catch (RecoverableModalException& e)
@@ -2222,20 +1951,6 @@ void BlockModelValuesCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* BlockModelValuesCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- vector<Expr> exportedTerms;
- for (std::vector<Expr>::const_iterator i = d_terms.begin();
- i != d_terms.end();
- ++i)
- {
- exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
- }
- BlockModelValuesCommand* c = new BlockModelValuesCommand(exportedTerms);
- return c;
-}
-
Command* BlockModelValuesCommand::clone() const
{
BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms);
@@ -2254,7 +1969,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdBlockModelValues(
- out, exprVectorToNodes(d_terms));
+ out, api::termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
@@ -2262,18 +1977,11 @@ void BlockModelValuesCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetProofCommand::GetProofCommand() {}
-void GetProofCommand::invoke(SmtEngine* smtEngine)
+void GetProofCommand::invoke(api::Solver* solver)
{
Unimplemented() << "Unimplemented get-proof\n";
}
-Command* GetProofCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- GetProofCommand* c = new GetProofCommand();
- return c;
-}
-
Command* GetProofCommand::clone() const
{
GetProofCommand* c = new GetProofCommand();
@@ -2296,11 +2004,11 @@ void GetProofCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
-void GetInstantiationsCommand::invoke(SmtEngine* smtEngine)
+void GetInstantiationsCommand::invoke(api::Solver* solver)
{
try
{
- d_smtEngine = smtEngine;
+ d_smtEngine = solver->getSmtEngine();
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -2322,15 +2030,6 @@ void GetInstantiationsCommand::printResult(std::ostream& out,
}
}
-Command* GetInstantiationsCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- GetInstantiationsCommand* c = new GetInstantiationsCommand();
- // c->d_result = d_result;
- c->d_smtEngine = d_smtEngine;
- return c;
-}
-
Command* GetInstantiationsCommand::clone() const
{
GetInstantiationsCommand* c = new GetInstantiationsCommand();
@@ -2358,11 +2057,11 @@ void GetInstantiationsCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
-void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine)
+void GetSynthSolutionCommand::invoke(api::Solver* solver)
{
try
{
- d_smtEngine = smtEngine;
+ d_smtEngine = solver->getSmtEngine();
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -2384,14 +2083,6 @@ void GetSynthSolutionCommand::printResult(std::ostream& out,
}
}
-Command* GetSynthSolutionCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
- c->d_smtEngine = d_smtEngine;
- return c;
-}
-
Command* GetSynthSolutionCommand::clone() const
{
GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
@@ -2417,21 +2108,14 @@ void GetSynthSolutionCommand::toStream(std::ostream& out,
/* class GetInterpolCommand */
/* -------------------------------------------------------------------------- */
-GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
- const std::string& name,
- api::Term conj)
- : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
+GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj)
+ : d_name(name), d_conj(conj), d_resultStatus(false)
{
}
-GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
- const std::string& name,
+GetInterpolCommand::GetInterpolCommand(const std::string& name,
api::Term conj,
api::Grammar* g)
- : Command(solver),
- d_name(name),
- d_conj(conj),
- d_sygus_grammar(g),
- d_resultStatus(false)
+ : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
{
}
@@ -2444,18 +2128,18 @@ const api::Grammar* GetInterpolCommand::getGrammar() const
api::Term GetInterpolCommand::getResult() const { return d_result; }
-void GetInterpolCommand::invoke(SmtEngine* smtEngine)
+void GetInterpolCommand::invoke(api::Solver* solver)
{
try
{
- if (!d_sygus_grammar)
+ if (d_sygus_grammar == nullptr)
{
- d_resultStatus = d_solver->getInterpolant(d_conj, d_result);
+ d_resultStatus = solver->getInterpolant(d_conj, d_result);
}
else
{
d_resultStatus =
- d_solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
+ solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
}
d_commandStatus = CommandSuccess::instance();
}
@@ -2487,16 +2171,10 @@ void GetInterpolCommand::printResult(std::ostream& out,
}
}
-Command* GetInterpolCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- Unimplemented();
-}
-
Command* GetInterpolCommand::clone() const
{
GetInterpolCommand* c =
- new GetInterpolCommand(d_solver, d_name, d_conj, d_sygus_grammar);
+ new GetInterpolCommand(d_name, d_conj, d_sygus_grammar);
c->d_result = d_result;
c->d_resultStatus = d_resultStatus;
return c;
@@ -2524,21 +2202,14 @@ void GetInterpolCommand::toStream(std::ostream& out,
/* class GetAbductCommand */
/* -------------------------------------------------------------------------- */
-GetAbductCommand::GetAbductCommand(const api::Solver* solver,
- const std::string& name,
- api::Term conj)
- : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
+GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj)
+ : d_name(name), d_conj(conj), d_resultStatus(false)
{
}
-GetAbductCommand::GetAbductCommand(const api::Solver* solver,
- const std::string& name,
+GetAbductCommand::GetAbductCommand(const std::string& name,
api::Term conj,
api::Grammar* g)
- : Command(solver),
- d_name(name),
- d_conj(conj),
- d_sygus_grammar(g),
- d_resultStatus(false)
+ : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
{
}
@@ -2552,17 +2223,17 @@ const api::Grammar* GetAbductCommand::getGrammar() const
std::string GetAbductCommand::getAbductName() const { return d_name; }
api::Term GetAbductCommand::getResult() const { return d_result; }
-void GetAbductCommand::invoke(SmtEngine* smtEngine)
+void GetAbductCommand::invoke(api::Solver* solver)
{
try
{
- if (!d_sygus_grammar)
+ if (d_sygus_grammar == nullptr)
{
- d_resultStatus = d_solver->getAbduct(d_conj, d_result);
+ d_resultStatus = solver->getAbduct(d_conj, d_result);
}
else
{
- d_resultStatus = d_solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
+ d_resultStatus = solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
}
d_commandStatus = CommandSuccess::instance();
}
@@ -2593,16 +2264,9 @@ void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* GetAbductCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- Unimplemented();
-}
-
Command* GetAbductCommand::clone() const
{
- GetAbductCommand* c =
- new GetAbductCommand(d_solver, d_name, d_conj, d_sygus_grammar);
+ GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar);
c->d_result = d_result;
c->d_resultStatus = d_resultStatus;
return c;
@@ -2628,24 +2292,24 @@ void GetAbductCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
- : d_expr(), d_doFull(true)
+ : d_term(), d_doFull(true)
{
}
GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
- const Expr& expr, bool doFull)
- : d_expr(expr), d_doFull(doFull)
+ const api::Term& term, bool doFull)
+ : d_term(term), d_doFull(doFull)
{
}
-Expr GetQuantifierEliminationCommand::getExpr() const { return d_expr; }
+api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
-void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine)
+void GetQuantifierEliminationCommand::invoke(api::Solver* solver)
{
try
{
- d_result =
- smtEngine->getQuantifierElimination(Node::fromExpr(d_expr), d_doFull)
- .toExpr();
+ d_result = api::Term(solver,
+ solver->getSmtEngine()->getQuantifierElimination(
+ d_term.getNode(), d_doFull));
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -2654,7 +2318,10 @@ void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine)
}
}
-Expr GetQuantifierEliminationCommand::getResult() const { return d_result; }
+api::Term GetQuantifierEliminationCommand::getResult() const
+{
+ return d_result;
+}
void GetQuantifierEliminationCommand::printResult(std::ostream& out,
uint32_t verbosity) const
{
@@ -2668,19 +2335,10 @@ void GetQuantifierEliminationCommand::printResult(std::ostream& out,
}
}
-Command* GetQuantifierEliminationCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(
- d_expr.exportTo(exprManager, variableMap), d_doFull);
- c->d_result = d_result;
- return c;
-}
-
Command* GetQuantifierEliminationCommand::clone() const
{
GetQuantifierEliminationCommand* c =
- new GetQuantifierEliminationCommand(d_expr, d_doFull);
+ new GetQuantifierEliminationCommand(d_term, d_doFull);
c->d_result = d_result;
return c;
}
@@ -2697,7 +2355,7 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
- out, Node::fromExpr(d_expr));
+ out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
@@ -2706,16 +2364,11 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out,
GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
-void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine)
+void GetUnsatAssumptionsCommand::invoke(api::Solver* solver)
{
try
{
- std::vector<Node> uassumps = smtEngine->getUnsatAssumptions();
- d_result.clear();
- for (const Node& n : uassumps)
- {
- d_result.push_back(n.toExpr());
- }
+ d_result = solver->getUnsatAssumptions();
d_commandStatus = CommandSuccess::instance();
}
catch (RecoverableModalException& e)
@@ -2728,7 +2381,7 @@ void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine)
}
}
-std::vector<Expr> GetUnsatAssumptionsCommand::getResult() const
+std::vector<api::Term> GetUnsatAssumptionsCommand::getResult() const
{
return d_result;
}
@@ -2746,14 +2399,6 @@ void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
}
}
-Command* GetUnsatAssumptionsCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
- c->d_result = d_result;
- return c;
-}
-
Command* GetUnsatAssumptionsCommand::clone() const
{
GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
@@ -2780,11 +2425,11 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetUnsatCoreCommand::GetUnsatCoreCommand() {}
-void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine)
+void GetUnsatCoreCommand::invoke(api::Solver* solver)
{
try
{
- d_result = smtEngine->getUnsatCore();
+ d_result = solver->getSmtEngine()->getUnsatCore();
d_commandStatus = CommandSuccess::instance();
}
catch (RecoverableModalException& e)
@@ -2816,14 +2461,6 @@ const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const
return d_result;
}
-Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
- c->d_result = d_result;
- return c;
-}
-
Command* GetUnsatCoreCommand::clone() const
{
GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
@@ -2850,14 +2487,14 @@ void GetUnsatCoreCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetAssertionsCommand::GetAssertionsCommand() {}
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine)
+void GetAssertionsCommand::invoke(api::Solver* solver)
{
try
{
stringstream ss;
- const vector<Expr> v = smtEngine->getAssertions();
+ const vector<api::Term> v = solver->getAssertions();
ss << "(\n";
- copy(v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n"));
+ copy(v.begin(), v.end(), ostream_iterator<api::Term>(ss, "\n"));
ss << ")\n";
d_result = ss.str();
d_commandStatus = CommandSuccess::instance();
@@ -2882,14 +2519,6 @@ void GetAssertionsCommand::printResult(std::ostream& out,
}
}
-Command* GetAssertionsCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- GetAssertionsCommand* c = new GetAssertionsCommand();
- c->d_result = d_result;
- return c;
-}
-
Command* GetAssertionsCommand::clone() const
{
GetAssertionsCommand* c = new GetAssertionsCommand();
@@ -2925,14 +2554,13 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
return d_status;
}
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine)
+void SetBenchmarkStatusCommand::invoke(api::Solver* solver)
{
try
{
stringstream ss;
ss << d_status;
- SExpr status = SExpr(ss.str());
- smtEngine->setInfo("status", status);
+ solver->setInfo("status", ss.str());
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -2941,12 +2569,6 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* SetBenchmarkStatusCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- return new SetBenchmarkStatusCommand(d_status);
-}
-
Command* SetBenchmarkStatusCommand::clone() const
{
return new SetBenchmarkStatusCommand(d_status);
@@ -2984,11 +2606,11 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
}
std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine)
+void SetBenchmarkLogicCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->setLogic(d_logic);
+ solver->setLogic(d_logic);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -2997,12 +2619,6 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* SetBenchmarkLogicCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- return new SetBenchmarkLogicCommand(d_logic);
-}
-
Command* SetBenchmarkLogicCommand::clone() const
{
return new SetBenchmarkLogicCommand(d_logic);
@@ -3033,11 +2649,11 @@ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
std::string SetInfoCommand::getFlag() const { return d_flag; }
SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
-void SetInfoCommand::invoke(SmtEngine* smtEngine)
+void SetInfoCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->setInfo(d_flag, d_sexpr);
+ solver->getSmtEngine()->setInfo(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
}
catch (UnrecognizedOptionException&)
@@ -3051,12 +2667,6 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* SetInfoCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new SetInfoCommand(d_flag, d_sexpr);
-}
-
Command* SetInfoCommand::clone() const
{
return new SetInfoCommand(d_flag, d_sexpr);
@@ -3079,13 +2689,13 @@ void SetInfoCommand::toStream(std::ostream& out,
GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
std::string GetInfoCommand::getFlag() const { return d_flag; }
-void GetInfoCommand::invoke(SmtEngine* smtEngine)
+void GetInfoCommand::invoke(api::Solver* solver)
{
try
{
vector<SExpr> v;
v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
- v.push_back(smtEngine->getInfo(d_flag));
+ v.emplace_back(solver->getSmtEngine()->getInfo(d_flag));
stringstream ss;
if (d_flag == "all-options" || d_flag == "all-statistics")
{
@@ -3122,14 +2732,6 @@ void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* GetInfoCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- GetInfoCommand* c = new GetInfoCommand(d_flag);
- c->d_result = d_result;
- return c;
-}
-
Command* GetInfoCommand::clone() const
{
GetInfoCommand* c = new GetInfoCommand(d_flag);
@@ -3159,11 +2761,11 @@ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
std::string SetOptionCommand::getFlag() const { return d_flag; }
SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
-void SetOptionCommand::invoke(SmtEngine* smtEngine)
+void SetOptionCommand::invoke(api::Solver* solver)
{
try
{
- smtEngine->setOption(d_flag, d_sexpr);
+ solver->getSmtEngine()->setOption(d_flag, d_sexpr);
d_commandStatus = CommandSuccess::instance();
}
catch (UnrecognizedOptionException&)
@@ -3176,12 +2778,6 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine)
}
}
-Command* SetOptionCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new SetOptionCommand(d_flag, d_sexpr);
-}
-
Command* SetOptionCommand::clone() const
{
return new SetOptionCommand(d_flag, d_sexpr);
@@ -3204,12 +2800,11 @@ void SetOptionCommand::toStream(std::ostream& out,
GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
std::string GetOptionCommand::getFlag() const { return d_flag; }
-void GetOptionCommand::invoke(SmtEngine* smtEngine)
+void GetOptionCommand::invoke(api::Solver* solver)
{
try
{
- SExpr res = smtEngine->getOption(d_flag);
- d_result = res.toString();
+ d_result = solver->getOption(d_flag);
d_commandStatus = CommandSuccess::instance();
}
catch (UnrecognizedOptionException&)
@@ -3235,14 +2830,6 @@ void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
}
}
-Command* GetOptionCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- GetOptionCommand* c = new GetOptionCommand(d_flag);
- c->d_result = d_result;
- return c;
-}
-
Command* GetOptionCommand::clone() const
{
GetOptionCommand* c = new GetOptionCommand(d_flag);
@@ -3265,28 +2852,21 @@ void GetOptionCommand::toStream(std::ostream& out,
/* class SetExpressionNameCommand */
/* -------------------------------------------------------------------------- */
-SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name)
- : d_expr(expr), d_name(name)
+SetExpressionNameCommand::SetExpressionNameCommand(api::Term term,
+ std::string name)
+ : d_term(term), d_name(name)
{
}
-void SetExpressionNameCommand::invoke(SmtEngine* smtEngine)
+void SetExpressionNameCommand::invoke(api::Solver* solver)
{
- smtEngine->setExpressionName(d_expr, d_name);
+ solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name);
d_commandStatus = CommandSuccess::instance();
}
-Command* SetExpressionNameCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- SetExpressionNameCommand* c = new SetExpressionNameCommand(
- d_expr.exportTo(exprManager, variableMap), d_name);
- return c;
-}
-
Command* SetExpressionNameCommand::clone() const
{
- SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name);
+ SetExpressionNameCommand* c = new SetExpressionNameCommand(d_term, d_name);
return c;
}
@@ -3302,42 +2882,36 @@ void SetExpressionNameCommand::toStream(std::ostream& out,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdSetExpressionName(
- out, Node::fromExpr(d_expr), d_name);
+ out, d_term.getNode(), d_name);
}
/* -------------------------------------------------------------------------- */
/* class DatatypeDeclarationCommand */
/* -------------------------------------------------------------------------- */
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const Type& datatype)
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(
+ const api::Sort& datatype)
: d_datatypes()
{
d_datatypes.push_back(datatype);
}
DatatypeDeclarationCommand::DatatypeDeclarationCommand(
- const std::vector<Type>& datatypes)
+ const std::vector<api::Sort>& datatypes)
: d_datatypes(datatypes)
{
}
-const std::vector<Type>& DatatypeDeclarationCommand::getDatatypes() const
+const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const
{
return d_datatypes;
}
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine)
+void DatatypeDeclarationCommand::invoke(api::Solver* solver)
{
d_commandStatus = CommandSuccess::instance();
}
-Command* DatatypeDeclarationCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- throw ExportUnsupportedException(
- "export of DatatypeDeclarationCommand unsupported");
-}
-
Command* DatatypeDeclarationCommand::clone() const
{
return new DatatypeDeclarationCommand(d_datatypes);
@@ -3355,7 +2929,7 @@ void DatatypeDeclarationCommand::toStream(std::ostream& out,
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
- out, typeVectorToTypeNodes(d_datatypes));
+ out, api::sortVectorToTypeNodes(d_datatypes));
}
} // namespace CVC4
diff --git a/src/smt/command.h b/src/smt/command.h
index 40853d323..32cf70602 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -200,8 +200,8 @@ class CVC4_PUBLIC Command
virtual ~Command();
- virtual void invoke(SmtEngine* smtEngine) = 0;
- virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
+ virtual void invoke(api::Solver* solver) = 0;
+ virtual void invoke(api::Solver* solver, std::ostream& out);
virtual void toStream(
std::ostream& out,
@@ -244,37 +244,10 @@ class CVC4_PUBLIC Command
virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const;
/**
- * Maps this Command into one for a different ExprManager, using
- * variableMap for the translation and extending it with any new
- * mappings.
- */
- virtual Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) = 0;
-
- /**
* Clone this Command (make a shallow copy).
*/
virtual Command* clone() const = 0;
- protected:
- class ExportTransformer
- {
- ExprManager* d_exprManager;
- ExprManagerMapCollection& d_variableMap;
-
- public:
- ExportTransformer(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
- : d_exprManager(exprManager), d_variableMap(variableMap)
- {
- }
- Expr operator()(Expr e) { return e.exportTo(d_exprManager, d_variableMap); }
- Type operator()(Type t) { return t.exportTo(d_exprManager, d_variableMap); }
- }; /* class Command::ExportTransformer */
-
- /** The solver instance that this command is associated with. */
- const api::Solver* d_solver;
-
/**
* This field contains a command status if the command has been
* invoked, or NULL if it has not. This field is either a
@@ -301,9 +274,7 @@ class CVC4_PUBLIC EmptyCommand : public Command
public:
EmptyCommand(std::string name = "");
std::string getName() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -324,10 +295,9 @@ class CVC4_PUBLIC EchoCommand : public Command
std::string getOutput() const;
- void invoke(SmtEngine* smtEngine) override;
- void invoke(SmtEngine* smtEngine, std::ostream& out) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
+ void invoke(api::Solver* solver, std::ostream& out) override;
+
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -344,17 +314,16 @@ class CVC4_PUBLIC EchoCommand : public Command
class CVC4_PUBLIC AssertCommand : public Command
{
protected:
- Expr d_expr;
+ api::Term d_term;
bool d_inUnsatCore;
public:
- AssertCommand(const Expr& e, bool inUnsatCore = true);
+ AssertCommand(const api::Term& t, bool inUnsatCore = true);
- Expr getExpr() const;
+ api::Term getTerm() const;
+
+ void invoke(api::Solver* solver) override;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -368,9 +337,7 @@ class CVC4_PUBLIC AssertCommand : public Command
class CVC4_PUBLIC PushCommand : public Command
{
public:
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -384,9 +351,7 @@ class CVC4_PUBLIC PushCommand : public Command
class CVC4_PUBLIC PopCommand : public Command
{
public:
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -405,29 +370,27 @@ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command
public:
DeclarationDefinitionCommand(const std::string& id);
- void invoke(SmtEngine* smtEngine) override = 0;
+ void invoke(api::Solver* solver) override = 0;
std::string getSymbol() const;
}; /* class DeclarationDefinitionCommand */
class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
{
protected:
- Expr d_func;
- Type d_type;
+ api::Term d_func;
+ api::Sort d_sort;
bool d_printInModel;
bool d_printInModelSetByUser;
public:
- DeclareFunctionCommand(const std::string& id, Expr func, Type type);
- Expr getFunction() const;
- Type getType() const;
+ DeclareFunctionCommand(const std::string& id, api::Term func, api::Sort sort);
+ api::Term getFunction() const;
+ api::Sort getSort() const;
bool getPrintInModel() const;
bool getPrintInModelSetByUser() const;
void setPrintInModel(bool p);
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -438,21 +401,19 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DeclareFunctionCommand */
-class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand
+class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand
{
protected:
size_t d_arity;
- Type d_type;
+ api::Sort d_sort;
public:
- DeclareTypeCommand(const std::string& id, size_t arity, Type t);
+ DeclareSortCommand(const std::string& id, size_t arity, api::Sort sort);
size_t getArity() const;
- Type getType() const;
+ api::Sort getSort() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -461,26 +422,24 @@ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand
bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
-}; /* class DeclareTypeCommand */
+}; /* class DeclareSortCommand */
-class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand
+class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand
{
protected:
- std::vector<Type> d_params;
- Type d_type;
+ std::vector<api::Sort> d_params;
+ api::Sort d_sort;
public:
- DefineTypeCommand(const std::string& id, Type t);
- DefineTypeCommand(const std::string& id,
- const std::vector<Type>& params,
- Type t);
+ DefineSortCommand(const std::string& id, api::Sort sort);
+ DefineSortCommand(const std::string& id,
+ const std::vector<api::Sort>& params,
+ api::Sort sort);
- const std::vector<Type>& getParameters() const;
- Type getType() const;
+ const std::vector<api::Sort>& getParameters() const;
+ api::Sort getSort() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -489,28 +448,26 @@ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand
bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
-}; /* class DefineTypeCommand */
+}; /* class DefineSortCommand */
class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
{
public:
DefineFunctionCommand(const std::string& id,
- Expr func,
- Expr formula,
+ api::Term func,
+ api::Term formula,
bool global);
DefineFunctionCommand(const std::string& id,
- Expr func,
- const std::vector<Expr>& formals,
- Expr formula,
+ api::Term func,
+ const std::vector<api::Term>& formals,
+ api::Term formula,
bool global);
- Expr getFunction() const;
- const std::vector<Expr>& getFormals() const;
- Expr getFormula() const;
+ api::Term getFunction() const;
+ const std::vector<api::Term>& getFormals() const;
+ api::Term getFormula() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -522,11 +479,11 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
protected:
/** The function we are defining */
- Expr d_func;
+ api::Term d_func;
/** The formal arguments for the function we are defining */
- std::vector<Expr> d_formals;
+ std::vector<api::Term> d_formals;
/** The formula corresponding to the body of the function we are defining */
- Expr d_formula;
+ api::Term d_formula;
/**
* Stores whether this definition is global (i.e. should persist when
* popping the user context.
@@ -543,13 +500,11 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
{
public:
DefineNamedFunctionCommand(const std::string& id,
- Expr func,
- const std::vector<Expr>& formals,
- Expr formula,
+ api::Term func,
+ const std::vector<api::Term>& formals,
+ api::Term formula,
bool global);
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
void toStream(
std::ostream& out,
@@ -567,13 +522,11 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
class CVC4_PUBLIC DefineFunctionRecCommand : public Command
{
public:
- DefineFunctionRecCommand(const api::Solver* solver,
- api::Term func,
+ DefineFunctionRecCommand(api::Term func,
const std::vector<api::Term>& formals,
api::Term formula,
bool global);
- DefineFunctionRecCommand(const api::Solver* solver,
- const std::vector<api::Term>& funcs,
+ DefineFunctionRecCommand(const std::vector<api::Term>& funcs,
const std::vector<std::vector<api::Term> >& formals,
const std::vector<api::Term>& formula,
bool global);
@@ -582,9 +535,7 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command
const std::vector<std::vector<api::Term> >& getFormals() const;
const std::vector<api::Term>& getFormulas() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -615,17 +566,15 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command
class CVC4_PUBLIC SetUserAttributeCommand : public Command
{
public:
- SetUserAttributeCommand(const std::string& attr, Expr expr);
+ SetUserAttributeCommand(const std::string& attr, api::Term term);
SetUserAttributeCommand(const std::string& attr,
- Expr expr,
- const std::vector<Expr>& values);
+ api::Term term,
+ const std::vector<api::Term>& values);
SetUserAttributeCommand(const std::string& attr,
- Expr expr,
+ api::Term term,
const std::string& value);
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -637,14 +586,14 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command
private:
SetUserAttributeCommand(const std::string& attr,
- Expr expr,
- const std::vector<Expr>& expr_values,
- const std::string& str_value);
+ api::Term term,
+ const std::vector<api::Term>& termValues,
+ const std::string& strValue);
const std::string d_attr;
- const Expr d_expr;
- const std::vector<Expr> d_expr_values;
- const std::string d_str_value;
+ const api::Term d_term;
+ const std::vector<api::Term> d_termValues;
+ const std::string d_strValue;
}; /* class SetUserAttributeCommand */
/**
@@ -655,14 +604,12 @@ class CVC4_PUBLIC CheckSatCommand : public Command
{
public:
CheckSatCommand();
- CheckSatCommand(const Expr& expr);
+ CheckSatCommand(const api::Term& term);
- Expr getExpr() const;
- Result getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ api::Term getTerm() const;
+ api::Result getResult() const;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -673,8 +620,8 @@ class CVC4_PUBLIC CheckSatCommand : public Command
OutputLanguage language = language::output::LANG_AUTO) const override;
private:
- Expr d_expr;
- Result d_result;
+ api::Term d_term;
+ api::Result d_result;
}; /* class CheckSatCommand */
/**
@@ -685,15 +632,13 @@ class CVC4_PUBLIC CheckSatCommand : public Command
class CVC4_PUBLIC CheckSatAssumingCommand : public Command
{
public:
- CheckSatAssumingCommand(Expr term);
- CheckSatAssumingCommand(const std::vector<Expr>& terms);
+ CheckSatAssumingCommand(api::Term term);
+ CheckSatAssumingCommand(const std::vector<api::Term>& terms);
- const std::vector<Expr>& getTerms() const;
- Result getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ const std::vector<api::Term>& getTerms() const;
+ api::Result getResult() const;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -704,26 +649,24 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command
OutputLanguage language = language::output::LANG_AUTO) const override;
private:
- std::vector<Expr> d_terms;
- Result d_result;
+ std::vector<api::Term> d_terms;
+ api::Result d_result;
}; /* class CheckSatAssumingCommand */
class CVC4_PUBLIC QueryCommand : public Command
{
protected:
- Expr d_expr;
- Result d_result;
+ api::Term d_term;
+ api::Result d_result;
bool d_inUnsatCore;
public:
- QueryCommand(const Expr& e, bool inUnsatCore = true);
+ QueryCommand(const api::Term& t, bool inUnsatCore = true);
- Expr getExpr() const;
- Result getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ api::Term getTerm() const;
+ api::Result getResult() const;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -740,20 +683,17 @@ class CVC4_PUBLIC QueryCommand : public Command
class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
{
public:
- DeclareSygusVarCommand(const std::string& id, Expr var, Type type);
+ DeclareSygusVarCommand(const std::string& id, api::Term var, api::Sort sort);
/** returns the declared variable */
- Expr getVar() const;
- /** returns the declared variable's type */
- Type getType() const;
+ api::Term getVar() const;
+ /** returns the declared variable's sort */
+ api::Sort getSort() const;
/** invokes this command
*
* The declared sygus variable is communicated to the SMT engine in case a
* synthesis conjecture is built later on.
*/
- void invoke(SmtEngine* smtEngine) override;
- /** exports command to given expression manager */
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
/** creates a copy of this command */
Command* clone() const override;
/** returns this command's name */
@@ -768,9 +708,9 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
protected:
/** the declared variable */
- Expr d_var;
- /** the declared variable's type */
- Type d_type;
+ api::Term d_var;
+ /** the declared variable's sort */
+ api::Sort d_sort;
};
/** Declares a sygus function-to-synthesize
@@ -781,8 +721,7 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
{
public:
- SynthFunCommand(const api::Solver* solver,
- const std::string& id,
+ SynthFunCommand(const std::string& id,
api::Term fun,
const std::vector<api::Term>& vars,
api::Sort sort,
@@ -804,10 +743,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
* The declared function-to-synthesize is communicated to the SMT engine in
* case a synthesis conjecture is built later on.
*/
- void invoke(SmtEngine* smtEngine) override;
- /** exports command to given expression manager */
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
/** creates a copy of this command */
Command* clone() const override;
/** returns this command's name */
@@ -837,18 +773,15 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
class CVC4_PUBLIC SygusConstraintCommand : public Command
{
public:
- SygusConstraintCommand(const Expr& e);
+ SygusConstraintCommand(const api::Term& t);
/** returns the declared constraint */
- Expr getExpr() const;
+ api::Term getTerm() const;
/** invokes this command
*
* The declared constraint is communicated to the SMT engine in case a
* synthesis conjecture is built later on.
*/
- void invoke(SmtEngine* smtEngine) override;
- /** exports command to given expression manager */
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
/** creates a copy of this command */
Command* clone() const override;
/** returns this command's name */
@@ -863,7 +796,7 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command
protected:
/** the declared constraint */
- Expr d_expr;
+ api::Term d_term;
};
/** Declares a sygus invariant constraint
@@ -879,23 +812,20 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command
class CVC4_PUBLIC SygusInvConstraintCommand : public Command
{
public:
- SygusInvConstraintCommand(const std::vector<Expr>& predicates);
- SygusInvConstraintCommand(const Expr& inv,
- const Expr& pre,
- const Expr& trans,
- const Expr& post);
+ SygusInvConstraintCommand(const std::vector<api::Term>& predicates);
+ SygusInvConstraintCommand(const api::Term& inv,
+ const api::Term& pre,
+ const api::Term& trans,
+ const api::Term& post);
/** returns the place holder predicates */
- const std::vector<Expr>& getPredicates() const;
+ const std::vector<api::Term>& getPredicates() const;
/** invokes this command
*
* The place holders are communicated to the SMT engine and the actual
* invariant constraint is built, in case an actual synthesis conjecture is
* built later on.
*/
- void invoke(SmtEngine* smtEngine) override;
- /** exports command to given expression manager */
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
/** creates a copy of this command */
Command* clone() const override;
/** returns this command's name */
@@ -912,7 +842,7 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command
/** the place holder predicates with which to build the actual constraint
* (i.e. the invariant, precondition, transition relation and postcondition)
*/
- std::vector<Expr> d_predicates;
+ std::vector<api::Term> d_predicates;
};
/** Declares a synthesis conjecture */
@@ -921,7 +851,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command
public:
CheckSynthCommand(){};
/** returns the result of the check-synth call */
- Result getResult() const;
+ api::Result getResult() const;
/** prints the result of the check-synth-call */
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
/** invokes this command
@@ -932,10 +862,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command
* and then perform a satisfiability check, whose result is stored in
* d_result.
*/
- void invoke(SmtEngine* smtEngine) override;
- /** exports command to given expression manager */
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
/** creates a copy of this command */
Command* clone() const override;
/** returns this command's name */
@@ -950,7 +877,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command
protected:
/** result of the check-synth call */
- Result d_result;
+ api::Result d_result;
/** string stream that stores the output of the solution */
std::stringstream d_solution;
};
@@ -961,18 +888,16 @@ class CVC4_PUBLIC CheckSynthCommand : public Command
class CVC4_PUBLIC SimplifyCommand : public Command
{
protected:
- Expr d_term;
- Expr d_result;
+ api::Term d_term;
+ api::Term d_result;
public:
- SimplifyCommand(Expr term);
+ SimplifyCommand(api::Term term);
- Expr getTerm() const;
- Expr getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ api::Term getTerm() const;
+ api::Term getResult() const;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -986,18 +911,16 @@ class CVC4_PUBLIC SimplifyCommand : public Command
class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
{
protected:
- Expr d_term;
- Expr d_result;
+ api::Term d_term;
+ api::Term d_result;
public:
- ExpandDefinitionsCommand(Expr term);
+ ExpandDefinitionsCommand(api::Term term);
- Expr getTerm() const;
- Expr getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ api::Term getTerm() const;
+ api::Term getResult() const;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1011,19 +934,17 @@ class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
class CVC4_PUBLIC GetValueCommand : public Command
{
protected:
- std::vector<Expr> d_terms;
- Expr d_result;
+ std::vector<api::Term> d_terms;
+ api::Term d_result;
public:
- GetValueCommand(Expr term);
- GetValueCommand(const std::vector<Expr>& terms);
+ GetValueCommand(api::Term term);
+ GetValueCommand(const std::vector<api::Term>& terms);
- const std::vector<Expr>& getTerms() const;
- Expr getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ const std::vector<api::Term>& getTerms() const;
+ api::Term getResult() const;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1043,10 +964,8 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command
GetAssignmentCommand();
SExpr getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1064,10 +983,8 @@ class CVC4_PUBLIC GetModelCommand : public Command
// Model is private to the library -- for now
// Model* getResult() const ;
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1088,9 +1005,7 @@ class CVC4_PUBLIC BlockModelCommand : public Command
public:
BlockModelCommand();
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1105,12 +1020,10 @@ class CVC4_PUBLIC BlockModelCommand : public Command
class CVC4_PUBLIC BlockModelValuesCommand : public Command
{
public:
- BlockModelValuesCommand(const std::vector<Expr>& terms);
+ BlockModelValuesCommand(const std::vector<api::Term>& terms);
- const std::vector<Expr>& getTerms() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ const std::vector<api::Term>& getTerms() const;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1122,7 +1035,7 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command
protected:
/** The terms we are blocking */
- std::vector<Expr> d_terms;
+ std::vector<api::Term> d_terms;
}; /* class BlockModelValuesCommand */
class CVC4_PUBLIC GetProofCommand : public Command
@@ -1130,9 +1043,7 @@ class CVC4_PUBLIC GetProofCommand : public Command
public:
GetProofCommand();
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1148,10 +1059,8 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command
public:
GetInstantiationsCommand();
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1170,10 +1079,8 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
public:
GetSynthSolutionCommand();
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1199,14 +1106,9 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
class CVC4_PUBLIC GetInterpolCommand : public Command
{
public:
- GetInterpolCommand(const api::Solver* solver,
- const std::string& name,
- api::Term conj);
+ GetInterpolCommand(const std::string& name, api::Term conj);
/** The argument g is the grammar of the interpolation query */
- GetInterpolCommand(const api::Solver* solver,
- const std::string& name,
- api::Term conj,
- api::Grammar* g);
+ GetInterpolCommand(const std::string& name, api::Term conj, api::Grammar* g);
/** Get the conjecture of the interpolation query */
api::Term getConjecture() const;
@@ -1216,10 +1118,8 @@ class CVC4_PUBLIC GetInterpolCommand : public Command
* query. */
api::Term getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1257,13 +1157,8 @@ class CVC4_PUBLIC GetInterpolCommand : public Command
class CVC4_PUBLIC GetAbductCommand : public Command
{
public:
- GetAbductCommand(const api::Solver* solver,
- const std::string& name,
- api::Term conj);
- GetAbductCommand(const api::Solver* solver,
- const std::string& name,
- api::Term conj,
- api::Grammar* g);
+ GetAbductCommand(const std::string& name, api::Term conj);
+ GetAbductCommand(const std::string& name, api::Term conj, api::Grammar* g);
/** Get the conjecture of the abduction query */
api::Term getConjecture() const;
@@ -1275,10 +1170,8 @@ class CVC4_PUBLIC GetAbductCommand : public Command
*/
api::Term getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1304,22 +1197,20 @@ class CVC4_PUBLIC GetAbductCommand : public Command
class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
{
protected:
- Expr d_expr;
+ api::Term d_term;
bool d_doFull;
- Expr d_result;
+ api::Term d_result;
public:
GetQuantifierEliminationCommand();
- GetQuantifierEliminationCommand(const Expr& expr, bool doFull);
+ GetQuantifierEliminationCommand(const api::Term& term, bool doFull);
- Expr getExpr() const;
+ api::Term getTerm() const;
bool getDoFull() const;
- void invoke(SmtEngine* smtEngine) override;
- Expr getResult() const;
+ void invoke(api::Solver* solver) override;
+ api::Term getResult() const;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1334,11 +1225,9 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
{
public:
GetUnsatAssumptionsCommand();
- void invoke(SmtEngine* smtEngine) override;
- std::vector<Expr> getResult() const;
+ void invoke(api::Solver* solver) override;
+ std::vector<api::Term> getResult() const;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1349,7 +1238,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
- std::vector<Expr> d_result;
+ std::vector<api::Term> d_result;
}; /* class GetUnsatAssumptionsCommand */
class CVC4_PUBLIC GetUnsatCoreCommand : public Command
@@ -1358,11 +1247,9 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
GetUnsatCoreCommand();
const UnsatCore& getUnsatCore() const;
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1385,11 +1272,9 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command
public:
GetAssertionsCommand();
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
std::string getResult() const;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1410,9 +1295,7 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
BenchmarkStatus getStatus() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1432,9 +1315,7 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
SetBenchmarkLogicCommand(std::string logic);
std::string getLogic() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1457,9 +1338,7 @@ class CVC4_PUBLIC SetInfoCommand : public Command
std::string getFlag() const;
SExpr getSExpr() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1482,10 +1361,8 @@ class CVC4_PUBLIC GetInfoCommand : public Command
std::string getFlag() const;
std::string getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1508,9 +1385,7 @@ class CVC4_PUBLIC SetOptionCommand : public Command
std::string getFlag() const;
SExpr getSExpr() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1533,10 +1408,8 @@ class CVC4_PUBLIC GetOptionCommand : public Command
std::string getFlag() const;
std::string getResult() const;
- void invoke(SmtEngine* smtEngine) override;
+ void invoke(api::Solver* solver) override;
void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1557,15 +1430,13 @@ class CVC4_PUBLIC GetOptionCommand : public Command
class CVC4_PUBLIC SetExpressionNameCommand : public Command
{
protected:
- Expr d_expr;
+ api::Term d_term;
std::string d_name;
public:
- SetExpressionNameCommand(Expr expr, std::string name);
+ SetExpressionNameCommand(api::Term term, std::string name);
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1579,16 +1450,14 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command
class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
{
private:
- std::vector<Type> d_datatypes;
+ std::vector<api::Sort> d_datatypes;
public:
- DatatypeDeclarationCommand(const Type& datatype);
+ DatatypeDeclarationCommand(const api::Sort& datatype);
- DatatypeDeclarationCommand(const std::vector<Type>& datatypes);
- const std::vector<Type>& getDatatypes() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ DatatypeDeclarationCommand(const std::vector<api::Sort>& datatypes);
+ const std::vector<api::Sort>& getDatatypes() const;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1603,9 +1472,7 @@ class CVC4_PUBLIC ResetCommand : public Command
{
public:
ResetCommand() {}
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1620,9 +1487,7 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command
{
public:
ResetAssertionsCommand() {}
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1637,9 +1502,7 @@ class CVC4_PUBLIC QuitCommand : public Command
{
public:
QuitCommand() {}
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1659,9 +1522,7 @@ class CVC4_PUBLIC CommentCommand : public Command
std::string getComment() const;
- void invoke(SmtEngine* smtEngine) override;
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
+ void invoke(api::Solver* solver) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
@@ -1687,8 +1548,8 @@ class CVC4_PUBLIC CommandSequence : public Command
void addCommand(Command* cmd);
void clear();
- void invoke(SmtEngine* smtEngine) override;
- void invoke(SmtEngine* smtEngine, std::ostream& out) override;
+ void invoke(api::Solver* solver) override;
+ void invoke(api::Solver* solver, std::ostream& out) override;
typedef std::vector<Command*>::iterator iterator;
typedef std::vector<Command*>::const_iterator const_iterator;
@@ -1699,8 +1560,6 @@ class CVC4_PUBLIC CommandSequence : public Command
iterator begin();
iterator end();
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index ce17ffc82..1b8789513 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -133,8 +133,6 @@ namespace theory {
class Rewriter;
}/* CVC4::theory namespace */
-std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs);
-
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
// hood): use a type parameter and have check() delegate, or subclass
// SmtEngine and override check()?
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 6f474e24f..e5781cfaa 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -68,7 +68,7 @@ void testGetInfo(api::Solver* solver, const char* s)
assert(c != NULL);
cout << c << endl;
stringstream ss;
- c->invoke(solver->getSmtEngine(), ss);
+ c->invoke(solver, ss);
assert(p->nextCommand() == NULL);
delete p;
delete c;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 40a5e5ded..d118690ed 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1390,7 +1390,6 @@ set(regress_1_tests
regress1/ho/issue4092-sinf.smt2
regress1/ho/issue4134-sinf.smt2
regress1/ho/nested_lambdas-AGT034^2.smt2
- regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
regress1/ho/NUM638^1.smt2
regress1/ho/NUM925^1.p
regress1/ho/soundness_fmf_SYO362^5-delta.p
@@ -2491,6 +2490,8 @@ set(regression_disabled_tests
regress1/crash_burn_locusts.smt2
# regress1/ho/hoa0102.smt2 results in an assertion failure (see issue #1650).
regress1/ho/hoa0102.smt2
+ # unknown after update to commands
+ regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
# issue1048-arrays-int-real.smt2 -- different errors on debug and production.
regress1/issue1048-arrays-int-real.smt2
# times out after update to tangent planes
diff --git a/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 b/test/regress/regress0/smtlib/get-unsat-assumptions.smt2
index 7a8113d8f..ba53610b3 100644
--- a/test/regress/regress0/smtlib/get-unsat-assumptions.smt2
+++ b/test/regress/regress0/smtlib/get-unsat-assumptions.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --incremental
; EXPECT: unsat
; EXPECT: (x x)
; SCRUBBER: sed -e 's/a[1-2]/x/g'
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback