src/smt/command.cpp

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