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