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