}
}
-// !!! 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 */
/* -------------------------------------------------------------------------- */
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)
{
}
&& 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())));
}
}
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"; }
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); }
/* 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)
}
}
-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"; }
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)
}
}
-Command* PushCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new PushCommand();
-}
-
Command* PushCommand::clone() const { return new PushCommand(); }
std::string PushCommand::getCommandName() const { return "push"; }
/* 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)
}
}
-Command* PopCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new PopCommand();
-}
-
Command* PopCommand::clone() const { return new PopCommand(); }
std::string PopCommand::getCommandName() const { return "pop"; }
/* 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)
}
}
-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())
}
}
-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;
}
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)
}
}
-Result CheckSatAssumingCommand::getResult() const
+api::Result CheckSatAssumingCommand::getResult() const
{
Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
return d_result;
}
}
-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);
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)
}
}
-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())
}
}
-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;
}
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdQuery(out, d_expr);
+ Printer::getPrinter(language)->toStreamCmdQuery(out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
/* -------------------------------------------------------------------------- */
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)
}
}
-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
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,
d_isInv(isInv),
d_grammar(g)
{
- d_solver = solver;
}
api::Term SynthFunCommand::getFunction() const { return d_fun; }
const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
-void SynthFunCommand::invoke(SmtEngine* smtEngine)
+void SynthFunCommand::invoke(api::Solver* solver)
{
try
{
{
vns.push_back(Node::fromExpr(t.getExpr()));
}
- smtEngine->declareSynthFun(
+ solver->getSmtEngine()->declareSynthFun(
d_symbol,
Node::fromExpr(d_fun.getExpr()),
TypeNode::fromType(d_grammar == nullptr
}
}
-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
/* 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)
}
}
-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
size_t dag,
OutputLanguage language) const
{
- Printer::getPrinter(language)->toStreamCmdConstraint(out,
- Node::fromExpr(d_expr));
+ Printer::getPrinter(language)->toStreamCmdConstraint(out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
/* -------------------------------------------------------------------------- */
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();
}
}
}
-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);
{
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)
{
}
}
// 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
// (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)
}
}
-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())
}
}
-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"; }
/* 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)
}
}
-Command* ResetCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new ResetCommand();
-}
-
Command* ResetCommand::clone() const { return new ResetCommand(); }
std::string ResetCommand::getCommandName() const { return "reset"; }
/* 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)
}
}
-Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- return new ResetAssertionsCommand();
-}
-
Command* ResetAssertionsCommand::clone() const
{
return new ResetAssertionsCommand();
/* 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"; }
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"; }
}
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
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
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();
/* -------------------------------------------------------------------------- */
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
{
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;
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,
Printer::getPrinter(language)->toStreamCmdDefineType(
out,
d_symbol,
- typeVectorToTypeNodes(d_params),
- TypeNode::fromType(d_type));
+ api::sortVectorToTypeNodes(d_params),
+ TypeNode::fromType(d_sort.getType()));
}
/* -------------------------------------------------------------------------- */
/* -------------------------------------------------------------------------- */
DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
- Expr func,
- Expr formula,
+ api::Term func,
+ api::Term formula,
bool global)
: DeclarationDefinitionCommand(id),
d_func(func),
{
}
-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();
}
}
}
-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(
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());
}
/* -------------------------------------------------------------------------- */
/* -------------------------------------------------------------------------- */
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(
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());
}
/* -------------------------------------------------------------------------- */
/* -------------------------------------------------------------------------- */
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);
}
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)
{
}
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)
}
}
-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
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();
}
}
}
-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
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)
}
}
-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())
}
}
-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);
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
{
}
}
-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);
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
// 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)
}
}
-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())
}
}
-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);
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdGetValue(
- out, exprVectorToNodes(d_terms));
+ out, api::termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
/* -------------------------------------------------------------------------- */
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)
{
}
}
-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();
/* -------------------------------------------------------------------------- */
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)
}
}
-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();
/* -------------------------------------------------------------------------- */
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)
}
}
-Command* BlockModelCommand::exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap)
-{
- BlockModelCommand* c = new BlockModelCommand();
- return c;
-}
-
Command* BlockModelCommand::clone() const
{
BlockModelCommand* c = new BlockModelCommand();
/* class BlockModelValuesCommand */
/* -------------------------------------------------------------------------- */
-BlockModelValuesCommand::BlockModelValuesCommand(const std::vector<Expr>& terms)
+BlockModelValuesCommand::BlockModelValuesCommand(
+ const std::vector<api::Term>& terms)
: d_terms(terms)
{
PrettyCheckArgument(terms.size() >= 1,
"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)
}
}
-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);
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdBlockModelValues(
- out, exprVectorToNodes(d_terms));
+ out, api::termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
/* -------------------------------------------------------------------------- */
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();
/* -------------------------------------------------------------------------- */
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)
}
}
-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();
/* -------------------------------------------------------------------------- */
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)
}
}
-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();
/* 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)
{
}
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();
}
}
}
-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;
/* 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)
{
}
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();
}
}
}
-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;
/* -------------------------------------------------------------------------- */
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)
}
}
-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
{
}
}
-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;
}
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
- out, Node::fromExpr(d_expr));
+ out, d_term.getNode());
}
/* -------------------------------------------------------------------------- */
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)
}
}
-std::vector<Expr> GetUnsatAssumptionsCommand::getResult() const
+std::vector<api::Term> GetUnsatAssumptionsCommand::getResult() const
{
return d_result;
}
}
}
-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;
/* -------------------------------------------------------------------------- */
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)
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;
/* -------------------------------------------------------------------------- */
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();
}
}
-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();
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)
}
}
-Command* SetBenchmarkStatusCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- return new SetBenchmarkStatusCommand(d_status);
-}
-
Command* SetBenchmarkStatusCommand::clone() const
{
return new SetBenchmarkStatusCommand(d_status);
}
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)
}
}
-Command* SetBenchmarkLogicCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
-{
- return new SetBenchmarkLogicCommand(d_logic);
-}
-
Command* SetBenchmarkLogicCommand::clone() const
{
return new SetBenchmarkLogicCommand(d_logic);
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&)
}
}
-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);
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")
{
}
}
-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);
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&)
}
}
-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);
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&)
}
}
-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);
/* 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;
}
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);
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
- out, typeVectorToTypeNodes(d_datatypes));
+ out, api::sortVectorToTypeNodes(d_datatypes));
}
} // namespace CVC4
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,
const CommandStatus* getCommandStatus() const { return d_commandStatus; }
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
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(
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(
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(
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(
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(
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(
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(
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(
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(
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.
{
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,
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);
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(
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(
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 */
/**
{
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(
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 */
/**
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(
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(
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 */
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
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,
* 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 */
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 */
protected:
/** the declared constraint */
- Expr d_expr;
+ api::Term d_term;
};
/** Declares a sygus invariant constraint
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 */
/** 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 */
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
* 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 */
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;
};
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(
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(
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(
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(
// 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(
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(
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(
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
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(
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(
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(
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;
* 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(
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;
*/
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(
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(
{
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(
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
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(
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(
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(
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(
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(
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(
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(
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(
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(
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(
{
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(
{
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(
{
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(
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(
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;
iterator begin();
iterator end();
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
void toStream(
projects / cvc5.git / commitdiff