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