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->query(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     : DeclarationDefinitionCommand(id),
1271       d_func(func),
1272       d_formals(),
1273       d_formula(formula)
1274 {
1275 }
1276
1277 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
1278                                              Expr func,
1279                                              const std::vector<Expr>& formals,
1280                                              Expr formula)
1281     : DeclarationDefinitionCommand(id),
1282       d_func(func),
1283       d_formals(formals),
1284       d_formula(formula)
1285 {
1286 }
1287
1288 Expr DefineFunctionCommand::getFunction() const { return d_func; }
1289 const std::vector<Expr>& DefineFunctionCommand::getFormals() const
1290 {
1291   return d_formals;
1292 }
1293
1294 Expr DefineFunctionCommand::getFormula() const { return d_formula; }
1295 void DefineFunctionCommand::invoke(SmtEngine* smtEngine)
1296 {
1297   try
1298   {
1299     if (!d_func.isNull())
1300     {
1301       smtEngine->defineFunction(d_func, d_formals, d_formula);
1302     }
1303     d_commandStatus = CommandSuccess::instance();
1304   }
1305   catch (exception& e)
1306   {
1307     d_commandStatus = new CommandFailure(e.what());
1308   }
1309 }
1310
1311 Command* DefineFunctionCommand::exportTo(ExprManager* exprManager,
1312                                          ExprManagerMapCollection& variableMap)
1313 {
1314   Expr func = d_func.exportTo(
1315       exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
1316   vector<Expr> formals;
1317   transform(d_formals.begin(),
1318             d_formals.end(),
1319             back_inserter(formals),
1320             ExportTransformer(exprManager, variableMap));
1321   Expr formula = d_formula.exportTo(exprManager, variableMap);
1322   return new DefineFunctionCommand(d_symbol, func, formals, formula);
1323 }
1324
1325 Command* DefineFunctionCommand::clone() const
1326 {
1327   return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula);
1328 }
1329
1330 std::string DefineFunctionCommand::getCommandName() const
1331 {
1332   return "define-fun";
1333 }
1334
1335 /* -------------------------------------------------------------------------- */
1336 /* class DefineNamedFunctionCommand                                           */
1337 /* -------------------------------------------------------------------------- */
1338
1339 DefineNamedFunctionCommand::DefineNamedFunctionCommand(
1340     const std::string& id,
1341     Expr func,
1342     const std::vector<Expr>& formals,
1343     Expr formula)
1344     : DefineFunctionCommand(id, func, formals, formula)
1345 {
1346 }
1347
1348 void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine)
1349 {
1350   this->DefineFunctionCommand::invoke(smtEngine);
1351   if (!d_func.isNull() && d_func.getType().isBoolean())
1352   {
1353     smtEngine->addToAssignment(d_func);
1354   }
1355   d_commandStatus = CommandSuccess::instance();
1356 }
1357
1358 Command* DefineNamedFunctionCommand::exportTo(
1359     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1360 {
1361   Expr func = d_func.exportTo(exprManager, variableMap);
1362   vector<Expr> formals;
1363   transform(d_formals.begin(),
1364             d_formals.end(),
1365             back_inserter(formals),
1366             ExportTransformer(exprManager, variableMap));
1367   Expr formula = d_formula.exportTo(exprManager, variableMap);
1368   return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
1369 }
1370
1371 Command* DefineNamedFunctionCommand::clone() const
1372 {
1373   return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
1374 }
1375
1376 /* -------------------------------------------------------------------------- */
1377 /* class DefineFunctionRecCommand                                             */
1378 /* -------------------------------------------------------------------------- */
1379
1380 DefineFunctionRecCommand::DefineFunctionRecCommand(
1381     Expr func, const std::vector<Expr>& formals, Expr formula)
1382 {
1383   d_funcs.push_back(func);
1384   d_formals.push_back(formals);
1385   d_formulas.push_back(formula);
1386 }
1387
1388 DefineFunctionRecCommand::DefineFunctionRecCommand(
1389     const std::vector<Expr>& funcs,
1390     const std::vector<std::vector<Expr>>& formals,
1391     const std::vector<Expr>& formulas)
1392 {
1393   d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end());
1394   d_formals.insert(d_formals.end(), formals.begin(), formals.end());
1395   d_formulas.insert(d_formulas.end(), formulas.begin(), formulas.end());
1396 }
1397
1398 const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const
1399 {
1400   return d_funcs;
1401 }
1402
1403 const std::vector<std::vector<Expr>>& DefineFunctionRecCommand::getFormals()
1404     const
1405 {
1406   return d_formals;
1407 }
1408
1409 const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const
1410 {
1411   return d_formulas;
1412 }
1413
1414 void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine)
1415 {
1416   try
1417   {
1418     smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas);
1419     d_commandStatus = CommandSuccess::instance();
1420   }
1421   catch (exception& e)
1422   {
1423     d_commandStatus = new CommandFailure(e.what());
1424   }
1425 }
1426
1427 Command* DefineFunctionRecCommand::exportTo(
1428     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1429 {
1430   std::vector<Expr> funcs;
1431   for (unsigned i = 0, size = d_funcs.size(); i < size; i++)
1432   {
1433     Expr func = d_funcs[i].exportTo(
1434         exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
1435     funcs.push_back(func);
1436   }
1437   std::vector<std::vector<Expr>> formals;
1438   for (unsigned i = 0, size = d_formals.size(); i < size; i++)
1439   {
1440     std::vector<Expr> formals_c;
1441     transform(d_formals[i].begin(),
1442               d_formals[i].end(),
1443               back_inserter(formals_c),
1444               ExportTransformer(exprManager, variableMap));
1445     formals.push_back(formals_c);
1446   }
1447   std::vector<Expr> formulas;
1448   for (unsigned i = 0, size = d_formulas.size(); i < size; i++)
1449   {
1450     Expr formula = d_formulas[i].exportTo(exprManager, variableMap);
1451     formulas.push_back(formula);
1452   }
1453   return new DefineFunctionRecCommand(funcs, formals, formulas);
1454 }
1455
1456 Command* DefineFunctionRecCommand::clone() const
1457 {
1458   return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas);
1459 }
1460
1461 std::string DefineFunctionRecCommand::getCommandName() const
1462 {
1463   return "define-fun-rec";
1464 }
1465
1466 /* -------------------------------------------------------------------------- */
1467 /* class SetUserAttribute                                                     */
1468 /* -------------------------------------------------------------------------- */
1469
1470 SetUserAttributeCommand::SetUserAttributeCommand(
1471     const std::string& attr,
1472     Expr expr,
1473     const std::vector<Expr>& expr_values,
1474     const std::string& str_value)
1475     : d_attr(attr),
1476       d_expr(expr),
1477       d_expr_values(expr_values),
1478       d_str_value(str_value)
1479 {
1480 }
1481
1482 SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
1483                                                  Expr expr)
1484     : SetUserAttributeCommand(attr, expr, {}, "")
1485 {
1486 }
1487
1488 SetUserAttributeCommand::SetUserAttributeCommand(
1489     const std::string& attr, Expr expr, const std::vector<Expr>& values)
1490     : SetUserAttributeCommand(attr, expr, values, "")
1491 {
1492 }
1493
1494 SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
1495                                                  Expr expr,
1496                                                  const std::string& value)
1497     : SetUserAttributeCommand(attr, expr, {}, value)
1498 {
1499 }
1500
1501 void SetUserAttributeCommand::invoke(SmtEngine* smtEngine)
1502 {
1503   try
1504   {
1505     if (!d_expr.isNull())
1506     {
1507       smtEngine->setUserAttribute(d_attr, d_expr, d_expr_values, d_str_value);
1508     }
1509     d_commandStatus = CommandSuccess::instance();
1510   }
1511   catch (exception& e)
1512   {
1513     d_commandStatus = new CommandFailure(e.what());
1514   }
1515 }
1516
1517 Command* SetUserAttributeCommand::exportTo(
1518     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1519 {
1520   Expr expr = d_expr.exportTo(exprManager, variableMap);
1521   return new SetUserAttributeCommand(d_attr, expr, d_expr_values, d_str_value);
1522 }
1523
1524 Command* SetUserAttributeCommand::clone() const
1525 {
1526   return new SetUserAttributeCommand(
1527       d_attr, d_expr, d_expr_values, d_str_value);
1528 }
1529
1530 std::string SetUserAttributeCommand::getCommandName() const
1531 {
1532   return "set-user-attribute";
1533 }
1534
1535 /* -------------------------------------------------------------------------- */
1536 /* class SimplifyCommand                                                      */
1537 /* -------------------------------------------------------------------------- */
1538
1539 SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) {}
1540 Expr SimplifyCommand::getTerm() const { return d_term; }
1541 void SimplifyCommand::invoke(SmtEngine* smtEngine)
1542 {
1543   try
1544   {
1545     d_result = smtEngine->simplify(d_term);
1546     d_commandStatus = CommandSuccess::instance();
1547   }
1548   catch (UnsafeInterruptException& e)
1549   {
1550     d_commandStatus = new CommandInterrupted();
1551   }
1552   catch (exception& e)
1553   {
1554     d_commandStatus = new CommandFailure(e.what());
1555   }
1556 }
1557
1558 Expr SimplifyCommand::getResult() const { return d_result; }
1559 void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
1560 {
1561   if (!ok())
1562   {
1563     this->Command::printResult(out, verbosity);
1564   }
1565   else
1566   {
1567     out << d_result << endl;
1568   }
1569 }
1570
1571 Command* SimplifyCommand::exportTo(ExprManager* exprManager,
1572                                    ExprManagerMapCollection& variableMap)
1573 {
1574   SimplifyCommand* c =
1575       new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
1576   c->d_result = d_result.exportTo(exprManager, variableMap);
1577   return c;
1578 }
1579
1580 Command* SimplifyCommand::clone() const
1581 {
1582   SimplifyCommand* c = new SimplifyCommand(d_term);
1583   c->d_result = d_result;
1584   return c;
1585 }
1586
1587 std::string SimplifyCommand::getCommandName() const { return "simplify"; }
1588
1589 /* -------------------------------------------------------------------------- */
1590 /* class ExpandDefinitionsCommand                                             */
1591 /* -------------------------------------------------------------------------- */
1592
1593 ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {}
1594 Expr ExpandDefinitionsCommand::getTerm() const { return d_term; }
1595 void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine)
1596 {
1597   d_result = smtEngine->expandDefinitions(d_term);
1598   d_commandStatus = CommandSuccess::instance();
1599 }
1600
1601 Expr ExpandDefinitionsCommand::getResult() const { return d_result; }
1602 void ExpandDefinitionsCommand::printResult(std::ostream& out,
1603                                            uint32_t verbosity) const
1604 {
1605   if (!ok())
1606   {
1607     this->Command::printResult(out, verbosity);
1608   }
1609   else
1610   {
1611     out << d_result << endl;
1612   }
1613 }
1614
1615 Command* ExpandDefinitionsCommand::exportTo(
1616     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1617 {
1618   ExpandDefinitionsCommand* c =
1619       new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
1620   c->d_result = d_result.exportTo(exprManager, variableMap);
1621   return c;
1622 }
1623
1624 Command* ExpandDefinitionsCommand::clone() const
1625 {
1626   ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
1627   c->d_result = d_result;
1628   return c;
1629 }
1630
1631 std::string ExpandDefinitionsCommand::getCommandName() const
1632 {
1633   return "expand-definitions";
1634 }
1635
1636 /* -------------------------------------------------------------------------- */
1637 /* class GetValueCommand                                                      */
1638 /* -------------------------------------------------------------------------- */
1639
1640 GetValueCommand::GetValueCommand(Expr term) : d_terms()
1641 {
1642   d_terms.push_back(term);
1643 }
1644
1645 GetValueCommand::GetValueCommand(const std::vector<Expr>& terms)
1646     : d_terms(terms)
1647 {
1648   PrettyCheckArgument(
1649       terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
1650 }
1651
1652 const std::vector<Expr>& GetValueCommand::getTerms() const { return d_terms; }
1653 void GetValueCommand::invoke(SmtEngine* smtEngine)
1654 {
1655   try
1656   {
1657     ExprManager* em = smtEngine->getExprManager();
1658     NodeManager* nm = NodeManager::fromExprManager(em);
1659     smt::SmtScope scope(smtEngine);
1660     vector<Expr> result = smtEngine->getValues(d_terms);
1661     Assert(result.size() == d_terms.size());
1662     for (int i = 0, size = d_terms.size(); i < size; i++)
1663     {
1664       Expr e = d_terms[i];
1665       Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
1666       Node request = Node::fromExpr(
1667           options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e);
1668       Node value = Node::fromExpr(result[i]);
1669       if (value.getType().isInteger() && request.getType() == nm->realType())
1670       {
1671         // Need to wrap in division-by-one so that output printers know this
1672         // is an integer-looking constant that really should be output as
1673         // a rational.  Necessary for SMT-LIB standards compliance.
1674         value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
1675       }
1676       result[i] = nm->mkNode(kind::SEXPR, request, value).toExpr();
1677     }
1678     d_result = em->mkExpr(kind::SEXPR, result);
1679     d_commandStatus = CommandSuccess::instance();
1680   }
1681   catch (RecoverableModalException& e)
1682   {
1683     d_commandStatus = new CommandRecoverableFailure(e.what());
1684   }
1685   catch (UnsafeInterruptException& e)
1686   {
1687     d_commandStatus = new CommandInterrupted();
1688   }
1689   catch (exception& e)
1690   {
1691     d_commandStatus = new CommandFailure(e.what());
1692   }
1693 }
1694
1695 Expr GetValueCommand::getResult() const { return d_result; }
1696 void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
1697 {
1698   if (!ok())
1699   {
1700     this->Command::printResult(out, verbosity);
1701   }
1702   else
1703   {
1704     expr::ExprDag::Scope scope(out, false);
1705     out << d_result << endl;
1706   }
1707 }
1708
1709 Command* GetValueCommand::exportTo(ExprManager* exprManager,
1710                                    ExprManagerMapCollection& variableMap)
1711 {
1712   vector<Expr> exportedTerms;
1713   for (std::vector<Expr>::const_iterator i = d_terms.begin();
1714        i != d_terms.end();
1715        ++i)
1716   {
1717     exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
1718   }
1719   GetValueCommand* c = new GetValueCommand(exportedTerms);
1720   c->d_result = d_result.exportTo(exprManager, variableMap);
1721   return c;
1722 }
1723
1724 Command* GetValueCommand::clone() const
1725 {
1726   GetValueCommand* c = new GetValueCommand(d_terms);
1727   c->d_result = d_result;
1728   return c;
1729 }
1730
1731 std::string GetValueCommand::getCommandName() const { return "get-value"; }
1732
1733 /* -------------------------------------------------------------------------- */
1734 /* class GetAssignmentCommand                                                 */
1735 /* -------------------------------------------------------------------------- */
1736
1737 GetAssignmentCommand::GetAssignmentCommand() {}
1738 void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
1739 {
1740   try
1741   {
1742     std::vector<std::pair<Expr, Expr>> assignments = smtEngine->getAssignment();
1743     vector<SExpr> sexprs;
1744     for (const auto& p : assignments)
1745     {
1746       vector<SExpr> v;
1747       v.emplace_back(SExpr::Keyword(p.first.toString()));
1748       v.emplace_back(SExpr::Keyword(p.second.toString()));
1749       sexprs.emplace_back(v);
1750     }
1751     d_result = SExpr(sexprs);
1752     d_commandStatus = CommandSuccess::instance();
1753   }
1754   catch (RecoverableModalException& e)
1755   {
1756     d_commandStatus = new CommandRecoverableFailure(e.what());
1757   }
1758   catch (UnsafeInterruptException& e)
1759   {
1760     d_commandStatus = new CommandInterrupted();
1761   }
1762   catch (exception& e)
1763   {
1764     d_commandStatus = new CommandFailure(e.what());
1765   }
1766 }
1767
1768 SExpr GetAssignmentCommand::getResult() const { return d_result; }
1769 void GetAssignmentCommand::printResult(std::ostream& out,
1770                                        uint32_t verbosity) const
1771 {
1772   if (!ok())
1773   {
1774     this->Command::printResult(out, verbosity);
1775   }
1776   else
1777   {
1778     out << d_result << endl;
1779   }
1780 }
1781
1782 Command* GetAssignmentCommand::exportTo(ExprManager* exprManager,
1783                                         ExprManagerMapCollection& variableMap)
1784 {
1785   GetAssignmentCommand* c = new GetAssignmentCommand();
1786   c->d_result = d_result;
1787   return c;
1788 }
1789
1790 Command* GetAssignmentCommand::clone() const
1791 {
1792   GetAssignmentCommand* c = new GetAssignmentCommand();
1793   c->d_result = d_result;
1794   return c;
1795 }
1796
1797 std::string GetAssignmentCommand::getCommandName() const
1798 {
1799   return "get-assignment";
1800 }
1801
1802 /* -------------------------------------------------------------------------- */
1803 /* class GetModelCommand                                                      */
1804 /* -------------------------------------------------------------------------- */
1805
1806 GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
1807 void GetModelCommand::invoke(SmtEngine* smtEngine)
1808 {
1809   try
1810   {
1811     d_result = smtEngine->getModel();
1812     d_smtEngine = smtEngine;
1813     d_commandStatus = CommandSuccess::instance();
1814   }
1815   catch (RecoverableModalException& e)
1816   {
1817     d_commandStatus = new CommandRecoverableFailure(e.what());
1818   }
1819   catch (UnsafeInterruptException& e)
1820   {
1821     d_commandStatus = new CommandInterrupted();
1822   }
1823   catch (exception& e)
1824   {
1825     d_commandStatus = new CommandFailure(e.what());
1826   }
1827 }
1828
1829 /* Model is private to the library -- for now
1830 Model* GetModelCommand::getResult() const  {
1831   return d_result;
1832 }
1833 */
1834
1835 void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
1836 {
1837   if (!ok())
1838   {
1839     this->Command::printResult(out, verbosity);
1840   }
1841   else
1842   {
1843     out << *d_result;
1844   }
1845 }
1846
1847 Command* GetModelCommand::exportTo(ExprManager* exprManager,
1848                                    ExprManagerMapCollection& variableMap)
1849 {
1850   GetModelCommand* c = new GetModelCommand();
1851   c->d_result = d_result;
1852   c->d_smtEngine = d_smtEngine;
1853   return c;
1854 }
1855
1856 Command* GetModelCommand::clone() const
1857 {
1858   GetModelCommand* c = new GetModelCommand();
1859   c->d_result = d_result;
1860   c->d_smtEngine = d_smtEngine;
1861   return c;
1862 }
1863
1864 std::string GetModelCommand::getCommandName() const { return "get-model"; }
1865
1866 /* -------------------------------------------------------------------------- */
1867 /* class BlockModelCommand */
1868 /* -------------------------------------------------------------------------- */
1869
1870 BlockModelCommand::BlockModelCommand() {}
1871 void BlockModelCommand::invoke(SmtEngine* smtEngine)
1872 {
1873   try
1874   {
1875     smtEngine->blockModel();
1876     d_commandStatus = CommandSuccess::instance();
1877   }
1878   catch (RecoverableModalException& e)
1879   {
1880     d_commandStatus = new CommandRecoverableFailure(e.what());
1881   }
1882   catch (UnsafeInterruptException& e)
1883   {
1884     d_commandStatus = new CommandInterrupted();
1885   }
1886   catch (exception& e)
1887   {
1888     d_commandStatus = new CommandFailure(e.what());
1889   }
1890 }
1891
1892 Command* BlockModelCommand::exportTo(ExprManager* exprManager,
1893                                      ExprManagerMapCollection& variableMap)
1894 {
1895   BlockModelCommand* c = new BlockModelCommand();
1896   return c;
1897 }
1898
1899 Command* BlockModelCommand::clone() const
1900 {
1901   BlockModelCommand* c = new BlockModelCommand();
1902   return c;
1903 }
1904
1905 std::string BlockModelCommand::getCommandName() const { return "block-model"; }
1906
1907 /* -------------------------------------------------------------------------- */
1908 /* class BlockModelValuesCommand */
1909 /* -------------------------------------------------------------------------- */
1910
1911 BlockModelValuesCommand::BlockModelValuesCommand(const std::vector<Expr>& terms)
1912     : d_terms(terms)
1913 {
1914   PrettyCheckArgument(terms.size() >= 1,
1915                       terms,
1916                       "cannot block-model-values of an empty set of terms");
1917 }
1918
1919 const std::vector<Expr>& BlockModelValuesCommand::getTerms() const
1920 {
1921   return d_terms;
1922 }
1923 void BlockModelValuesCommand::invoke(SmtEngine* smtEngine)
1924 {
1925   try
1926   {
1927     smtEngine->blockModelValues(d_terms);
1928     d_commandStatus = CommandSuccess::instance();
1929   }
1930   catch (RecoverableModalException& e)
1931   {
1932     d_commandStatus = new CommandRecoverableFailure(e.what());
1933   }
1934   catch (UnsafeInterruptException& e)
1935   {
1936     d_commandStatus = new CommandInterrupted();
1937   }
1938   catch (exception& e)
1939   {
1940     d_commandStatus = new CommandFailure(e.what());
1941   }
1942 }
1943
1944 Command* BlockModelValuesCommand::exportTo(
1945     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1946 {
1947   vector<Expr> exportedTerms;
1948   for (std::vector<Expr>::const_iterator i = d_terms.begin();
1949        i != d_terms.end();
1950        ++i)
1951   {
1952     exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
1953   }
1954   BlockModelValuesCommand* c = new BlockModelValuesCommand(exportedTerms);
1955   return c;
1956 }
1957
1958 Command* BlockModelValuesCommand::clone() const
1959 {
1960   BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms);
1961   return c;
1962 }
1963
1964 std::string BlockModelValuesCommand::getCommandName() const
1965 {
1966   return "block-model-values";
1967 }
1968
1969 /* -------------------------------------------------------------------------- */
1970 /* class GetProofCommand                                                      */
1971 /* -------------------------------------------------------------------------- */
1972
1973 GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {}
1974 void GetProofCommand::invoke(SmtEngine* smtEngine)
1975 {
1976   try
1977   {
1978     d_smtEngine = smtEngine;
1979     d_result = &smtEngine->getProof();
1980     d_commandStatus = CommandSuccess::instance();
1981   }
1982   catch (RecoverableModalException& e)
1983   {
1984     d_commandStatus = new CommandRecoverableFailure(e.what());
1985   }
1986   catch (UnsafeInterruptException& e)
1987   {
1988     d_commandStatus = new CommandInterrupted();
1989   }
1990   catch (exception& e)
1991   {
1992     d_commandStatus = new CommandFailure(e.what());
1993   }
1994 }
1995
1996 const Proof& GetProofCommand::getResult() const { return *d_result; }
1997 void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
1998 {
1999   if (!ok())
2000   {
2001     this->Command::printResult(out, verbosity);
2002   }
2003   else
2004   {
2005     smt::SmtScope scope(d_smtEngine);
2006     d_result->toStream(out);
2007   }
2008 }
2009
2010 Command* GetProofCommand::exportTo(ExprManager* exprManager,
2011                                    ExprManagerMapCollection& variableMap)
2012 {
2013   GetProofCommand* c = new GetProofCommand();
2014   c->d_result = d_result;
2015   c->d_smtEngine = d_smtEngine;
2016   return c;
2017 }
2018
2019 Command* GetProofCommand::clone() const
2020 {
2021   GetProofCommand* c = new GetProofCommand();
2022   c->d_result = d_result;
2023   c->d_smtEngine = d_smtEngine;
2024   return c;
2025 }
2026
2027 std::string GetProofCommand::getCommandName() const { return "get-proof"; }
2028
2029 /* -------------------------------------------------------------------------- */
2030 /* class GetInstantiationsCommand                                             */
2031 /* -------------------------------------------------------------------------- */
2032
2033 GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
2034 void GetInstantiationsCommand::invoke(SmtEngine* smtEngine)
2035 {
2036   try
2037   {
2038     d_smtEngine = smtEngine;
2039     d_commandStatus = CommandSuccess::instance();
2040   }
2041   catch (exception& e)
2042   {
2043     d_commandStatus = new CommandFailure(e.what());
2044   }
2045 }
2046
2047 void GetInstantiationsCommand::printResult(std::ostream& out,
2048                                            uint32_t verbosity) const
2049 {
2050   if (!ok())
2051   {
2052     this->Command::printResult(out, verbosity);
2053   }
2054   else
2055   {
2056     d_smtEngine->printInstantiations(out);
2057   }
2058 }
2059
2060 Command* GetInstantiationsCommand::exportTo(
2061     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2062 {
2063   GetInstantiationsCommand* c = new GetInstantiationsCommand();
2064   // c->d_result = d_result;
2065   c->d_smtEngine = d_smtEngine;
2066   return c;
2067 }
2068
2069 Command* GetInstantiationsCommand::clone() const
2070 {
2071   GetInstantiationsCommand* c = new GetInstantiationsCommand();
2072   // c->d_result = d_result;
2073   c->d_smtEngine = d_smtEngine;
2074   return c;
2075 }
2076
2077 std::string GetInstantiationsCommand::getCommandName() const
2078 {
2079   return "get-instantiations";
2080 }
2081
2082 /* -------------------------------------------------------------------------- */
2083 /* class GetSynthSolutionCommand                                              */
2084 /* -------------------------------------------------------------------------- */
2085
2086 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
2087 void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine)
2088 {
2089   try
2090   {
2091     d_smtEngine = smtEngine;
2092     d_commandStatus = CommandSuccess::instance();
2093   }
2094   catch (exception& e)
2095   {
2096     d_commandStatus = new CommandFailure(e.what());
2097   }
2098 }
2099
2100 void GetSynthSolutionCommand::printResult(std::ostream& out,
2101                                           uint32_t verbosity) const
2102 {
2103   if (!ok())
2104   {
2105     this->Command::printResult(out, verbosity);
2106   }
2107   else
2108   {
2109     d_smtEngine->printSynthSolution(out);
2110   }
2111 }
2112
2113 Command* GetSynthSolutionCommand::exportTo(
2114     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2115 {
2116   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
2117   c->d_smtEngine = d_smtEngine;
2118   return c;
2119 }
2120
2121 Command* GetSynthSolutionCommand::clone() const
2122 {
2123   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
2124   c->d_smtEngine = d_smtEngine;
2125   return c;
2126 }
2127
2128 std::string GetSynthSolutionCommand::getCommandName() const
2129 {
2130   return "get-instantiations";
2131 }
2132
2133 GetAbductCommand::GetAbductCommand() {}
2134 GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
2135     : d_name(name), d_conj(conj), d_resultStatus(false)
2136 {
2137 }
2138 GetAbductCommand::GetAbductCommand(const std::string& name,
2139                                    Expr conj,
2140                                    const Type& gtype)
2141     : d_name(name),
2142       d_conj(conj),
2143       d_sygus_grammar_type(gtype),
2144       d_resultStatus(false)
2145 {
2146 }
2147
2148 Expr GetAbductCommand::getConjecture() const { return d_conj; }
2149 Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; }
2150 Expr GetAbductCommand::getResult() const { return d_result; }
2151
2152 void GetAbductCommand::invoke(SmtEngine* smtEngine)
2153 {
2154   try
2155   {
2156     if (d_sygus_grammar_type.isNull())
2157     {
2158       d_resultStatus = smtEngine->getAbduct(d_conj, d_result);
2159     }
2160     else
2161     {
2162       d_resultStatus =
2163           smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result);
2164     }
2165     d_commandStatus = CommandSuccess::instance();
2166   }
2167   catch (exception& e)
2168   {
2169     d_commandStatus = new CommandFailure(e.what());
2170   }
2171 }
2172
2173 void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
2174 {
2175   if (!ok())
2176   {
2177     this->Command::printResult(out, verbosity);
2178   }
2179   else
2180   {
2181     expr::ExprDag::Scope scope(out, false);
2182     if (d_resultStatus)
2183     {
2184       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
2185           << std::endl;
2186     }
2187     else
2188     {
2189       out << "none" << std::endl;
2190     }
2191   }
2192 }
2193
2194 Command* GetAbductCommand::exportTo(ExprManager* exprManager,
2195                                     ExprManagerMapCollection& variableMap)
2196 {
2197   GetAbductCommand* c =
2198       new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap));
2199   c->d_sygus_grammar_type =
2200       d_sygus_grammar_type.exportTo(exprManager, variableMap);
2201   c->d_result = d_result.exportTo(exprManager, variableMap);
2202   c->d_resultStatus = d_resultStatus;
2203   return c;
2204 }
2205
2206 Command* GetAbductCommand::clone() const
2207 {
2208   GetAbductCommand* c = new GetAbductCommand(d_name, d_conj);
2209   c->d_sygus_grammar_type = d_sygus_grammar_type;
2210   c->d_result = d_result;
2211   c->d_resultStatus = d_resultStatus;
2212   return c;
2213 }
2214
2215 std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
2216
2217 /* -------------------------------------------------------------------------- */
2218 /* class GetQuantifierEliminationCommand                                      */
2219 /* -------------------------------------------------------------------------- */
2220
2221 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
2222     : d_expr(), d_doFull(true)
2223 {
2224 }
2225 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
2226     const Expr& expr, bool doFull)
2227     : d_expr(expr), d_doFull(doFull)
2228 {
2229 }
2230
2231 Expr GetQuantifierEliminationCommand::getExpr() const { return d_expr; }
2232 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
2233 void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine)
2234 {
2235   try
2236   {
2237     d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
2238     d_commandStatus = CommandSuccess::instance();
2239   }
2240   catch (exception& e)
2241   {
2242     d_commandStatus = new CommandFailure(e.what());
2243   }
2244 }
2245
2246 Expr GetQuantifierEliminationCommand::getResult() const { return d_result; }
2247 void GetQuantifierEliminationCommand::printResult(std::ostream& out,
2248                                                   uint32_t verbosity) const
2249 {
2250   if (!ok())
2251   {
2252     this->Command::printResult(out, verbosity);
2253   }
2254   else
2255   {
2256     out << d_result << endl;
2257   }
2258 }
2259
2260 Command* GetQuantifierEliminationCommand::exportTo(
2261     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2262 {
2263   GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(
2264       d_expr.exportTo(exprManager, variableMap), d_doFull);
2265   c->d_result = d_result;
2266   return c;
2267 }
2268
2269 Command* GetQuantifierEliminationCommand::clone() const
2270 {
2271   GetQuantifierEliminationCommand* c =
2272       new GetQuantifierEliminationCommand(d_expr, d_doFull);
2273   c->d_result = d_result;
2274   return c;
2275 }
2276
2277 std::string GetQuantifierEliminationCommand::getCommandName() const
2278 {
2279   return d_doFull ? "get-qe" : "get-qe-disjunct";
2280 }
2281
2282 /* -------------------------------------------------------------------------- */
2283 /* class GetUnsatAssumptionsCommand                                           */
2284 /* -------------------------------------------------------------------------- */
2285
2286 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
2287
2288 void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine)
2289 {
2290   try
2291   {
2292     d_result = smtEngine->getUnsatAssumptions();
2293     d_commandStatus = CommandSuccess::instance();
2294   }
2295   catch (RecoverableModalException& e)
2296   {
2297     d_commandStatus = new CommandRecoverableFailure(e.what());
2298   }
2299   catch (exception& e)
2300   {
2301     d_commandStatus = new CommandFailure(e.what());
2302   }
2303 }
2304
2305 std::vector<Expr> GetUnsatAssumptionsCommand::getResult() const
2306 {
2307   return d_result;
2308 }
2309
2310 void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
2311                                              uint32_t verbosity) const
2312 {
2313   if (!ok())
2314   {
2315     this->Command::printResult(out, verbosity);
2316   }
2317   else
2318   {
2319     container_to_stream(out, d_result, "(", ")\n", " ");
2320   }
2321 }
2322
2323 Command* GetUnsatAssumptionsCommand::exportTo(
2324     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2325 {
2326   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
2327   c->d_result = d_result;
2328   return c;
2329 }
2330
2331 Command* GetUnsatAssumptionsCommand::clone() const
2332 {
2333   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
2334   c->d_result = d_result;
2335   return c;
2336 }
2337
2338 std::string GetUnsatAssumptionsCommand::getCommandName() const
2339 {
2340   return "get-unsat-assumptions";
2341 }
2342
2343 /* -------------------------------------------------------------------------- */
2344 /* class GetUnsatCoreCommand                                                  */
2345 /* -------------------------------------------------------------------------- */
2346
2347 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
2348 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine)
2349 {
2350   try
2351   {
2352     d_result = smtEngine->getUnsatCore();
2353     d_commandStatus = CommandSuccess::instance();
2354   }
2355   catch (RecoverableModalException& e)
2356   {
2357     d_commandStatus = new CommandRecoverableFailure(e.what());
2358   }
2359   catch (exception& e)
2360   {
2361     d_commandStatus = new CommandFailure(e.what());
2362   }
2363 }
2364
2365 void GetUnsatCoreCommand::printResult(std::ostream& out,
2366                                       uint32_t verbosity) const
2367 {
2368   if (!ok())
2369   {
2370     this->Command::printResult(out, verbosity);
2371   }
2372   else
2373   {
2374     d_result.toStream(out);
2375   }
2376 }
2377
2378 const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const
2379 {
2380   // of course, this will be empty if the command hasn't been invoked yet
2381   return d_result;
2382 }
2383
2384 Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager,
2385                                        ExprManagerMapCollection& variableMap)
2386 {
2387   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
2388   c->d_result = d_result;
2389   return c;
2390 }
2391
2392 Command* GetUnsatCoreCommand::clone() const
2393 {
2394   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
2395   c->d_result = d_result;
2396   return c;
2397 }
2398
2399 std::string GetUnsatCoreCommand::getCommandName() const
2400 {
2401   return "get-unsat-core";
2402 }
2403
2404 /* -------------------------------------------------------------------------- */
2405 /* class GetAssertionsCommand                                                 */
2406 /* -------------------------------------------------------------------------- */
2407
2408 GetAssertionsCommand::GetAssertionsCommand() {}
2409 void GetAssertionsCommand::invoke(SmtEngine* smtEngine)
2410 {
2411   try
2412   {
2413     stringstream ss;
2414     const vector<Expr> v = smtEngine->getAssertions();
2415     ss << "(\n";
2416     copy(v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n"));
2417     ss << ")\n";
2418     d_result = ss.str();
2419     d_commandStatus = CommandSuccess::instance();
2420   }
2421   catch (exception& e)
2422   {
2423     d_commandStatus = new CommandFailure(e.what());
2424   }
2425 }
2426
2427 std::string GetAssertionsCommand::getResult() const { return d_result; }
2428 void GetAssertionsCommand::printResult(std::ostream& out,
2429                                        uint32_t verbosity) const
2430 {
2431   if (!ok())
2432   {
2433     this->Command::printResult(out, verbosity);
2434   }
2435   else
2436   {
2437     out << d_result;
2438   }
2439 }
2440
2441 Command* GetAssertionsCommand::exportTo(ExprManager* exprManager,
2442                                         ExprManagerMapCollection& variableMap)
2443 {
2444   GetAssertionsCommand* c = new GetAssertionsCommand();
2445   c->d_result = d_result;
2446   return c;
2447 }
2448
2449 Command* GetAssertionsCommand::clone() const
2450 {
2451   GetAssertionsCommand* c = new GetAssertionsCommand();
2452   c->d_result = d_result;
2453   return c;
2454 }
2455
2456 std::string GetAssertionsCommand::getCommandName() const
2457 {
2458   return "get-assertions";
2459 }
2460
2461 /* -------------------------------------------------------------------------- */
2462 /* class SetBenchmarkStatusCommand                                            */
2463 /* -------------------------------------------------------------------------- */
2464
2465 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
2466     : d_status(status)
2467 {
2468 }
2469
2470 BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
2471 {
2472   return d_status;
2473 }
2474
2475 void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine)
2476 {
2477   try
2478   {
2479     stringstream ss;
2480     ss << d_status;
2481     SExpr status = SExpr(ss.str());
2482     smtEngine->setInfo("status", status);
2483     d_commandStatus = CommandSuccess::instance();
2484   }
2485   catch (exception& e)
2486   {
2487     d_commandStatus = new CommandFailure(e.what());
2488   }
2489 }
2490
2491 Command* SetBenchmarkStatusCommand::exportTo(
2492     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2493 {
2494   return new SetBenchmarkStatusCommand(d_status);
2495 }
2496
2497 Command* SetBenchmarkStatusCommand::clone() const
2498 {
2499   return new SetBenchmarkStatusCommand(d_status);
2500 }
2501
2502 std::string SetBenchmarkStatusCommand::getCommandName() const
2503 {
2504   return "set-info";
2505 }
2506
2507 /* -------------------------------------------------------------------------- */
2508 /* class SetBenchmarkLogicCommand                                             */
2509 /* -------------------------------------------------------------------------- */
2510
2511 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
2512     : d_logic(logic)
2513 {
2514 }
2515
2516 std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
2517 void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine)
2518 {
2519   try
2520   {
2521     smtEngine->setLogic(d_logic);
2522     d_commandStatus = CommandSuccess::instance();
2523   }
2524   catch (exception& e)
2525   {
2526     d_commandStatus = new CommandFailure(e.what());
2527   }
2528 }
2529
2530 Command* SetBenchmarkLogicCommand::exportTo(
2531     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2532 {
2533   return new SetBenchmarkLogicCommand(d_logic);
2534 }
2535
2536 Command* SetBenchmarkLogicCommand::clone() const
2537 {
2538   return new SetBenchmarkLogicCommand(d_logic);
2539 }
2540
2541 std::string SetBenchmarkLogicCommand::getCommandName() const
2542 {
2543   return "set-logic";
2544 }
2545
2546 /* -------------------------------------------------------------------------- */
2547 /* class SetInfoCommand                                                       */
2548 /* -------------------------------------------------------------------------- */
2549
2550 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
2551     : d_flag(flag), d_sexpr(sexpr)
2552 {
2553 }
2554
2555 std::string SetInfoCommand::getFlag() const { return d_flag; }
2556 SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
2557 void SetInfoCommand::invoke(SmtEngine* smtEngine)
2558 {
2559   try
2560   {
2561     smtEngine->setInfo(d_flag, d_sexpr);
2562     d_commandStatus = CommandSuccess::instance();
2563   }
2564   catch (UnrecognizedOptionException&)
2565   {
2566     // As per SMT-LIB spec, silently accept unknown set-info keys
2567     d_commandStatus = CommandSuccess::instance();
2568   }
2569   catch (exception& e)
2570   {
2571     d_commandStatus = new CommandFailure(e.what());
2572   }
2573 }
2574
2575 Command* SetInfoCommand::exportTo(ExprManager* exprManager,
2576                                   ExprManagerMapCollection& variableMap)
2577 {
2578   return new SetInfoCommand(d_flag, d_sexpr);
2579 }
2580
2581 Command* SetInfoCommand::clone() const
2582 {
2583   return new SetInfoCommand(d_flag, d_sexpr);
2584 }
2585
2586 std::string SetInfoCommand::getCommandName() const { return "set-info"; }
2587
2588 /* -------------------------------------------------------------------------- */
2589 /* class GetInfoCommand                                                       */
2590 /* -------------------------------------------------------------------------- */
2591
2592 GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
2593 std::string GetInfoCommand::getFlag() const { return d_flag; }
2594 void GetInfoCommand::invoke(SmtEngine* smtEngine)
2595 {
2596   try
2597   {
2598     vector<SExpr> v;
2599     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
2600     v.push_back(smtEngine->getInfo(d_flag));
2601     stringstream ss;
2602     if (d_flag == "all-options" || d_flag == "all-statistics")
2603     {
2604       ss << PrettySExprs(true);
2605     }
2606     ss << SExpr(v);
2607     d_result = ss.str();
2608     d_commandStatus = CommandSuccess::instance();
2609   }
2610   catch (UnrecognizedOptionException&)
2611   {
2612     d_commandStatus = new CommandUnsupported();
2613   }
2614   catch (RecoverableModalException& e)
2615   {
2616     d_commandStatus = new CommandRecoverableFailure(e.what());
2617   }
2618   catch (exception& e)
2619   {
2620     d_commandStatus = new CommandFailure(e.what());
2621   }
2622 }
2623
2624 std::string GetInfoCommand::getResult() const { return d_result; }
2625 void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
2626 {
2627   if (!ok())
2628   {
2629     this->Command::printResult(out, verbosity);
2630   }
2631   else if (d_result != "")
2632   {
2633     out << d_result << endl;
2634   }
2635 }
2636
2637 Command* GetInfoCommand::exportTo(ExprManager* exprManager,
2638                                   ExprManagerMapCollection& variableMap)
2639 {
2640   GetInfoCommand* c = new GetInfoCommand(d_flag);
2641   c->d_result = d_result;
2642   return c;
2643 }
2644
2645 Command* GetInfoCommand::clone() const
2646 {
2647   GetInfoCommand* c = new GetInfoCommand(d_flag);
2648   c->d_result = d_result;
2649   return c;
2650 }
2651
2652 std::string GetInfoCommand::getCommandName() const { return "get-info"; }
2653
2654 /* -------------------------------------------------------------------------- */
2655 /* class SetOptionCommand                                                     */
2656 /* -------------------------------------------------------------------------- */
2657
2658 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
2659     : d_flag(flag), d_sexpr(sexpr)
2660 {
2661 }
2662
2663 std::string SetOptionCommand::getFlag() const { return d_flag; }
2664 SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
2665 void SetOptionCommand::invoke(SmtEngine* smtEngine)
2666 {
2667   try
2668   {
2669     smtEngine->setOption(d_flag, d_sexpr);
2670     d_commandStatus = CommandSuccess::instance();
2671   }
2672   catch (UnrecognizedOptionException&)
2673   {
2674     d_commandStatus = new CommandUnsupported();
2675   }
2676   catch (exception& e)
2677   {
2678     d_commandStatus = new CommandFailure(e.what());
2679   }
2680 }
2681
2682 Command* SetOptionCommand::exportTo(ExprManager* exprManager,
2683                                     ExprManagerMapCollection& variableMap)
2684 {
2685   return new SetOptionCommand(d_flag, d_sexpr);
2686 }
2687
2688 Command* SetOptionCommand::clone() const
2689 {
2690   return new SetOptionCommand(d_flag, d_sexpr);
2691 }
2692
2693 std::string SetOptionCommand::getCommandName() const { return "set-option"; }
2694
2695 /* -------------------------------------------------------------------------- */
2696 /* class GetOptionCommand                                                     */
2697 /* -------------------------------------------------------------------------- */
2698
2699 GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
2700 std::string GetOptionCommand::getFlag() const { return d_flag; }
2701 void GetOptionCommand::invoke(SmtEngine* smtEngine)
2702 {
2703   try
2704   {
2705     SExpr res = smtEngine->getOption(d_flag);
2706     d_result = res.toString();
2707     d_commandStatus = CommandSuccess::instance();
2708   }
2709   catch (UnrecognizedOptionException&)
2710   {
2711     d_commandStatus = new CommandUnsupported();
2712   }
2713   catch (exception& e)
2714   {
2715     d_commandStatus = new CommandFailure(e.what());
2716   }
2717 }
2718
2719 std::string GetOptionCommand::getResult() const { return d_result; }
2720 void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
2721 {
2722   if (!ok())
2723   {
2724     this->Command::printResult(out, verbosity);
2725   }
2726   else if (d_result != "")
2727   {
2728     out << d_result << endl;
2729   }
2730 }
2731
2732 Command* GetOptionCommand::exportTo(ExprManager* exprManager,
2733                                     ExprManagerMapCollection& variableMap)
2734 {
2735   GetOptionCommand* c = new GetOptionCommand(d_flag);
2736   c->d_result = d_result;
2737   return c;
2738 }
2739
2740 Command* GetOptionCommand::clone() const
2741 {
2742   GetOptionCommand* c = new GetOptionCommand(d_flag);
2743   c->d_result = d_result;
2744   return c;
2745 }
2746
2747 std::string GetOptionCommand::getCommandName() const { return "get-option"; }
2748
2749 /* -------------------------------------------------------------------------- */
2750 /* class SetExpressionNameCommand                                             */
2751 /* -------------------------------------------------------------------------- */
2752
2753 SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name)
2754     : d_expr(expr), d_name(name)
2755 {
2756 }
2757
2758 void SetExpressionNameCommand::invoke(SmtEngine* smtEngine)
2759 {
2760   smtEngine->setExpressionName(d_expr, d_name);
2761   d_commandStatus = CommandSuccess::instance();
2762 }
2763
2764 Command* SetExpressionNameCommand::exportTo(
2765     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2766 {
2767   SetExpressionNameCommand* c = new SetExpressionNameCommand(
2768       d_expr.exportTo(exprManager, variableMap), d_name);
2769   return c;
2770 }
2771
2772 Command* SetExpressionNameCommand::clone() const
2773 {
2774   SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name);
2775   return c;
2776 }
2777
2778 std::string SetExpressionNameCommand::getCommandName() const
2779 {
2780   return "set-expr-name";
2781 }
2782
2783 /* -------------------------------------------------------------------------- */
2784 /* class DatatypeDeclarationCommand                                           */
2785 /* -------------------------------------------------------------------------- */
2786
2787 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const Type& datatype)
2788     : d_datatypes()
2789 {
2790   d_datatypes.push_back(datatype);
2791 }
2792
2793 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2794     const std::vector<Type>& datatypes)
2795     : d_datatypes(datatypes)
2796 {
2797 }
2798
2799 const std::vector<Type>& DatatypeDeclarationCommand::getDatatypes() const
2800 {
2801   return d_datatypes;
2802 }
2803
2804 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine)
2805 {
2806   d_commandStatus = CommandSuccess::instance();
2807 }
2808
2809 Command* DatatypeDeclarationCommand::exportTo(
2810     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2811 {
2812   throw ExportUnsupportedException(
2813       "export of DatatypeDeclarationCommand unsupported");
2814 }
2815
2816 Command* DatatypeDeclarationCommand::clone() const
2817 {
2818   return new DatatypeDeclarationCommand(d_datatypes);
2819 }
2820
2821 std::string DatatypeDeclarationCommand::getCommandName() const
2822 {
2823   return "declare-datatypes";
2824 }
2825
2826 }  // namespace CVC4