GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/command.cpp Lines: 621 1228 50.6 %
Date: 2021-03-22 Branches: 452 1509 30.0 %

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