src/smt/command.cpp

   1 /*********************                                                        */
   2 /*! \file command.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of command objects.
  13  **
  14  ** Implementation of command objects.
  15  **/
  16
  17 #include "smt/command.h"
  18
  19 #include <exception>
  20 #include <iostream>
  21 #include <iterator>
  22 #include <sstream>
  23 #include <utility>
  24 #include <vector>
  25
  26 #include "api/cvc4cpp.h"
  27 #include "base/check.h"
  28 #include "base/output.h"
  29 #include "expr/expr_iomanip.h"
  30 #include "expr/node.h"
  31 #include "expr/type.h"
  32 #include "options/options.h"
  33 #include "options/smt_options.h"
  34 #include "printer/printer.h"
  35 #include "smt/dump.h"
  36 #include "smt/model.h"
  37 #include "smt/smt_engine.h"
  38 #include "smt/smt_engine_scope.h"
  39 #include "util/sexpr.h"
  40 #include "util/utility.h"
  41
  42 using namespace std;
  43
  44 namespace CVC4 {
  45
  46 const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
  47 const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
  48 const CommandInterrupted* CommandInterrupted::s_instance =
  49     new CommandInterrupted();
  50
  51 std::ostream& operator<<(std::ostream& out, const Command& c)
  52 {
  53   c.toStream(out,
  54              Node::setdepth::getDepth(out),
  55              Node::printtypes::getPrintTypes(out),
  56              Node::dag::getDag(out),
  57              Node::setlanguage::getLanguage(out));
  58   return out;
  59 }
  60
  61 ostream& operator<<(ostream& out, const Command* c)
  62 {
  63   if (c == NULL)
  64   {
  65     out << "null";
  66   }
  67   else
  68   {
  69     out << *c;
  70   }
  71   return out;
  72 }
  73
  74 std::ostream& operator<<(std::ostream& out, const CommandStatus& s)
  75 {
  76   s.toStream(out, Node::setlanguage::getLanguage(out));
  77   return out;
  78 }
  79
  80 ostream& operator<<(ostream& out, const CommandStatus* s)
  81 {
  82   if (s == NULL)
  83   {
  84     out << "null";
  85   }
  86   else
  87   {
  88     out << *s;
  89   }
  90   return out;
  91 }
  92
  93 /* output stream insertion operator for benchmark statuses */
  94 std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
  95 {
  96   switch (status)
  97   {
  98     case SMT_SATISFIABLE: return out << "sat";
  99
 100     case SMT_UNSATISFIABLE: return out << "unsat";
 101
 102     case SMT_UNKNOWN: return out << "unknown";
 103
 104     default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
 105   }
 106 }
 107
 108 // !!! Temporary until commands are migrated to the new API !!!
 109 std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs)
 110 {
 111   std::vector<Node> nodes;
 112   nodes.reserve(exprs.size());
 113
 114   for (Expr e : exprs)
 115   {
 116     nodes.push_back(Node::fromExpr(e));
 117   }
 118
 119   return nodes;
 120 }
 121
 122 // !!! Temporary until commands are migrated to the new API !!!
 123 std::vector<TypeNode> typeVectorToTypeNodes(const std::vector<Type>& types)
 124 {
 125   std::vector<TypeNode> typeNodes;
 126   typeNodes.reserve(types.size());
 127
 128   for (Type t : types)
 129   {
 130     typeNodes.push_back(TypeNode::fromType(t));
 131   }
 132
 133   return typeNodes;
 134 }
 135
 136 /* -------------------------------------------------------------------------- */
 137 /* class CommandPrintSuccess                                                  */
 138 /* -------------------------------------------------------------------------- */
 139
 140 void CommandPrintSuccess::applyPrintSuccess(std::ostream& out)
 141 {
 142   out.iword(s_iosIndex) = d_printSuccess;
 143 }
 144
 145 bool CommandPrintSuccess::getPrintSuccess(std::ostream& out)
 146 {
 147   return out.iword(s_iosIndex);
 148 }
 149
 150 void CommandPrintSuccess::setPrintSuccess(std::ostream& out, bool printSuccess)
 151 {
 152   out.iword(s_iosIndex) = printSuccess;
 153 }
 154
 155 std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
 156 {
 157   cps.applyPrintSuccess(out);
 158   return out;
 159 }
 160
 161 /* -------------------------------------------------------------------------- */
 162 /* class Command                                                              */
 163 /* -------------------------------------------------------------------------- */
 164
 165 Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
 166
 167 Command::Command(const api::Solver* solver)
 168     : d_solver(solver), d_commandStatus(nullptr), d_muted(false)
 169 {
 170 }
 171
 172 Command::Command(const Command& cmd)
 173 {
 174   d_commandStatus =
 175       (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
 176   d_muted = cmd.d_muted;
 177 }
 178
 179 Command::~Command()
 180 {
 181   if (d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance())
 182   {
 183     delete d_commandStatus;
 184   }
 185 }
 186
 187 bool Command::ok() const
 188 {
 189   // either we haven't run the command yet, or it ran successfully
 190   return d_commandStatus == NULL
 191          || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
 192 }
 193
 194 bool Command::fail() const
 195 {
 196   return d_commandStatus != NULL
 197          && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
 198 }
 199
 200 bool Command::interrupted() const
 201 {
 202   return d_commandStatus != NULL
 203          && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
 204 }
 205
 206 void Command::invoke(SmtEngine* smtEngine, std::ostream& out)
 207 {
 208   invoke(smtEngine);
 209   if (!(isMuted() && ok()))
 210   {
 211     printResult(out,
 212                 smtEngine->getOption("command-verbosity:" + getCommandName())
 213                     .getIntegerValue()
 214                     .toUnsignedInt());
 215   }
 216 }
 217
 218 std::string Command::toString() const
 219 {
 220   std::stringstream ss;
 221   toStream(ss);
 222   return ss.str();
 223 }
 224
 225 void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const
 226 {
 227   Printer::getPrinter(language)->toStream(out, this);
 228 }
 229
 230 void Command::printResult(std::ostream& out, uint32_t verbosity) const
 231 {
 232   if (d_commandStatus != NULL)
 233   {
 234     if ((!ok() && verbosity >= 1) || verbosity >= 2)
 235     {
 236       out << *d_commandStatus;
 237     }
 238   }
 239 }
 240
 241 /* -------------------------------------------------------------------------- */
 242 /* class EmptyCommand                                                         */
 243 /* -------------------------------------------------------------------------- */
 244
 245 EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
 246 std::string EmptyCommand::getName() const { return d_name; }
 247 void EmptyCommand::invoke(SmtEngine* smtEngine)
 248 {
 249   /* empty commands have no implementation */
 250   d_commandStatus = CommandSuccess::instance();
 251 }
 252
 253 Command* EmptyCommand::exportTo(ExprManager* exprManager,
 254                                 ExprManagerMapCollection& variableMap)
 255 {
 256   return new EmptyCommand(d_name);
 257 }
 258
 259 Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
 260 std::string EmptyCommand::getCommandName() const { return "empty"; }
 261
 262 void EmptyCommand::toStream(std::ostream& out,
 263                             int toDepth,
 264                             bool types,
 265                             size_t dag,
 266                             OutputLanguage language) const
 267 {
 268   Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
 269 }
 270
 271 /* -------------------------------------------------------------------------- */
 272 /* class EchoCommand                                                          */
 273 /* -------------------------------------------------------------------------- */
 274
 275 EchoCommand::EchoCommand(std::string output) : d_output(output) {}
 276 std::string EchoCommand::getOutput() const { return d_output; }
 277 void EchoCommand::invoke(SmtEngine* smtEngine)
 278 {
 279   /* we don't have an output stream here, nothing to do */
 280   d_commandStatus = CommandSuccess::instance();
 281 }
 282
 283 void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out)
 284 {
 285   out << d_output << std::endl;
 286   Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
 287                            << std::endl;
 288   d_commandStatus = CommandSuccess::instance();
 289   printResult(out,
 290               smtEngine->getOption("command-verbosity:" + getCommandName())
 291                   .getIntegerValue()
 292                   .toUnsignedInt());
 293 }
 294
 295 Command* EchoCommand::exportTo(ExprManager* exprManager,
 296                                ExprManagerMapCollection& variableMap)
 297 {
 298   return new EchoCommand(d_output);
 299 }
 300
 301 Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
 302 std::string EchoCommand::getCommandName() const { return "echo"; }
 303
 304 void EchoCommand::toStream(std::ostream& out,
 305                            int toDepth,
 306                            bool types,
 307                            size_t dag,
 308                            OutputLanguage language) const
 309 {
 310   Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
 311 }
 312
 313 /* -------------------------------------------------------------------------- */
 314 /* class AssertCommand                                                        */
 315 /* -------------------------------------------------------------------------- */
 316
 317 AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore)
 318     : d_expr(e), d_inUnsatCore(inUnsatCore)
 319 {
 320 }
 321
 322 Expr AssertCommand::getExpr() const { return d_expr; }
 323 void AssertCommand::invoke(SmtEngine* smtEngine)
 324 {
 325   try
 326   {
 327     smtEngine->assertFormula(d_expr, d_inUnsatCore);
 328     d_commandStatus = CommandSuccess::instance();
 329   }
 330   catch (UnsafeInterruptException& e)
 331   {
 332     d_commandStatus = new CommandInterrupted();
 333   }
 334   catch (exception& e)
 335   {
 336     d_commandStatus = new CommandFailure(e.what());
 337   }
 338 }
 339
 340 Command* AssertCommand::exportTo(ExprManager* exprManager,
 341                                  ExprManagerMapCollection& variableMap)
 342 {
 343   return new AssertCommand(d_expr.exportTo(exprManager, variableMap),
 344                            d_inUnsatCore);
 345 }
 346
 347 Command* AssertCommand::clone() const
 348 {
 349   return new AssertCommand(d_expr, d_inUnsatCore);
 350 }
 351
 352 std::string AssertCommand::getCommandName() const { return "assert"; }
 353
 354 void AssertCommand::toStream(std::ostream& out,
 355                              int toDepth,
 356                              bool types,
 357                              size_t dag,
 358                              OutputLanguage language) const
 359 {
 360   Printer::getPrinter(language)->toStreamCmdAssert(out, Node::fromExpr(d_expr));
 361 }
 362
 363 /* -------------------------------------------------------------------------- */
 364 /* class PushCommand                                                          */
 365 /* -------------------------------------------------------------------------- */
 366
 367 void PushCommand::invoke(SmtEngine* smtEngine)
 368 {
 369   try
 370   {
 371     smtEngine->push();
 372     d_commandStatus = CommandSuccess::instance();
 373   }
 374   catch (UnsafeInterruptException& e)
 375   {
 376     d_commandStatus = new CommandInterrupted();
 377   }
 378   catch (exception& e)
 379   {
 380     d_commandStatus = new CommandFailure(e.what());
 381   }
 382 }
 383
 384 Command* PushCommand::exportTo(ExprManager* exprManager,
 385                                ExprManagerMapCollection& variableMap)
 386 {
 387   return new PushCommand();
 388 }
 389
 390 Command* PushCommand::clone() const { return new PushCommand(); }
 391 std::string PushCommand::getCommandName() const { return "push"; }
 392
 393 void PushCommand::toStream(std::ostream& out,
 394                            int toDepth,
 395                            bool types,
 396                            size_t dag,
 397                            OutputLanguage language) const
 398 {
 399   Printer::getPrinter(language)->toStreamCmdPush(out);
 400 }
 401
 402 /* -------------------------------------------------------------------------- */
 403 /* class PopCommand                                                           */
 404 /* -------------------------------------------------------------------------- */
 405
 406 void PopCommand::invoke(SmtEngine* smtEngine)
 407 {
 408   try
 409   {
 410     smtEngine->pop();
 411     d_commandStatus = CommandSuccess::instance();
 412   }
 413   catch (UnsafeInterruptException& e)
 414   {
 415     d_commandStatus = new CommandInterrupted();
 416   }
 417   catch (exception& e)
 418   {
 419     d_commandStatus = new CommandFailure(e.what());
 420   }
 421 }
 422
 423 Command* PopCommand::exportTo(ExprManager* exprManager,
 424                               ExprManagerMapCollection& variableMap)
 425 {
 426   return new PopCommand();
 427 }
 428
 429 Command* PopCommand::clone() const { return new PopCommand(); }
 430 std::string PopCommand::getCommandName() const { return "pop"; }
 431
 432 void PopCommand::toStream(std::ostream& out,
 433                           int toDepth,
 434                           bool types,
 435                           size_t dag,
 436                           OutputLanguage language) const
 437 {
 438   Printer::getPrinter(language)->toStreamCmdPop(out);
 439 }
 440
 441 /* -------------------------------------------------------------------------- */
 442 /* class CheckSatCommand                                                      */
 443 /* -------------------------------------------------------------------------- */
 444
 445 CheckSatCommand::CheckSatCommand() : d_expr() {}
 446
 447 CheckSatCommand::CheckSatCommand(const Expr& expr) : d_expr(expr) {}
 448
 449 Expr CheckSatCommand::getExpr() const { return d_expr; }
 450 void CheckSatCommand::invoke(SmtEngine* smtEngine)
 451 {
 452   Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
 453                            << std::endl;
 454   try
 455   {
 456     d_result = smtEngine->checkSat(d_expr);
 457     d_commandStatus = CommandSuccess::instance();
 458   }
 459   catch (exception& e)
 460   {
 461     d_commandStatus = new CommandFailure(e.what());
 462   }
 463 }
 464
 465 Result CheckSatCommand::getResult() const { return d_result; }
 466 void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
 467 {
 468   if (!ok())
 469   {
 470     this->Command::printResult(out, verbosity);
 471   }
 472   else
 473   {
 474     Trace("dtview::command") << "* RESULT: " << d_result << std::endl;
 475     out << d_result << endl;
 476   }
 477 }
 478
 479 Command* CheckSatCommand::exportTo(ExprManager* exprManager,
 480                                    ExprManagerMapCollection& variableMap)
 481 {
 482   CheckSatCommand* c =
 483       new CheckSatCommand(d_expr.exportTo(exprManager, variableMap));
 484   c->d_result = d_result;
 485   return c;
 486 }
 487
 488 Command* CheckSatCommand::clone() const
 489 {
 490   CheckSatCommand* c = new CheckSatCommand(d_expr);
 491   c->d_result = d_result;
 492   return c;
 493 }
 494
 495 std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
 496
 497 void CheckSatCommand::toStream(std::ostream& out,
 498                                int toDepth,
 499                                bool types,
 500                                size_t dag,
 501                                OutputLanguage language) const
 502 {
 503   Printer::getPrinter(language)->toStreamCmdCheckSat(out,
 504                                                      Node::fromExpr(d_expr));
 505 }
 506
 507 /* -------------------------------------------------------------------------- */
 508 /* class CheckSatAssumingCommand                                              */
 509 /* -------------------------------------------------------------------------- */
 510
 511 CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms({term}) {}
 512
 513 CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms)
 514     : d_terms(terms)
 515 {
 516 }
 517
 518 const std::vector<Expr>& CheckSatAssumingCommand::getTerms() const
 519 {
 520   return d_terms;
 521 }
 522
 523 void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine)
 524 {
 525   Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
 526                            << " )~" << std::endl;
 527   try
 528   {
 529     d_result = smtEngine->checkSat(d_terms);
 530     d_commandStatus = CommandSuccess::instance();
 531   }
 532   catch (exception& e)
 533   {
 534     d_commandStatus = new CommandFailure(e.what());
 535   }
 536 }
 537
 538 Result CheckSatAssumingCommand::getResult() const
 539 {
 540   Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
 541   return d_result;
 542 }
 543
 544 void CheckSatAssumingCommand::printResult(std::ostream& out,
 545                                           uint32_t verbosity) const
 546 {
 547   if (!ok())
 548   {
 549     this->Command::printResult(out, verbosity);
 550   }
 551   else
 552   {
 553     out << d_result << endl;
 554   }
 555 }
 556
 557 Command* CheckSatAssumingCommand::exportTo(
 558     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
 559 {
 560   vector<Expr> exportedTerms;
 561   for (const Expr& e : d_terms)
 562   {
 563     exportedTerms.push_back(e.exportTo(exprManager, variableMap));
 564   }
 565   CheckSatAssumingCommand* c = new CheckSatAssumingCommand(exportedTerms);
 566   c->d_result = d_result;
 567   return c;
 568 }
 569
 570 Command* CheckSatAssumingCommand::clone() const
 571 {
 572   CheckSatAssumingCommand* c = new CheckSatAssumingCommand(d_terms);
 573   c->d_result = d_result;
 574   return c;
 575 }
 576
 577 std::string CheckSatAssumingCommand::getCommandName() const
 578 {
 579   return "check-sat-assuming";
 580 }
 581
 582 void CheckSatAssumingCommand::toStream(std::ostream& out,
 583                                        int toDepth,
 584                                        bool types,
 585                                        size_t dag,
 586                                        OutputLanguage language) const
 587 {
 588   std::vector<Node> nodes;
 589   nodes.reserve(d_terms.size());
 590   for (const Expr& e : d_terms)
 591   {
 592     nodes.push_back(Node::fromExpr(e));
 593   }
 594   Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(out, nodes);
 595 }
 596
 597 /* -------------------------------------------------------------------------- */
 598 /* class QueryCommand                                                         */
 599 /* -------------------------------------------------------------------------- */
 600
 601 QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore)
 602     : d_expr(e), d_inUnsatCore(inUnsatCore)
 603 {
 604 }
 605
 606 Expr QueryCommand::getExpr() const { return d_expr; }
 607 void QueryCommand::invoke(SmtEngine* smtEngine)
 608 {
 609   try
 610   {
 611     d_result = smtEngine->checkEntailed(d_expr);
 612     d_commandStatus = CommandSuccess::instance();
 613   }
 614   catch (exception& e)
 615   {
 616     d_commandStatus = new CommandFailure(e.what());
 617   }
 618 }
 619
 620 Result QueryCommand::getResult() const { return d_result; }
 621 void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
 622 {
 623   if (!ok())
 624   {
 625     this->Command::printResult(out, verbosity);
 626   }
 627   else
 628   {
 629     out << d_result << endl;
 630   }
 631 }
 632
 633 Command* QueryCommand::exportTo(ExprManager* exprManager,
 634                                 ExprManagerMapCollection& variableMap)
 635 {
 636   QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap),
 637                                      d_inUnsatCore);
 638   c->d_result = d_result;
 639   return c;
 640 }
 641
 642 Command* QueryCommand::clone() const
 643 {
 644   QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore);
 645   c->d_result = d_result;
 646   return c;
 647 }
 648
 649 std::string QueryCommand::getCommandName() const { return "query"; }
 650
 651 void QueryCommand::toStream(std::ostream& out,
 652                             int toDepth,
 653                             bool types,
 654                             size_t dag,
 655                             OutputLanguage language) const
 656 {
 657   Printer::getPrinter(language)->toStreamCmdQuery(out, d_expr);
 658 }
 659
 660 /* -------------------------------------------------------------------------- */
 661 /* class DeclareSygusVarCommand */
 662 /* -------------------------------------------------------------------------- */
 663
 664 DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
 665                                                Expr var,
 666                                                Type t)
 667     : DeclarationDefinitionCommand(id), d_var(var), d_type(t)
 668 {
 669 }
 670
 671 Expr DeclareSygusVarCommand::getVar() const { return d_var; }
 672 Type DeclareSygusVarCommand::getType() const { return d_type; }
 673
 674 void DeclareSygusVarCommand::invoke(SmtEngine* smtEngine)
 675 {
 676   try
 677   {
 678     smtEngine->declareSygusVar(
 679         d_symbol, Node::fromExpr(d_var), TypeNode::fromType(d_type));
 680     d_commandStatus = CommandSuccess::instance();
 681   }
 682   catch (exception& e)
 683   {
 684     d_commandStatus = new CommandFailure(e.what());
 685   }
 686 }
 687
 688 Command* DeclareSygusVarCommand::exportTo(ExprManager* exprManager,
 689                                           ExprManagerMapCollection& variableMap)
 690 {
 691   return new DeclareSygusVarCommand(d_symbol,
 692                                     d_var.exportTo(exprManager, variableMap),
 693                                     d_type.exportTo(exprManager, variableMap));
 694 }
 695
 696 Command* DeclareSygusVarCommand::clone() const
 697 {
 698   return new DeclareSygusVarCommand(d_symbol, d_var, d_type);
 699 }
 700
 701 std::string DeclareSygusVarCommand::getCommandName() const
 702 {
 703   return "declare-var";
 704 }
 705
 706 void DeclareSygusVarCommand::toStream(std::ostream& out,
 707                                       int toDepth,
 708                                       bool types,
 709                                       size_t dag,
 710                                       OutputLanguage language) const
 711 {
 712   Printer::getPrinter(language)->toStreamCmdDeclareVar(
 713       out, Node::fromExpr(d_var), TypeNode::fromType(d_type));
 714 }
 715
 716 /* -------------------------------------------------------------------------- */
 717 /* class SynthFunCommand                                                      */
 718 /* -------------------------------------------------------------------------- */
 719
 720 SynthFunCommand::SynthFunCommand(const api::Solver* solver,
 721                                  const std::string& id,
 722                                  api::Term fun,
 723                                  const std::vector<api::Term>& vars,
 724                                  api::Sort sort,
 725                                  bool isInv,
 726                                  api::Grammar* g)
 727     : DeclarationDefinitionCommand(id),
 728       d_fun(fun),
 729       d_vars(vars),
 730       d_sort(sort),
 731       d_isInv(isInv),
 732       d_grammar(g)
 733 {
 734   d_solver = solver;
 735 }
 736
 737 api::Term SynthFunCommand::getFunction() const { return d_fun; }
 738
 739 const std::vector<api::Term>& SynthFunCommand::getVars() const
 740 {
 741   return d_vars;
 742 }
 743
 744 api::Sort SynthFunCommand::getSort() const { return d_sort; }
 745 bool SynthFunCommand::isInv() const { return d_isInv; }
 746
 747 const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
 748
 749 void SynthFunCommand::invoke(SmtEngine* smtEngine)
 750 {
 751   try
 752   {
 753     std::vector<Node> vns;
 754     for (const api::Term& t : d_vars)
 755     {
 756       vns.push_back(Node::fromExpr(t.getExpr()));
 757     }
 758     smtEngine->declareSynthFun(
 759         d_symbol,
 760         Node::fromExpr(d_fun.getExpr()),
 761         TypeNode::fromType(d_grammar == nullptr
 762                                ? d_sort.getType()
 763                                : d_grammar->resolve().getType()),
 764         d_isInv,
 765         vns);
 766     d_commandStatus = CommandSuccess::instance();
 767   }
 768   catch (exception& e)
 769   {
 770     d_commandStatus = new CommandFailure(e.what());
 771   }
 772 }
 773
 774 Command* SynthFunCommand::exportTo(ExprManager* exprManager,
 775                                    ExprManagerMapCollection& variableMap)
 776 {
 777   Unimplemented();
 778 }
 779
 780 Command* SynthFunCommand::clone() const
 781 {
 782   return new SynthFunCommand(
 783       d_solver, d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
 784 }
 785
 786 std::string SynthFunCommand::getCommandName() const
 787 {
 788   return d_isInv ? "synth-inv" : "synth-fun";
 789 }
 790
 791 void SynthFunCommand::toStream(std::ostream& out,
 792                                int toDepth,
 793                                bool types,
 794                                size_t dag,
 795                                OutputLanguage language) const
 796 {
 797   std::vector<Node> nodeVars = termVectorToNodes(d_vars);
 798   Printer::getPrinter(language)->toStreamCmdSynthFun(
 799       out,
 800       d_symbol,
 801       nodeVars,
 802       TypeNode::fromType(d_sort.getType()),
 803       d_isInv,
 804       TypeNode::fromType(d_grammar->resolve().getType()));
 805 }
 806
 807 /* -------------------------------------------------------------------------- */
 808 /* class SygusConstraintCommand */
 809 /* -------------------------------------------------------------------------- */
 810
 811 SygusConstraintCommand::SygusConstraintCommand(const Expr& e) : d_expr(e) {}
 812
 813 void SygusConstraintCommand::invoke(SmtEngine* smtEngine)
 814 {
 815   try
 816   {
 817     smtEngine->assertSygusConstraint(d_expr);
 818     d_commandStatus = CommandSuccess::instance();
 819   }
 820   catch (exception& e)
 821   {
 822     d_commandStatus = new CommandFailure(e.what());
 823   }
 824 }
 825
 826 Expr SygusConstraintCommand::getExpr() const { return d_expr; }
 827
 828 Command* SygusConstraintCommand::exportTo(ExprManager* exprManager,
 829                                           ExprManagerMapCollection& variableMap)
 830 {
 831   return new SygusConstraintCommand(d_expr.exportTo(exprManager, variableMap));
 832 }
 833
 834 Command* SygusConstraintCommand::clone() const
 835 {
 836   return new SygusConstraintCommand(d_expr);
 837 }
 838
 839 std::string SygusConstraintCommand::getCommandName() const
 840 {
 841   return "constraint";
 842 }
 843
 844 void SygusConstraintCommand::toStream(std::ostream& out,
 845                                       int toDepth,
 846                                       bool types,
 847                                       size_t dag,
 848                                       OutputLanguage language) const
 849 {
 850   Printer::getPrinter(language)->toStreamCmdConstraint(out,
 851                                                        Node::fromExpr(d_expr));
 852 }
 853
 854 /* -------------------------------------------------------------------------- */
 855 /* class SygusInvConstraintCommand */
 856 /* -------------------------------------------------------------------------- */
 857
 858 SygusInvConstraintCommand::SygusInvConstraintCommand(
 859     const std::vector<Expr>& predicates)
 860     : d_predicates(predicates)
 861 {
 862 }
 863
 864 SygusInvConstraintCommand::SygusInvConstraintCommand(const Expr& inv,
 865                                                      const Expr& pre,
 866                                                      const Expr& trans,
 867                                                      const Expr& post)
 868     : SygusInvConstraintCommand(std::vector<Expr>{inv, pre, trans, post})
 869 {
 870 }
 871
 872 void SygusInvConstraintCommand::invoke(SmtEngine* smtEngine)
 873 {
 874   try
 875   {
 876     smtEngine->assertSygusInvConstraint(
 877         d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
 878     d_commandStatus = CommandSuccess::instance();
 879   }
 880   catch (exception& e)
 881   {
 882     d_commandStatus = new CommandFailure(e.what());
 883   }
 884 }
 885
 886 const std::vector<Expr>& SygusInvConstraintCommand::getPredicates() const
 887 {
 888   return d_predicates;
 889 }
 890
 891 Command* SygusInvConstraintCommand::exportTo(
 892     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
 893 {
 894   return new SygusInvConstraintCommand(d_predicates);
 895 }
 896
 897 Command* SygusInvConstraintCommand::clone() const
 898 {
 899   return new SygusInvConstraintCommand(d_predicates);
 900 }
 901
 902 std::string SygusInvConstraintCommand::getCommandName() const
 903 {
 904   return "inv-constraint";
 905 }
 906
 907 void SygusInvConstraintCommand::toStream(std::ostream& out,
 908                                          int toDepth,
 909                                          bool types,
 910                                          size_t dag,
 911                                          OutputLanguage language) const
 912 {
 913   Printer::getPrinter(language)->toStreamCmdInvConstraint(
 914       out,
 915       Node::fromExpr(d_predicates[0]),
 916       Node::fromExpr(d_predicates[1]),
 917       Node::fromExpr(d_predicates[2]),
 918       Node::fromExpr(d_predicates[3]));
 919 }
 920
 921 /* -------------------------------------------------------------------------- */
 922 /* class CheckSynthCommand                                                    */
 923 /* -------------------------------------------------------------------------- */
 924
 925 void CheckSynthCommand::invoke(SmtEngine* smtEngine)
 926 {
 927   try
 928   {
 929     d_result = smtEngine->checkSynth();
 930     d_commandStatus = CommandSuccess::instance();
 931     smt::SmtScope scope(smtEngine);
 932     d_solution.clear();
 933     // check whether we should print the status
 934     if (d_result.asSatisfiabilityResult() != Result::UNSAT
 935         || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF
 936         || options::sygusOut() == options::SygusSolutionOutMode::STATUS)
 937     {
 938       if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD)
 939       {
 940         d_solution << "(fail)" << endl;
 941       }
 942       else
 943       {
 944         d_solution << d_result << endl;
 945       }
 946     }
 947     // check whether we should print the solution
 948     if (d_result.asSatisfiabilityResult() == Result::UNSAT
 949         && options::sygusOut() != options::SygusSolutionOutMode::STATUS)
 950     {
 951       // printing a synthesis solution is a non-constant
 952       // method, since it invokes a sophisticated algorithm
 953       // (Figure 5 of Reynolds et al. CAV 2015).
 954       // Hence, we must call here print solution here,
 955       // instead of during printResult.
 956       smtEngine->printSynthSolution(d_solution);
 957     }
 958   }
 959   catch (exception& e)
 960   {
 961     d_commandStatus = new CommandFailure(e.what());
 962   }
 963 }
 964
 965 Result CheckSynthCommand::getResult() const { return d_result; }
 966 void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
 967 {
 968   if (!ok())
 969   {
 970     this->Command::printResult(out, verbosity);
 971   }
 972   else
 973   {
 974     out << d_solution.str();
 975   }
 976 }
 977
 978 Command* CheckSynthCommand::exportTo(ExprManager* exprManager,
 979                                      ExprManagerMapCollection& variableMap)
 980 {
 981   return new CheckSynthCommand();
 982 }
 983
 984 Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
 985
 986 std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
 987
 988 void CheckSynthCommand::toStream(std::ostream& out,
 989                                  int toDepth,
 990                                  bool types,
 991                                  size_t dag,
 992                                  OutputLanguage language) const
 993 {
 994   Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
 995 }
 996
 997 /* -------------------------------------------------------------------------- */
 998 /* class ResetCommand                                                         */
 999 /* -------------------------------------------------------------------------- */
1000
1001 void ResetCommand::invoke(SmtEngine* smtEngine)
1002 {
1003   try
1004   {
1005     smtEngine->reset();
1006     d_commandStatus = CommandSuccess::instance();
1007   }
1008   catch (exception& e)
1009   {
1010     d_commandStatus = new CommandFailure(e.what());
1011   }
1012 }
1013
1014 Command* ResetCommand::exportTo(ExprManager* exprManager,
1015                                 ExprManagerMapCollection& variableMap)
1016 {
1017   return new ResetCommand();
1018 }
1019
1020 Command* ResetCommand::clone() const { return new ResetCommand(); }
1021 std::string ResetCommand::getCommandName() const { return "reset"; }
1022
1023 void ResetCommand::toStream(std::ostream& out,
1024                             int toDepth,
1025                             bool types,
1026                             size_t dag,
1027                             OutputLanguage language) const
1028 {
1029   Printer::getPrinter(language)->toStreamCmdReset(out);
1030 }
1031
1032 /* -------------------------------------------------------------------------- */
1033 /* class ResetAssertionsCommand                                               */
1034 /* -------------------------------------------------------------------------- */
1035
1036 void ResetAssertionsCommand::invoke(SmtEngine* smtEngine)
1037 {
1038   try
1039   {
1040     smtEngine->resetAssertions();
1041     d_commandStatus = CommandSuccess::instance();
1042   }
1043   catch (exception& e)
1044   {
1045     d_commandStatus = new CommandFailure(e.what());
1046   }
1047 }
1048
1049 Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager,
1050                                           ExprManagerMapCollection& variableMap)
1051 {
1052   return new ResetAssertionsCommand();
1053 }
1054
1055 Command* ResetAssertionsCommand::clone() const
1056 {
1057   return new ResetAssertionsCommand();
1058 }
1059
1060 std::string ResetAssertionsCommand::getCommandName() const
1061 {
1062   return "reset-assertions";
1063 }
1064
1065 void ResetAssertionsCommand::toStream(std::ostream& out,
1066                                       int toDepth,
1067                                       bool types,
1068                                       size_t dag,
1069                                       OutputLanguage language) const
1070 {
1071   Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
1072 }
1073
1074 /* -------------------------------------------------------------------------- */
1075 /* class QuitCommand                                                          */
1076 /* -------------------------------------------------------------------------- */
1077
1078 void QuitCommand::invoke(SmtEngine* smtEngine)
1079 {
1080   Dump("benchmark") << *this;
1081   d_commandStatus = CommandSuccess::instance();
1082 }
1083
1084 Command* QuitCommand::exportTo(ExprManager* exprManager,
1085                                ExprManagerMapCollection& variableMap)
1086 {
1087   return new QuitCommand();
1088 }
1089
1090 Command* QuitCommand::clone() const { return new QuitCommand(); }
1091 std::string QuitCommand::getCommandName() const { return "exit"; }
1092
1093 void QuitCommand::toStream(std::ostream& out,
1094                            int toDepth,
1095                            bool types,
1096                            size_t dag,
1097                            OutputLanguage language) const
1098 {
1099   Printer::getPrinter(language)->toStreamCmdQuit(out);
1100 }
1101
1102 /* -------------------------------------------------------------------------- */
1103 /* class CommentCommand                                                       */
1104 /* -------------------------------------------------------------------------- */
1105
1106 CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
1107 std::string CommentCommand::getComment() const { return d_comment; }
1108 void CommentCommand::invoke(SmtEngine* smtEngine)
1109 {
1110   Dump("benchmark") << *this;
1111   d_commandStatus = CommandSuccess::instance();
1112 }
1113
1114 Command* CommentCommand::exportTo(ExprManager* exprManager,
1115                                   ExprManagerMapCollection& variableMap)
1116 {
1117   return new CommentCommand(d_comment);
1118 }
1119
1120 Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
1121 std::string CommentCommand::getCommandName() const { return "comment"; }
1122
1123 void CommentCommand::toStream(std::ostream& out,
1124                               int toDepth,
1125                               bool types,
1126                               size_t dag,
1127                               OutputLanguage language) const
1128 {
1129   Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
1130 }
1131
1132 /* -------------------------------------------------------------------------- */
1133 /* class CommandSequence                                                      */
1134 /* -------------------------------------------------------------------------- */
1135
1136 CommandSequence::CommandSequence() : d_index(0) {}
1137 CommandSequence::~CommandSequence()
1138 {
1139   for (unsigned i = d_index; i < d_commandSequence.size(); ++i)
1140   {
1141     delete d_commandSequence[i];
1142   }
1143 }
1144
1145 void CommandSequence::addCommand(Command* cmd)
1146 {
1147   d_commandSequence.push_back(cmd);
1148 }
1149
1150 void CommandSequence::clear() { d_commandSequence.clear(); }
1151 void CommandSequence::invoke(SmtEngine* smtEngine)
1152 {
1153   for (; d_index < d_commandSequence.size(); ++d_index)
1154   {
1155     d_commandSequence[d_index]->invoke(smtEngine);
1156     if (!d_commandSequence[d_index]->ok())
1157     {
1158       // abort execution
1159       d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
1160       return;
1161     }
1162     delete d_commandSequence[d_index];
1163   }
1164
1165   AlwaysAssert(d_commandStatus == NULL);
1166   d_commandStatus = CommandSuccess::instance();
1167 }
1168
1169 void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out)
1170 {
1171   for (; d_index < d_commandSequence.size(); ++d_index)
1172   {
1173     d_commandSequence[d_index]->invoke(smtEngine, out);
1174     if (!d_commandSequence[d_index]->ok())
1175     {
1176       // abort execution
1177       d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
1178       return;
1179     }
1180     delete d_commandSequence[d_index];
1181   }
1182
1183   AlwaysAssert(d_commandStatus == NULL);
1184   d_commandStatus = CommandSuccess::instance();
1185 }
1186
1187 Command* CommandSequence::exportTo(ExprManager* exprManager,
1188                                    ExprManagerMapCollection& variableMap)
1189 {
1190   CommandSequence* seq = new CommandSequence();
1191   for (iterator i = begin(); i != end(); ++i)
1192   {
1193     Command* cmd_to_export = *i;
1194     Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
1195     seq->addCommand(cmd);
1196     Debug("export") << "[export] so far converted: " << seq << endl;
1197   }
1198   seq->d_index = d_index;
1199   return seq;
1200 }
1201
1202 Command* CommandSequence::clone() const
1203 {
1204   CommandSequence* seq = new CommandSequence();
1205   for (const_iterator i = begin(); i != end(); ++i)
1206   {
1207     seq->addCommand((*i)->clone());
1208   }
1209   seq->d_index = d_index;
1210   return seq;
1211 }
1212
1213 CommandSequence::const_iterator CommandSequence::begin() const
1214 {
1215   return d_commandSequence.begin();
1216 }
1217
1218 CommandSequence::const_iterator CommandSequence::end() const
1219 {
1220   return d_commandSequence.end();
1221 }
1222
1223 CommandSequence::iterator CommandSequence::begin()
1224 {
1225   return d_commandSequence.begin();
1226 }
1227
1228 CommandSequence::iterator CommandSequence::end()
1229 {
1230   return d_commandSequence.end();
1231 }
1232
1233 std::string CommandSequence::getCommandName() const { return "sequence"; }
1234
1235 void CommandSequence::toStream(std::ostream& out,
1236                                int toDepth,
1237                                bool types,
1238                                size_t dag,
1239                                OutputLanguage language) const
1240 {
1241   Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
1242                                                             d_commandSequence);
1243 }
1244
1245 /* -------------------------------------------------------------------------- */
1246 /* class DeclarationSequence                                                  */
1247 /* -------------------------------------------------------------------------- */
1248
1249 void DeclarationSequence::toStream(std::ostream& out,
1250                                    int toDepth,
1251                                    bool types,
1252                                    size_t dag,
1253                                    OutputLanguage language) const
1254 {
1255   Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
1256       out, d_commandSequence);
1257 }
1258
1259 /* -------------------------------------------------------------------------- */
1260 /* class DeclarationDefinitionCommand                                         */
1261 /* -------------------------------------------------------------------------- */
1262
1263 DeclarationDefinitionCommand::DeclarationDefinitionCommand(
1264     const std::string& id)
1265     : d_symbol(id)
1266 {
1267 }
1268
1269 std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }
1270
1271 /* -------------------------------------------------------------------------- */
1272 /* class DeclareFunctionCommand                                               */
1273 /* -------------------------------------------------------------------------- */
1274
1275 DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
1276                                                Expr func,
1277                                                Type t)
1278     : DeclarationDefinitionCommand(id),
1279       d_func(func),
1280       d_type(t),
1281       d_printInModel(true),
1282       d_printInModelSetByUser(false)
1283 {
1284 }
1285
1286 Expr DeclareFunctionCommand::getFunction() const { return d_func; }
1287 Type DeclareFunctionCommand::getType() const { return d_type; }
1288 bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; }
1289 bool DeclareFunctionCommand::getPrintInModelSetByUser() const
1290 {
1291   return d_printInModelSetByUser;
1292 }
1293
1294 void DeclareFunctionCommand::setPrintInModel(bool p)
1295 {
1296   d_printInModel = p;
1297   d_printInModelSetByUser = true;
1298 }
1299
1300 void DeclareFunctionCommand::invoke(SmtEngine* smtEngine)
1301 {
1302   d_commandStatus = CommandSuccess::instance();
1303 }
1304
1305 Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
1306                                           ExprManagerMapCollection& variableMap)
1307 {
1308   DeclareFunctionCommand* dfc =
1309       new DeclareFunctionCommand(d_symbol,
1310                                  d_func.exportTo(exprManager, variableMap),
1311                                  d_type.exportTo(exprManager, variableMap));
1312   dfc->d_printInModel = d_printInModel;
1313   dfc->d_printInModelSetByUser = d_printInModelSetByUser;
1314   return dfc;
1315 }
1316
1317 Command* DeclareFunctionCommand::clone() const
1318 {
1319   DeclareFunctionCommand* dfc =
1320       new DeclareFunctionCommand(d_symbol, d_func, d_type);
1321   dfc->d_printInModel = d_printInModel;
1322   dfc->d_printInModelSetByUser = d_printInModelSetByUser;
1323   return dfc;
1324 }
1325
1326 std::string DeclareFunctionCommand::getCommandName() const
1327 {
1328   return "declare-fun";
1329 }
1330
1331 void DeclareFunctionCommand::toStream(std::ostream& out,
1332                                       int toDepth,
1333                                       bool types,
1334                                       size_t dag,
1335                                       OutputLanguage language) const
1336 {
1337   Printer::getPrinter(language)->toStreamCmdDeclareFunction(
1338       out, d_func.toString(), TypeNode::fromType(d_type));
1339 }
1340
1341 /* -------------------------------------------------------------------------- */
1342 /* class DeclareTypeCommand                                                   */
1343 /* -------------------------------------------------------------------------- */
1344
1345 DeclareTypeCommand::DeclareTypeCommand(const std::string& id,
1346                                        size_t arity,
1347                                        Type t)
1348     : DeclarationDefinitionCommand(id), d_arity(arity), d_type(t)
1349 {
1350 }
1351
1352 size_t DeclareTypeCommand::getArity() const { return d_arity; }
1353 Type DeclareTypeCommand::getType() const { return d_type; }
1354 void DeclareTypeCommand::invoke(SmtEngine* smtEngine)
1355 {
1356   d_commandStatus = CommandSuccess::instance();
1357 }
1358
1359 Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
1360                                       ExprManagerMapCollection& variableMap)
1361 {
1362   return new DeclareTypeCommand(
1363       d_symbol, d_arity, d_type.exportTo(exprManager, variableMap));
1364 }
1365
1366 Command* DeclareTypeCommand::clone() const
1367 {
1368   return new DeclareTypeCommand(d_symbol, d_arity, d_type);
1369 }
1370
1371 std::string DeclareTypeCommand::getCommandName() const
1372 {
1373   return "declare-sort";
1374 }
1375
1376 void DeclareTypeCommand::toStream(std::ostream& out,
1377                                   int toDepth,
1378                                   bool types,
1379                                   size_t dag,
1380                                   OutputLanguage language) const
1381 {
1382   Printer::getPrinter(language)->toStreamCmdDeclareType(
1383       out, d_type.toString(), d_arity, TypeNode::fromType(d_type));
1384 }
1385
1386 /* -------------------------------------------------------------------------- */
1387 /* class DefineTypeCommand                                                    */
1388 /* -------------------------------------------------------------------------- */
1389
1390 DefineTypeCommand::DefineTypeCommand(const std::string& id, Type t)
1391     : DeclarationDefinitionCommand(id), d_params(), d_type(t)
1392 {
1393 }
1394
1395 DefineTypeCommand::DefineTypeCommand(const std::string& id,
1396                                      const std::vector<Type>& params,
1397                                      Type t)
1398     : DeclarationDefinitionCommand(id), d_params(params), d_type(t)
1399 {
1400 }
1401
1402 const std::vector<Type>& DefineTypeCommand::getParameters() const
1403 {
1404   return d_params;
1405 }
1406
1407 Type DefineTypeCommand::getType() const { return d_type; }
1408 void DefineTypeCommand::invoke(SmtEngine* smtEngine)
1409 {
1410   d_commandStatus = CommandSuccess::instance();
1411 }
1412
1413 Command* DefineTypeCommand::exportTo(ExprManager* exprManager,
1414                                      ExprManagerMapCollection& variableMap)
1415 {
1416   vector<Type> params;
1417   transform(d_params.begin(),
1418             d_params.end(),
1419             back_inserter(params),
1420             ExportTransformer(exprManager, variableMap));
1421   Type type = d_type.exportTo(exprManager, variableMap);
1422   return new DefineTypeCommand(d_symbol, params, type);
1423 }
1424
1425 Command* DefineTypeCommand::clone() const
1426 {
1427   return new DefineTypeCommand(d_symbol, d_params, d_type);
1428 }
1429
1430 std::string DefineTypeCommand::getCommandName() const { return "define-sort"; }
1431
1432 void DefineTypeCommand::toStream(std::ostream& out,
1433                                  int toDepth,
1434                                  bool types,
1435                                  size_t dag,
1436                                  OutputLanguage language) const
1437 {
1438   Printer::getPrinter(language)->toStreamCmdDefineType(
1439       out,
1440       d_symbol,
1441       typeVectorToTypeNodes(d_params),
1442       TypeNode::fromType(d_type));
1443 }
1444
1445 /* -------------------------------------------------------------------------- */
1446 /* class DefineFunctionCommand                                                */
1447 /* -------------------------------------------------------------------------- */
1448
1449 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
1450                                              Expr func,
1451                                              Expr formula,
1452                                              bool global)
1453     : DeclarationDefinitionCommand(id),
1454       d_func(func),
1455       d_formals(),
1456       d_formula(formula),
1457       d_global(global)
1458 {
1459 }
1460
1461 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
1462                                              Expr func,
1463                                              const std::vector<Expr>& formals,
1464                                              Expr formula,
1465                                              bool global)
1466     : DeclarationDefinitionCommand(id),
1467       d_func(func),
1468       d_formals(formals),
1469       d_formula(formula),
1470       d_global(global)
1471
1472 {
1473 }
1474
1475 Expr DefineFunctionCommand::getFunction() const { return d_func; }
1476 const std::vector<Expr>& DefineFunctionCommand::getFormals() const
1477 {
1478   return d_formals;
1479 }
1480
1481 Expr DefineFunctionCommand::getFormula() const { return d_formula; }
1482 void DefineFunctionCommand::invoke(SmtEngine* smtEngine)
1483 {
1484   try
1485   {
1486     if (!d_func.isNull())
1487     {
1488       smtEngine->defineFunction(d_func, d_formals, d_formula, d_global);
1489     }
1490     d_commandStatus = CommandSuccess::instance();
1491   }
1492   catch (exception& e)
1493   {
1494     d_commandStatus = new CommandFailure(e.what());
1495   }
1496 }
1497
1498 Command* DefineFunctionCommand::exportTo(ExprManager* exprManager,
1499                                          ExprManagerMapCollection& variableMap)
1500 {
1501   Expr func = d_func.exportTo(
1502       exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
1503   vector<Expr> formals;
1504   transform(d_formals.begin(),
1505             d_formals.end(),
1506             back_inserter(formals),
1507             ExportTransformer(exprManager, variableMap));
1508   Expr formula = d_formula.exportTo(exprManager, variableMap);
1509   return new DefineFunctionCommand(d_symbol, func, formals, formula, d_global);
1510 }
1511
1512 Command* DefineFunctionCommand::clone() const
1513 {
1514   return new DefineFunctionCommand(
1515       d_symbol, d_func, d_formals, d_formula, d_global);
1516 }
1517
1518 std::string DefineFunctionCommand::getCommandName() const
1519 {
1520   return "define-fun";
1521 }
1522
1523 void DefineFunctionCommand::toStream(std::ostream& out,
1524                                      int toDepth,
1525                                      bool types,
1526                                      size_t dag,
1527                                      OutputLanguage language) const
1528 {
1529   Printer::getPrinter(language)->toStreamCmdDefineFunction(
1530       out,
1531       d_func.toString(),
1532       exprVectorToNodes(d_formals),
1533       Node::fromExpr(d_func).getType().getRangeType(),
1534       Node::fromExpr(d_formula));
1535 }
1536
1537 /* -------------------------------------------------------------------------- */
1538 /* class DefineNamedFunctionCommand                                           */
1539 /* -------------------------------------------------------------------------- */
1540
1541 DefineNamedFunctionCommand::DefineNamedFunctionCommand(
1542     const std::string& id,
1543     Expr func,
1544     const std::vector<Expr>& formals,
1545     Expr formula,
1546     bool global)
1547     : DefineFunctionCommand(id, func, formals, formula, global)
1548 {
1549 }
1550
1551 void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine)
1552 {
1553   this->DefineFunctionCommand::invoke(smtEngine);
1554   if (!d_func.isNull() && d_func.getType().isBoolean())
1555   {
1556     smtEngine->addToAssignment(d_func);
1557   }
1558   d_commandStatus = CommandSuccess::instance();
1559 }
1560
1561 Command* DefineNamedFunctionCommand::exportTo(
1562     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1563 {
1564   Expr func = d_func.exportTo(exprManager, variableMap);
1565   vector<Expr> formals;
1566   transform(d_formals.begin(),
1567             d_formals.end(),
1568             back_inserter(formals),
1569             ExportTransformer(exprManager, variableMap));
1570   Expr formula = d_formula.exportTo(exprManager, variableMap);
1571   return new DefineNamedFunctionCommand(
1572       d_symbol, func, formals, formula, d_global);
1573 }
1574
1575 Command* DefineNamedFunctionCommand::clone() const
1576 {
1577   return new DefineNamedFunctionCommand(
1578       d_symbol, d_func, d_formals, d_formula, d_global);
1579 }
1580
1581 void DefineNamedFunctionCommand::toStream(std::ostream& out,
1582                                           int toDepth,
1583                                           bool types,
1584                                           size_t dag,
1585                                           OutputLanguage language) const
1586 {
1587   Printer::getPrinter(language)->toStreamCmdDefineNamedFunction(
1588       out,
1589       d_func.toString(),
1590       exprVectorToNodes(d_formals),
1591       Node::fromExpr(d_func).getType().getRangeType(),
1592       Node::fromExpr(d_formula));
1593 }
1594
1595 /* -------------------------------------------------------------------------- */
1596 /* class DefineFunctionRecCommand                                             */
1597 /* -------------------------------------------------------------------------- */
1598
1599 DefineFunctionRecCommand::DefineFunctionRecCommand(
1600     const api::Solver* solver,
1601     api::Term func,
1602     const std::vector<api::Term>& formals,
1603     api::Term formula,
1604     bool global)
1605     : Command(solver), d_global(global)
1606 {
1607   d_funcs.push_back(func);
1608   d_formals.push_back(formals);
1609   d_formulas.push_back(formula);
1610 }
1611
1612 DefineFunctionRecCommand::DefineFunctionRecCommand(
1613     const api::Solver* solver,
1614     const std::vector<api::Term>& funcs,
1615     const std::vector<std::vector<api::Term>>& formals,
1616     const std::vector<api::Term>& formulas,
1617     bool global)
1618     : Command(solver),
1619       d_funcs(funcs),
1620       d_formals(formals),
1621       d_formulas(formulas),
1622       d_global(global)
1623 {
1624 }
1625
1626 const std::vector<api::Term>& DefineFunctionRecCommand::getFunctions() const
1627 {
1628   return d_funcs;
1629 }
1630
1631 const std::vector<std::vector<api::Term>>&
1632 DefineFunctionRecCommand::getFormals() const
1633 {
1634   return d_formals;
1635 }
1636
1637 const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
1638 {
1639   return d_formulas;
1640 }
1641
1642 void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine)
1643 {
1644   try
1645   {
1646     d_solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global);
1647     d_commandStatus = CommandSuccess::instance();
1648   }
1649   catch (exception& e)
1650   {
1651     d_commandStatus = new CommandFailure(e.what());
1652   }
1653 }
1654
1655 Command* DefineFunctionRecCommand::exportTo(
1656     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1657 {
1658   Unimplemented();
1659 }
1660
1661 Command* DefineFunctionRecCommand::clone() const
1662 {
1663   return new DefineFunctionRecCommand(
1664       d_solver, d_funcs, d_formals, d_formulas, d_global);
1665 }
1666
1667 std::string DefineFunctionRecCommand::getCommandName() const
1668 {
1669   return "define-fun-rec";
1670 }
1671
1672 void DefineFunctionRecCommand::toStream(std::ostream& out,
1673                                         int toDepth,
1674                                         bool types,
1675                                         size_t dag,
1676                                         OutputLanguage language) const
1677 {
1678   std::vector<std::vector<Node>> formals;
1679   formals.reserve(d_formals.size());
1680   for (const std::vector<api::Term>& formal : d_formals)
1681   {
1682     formals.push_back(api::termVectorToNodes(formal));
1683   }
1684
1685   Printer::getPrinter(language)->toStreamCmdDefineFunctionRec(
1686       out,
1687       api::termVectorToNodes(d_funcs),
1688       formals,
1689       api::termVectorToNodes(d_formulas));
1690 }
1691
1692 /* -------------------------------------------------------------------------- */
1693 /* class SetUserAttribute                                                     */
1694 /* -------------------------------------------------------------------------- */
1695
1696 SetUserAttributeCommand::SetUserAttributeCommand(
1697     const std::string& attr,
1698     Expr expr,
1699     const std::vector<Expr>& expr_values,
1700     const std::string& str_value)
1701     : d_attr(attr),
1702       d_expr(expr),
1703       d_expr_values(expr_values),
1704       d_str_value(str_value)
1705 {
1706 }
1707
1708 SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
1709                                                  Expr expr)
1710     : SetUserAttributeCommand(attr, expr, {}, "")
1711 {
1712 }
1713
1714 SetUserAttributeCommand::SetUserAttributeCommand(
1715     const std::string& attr, Expr expr, const std::vector<Expr>& values)
1716     : SetUserAttributeCommand(attr, expr, values, "")
1717 {
1718 }
1719
1720 SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
1721                                                  Expr expr,
1722                                                  const std::string& value)
1723     : SetUserAttributeCommand(attr, expr, {}, value)
1724 {
1725 }
1726
1727 void SetUserAttributeCommand::invoke(SmtEngine* smtEngine)
1728 {
1729   try
1730   {
1731     if (!d_expr.isNull())
1732     {
1733       smtEngine->setUserAttribute(d_attr, d_expr, d_expr_values, d_str_value);
1734     }
1735     d_commandStatus = CommandSuccess::instance();
1736   }
1737   catch (exception& e)
1738   {
1739     d_commandStatus = new CommandFailure(e.what());
1740   }
1741 }
1742
1743 Command* SetUserAttributeCommand::exportTo(
1744     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1745 {
1746   Expr expr = d_expr.exportTo(exprManager, variableMap);
1747   return new SetUserAttributeCommand(d_attr, expr, d_expr_values, d_str_value);
1748 }
1749
1750 Command* SetUserAttributeCommand::clone() const
1751 {
1752   return new SetUserAttributeCommand(
1753       d_attr, d_expr, d_expr_values, d_str_value);
1754 }
1755
1756 std::string SetUserAttributeCommand::getCommandName() const
1757 {
1758   return "set-user-attribute";
1759 }
1760
1761 void SetUserAttributeCommand::toStream(std::ostream& out,
1762                                        int toDepth,
1763                                        bool types,
1764                                        size_t dag,
1765                                        OutputLanguage language) const
1766 {
1767   Printer::getPrinter(language)->toStreamCmdSetUserAttribute(
1768       out, d_attr, Node::fromExpr(d_expr));
1769 }
1770
1771 /* -------------------------------------------------------------------------- */
1772 /* class SimplifyCommand                                                      */
1773 /* -------------------------------------------------------------------------- */
1774
1775 SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) {}
1776 Expr SimplifyCommand::getTerm() const { return d_term; }
1777 void SimplifyCommand::invoke(SmtEngine* smtEngine)
1778 {
1779   try
1780   {
1781     d_result = smtEngine->simplify(Node::fromExpr(d_term)).toExpr();
1782     d_commandStatus = CommandSuccess::instance();
1783   }
1784   catch (UnsafeInterruptException& e)
1785   {
1786     d_commandStatus = new CommandInterrupted();
1787   }
1788   catch (exception& e)
1789   {
1790     d_commandStatus = new CommandFailure(e.what());
1791   }
1792 }
1793
1794 Expr SimplifyCommand::getResult() const { return d_result; }
1795 void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
1796 {
1797   if (!ok())
1798   {
1799     this->Command::printResult(out, verbosity);
1800   }
1801   else
1802   {
1803     out << d_result << endl;
1804   }
1805 }
1806
1807 Command* SimplifyCommand::exportTo(ExprManager* exprManager,
1808                                    ExprManagerMapCollection& variableMap)
1809 {
1810   SimplifyCommand* c =
1811       new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
1812   c->d_result = d_result.exportTo(exprManager, variableMap);
1813   return c;
1814 }
1815
1816 Command* SimplifyCommand::clone() const
1817 {
1818   SimplifyCommand* c = new SimplifyCommand(d_term);
1819   c->d_result = d_result;
1820   return c;
1821 }
1822
1823 std::string SimplifyCommand::getCommandName() const { return "simplify"; }
1824
1825 void SimplifyCommand::toStream(std::ostream& out,
1826                                int toDepth,
1827                                bool types,
1828                                size_t dag,
1829                                OutputLanguage language) const
1830 {
1831   Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term);
1832 }
1833
1834 /* -------------------------------------------------------------------------- */
1835 /* class ExpandDefinitionsCommand                                             */
1836 /* -------------------------------------------------------------------------- */
1837
1838 ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {}
1839 Expr ExpandDefinitionsCommand::getTerm() const { return d_term; }
1840 void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine)
1841 {
1842   Node t = Node::fromExpr(d_term);
1843   d_result = smtEngine->expandDefinitions(t).toExpr();
1844   d_commandStatus = CommandSuccess::instance();
1845 }
1846
1847 Expr ExpandDefinitionsCommand::getResult() const { return d_result; }
1848 void ExpandDefinitionsCommand::printResult(std::ostream& out,
1849                                            uint32_t verbosity) const
1850 {
1851   if (!ok())
1852   {
1853     this->Command::printResult(out, verbosity);
1854   }
1855   else
1856   {
1857     out << d_result << endl;
1858   }
1859 }
1860
1861 Command* ExpandDefinitionsCommand::exportTo(
1862     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1863 {
1864   ExpandDefinitionsCommand* c =
1865       new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
1866   c->d_result = d_result.exportTo(exprManager, variableMap);
1867   return c;
1868 }
1869
1870 Command* ExpandDefinitionsCommand::clone() const
1871 {
1872   ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
1873   c->d_result = d_result;
1874   return c;
1875 }
1876
1877 std::string ExpandDefinitionsCommand::getCommandName() const
1878 {
1879   return "expand-definitions";
1880 }
1881
1882 void ExpandDefinitionsCommand::toStream(std::ostream& out,
1883                                         int toDepth,
1884                                         bool types,
1885                                         size_t dag,
1886                                         OutputLanguage language) const
1887 {
1888   Printer::getPrinter(language)->toStreamCmdExpandDefinitions(
1889       out, Node::fromExpr(d_term));
1890 }
1891
1892 /* -------------------------------------------------------------------------- */
1893 /* class GetValueCommand                                                      */
1894 /* -------------------------------------------------------------------------- */
1895
1896 GetValueCommand::GetValueCommand(Expr term) : d_terms()
1897 {
1898   d_terms.push_back(term);
1899 }
1900
1901 GetValueCommand::GetValueCommand(const std::vector<Expr>& terms)
1902     : d_terms(terms)
1903 {
1904   PrettyCheckArgument(
1905       terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
1906 }
1907
1908 const std::vector<Expr>& GetValueCommand::getTerms() const { return d_terms; }
1909 void GetValueCommand::invoke(SmtEngine* smtEngine)
1910 {
1911   try
1912   {
1913     ExprManager* em = smtEngine->getExprManager();
1914     NodeManager* nm = NodeManager::fromExprManager(em);
1915     smt::SmtScope scope(smtEngine);
1916     vector<Expr> result = smtEngine->getValues(d_terms);
1917     Assert(result.size() == d_terms.size());
1918     for (int i = 0, size = d_terms.size(); i < size; i++)
1919     {
1920       Expr e = d_terms[i];
1921       Node eNode = Node::fromExpr(e);
1922       Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
1923       Node request = options::expandDefinitions()
1924                          ? smtEngine->expandDefinitions(eNode)
1925                          : eNode;
1926       Node value = Node::fromExpr(result[i]);
1927       if (value.getType().isInteger() && request.getType() == nm->realType())
1928       {
1929         // Need to wrap in division-by-one so that output printers know this
1930         // is an integer-looking constant that really should be output as
1931         // a rational.  Necessary for SMT-LIB standards compliance.
1932         value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
1933       }
1934       result[i] = nm->mkNode(kind::SEXPR, request, value).toExpr();
1935     }
1936     d_result = em->mkExpr(kind::SEXPR, result);
1937     d_commandStatus = CommandSuccess::instance();
1938   }
1939   catch (RecoverableModalException& e)
1940   {
1941     d_commandStatus = new CommandRecoverableFailure(e.what());
1942   }
1943   catch (UnsafeInterruptException& e)
1944   {
1945     d_commandStatus = new CommandInterrupted();
1946   }
1947   catch (exception& e)
1948   {
1949     d_commandStatus = new CommandFailure(e.what());
1950   }
1951 }
1952
1953 Expr GetValueCommand::getResult() const { return d_result; }
1954 void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
1955 {
1956   if (!ok())
1957   {
1958     this->Command::printResult(out, verbosity);
1959   }
1960   else
1961   {
1962     expr::ExprDag::Scope scope(out, false);
1963     out << d_result << endl;
1964   }
1965 }
1966
1967 Command* GetValueCommand::exportTo(ExprManager* exprManager,
1968                                    ExprManagerMapCollection& variableMap)
1969 {
1970   vector<Expr> exportedTerms;
1971   for (std::vector<Expr>::const_iterator i = d_terms.begin();
1972        i != d_terms.end();
1973        ++i)
1974   {
1975     exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
1976   }
1977   GetValueCommand* c = new GetValueCommand(exportedTerms);
1978   c->d_result = d_result.exportTo(exprManager, variableMap);
1979   return c;
1980 }
1981
1982 Command* GetValueCommand::clone() const
1983 {
1984   GetValueCommand* c = new GetValueCommand(d_terms);
1985   c->d_result = d_result;
1986   return c;
1987 }
1988
1989 std::string GetValueCommand::getCommandName() const { return "get-value"; }
1990
1991 void GetValueCommand::toStream(std::ostream& out,
1992                                int toDepth,
1993                                bool types,
1994                                size_t dag,
1995                                OutputLanguage language) const
1996 {
1997   Printer::getPrinter(language)->toStreamCmdGetValue(
1998       out, exprVectorToNodes(d_terms));
1999 }
2000
2001 /* -------------------------------------------------------------------------- */
2002 /* class GetAssignmentCommand                                                 */
2003 /* -------------------------------------------------------------------------- */
2004
2005 GetAssignmentCommand::GetAssignmentCommand() {}
2006 void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
2007 {
2008   try
2009   {
2010     std::vector<std::pair<Expr, Expr>> assignments = smtEngine->getAssignment();
2011     vector<SExpr> sexprs;
2012     for (const auto& p : assignments)
2013     {
2014       vector<SExpr> v;
2015       v.emplace_back(SExpr::Keyword(p.first.toString()));
2016       v.emplace_back(SExpr::Keyword(p.second.toString()));
2017       sexprs.emplace_back(v);
2018     }
2019     d_result = SExpr(sexprs);
2020     d_commandStatus = CommandSuccess::instance();
2021   }
2022   catch (RecoverableModalException& e)
2023   {
2024     d_commandStatus = new CommandRecoverableFailure(e.what());
2025   }
2026   catch (UnsafeInterruptException& e)
2027   {
2028     d_commandStatus = new CommandInterrupted();
2029   }
2030   catch (exception& e)
2031   {
2032     d_commandStatus = new CommandFailure(e.what());
2033   }
2034 }
2035
2036 SExpr GetAssignmentCommand::getResult() const { return d_result; }
2037 void GetAssignmentCommand::printResult(std::ostream& out,
2038                                        uint32_t verbosity) const
2039 {
2040   if (!ok())
2041   {
2042     this->Command::printResult(out, verbosity);
2043   }
2044   else
2045   {
2046     out << d_result << endl;
2047   }
2048 }
2049
2050 Command* GetAssignmentCommand::exportTo(ExprManager* exprManager,
2051                                         ExprManagerMapCollection& variableMap)
2052 {
2053   GetAssignmentCommand* c = new GetAssignmentCommand();
2054   c->d_result = d_result;
2055   return c;
2056 }
2057
2058 Command* GetAssignmentCommand::clone() const
2059 {
2060   GetAssignmentCommand* c = new GetAssignmentCommand();
2061   c->d_result = d_result;
2062   return c;
2063 }
2064
2065 std::string GetAssignmentCommand::getCommandName() const
2066 {
2067   return "get-assignment";
2068 }
2069
2070 void GetAssignmentCommand::toStream(std::ostream& out,
2071                                     int toDepth,
2072                                     bool types,
2073                                     size_t dag,
2074                                     OutputLanguage language) const
2075 {
2076   Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
2077 }
2078
2079 /* -------------------------------------------------------------------------- */
2080 /* class GetModelCommand                                                      */
2081 /* -------------------------------------------------------------------------- */
2082
2083 GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
2084 void GetModelCommand::invoke(SmtEngine* smtEngine)
2085 {
2086   try
2087   {
2088     d_result = smtEngine->getModel();
2089     d_smtEngine = smtEngine;
2090     d_commandStatus = CommandSuccess::instance();
2091   }
2092   catch (RecoverableModalException& e)
2093   {
2094     d_commandStatus = new CommandRecoverableFailure(e.what());
2095   }
2096   catch (UnsafeInterruptException& e)
2097   {
2098     d_commandStatus = new CommandInterrupted();
2099   }
2100   catch (exception& e)
2101   {
2102     d_commandStatus = new CommandFailure(e.what());
2103   }
2104 }
2105
2106 /* Model is private to the library -- for now
2107 Model* GetModelCommand::getResult() const  {
2108   return d_result;
2109 }
2110 */
2111
2112 void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
2113 {
2114   if (!ok())
2115   {
2116     this->Command::printResult(out, verbosity);
2117   }
2118   else
2119   {
2120     out << *d_result;
2121   }
2122 }
2123
2124 Command* GetModelCommand::exportTo(ExprManager* exprManager,
2125                                    ExprManagerMapCollection& variableMap)
2126 {
2127   GetModelCommand* c = new GetModelCommand();
2128   c->d_result = d_result;
2129   c->d_smtEngine = d_smtEngine;
2130   return c;
2131 }
2132
2133 Command* GetModelCommand::clone() const
2134 {
2135   GetModelCommand* c = new GetModelCommand();
2136   c->d_result = d_result;
2137   c->d_smtEngine = d_smtEngine;
2138   return c;
2139 }
2140
2141 std::string GetModelCommand::getCommandName() const { return "get-model"; }
2142
2143 void GetModelCommand::toStream(std::ostream& out,
2144                                int toDepth,
2145                                bool types,
2146                                size_t dag,
2147                                OutputLanguage language) const
2148 {
2149   Printer::getPrinter(language)->toStreamCmdGetModel(out);
2150 }
2151
2152 /* -------------------------------------------------------------------------- */
2153 /* class BlockModelCommand */
2154 /* -------------------------------------------------------------------------- */
2155
2156 BlockModelCommand::BlockModelCommand() {}
2157 void BlockModelCommand::invoke(SmtEngine* smtEngine)
2158 {
2159   try
2160   {
2161     smtEngine->blockModel();
2162     d_commandStatus = CommandSuccess::instance();
2163   }
2164   catch (RecoverableModalException& e)
2165   {
2166     d_commandStatus = new CommandRecoverableFailure(e.what());
2167   }
2168   catch (UnsafeInterruptException& e)
2169   {
2170     d_commandStatus = new CommandInterrupted();
2171   }
2172   catch (exception& e)
2173   {
2174     d_commandStatus = new CommandFailure(e.what());
2175   }
2176 }
2177
2178 Command* BlockModelCommand::exportTo(ExprManager* exprManager,
2179                                      ExprManagerMapCollection& variableMap)
2180 {
2181   BlockModelCommand* c = new BlockModelCommand();
2182   return c;
2183 }
2184
2185 Command* BlockModelCommand::clone() const
2186 {
2187   BlockModelCommand* c = new BlockModelCommand();
2188   return c;
2189 }
2190
2191 std::string BlockModelCommand::getCommandName() const { return "block-model"; }
2192
2193 void BlockModelCommand::toStream(std::ostream& out,
2194                                  int toDepth,
2195                                  bool types,
2196                                  size_t dag,
2197                                  OutputLanguage language) const
2198 {
2199   Printer::getPrinter(language)->toStreamCmdBlockModel(out);
2200 }
2201
2202 /* -------------------------------------------------------------------------- */
2203 /* class BlockModelValuesCommand */
2204 /* -------------------------------------------------------------------------- */
2205
2206 BlockModelValuesCommand::BlockModelValuesCommand(const std::vector<Expr>& terms)
2207     : d_terms(terms)
2208 {
2209   PrettyCheckArgument(terms.size() >= 1,
2210                       terms,
2211                       "cannot block-model-values of an empty set of terms");
2212 }
2213
2214 const std::vector<Expr>& BlockModelValuesCommand::getTerms() const
2215 {
2216   return d_terms;
2217 }
2218 void BlockModelValuesCommand::invoke(SmtEngine* smtEngine)
2219 {
2220   try
2221   {
2222     smtEngine->blockModelValues(d_terms);
2223     d_commandStatus = CommandSuccess::instance();
2224   }
2225   catch (RecoverableModalException& e)
2226   {
2227     d_commandStatus = new CommandRecoverableFailure(e.what());
2228   }
2229   catch (UnsafeInterruptException& e)
2230   {
2231     d_commandStatus = new CommandInterrupted();
2232   }
2233   catch (exception& e)
2234   {
2235     d_commandStatus = new CommandFailure(e.what());
2236   }
2237 }
2238
2239 Command* BlockModelValuesCommand::exportTo(
2240     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2241 {
2242   vector<Expr> exportedTerms;
2243   for (std::vector<Expr>::const_iterator i = d_terms.begin();
2244        i != d_terms.end();
2245        ++i)
2246   {
2247     exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
2248   }
2249   BlockModelValuesCommand* c = new BlockModelValuesCommand(exportedTerms);
2250   return c;
2251 }
2252
2253 Command* BlockModelValuesCommand::clone() const
2254 {
2255   BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms);
2256   return c;
2257 }
2258
2259 std::string BlockModelValuesCommand::getCommandName() const
2260 {
2261   return "block-model-values";
2262 }
2263
2264 void BlockModelValuesCommand::toStream(std::ostream& out,
2265                                        int toDepth,
2266                                        bool types,
2267                                        size_t dag,
2268                                        OutputLanguage language) const
2269 {
2270   Printer::getPrinter(language)->toStreamCmdBlockModelValues(
2271       out, exprVectorToNodes(d_terms));
2272 }
2273
2274 /* -------------------------------------------------------------------------- */
2275 /* class GetProofCommand                                                      */
2276 /* -------------------------------------------------------------------------- */
2277
2278 GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {}
2279 void GetProofCommand::invoke(SmtEngine* smtEngine)
2280 {
2281   try
2282   {
2283     d_smtEngine = smtEngine;
2284     d_result = &smtEngine->getProof();
2285     d_commandStatus = CommandSuccess::instance();
2286   }
2287   catch (RecoverableModalException& e)
2288   {
2289     d_commandStatus = new CommandRecoverableFailure(e.what());
2290   }
2291   catch (UnsafeInterruptException& e)
2292   {
2293     d_commandStatus = new CommandInterrupted();
2294   }
2295   catch (exception& e)
2296   {
2297     d_commandStatus = new CommandFailure(e.what());
2298   }
2299 }
2300
2301 const Proof& GetProofCommand::getResult() const { return *d_result; }
2302 void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
2303 {
2304   if (!ok())
2305   {
2306     this->Command::printResult(out, verbosity);
2307   }
2308   else
2309   {
2310     smt::SmtScope scope(d_smtEngine);
2311     d_result->toStream(out);
2312   }
2313 }
2314
2315 Command* GetProofCommand::exportTo(ExprManager* exprManager,
2316                                    ExprManagerMapCollection& variableMap)
2317 {
2318   GetProofCommand* c = new GetProofCommand();
2319   c->d_result = d_result;
2320   c->d_smtEngine = d_smtEngine;
2321   return c;
2322 }
2323
2324 Command* GetProofCommand::clone() const
2325 {
2326   GetProofCommand* c = new GetProofCommand();
2327   c->d_result = d_result;
2328   c->d_smtEngine = d_smtEngine;
2329   return c;
2330 }
2331
2332 std::string GetProofCommand::getCommandName() const { return "get-proof"; }
2333
2334 void GetProofCommand::toStream(std::ostream& out,
2335                                int toDepth,
2336                                bool types,
2337                                size_t dag,
2338                                OutputLanguage language) const
2339 {
2340   Printer::getPrinter(language)->toStreamCmdGetProof(out);
2341 }
2342
2343 /* -------------------------------------------------------------------------- */
2344 /* class GetInstantiationsCommand                                             */
2345 /* -------------------------------------------------------------------------- */
2346
2347 GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
2348 void GetInstantiationsCommand::invoke(SmtEngine* smtEngine)
2349 {
2350   try
2351   {
2352     d_smtEngine = smtEngine;
2353     d_commandStatus = CommandSuccess::instance();
2354   }
2355   catch (exception& e)
2356   {
2357     d_commandStatus = new CommandFailure(e.what());
2358   }
2359 }
2360
2361 void GetInstantiationsCommand::printResult(std::ostream& out,
2362                                            uint32_t verbosity) const
2363 {
2364   if (!ok())
2365   {
2366     this->Command::printResult(out, verbosity);
2367   }
2368   else
2369   {
2370     d_smtEngine->printInstantiations(out);
2371   }
2372 }
2373
2374 Command* GetInstantiationsCommand::exportTo(
2375     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2376 {
2377   GetInstantiationsCommand* c = new GetInstantiationsCommand();
2378   // c->d_result = d_result;
2379   c->d_smtEngine = d_smtEngine;
2380   return c;
2381 }
2382
2383 Command* GetInstantiationsCommand::clone() const
2384 {
2385   GetInstantiationsCommand* c = new GetInstantiationsCommand();
2386   // c->d_result = d_result;
2387   c->d_smtEngine = d_smtEngine;
2388   return c;
2389 }
2390
2391 std::string GetInstantiationsCommand::getCommandName() const
2392 {
2393   return "get-instantiations";
2394 }
2395
2396 void GetInstantiationsCommand::toStream(std::ostream& out,
2397                                         int toDepth,
2398                                         bool types,
2399                                         size_t dag,
2400                                         OutputLanguage language) const
2401 {
2402   Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
2403 }
2404
2405 /* -------------------------------------------------------------------------- */
2406 /* class GetSynthSolutionCommand                                              */
2407 /* -------------------------------------------------------------------------- */
2408
2409 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
2410 void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine)
2411 {
2412   try
2413   {
2414     d_smtEngine = smtEngine;
2415     d_commandStatus = CommandSuccess::instance();
2416   }
2417   catch (exception& e)
2418   {
2419     d_commandStatus = new CommandFailure(e.what());
2420   }
2421 }
2422
2423 void GetSynthSolutionCommand::printResult(std::ostream& out,
2424                                           uint32_t verbosity) const
2425 {
2426   if (!ok())
2427   {
2428     this->Command::printResult(out, verbosity);
2429   }
2430   else
2431   {
2432     d_smtEngine->printSynthSolution(out);
2433   }
2434 }
2435
2436 Command* GetSynthSolutionCommand::exportTo(
2437     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2438 {
2439   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
2440   c->d_smtEngine = d_smtEngine;
2441   return c;
2442 }
2443
2444 Command* GetSynthSolutionCommand::clone() const
2445 {
2446   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
2447   c->d_smtEngine = d_smtEngine;
2448   return c;
2449 }
2450
2451 std::string GetSynthSolutionCommand::getCommandName() const
2452 {
2453   return "get-synth-solution";
2454 }
2455
2456 void GetSynthSolutionCommand::toStream(std::ostream& out,
2457                                        int toDepth,
2458                                        bool types,
2459                                        size_t dag,
2460                                        OutputLanguage language) const
2461 {
2462   Printer::getPrinter(language)->toStreamCmdGetSynthSolution(out);
2463 }
2464
2465 /* -------------------------------------------------------------------------- */
2466 /* class GetInterpolCommand                                                   */
2467 /* -------------------------------------------------------------------------- */
2468
2469 GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
2470                                        const std::string& name,
2471                                        api::Term conj)
2472     : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
2473 {
2474 }
2475 GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
2476                                        const std::string& name,
2477                                        api::Term conj,
2478                                        api::Grammar* g)
2479     : Command(solver),
2480       d_name(name),
2481       d_conj(conj),
2482       d_sygus_grammar(g),
2483       d_resultStatus(false)
2484 {
2485 }
2486
2487 api::Term GetInterpolCommand::getConjecture() const { return d_conj; }
2488
2489 const api::Grammar* GetInterpolCommand::getGrammar() const
2490 {
2491   return d_sygus_grammar;
2492 }
2493
2494 api::Term GetInterpolCommand::getResult() const { return d_result; }
2495
2496 void GetInterpolCommand::invoke(SmtEngine* smtEngine)
2497 {
2498   try
2499   {
2500     if (!d_sygus_grammar)
2501     {
2502       d_resultStatus = d_solver->getInterpolant(d_conj, d_result);
2503     }
2504     else
2505     {
2506       d_resultStatus =
2507           d_solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
2508     }
2509     d_commandStatus = CommandSuccess::instance();
2510   }
2511   catch (exception& e)
2512   {
2513     d_commandStatus = new CommandFailure(e.what());
2514   }
2515 }
2516
2517 void GetInterpolCommand::printResult(std::ostream& out,
2518                                      uint32_t verbosity) const
2519 {
2520   if (!ok())
2521   {
2522     this->Command::printResult(out, verbosity);
2523   }
2524   else
2525   {
2526     expr::ExprDag::Scope scope(out, false);
2527     if (d_resultStatus)
2528     {
2529       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
2530           << std::endl;
2531     }
2532     else
2533     {
2534       out << "none" << std::endl;
2535     }
2536   }
2537 }
2538
2539 Command* GetInterpolCommand::exportTo(ExprManager* exprManager,
2540                                       ExprManagerMapCollection& variableMap)
2541 {
2542   Unimplemented();
2543 }
2544
2545 Command* GetInterpolCommand::clone() const
2546 {
2547   GetInterpolCommand* c =
2548       new GetInterpolCommand(d_solver, d_name, d_conj, d_sygus_grammar);
2549   c->d_result = d_result;
2550   c->d_resultStatus = d_resultStatus;
2551   return c;
2552 }
2553
2554 std::string GetInterpolCommand::getCommandName() const
2555 {
2556   return "get-interpol";
2557 }
2558
2559 void GetInterpolCommand::toStream(std::ostream& out,
2560                                   int toDepth,
2561                                   bool types,
2562                                   size_t dag,
2563                                   OutputLanguage language) const
2564 {
2565   Printer::getPrinter(language)->toStreamCmdGetInterpol(
2566       out,
2567       d_name,
2568       d_conj.getNode(),
2569       TypeNode::fromType(d_sygus_grammar->resolve().getType()));
2570 }
2571
2572 /* -------------------------------------------------------------------------- */
2573 /* class GetAbductCommand                                                     */
2574 /* -------------------------------------------------------------------------- */
2575
2576 GetAbductCommand::GetAbductCommand(const api::Solver* solver,
2577                                    const std::string& name,
2578                                    api::Term conj)
2579     : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
2580 {
2581 }
2582 GetAbductCommand::GetAbductCommand(const api::Solver* solver,
2583                                    const std::string& name,
2584                                    api::Term conj,
2585                                    api::Grammar* g)
2586     : Command(solver),
2587       d_name(name),
2588       d_conj(conj),
2589       d_sygus_grammar(g),
2590       d_resultStatus(false)
2591 {
2592 }
2593
2594 api::Term GetAbductCommand::getConjecture() const { return d_conj; }
2595
2596 const api::Grammar* GetAbductCommand::getGrammar() const
2597 {
2598   return d_sygus_grammar;
2599 }
2600
2601 std::string GetAbductCommand::getAbductName() const { return d_name; }
2602 api::Term GetAbductCommand::getResult() const { return d_result; }
2603
2604 void GetAbductCommand::invoke(SmtEngine* smtEngine)
2605 {
2606   try
2607   {
2608     if (!d_sygus_grammar)
2609     {
2610       d_resultStatus = d_solver->getAbduct(d_conj, d_result);
2611     }
2612     else
2613     {
2614       d_resultStatus = d_solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
2615     }
2616     d_commandStatus = CommandSuccess::instance();
2617   }
2618   catch (exception& e)
2619   {
2620     d_commandStatus = new CommandFailure(e.what());
2621   }
2622 }
2623
2624 void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
2625 {
2626   if (!ok())
2627   {
2628     this->Command::printResult(out, verbosity);
2629   }
2630   else
2631   {
2632     expr::ExprDag::Scope scope(out, false);
2633     if (d_resultStatus)
2634     {
2635       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
2636           << std::endl;
2637     }
2638     else
2639     {
2640       out << "none" << std::endl;
2641     }
2642   }
2643 }
2644
2645 Command* GetAbductCommand::exportTo(ExprManager* exprManager,
2646                                     ExprManagerMapCollection& variableMap)
2647 {
2648   Unimplemented();
2649 }
2650
2651 Command* GetAbductCommand::clone() const
2652 {
2653   GetAbductCommand* c =
2654       new GetAbductCommand(d_solver, d_name, d_conj, d_sygus_grammar);
2655   c->d_result = d_result;
2656   c->d_resultStatus = d_resultStatus;
2657   return c;
2658 }
2659
2660 std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
2661
2662 void GetAbductCommand::toStream(std::ostream& out,
2663                                 int toDepth,
2664                                 bool types,
2665                                 size_t dag,
2666                                 OutputLanguage language) const
2667 {
2668   Printer::getPrinter(language)->toStreamCmdGetAbduct(
2669       out,
2670       d_name,
2671       d_conj.getNode(),
2672       TypeNode::fromType(d_sygus_grammar->resolve().getType()));
2673 }
2674
2675 /* -------------------------------------------------------------------------- */
2676 /* class GetQuantifierEliminationCommand                                      */
2677 /* -------------------------------------------------------------------------- */
2678
2679 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
2680     : d_expr(), d_doFull(true)
2681 {
2682 }
2683 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
2684     const Expr& expr, bool doFull)
2685     : d_expr(expr), d_doFull(doFull)
2686 {
2687 }
2688
2689 Expr GetQuantifierEliminationCommand::getExpr() const { return d_expr; }
2690 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
2691 void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine)
2692 {
2693   try
2694   {
2695     d_result =
2696         smtEngine->getQuantifierElimination(Node::fromExpr(d_expr), d_doFull)
2697             .toExpr();
2698     d_commandStatus = CommandSuccess::instance();
2699   }
2700   catch (exception& e)
2701   {
2702     d_commandStatus = new CommandFailure(e.what());
2703   }
2704 }
2705
2706 Expr GetQuantifierEliminationCommand::getResult() const { return d_result; }
2707 void GetQuantifierEliminationCommand::printResult(std::ostream& out,
2708                                                   uint32_t verbosity) const
2709 {
2710   if (!ok())
2711   {
2712     this->Command::printResult(out, verbosity);
2713   }
2714   else
2715   {
2716     out << d_result << endl;
2717   }
2718 }
2719
2720 Command* GetQuantifierEliminationCommand::exportTo(
2721     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2722 {
2723   GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(
2724       d_expr.exportTo(exprManager, variableMap), d_doFull);
2725   c->d_result = d_result;
2726   return c;
2727 }
2728
2729 Command* GetQuantifierEliminationCommand::clone() const
2730 {
2731   GetQuantifierEliminationCommand* c =
2732       new GetQuantifierEliminationCommand(d_expr, d_doFull);
2733   c->d_result = d_result;
2734   return c;
2735 }
2736
2737 std::string GetQuantifierEliminationCommand::getCommandName() const
2738 {
2739   return d_doFull ? "get-qe" : "get-qe-disjunct";
2740 }
2741
2742 void GetQuantifierEliminationCommand::toStream(std::ostream& out,
2743                                                int toDepth,
2744                                                bool types,
2745                                                size_t dag,
2746                                                OutputLanguage language) const
2747 {
2748   Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
2749       out, Node::fromExpr(d_expr));
2750 }
2751
2752 /* -------------------------------------------------------------------------- */
2753 /* class GetUnsatAssumptionsCommand                                           */
2754 /* -------------------------------------------------------------------------- */
2755
2756 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
2757
2758 void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine)
2759 {
2760   try
2761   {
2762     std::vector<Node> uassumps = smtEngine->getUnsatAssumptions();
2763     d_result.clear();
2764     for (const Node& n : uassumps)
2765     {
2766       d_result.push_back(n.toExpr());
2767     }
2768     d_commandStatus = CommandSuccess::instance();
2769   }
2770   catch (RecoverableModalException& e)
2771   {
2772     d_commandStatus = new CommandRecoverableFailure(e.what());
2773   }
2774   catch (exception& e)
2775   {
2776     d_commandStatus = new CommandFailure(e.what());
2777   }
2778 }
2779
2780 std::vector<Expr> GetUnsatAssumptionsCommand::getResult() const
2781 {
2782   return d_result;
2783 }
2784
2785 void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
2786                                              uint32_t verbosity) const
2787 {
2788   if (!ok())
2789   {
2790     this->Command::printResult(out, verbosity);
2791   }
2792   else
2793   {
2794     container_to_stream(out, d_result, "(", ")\n", " ");
2795   }
2796 }
2797
2798 Command* GetUnsatAssumptionsCommand::exportTo(
2799     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2800 {
2801   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
2802   c->d_result = d_result;
2803   return c;
2804 }
2805
2806 Command* GetUnsatAssumptionsCommand::clone() const
2807 {
2808   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
2809   c->d_result = d_result;
2810   return c;
2811 }
2812
2813 std::string GetUnsatAssumptionsCommand::getCommandName() const
2814 {
2815   return "get-unsat-assumptions";
2816 }
2817
2818 void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
2819                                           int toDepth,
2820                                           bool types,
2821                                           size_t dag,
2822                                           OutputLanguage language) const
2823 {
2824   Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
2825 }
2826
2827 /* -------------------------------------------------------------------------- */
2828 /* class GetUnsatCoreCommand                                                  */
2829 /* -------------------------------------------------------------------------- */
2830
2831 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
2832 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine)
2833 {
2834   try
2835   {
2836     d_result = smtEngine->getUnsatCore();
2837     d_commandStatus = CommandSuccess::instance();
2838   }
2839   catch (RecoverableModalException& e)
2840   {
2841     d_commandStatus = new CommandRecoverableFailure(e.what());
2842   }
2843   catch (exception& e)
2844   {
2845     d_commandStatus = new CommandFailure(e.what());
2846   }
2847 }
2848
2849 void GetUnsatCoreCommand::printResult(std::ostream& out,
2850                                       uint32_t verbosity) const
2851 {
2852   if (!ok())
2853   {
2854     this->Command::printResult(out, verbosity);
2855   }
2856   else
2857   {
2858     d_result.toStream(out);
2859   }
2860 }
2861
2862 const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const
2863 {
2864   // of course, this will be empty if the command hasn't been invoked yet
2865   return d_result;
2866 }
2867
2868 Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager,
2869                                        ExprManagerMapCollection& variableMap)
2870 {
2871   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
2872   c->d_result = d_result;
2873   return c;
2874 }
2875
2876 Command* GetUnsatCoreCommand::clone() const
2877 {
2878   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
2879   c->d_result = d_result;
2880   return c;
2881 }
2882
2883 std::string GetUnsatCoreCommand::getCommandName() const
2884 {
2885   return "get-unsat-core";
2886 }
2887
2888 void GetUnsatCoreCommand::toStream(std::ostream& out,
2889                                    int toDepth,
2890                                    bool types,
2891                                    size_t dag,
2892                                    OutputLanguage language) const
2893 {
2894   Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
2895 }
2896
2897 /* -------------------------------------------------------------------------- */
2898 /* class GetAssertionsCommand                                                 */
2899 /* -------------------------------------------------------------------------- */
2900
2901 GetAssertionsCommand::GetAssertionsCommand() {}
2902 void GetAssertionsCommand::invoke(SmtEngine* smtEngine)
2903 {
2904   try
2905   {
2906     stringstream ss;
2907     const vector<Expr> v = smtEngine->getAssertions();
2908     ss << "(\n";
2909     copy(v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n"));
2910     ss << ")\n";
2911     d_result = ss.str();
2912     d_commandStatus = CommandSuccess::instance();
2913   }
2914   catch (exception& e)
2915   {
2916     d_commandStatus = new CommandFailure(e.what());
2917   }
2918 }
2919
2920 std::string GetAssertionsCommand::getResult() const { return d_result; }
2921 void GetAssertionsCommand::printResult(std::ostream& out,
2922                                        uint32_t verbosity) const
2923 {
2924   if (!ok())
2925   {
2926     this->Command::printResult(out, verbosity);
2927   }
2928   else
2929   {
2930     out << d_result;
2931   }
2932 }
2933
2934 Command* GetAssertionsCommand::exportTo(ExprManager* exprManager,
2935                                         ExprManagerMapCollection& variableMap)
2936 {
2937   GetAssertionsCommand* c = new GetAssertionsCommand();
2938   c->d_result = d_result;
2939   return c;
2940 }
2941
2942 Command* GetAssertionsCommand::clone() const
2943 {
2944   GetAssertionsCommand* c = new GetAssertionsCommand();
2945   c->d_result = d_result;
2946   return c;
2947 }
2948
2949 std::string GetAssertionsCommand::getCommandName() const
2950 {
2951   return "get-assertions";
2952 }
2953
2954 void GetAssertionsCommand::toStream(std::ostream& out,
2955                                     int toDepth,
2956                                     bool types,
2957                                     size_t dag,
2958                                     OutputLanguage language) const
2959 {
2960   Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
2961 }
2962
2963 /* -------------------------------------------------------------------------- */
2964 /* class SetBenchmarkStatusCommand                                            */
2965 /* -------------------------------------------------------------------------- */
2966
2967 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
2968     : d_status(status)
2969 {
2970 }
2971
2972 BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
2973 {
2974   return d_status;
2975 }
2976
2977 void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine)
2978 {
2979   try
2980   {
2981     stringstream ss;
2982     ss << d_status;
2983     SExpr status = SExpr(ss.str());
2984     smtEngine->setInfo("status", status);
2985     d_commandStatus = CommandSuccess::instance();
2986   }
2987   catch (exception& e)
2988   {
2989     d_commandStatus = new CommandFailure(e.what());
2990   }
2991 }
2992
2993 Command* SetBenchmarkStatusCommand::exportTo(
2994     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2995 {
2996   return new SetBenchmarkStatusCommand(d_status);
2997 }
2998
2999 Command* SetBenchmarkStatusCommand::clone() const
3000 {
3001   return new SetBenchmarkStatusCommand(d_status);
3002 }
3003
3004 std::string SetBenchmarkStatusCommand::getCommandName() const
3005 {
3006   return "set-info";
3007 }
3008
3009 void SetBenchmarkStatusCommand::toStream(std::ostream& out,
3010                                          int toDepth,
3011                                          bool types,
3012                                          size_t dag,
3013                                          OutputLanguage language) const
3014 {
3015   Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, d_status);
3016 }
3017
3018 /* -------------------------------------------------------------------------- */
3019 /* class SetBenchmarkLogicCommand                                             */
3020 /* -------------------------------------------------------------------------- */
3021
3022 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
3023     : d_logic(logic)
3024 {
3025 }
3026
3027 std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
3028 void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine)
3029 {
3030   try
3031   {
3032     smtEngine->setLogic(d_logic);
3033     d_commandStatus = CommandSuccess::instance();
3034   }
3035   catch (exception& e)
3036   {
3037     d_commandStatus = new CommandFailure(e.what());
3038   }
3039 }
3040
3041 Command* SetBenchmarkLogicCommand::exportTo(
3042     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
3043 {
3044   return new SetBenchmarkLogicCommand(d_logic);
3045 }
3046
3047 Command* SetBenchmarkLogicCommand::clone() const
3048 {
3049   return new SetBenchmarkLogicCommand(d_logic);
3050 }
3051
3052 std::string SetBenchmarkLogicCommand::getCommandName() const
3053 {
3054   return "set-logic";
3055 }
3056
3057 void SetBenchmarkLogicCommand::toStream(std::ostream& out,
3058                                         int toDepth,
3059                                         bool types,
3060                                         size_t dag,
3061                                         OutputLanguage language) const
3062 {
3063   Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
3064 }
3065
3066 /* -------------------------------------------------------------------------- */
3067 /* class SetInfoCommand                                                       */
3068 /* -------------------------------------------------------------------------- */
3069
3070 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
3071     : d_flag(flag), d_sexpr(sexpr)
3072 {
3073 }
3074
3075 std::string SetInfoCommand::getFlag() const { return d_flag; }
3076 SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
3077 void SetInfoCommand::invoke(SmtEngine* smtEngine)
3078 {
3079   try
3080   {
3081     smtEngine->setInfo(d_flag, d_sexpr);
3082     d_commandStatus = CommandSuccess::instance();
3083   }
3084   catch (UnrecognizedOptionException&)
3085   {
3086     // As per SMT-LIB spec, silently accept unknown set-info keys
3087     d_commandStatus = CommandSuccess::instance();
3088   }
3089   catch (exception& e)
3090   {
3091     d_commandStatus = new CommandFailure(e.what());
3092   }
3093 }
3094
3095 Command* SetInfoCommand::exportTo(ExprManager* exprManager,
3096                                   ExprManagerMapCollection& variableMap)
3097 {
3098   return new SetInfoCommand(d_flag, d_sexpr);
3099 }
3100
3101 Command* SetInfoCommand::clone() const
3102 {
3103   return new SetInfoCommand(d_flag, d_sexpr);
3104 }
3105
3106 std::string SetInfoCommand::getCommandName() const { return "set-info"; }
3107
3108 void SetInfoCommand::toStream(std::ostream& out,
3109                               int toDepth,
3110                               bool types,
3111                               size_t dag,
3112                               OutputLanguage language) const
3113 {
3114   Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_sexpr);
3115 }
3116
3117 /* -------------------------------------------------------------------------- */
3118 /* class GetInfoCommand                                                       */
3119 /* -------------------------------------------------------------------------- */
3120
3121 GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
3122 std::string GetInfoCommand::getFlag() const { return d_flag; }
3123 void GetInfoCommand::invoke(SmtEngine* smtEngine)
3124 {
3125   try
3126   {
3127     vector<SExpr> v;
3128     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
3129     v.push_back(smtEngine->getInfo(d_flag));
3130     stringstream ss;
3131     if (d_flag == "all-options" || d_flag == "all-statistics")
3132     {
3133       ss << PrettySExprs(true);
3134     }
3135     ss << SExpr(v);
3136     d_result = ss.str();
3137     d_commandStatus = CommandSuccess::instance();
3138   }
3139   catch (UnrecognizedOptionException&)
3140   {
3141     d_commandStatus = new CommandUnsupported();
3142   }
3143   catch (RecoverableModalException& e)
3144   {
3145     d_commandStatus = new CommandRecoverableFailure(e.what());
3146   }
3147   catch (exception& e)
3148   {
3149     d_commandStatus = new CommandFailure(e.what());
3150   }
3151 }
3152
3153 std::string GetInfoCommand::getResult() const { return d_result; }
3154 void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
3155 {
3156   if (!ok())
3157   {
3158     this->Command::printResult(out, verbosity);
3159   }
3160   else if (d_result != "")
3161   {
3162     out << d_result << endl;
3163   }
3164 }
3165
3166 Command* GetInfoCommand::exportTo(ExprManager* exprManager,
3167                                   ExprManagerMapCollection& variableMap)
3168 {
3169   GetInfoCommand* c = new GetInfoCommand(d_flag);
3170   c->d_result = d_result;
3171   return c;
3172 }
3173
3174 Command* GetInfoCommand::clone() const
3175 {
3176   GetInfoCommand* c = new GetInfoCommand(d_flag);
3177   c->d_result = d_result;
3178   return c;
3179 }
3180
3181 std::string GetInfoCommand::getCommandName() const { return "get-info"; }
3182
3183 void GetInfoCommand::toStream(std::ostream& out,
3184                               int toDepth,
3185                               bool types,
3186                               size_t dag,
3187                               OutputLanguage language) const
3188 {
3189   Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
3190 }
3191
3192 /* -------------------------------------------------------------------------- */
3193 /* class SetOptionCommand                                                     */
3194 /* -------------------------------------------------------------------------- */
3195
3196 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
3197     : d_flag(flag), d_sexpr(sexpr)
3198 {
3199 }
3200
3201 std::string SetOptionCommand::getFlag() const { return d_flag; }
3202 SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
3203 void SetOptionCommand::invoke(SmtEngine* smtEngine)
3204 {
3205   try
3206   {
3207     smtEngine->setOption(d_flag, d_sexpr);
3208     d_commandStatus = CommandSuccess::instance();
3209   }
3210   catch (UnrecognizedOptionException&)
3211   {
3212     d_commandStatus = new CommandUnsupported();
3213   }
3214   catch (exception& e)
3215   {
3216     d_commandStatus = new CommandFailure(e.what());
3217   }
3218 }
3219
3220 Command* SetOptionCommand::exportTo(ExprManager* exprManager,
3221                                     ExprManagerMapCollection& variableMap)
3222 {
3223   return new SetOptionCommand(d_flag, d_sexpr);
3224 }
3225
3226 Command* SetOptionCommand::clone() const
3227 {
3228   return new SetOptionCommand(d_flag, d_sexpr);
3229 }
3230
3231 std::string SetOptionCommand::getCommandName() const { return "set-option"; }
3232
3233 void SetOptionCommand::toStream(std::ostream& out,
3234                                 int toDepth,
3235                                 bool types,
3236                                 size_t dag,
3237                                 OutputLanguage language) const
3238 {
3239   Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_sexpr);
3240 }
3241
3242 /* -------------------------------------------------------------------------- */
3243 /* class GetOptionCommand                                                     */
3244 /* -------------------------------------------------------------------------- */
3245
3246 GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
3247 std::string GetOptionCommand::getFlag() const { return d_flag; }
3248 void GetOptionCommand::invoke(SmtEngine* smtEngine)
3249 {
3250   try
3251   {
3252     SExpr res = smtEngine->getOption(d_flag);
3253     d_result = res.toString();
3254     d_commandStatus = CommandSuccess::instance();
3255   }
3256   catch (UnrecognizedOptionException&)
3257   {
3258     d_commandStatus = new CommandUnsupported();
3259   }
3260   catch (exception& e)
3261   {
3262     d_commandStatus = new CommandFailure(e.what());
3263   }
3264 }
3265
3266 std::string GetOptionCommand::getResult() const { return d_result; }
3267 void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
3268 {
3269   if (!ok())
3270   {
3271     this->Command::printResult(out, verbosity);
3272   }
3273   else if (d_result != "")
3274   {
3275     out << d_result << endl;
3276   }
3277 }
3278
3279 Command* GetOptionCommand::exportTo(ExprManager* exprManager,
3280                                     ExprManagerMapCollection& variableMap)
3281 {
3282   GetOptionCommand* c = new GetOptionCommand(d_flag);
3283   c->d_result = d_result;
3284   return c;
3285 }
3286
3287 Command* GetOptionCommand::clone() const
3288 {
3289   GetOptionCommand* c = new GetOptionCommand(d_flag);
3290   c->d_result = d_result;
3291   return c;
3292 }
3293
3294 std::string GetOptionCommand::getCommandName() const { return "get-option"; }
3295
3296 void GetOptionCommand::toStream(std::ostream& out,
3297                                 int toDepth,
3298                                 bool types,
3299                                 size_t dag,
3300                                 OutputLanguage language) const
3301 {
3302   Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
3303 }
3304
3305 /* -------------------------------------------------------------------------- */
3306 /* class SetExpressionNameCommand                                             */
3307 /* -------------------------------------------------------------------------- */
3308
3309 SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name)
3310     : d_expr(expr), d_name(name)
3311 {
3312 }
3313
3314 void SetExpressionNameCommand::invoke(SmtEngine* smtEngine)
3315 {
3316   smtEngine->setExpressionName(d_expr, d_name);
3317   d_commandStatus = CommandSuccess::instance();
3318 }
3319
3320 Command* SetExpressionNameCommand::exportTo(
3321     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
3322 {
3323   SetExpressionNameCommand* c = new SetExpressionNameCommand(
3324       d_expr.exportTo(exprManager, variableMap), d_name);
3325   return c;
3326 }
3327
3328 Command* SetExpressionNameCommand::clone() const
3329 {
3330   SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name);
3331   return c;
3332 }
3333
3334 std::string SetExpressionNameCommand::getCommandName() const
3335 {
3336   return "set-expr-name";
3337 }
3338
3339 void SetExpressionNameCommand::toStream(std::ostream& out,
3340                                         int toDepth,
3341                                         bool types,
3342                                         size_t dag,
3343                                         OutputLanguage language) const
3344 {
3345   Printer::getPrinter(language)->toStreamCmdSetExpressionName(
3346       out, Node::fromExpr(d_expr), d_name);
3347 }
3348
3349 /* -------------------------------------------------------------------------- */
3350 /* class DatatypeDeclarationCommand                                           */
3351 /* -------------------------------------------------------------------------- */
3352
3353 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const Type& datatype)
3354     : d_datatypes()
3355 {
3356   d_datatypes.push_back(datatype);
3357 }
3358
3359 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
3360     const std::vector<Type>& datatypes)
3361     : d_datatypes(datatypes)
3362 {
3363 }
3364
3365 const std::vector<Type>& DatatypeDeclarationCommand::getDatatypes() const
3366 {
3367   return d_datatypes;
3368 }
3369
3370 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine)
3371 {
3372   d_commandStatus = CommandSuccess::instance();
3373 }
3374
3375 Command* DatatypeDeclarationCommand::exportTo(
3376     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
3377 {
3378   throw ExportUnsupportedException(
3379       "export of DatatypeDeclarationCommand unsupported");
3380 }
3381
3382 Command* DatatypeDeclarationCommand::clone() const
3383 {
3384   return new DatatypeDeclarationCommand(d_datatypes);
3385 }
3386
3387 std::string DatatypeDeclarationCommand::getCommandName() const
3388 {
3389   return "declare-datatypes";
3390 }
3391
3392 void DatatypeDeclarationCommand::toStream(std::ostream& out,
3393                                           int toDepth,
3394                                           bool types,
3395                                           size_t dag,
3396                                           OutputLanguage language) const
3397 {
3398   Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
3399       out, typeVectorToTypeNodes(d_datatypes));
3400 }
3401
3402 }  // namespace CVC4