GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/command.h Lines: 59 78 75.6 %
Date: 2021-03-23 Branches: 4 16 25.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file command.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Abdalrhman Mohamed, Tim King, 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 the command pattern on SmtEngines.
13
 **
14
 ** Implementation of the command pattern on SmtEngines.  Command
15
 ** objects are generated by the parser (typically) to implement the
16
 ** commands in parsed input (see Parser::parseNextCommand()), or by
17
 ** client code.
18
 **/
19
20
#include "cvc4_public.h"
21
22
#ifndef CVC4__COMMAND_H
23
#define CVC4__COMMAND_H
24
25
#include <iosfwd>
26
#include <sstream>
27
#include <string>
28
#include <vector>
29
30
#include "api/cvc4cpp.h"
31
#include "cvc4_export.h"
32
#include "options/language.h"
33
34
namespace CVC4 {
35
36
namespace api {
37
class Solver;
38
class Term;
39
}  // namespace api
40
41
class SymbolManager;
42
class Command;
43
class CommandStatus;
44
45
namespace smt {
46
class Model;
47
}
48
49
/**
50
 * Convert a symbolic expression to string. This method differs from
51
 * Term::toString in that it does not depend on the output language.
52
 *
53
 * @param sexpr the symbolic expression to convert
54
 * @return the symbolic expression as string
55
 */
56
std::string sexprToString(api::Term sexpr) CVC4_EXPORT;
57
58
std::ostream& operator<<(std::ostream&, const Command&) CVC4_EXPORT;
59
std::ostream& operator<<(std::ostream&, const Command*) CVC4_EXPORT;
60
std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_EXPORT;
61
std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC4_EXPORT;
62
63
/** The status an SMT benchmark can have */
64
enum BenchmarkStatus
65
{
66
  /** Benchmark is satisfiable */
67
  SMT_SATISFIABLE,
68
  /** Benchmark is unsatisfiable */
69
  SMT_UNSATISFIABLE,
70
  /** The status of the benchmark is unknown */
71
  SMT_UNKNOWN
72
}; /* enum BenchmarkStatus */
73
74
std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC4_EXPORT;
75
76
/**
77
 * IOStream manipulator to print success messages or not.
78
 *
79
 *   out << Command::printsuccess(false) << CommandSuccess();
80
 *
81
 * prints nothing, but
82
 *
83
 *   out << Command::printsuccess(true) << CommandSuccess();
84
 *
85
 * prints a success message (in a manner appropriate for the current
86
 * output language).
87
 */
88
class CVC4_EXPORT CommandPrintSuccess
89
{
90
 public:
91
  /** Construct a CommandPrintSuccess with the given setting. */
92
150
  CommandPrintSuccess(bool printSuccess) : d_printSuccess(printSuccess) {}
93
  void applyPrintSuccess(std::ostream& out);
94
  static bool getPrintSuccess(std::ostream& out);
95
  static void setPrintSuccess(std::ostream& out, bool printSuccess);
96
97
 private:
98
  /** The allocated index in ios_base for our depth setting. */
99
  static const int s_iosIndex;
100
101
  /**
102
   * The default setting, for ostreams that haven't yet had a setdepth()
103
   * applied to them.
104
   */
105
  static const int s_defaultPrintSuccess = false;
106
107
  /** When this manipulator is used, the setting is stored here. */
108
  bool d_printSuccess;
109
110
}; /* class CommandPrintSuccess */
111
112
/**
113
 * Sets the default print-success setting when pretty-printing an Expr
114
 * to an ostream.  Use like this:
115
 *
116
 *   // let out be an ostream, e an Expr
117
 *   out << Expr::setdepth(n) << e << endl;
118
 *
119
 * The depth stays permanently (until set again) with the stream.
120
 */
121
std::ostream& operator<<(std::ostream& out,
122
                         CommandPrintSuccess cps) CVC4_EXPORT;
123
124
class CVC4_EXPORT CommandStatus
125
{
126
 protected:
127
  // shouldn't construct a CommandStatus (use a derived class)
128
17850
  CommandStatus() {}
129
130
 public:
131
56
  virtual ~CommandStatus() {}
132
  void toStream(std::ostream& out,
133
                OutputLanguage language = language::output::LANG_AUTO) const;
134
  virtual CommandStatus& clone() const = 0;
135
}; /* class CommandStatus */
136
137
8897
class CVC4_EXPORT CommandSuccess : public CommandStatus
138
{
139
  static const CommandSuccess* s_instance;
140
141
 public:
142
566112
  static const CommandSuccess* instance() { return s_instance; }
143
  CommandStatus& clone() const override
144
  {
145
    return const_cast<CommandSuccess&>(*this);
146
  }
147
}; /* class CommandSuccess */
148
149
8897
class CVC4_EXPORT CommandInterrupted : public CommandStatus
150
{
151
  static const CommandInterrupted* s_instance;
152
153
 public:
154
  static const CommandInterrupted* instance() { return s_instance; }
155
  CommandStatus& clone() const override
156
  {
157
    return const_cast<CommandInterrupted&>(*this);
158
  }
159
}; /* class CommandInterrupted */
160
161
class CVC4_EXPORT CommandUnsupported : public CommandStatus
162
{
163
 public:
164
  CommandStatus& clone() const override
165
  {
166
    return *new CommandUnsupported(*this);
167
  }
168
}; /* class CommandSuccess */
169
170
80
class CVC4_EXPORT CommandFailure : public CommandStatus
171
{
172
  std::string d_message;
173
174
 public:
175
40
  CommandFailure(std::string message) : d_message(message) {}
176
  CommandFailure& clone() const override { return *new CommandFailure(*this); }
177
40
  std::string getMessage() const { return d_message; }
178
}; /* class CommandFailure */
179
180
/**
181
 * The execution of the command resulted in a non-fatal error and further
182
 * commands can be processed. This status is for example used when a user asks
183
 * for an unsat core in a place that is not immediately preceded by an
184
 * unsat/valid response.
185
 */
186
32
class CVC4_EXPORT CommandRecoverableFailure : public CommandStatus
187
{
188
  std::string d_message;
189
190
 public:
191
16
  CommandRecoverableFailure(std::string message) : d_message(message) {}
192
  CommandRecoverableFailure& clone() const override
193
  {
194
    return *new CommandRecoverableFailure(*this);
195
  }
196
16
  std::string getMessage() const { return d_message; }
197
}; /* class CommandRecoverableFailure */
198
199
class CVC4_EXPORT Command
200
{
201
 public:
202
  typedef CommandPrintSuccess printsuccess;
203
204
  Command();
205
  Command(const Command& cmd);
206
207
  virtual ~Command();
208
209
  /**
210
   * Invoke the command on the solver and symbol manager sm.
211
   */
212
  virtual void invoke(api::Solver* solver, SymbolManager* sm) = 0;
213
  /**
214
   * Same as above, and prints the result to output stream out.
215
   */
216
  virtual void invoke(api::Solver* solver,
217
                      SymbolManager* sm,
218
                      std::ostream& out);
219
220
  virtual void toStream(
221
      std::ostream& out,
222
      int toDepth = -1,
223
224
      size_t dag = 1,
225
      OutputLanguage language = language::output::LANG_AUTO) const = 0;
226
227
  std::string toString() const;
228
229
  virtual std::string getCommandName() const = 0;
230
231
  /**
232
   * If false, instruct this Command not to print a success message.
233
   */
234
10225
  void setMuted(bool muted) { d_muted = muted; }
235
  /**
236
   * Determine whether this Command will print a success message.
237
   */
238
283171
  bool isMuted() { return d_muted; }
239
  /**
240
   * Either the command hasn't run yet, or it completed successfully
241
   * (CommandSuccess, not CommandUnsupported or CommandFailure).
242
   */
243
  bool ok() const;
244
245
  /**
246
   * The command completed in a failure state (CommandFailure, not
247
   * CommandSuccess or CommandUnsupported).
248
   */
249
  bool fail() const;
250
251
  /**
252
   * The command was ran but was interrupted due to resource limiting.
253
   */
254
  bool interrupted() const;
255
256
  /** Get the command status (it's NULL if we haven't run yet). */
257
  const CommandStatus* getCommandStatus() const { return d_commandStatus; }
258
  virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const;
259
260
  /**
261
   * Clone this Command (make a shallow copy).
262
   */
263
  virtual Command* clone() const = 0;
264
265
  /**
266
   * This field contains a command status if the command has been
267
   * invoked, or NULL if it has not.  This field is either a
268
   * dynamically-allocated pointer, or it's a pointer to the singleton
269
   * CommandSuccess instance.  Doing so is somewhat asymmetric, but
270
   * it avoids the need to dynamically allocate memory in the common
271
   * case of a successful command.
272
   */
273
  const CommandStatus* d_commandStatus;
274
275
  /**
276
   * True if this command is "muted"---i.e., don't print "success" on
277
   * successful execution.
278
   */
279
  bool d_muted;
280
}; /* class Command */
281
282
/**
283
 * EmptyCommands are the residue of a command after the parser handles
284
 * them (and there's nothing left to do).
285
 */
286
834
class CVC4_EXPORT EmptyCommand : public Command
287
{
288
 public:
289
  EmptyCommand(std::string name = "");
290
  std::string getName() const;
291
  void invoke(api::Solver* solver, SymbolManager* sm) override;
292
  Command* clone() const override;
293
  std::string getCommandName() const override;
294
  void toStream(
295
      std::ostream& out,
296
      int toDepth = -1,
297
      size_t dag = 1,
298
      OutputLanguage language = language::output::LANG_AUTO) const override;
299
300
 protected:
301
  std::string d_name;
302
}; /* class EmptyCommand */
303
304
class CVC4_EXPORT EchoCommand : public Command
305
{
306
 public:
307
  EchoCommand(std::string output = "");
308
309
  std::string getOutput() const;
310
311
  void invoke(api::Solver* solver, SymbolManager* sm) override;
312
  void invoke(api::Solver* solver,
313
              SymbolManager* sm,
314
              std::ostream& out) override;
315
316
  Command* clone() const override;
317
  std::string getCommandName() const override;
318
  void toStream(
319
      std::ostream& out,
320
      int toDepth = -1,
321
      size_t dag = 1,
322
      OutputLanguage language = language::output::LANG_AUTO) const override;
323
324
 protected:
325
  std::string d_output;
326
}; /* class EchoCommand */
327
328
148880
class CVC4_EXPORT AssertCommand : public Command
329
{
330
 protected:
331
  api::Term d_term;
332
  bool d_inUnsatCore;
333
334
 public:
335
  AssertCommand(const api::Term& t, bool inUnsatCore = true);
336
337
  api::Term getTerm() const;
338
339
  void invoke(api::Solver* solver, SymbolManager* sm) override;
340
341
  Command* clone() const override;
342
  std::string getCommandName() const override;
343
  void toStream(
344
      std::ostream& out,
345
      int toDepth = -1,
346
      size_t dag = 1,
347
      OutputLanguage language = language::output::LANG_AUTO) const override;
348
}; /* class AssertCommand */
349
350
7530
class CVC4_EXPORT PushCommand : public Command
351
{
352
 public:
353
  void invoke(api::Solver* solver, SymbolManager* sm) override;
354
  Command* clone() const override;
355
  std::string getCommandName() const override;
356
  void toStream(
357
      std::ostream& out,
358
      int toDepth = -1,
359
      size_t dag = 1,
360
      OutputLanguage language = language::output::LANG_AUTO) const override;
361
}; /* class PushCommand */
362
363
6294
class CVC4_EXPORT PopCommand : public Command
364
{
365
 public:
366
  void invoke(api::Solver* solver, SymbolManager* sm) override;
367
  Command* clone() const override;
368
  std::string getCommandName() const override;
369
  void toStream(
370
      std::ostream& out,
371
      int toDepth = -1,
372
      size_t dag = 1,
373
      OutputLanguage language = language::output::LANG_AUTO) const override;
374
}; /* class PopCommand */
375
376
174321
class CVC4_EXPORT DeclarationDefinitionCommand : public Command
377
{
378
 protected:
379
  std::string d_symbol;
380
381
 public:
382
  DeclarationDefinitionCommand(const std::string& id);
383
384
  void invoke(api::Solver* solver, SymbolManager* sm) override = 0;
385
  std::string getSymbol() const;
386
}; /* class DeclarationDefinitionCommand */
387
388
333466
class CVC4_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand
389
{
390
 protected:
391
  api::Term d_func;
392
  api::Sort d_sort;
393
394
 public:
395
  DeclareFunctionCommand(const std::string& id, api::Term func, api::Sort sort);
396
  api::Term getFunction() const;
397
  api::Sort getSort() const;
398
399
  void invoke(api::Solver* solver, SymbolManager* sm) override;
400
  Command* clone() const override;
401
  std::string getCommandName() const override;
402
  void toStream(
403
      std::ostream& out,
404
      int toDepth = -1,
405
      size_t dag = 1,
406
      OutputLanguage language = language::output::LANG_AUTO) const override;
407
}; /* class DeclareFunctionCommand */
408
409
7898
class CVC4_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
410
{
411
 protected:
412
  size_t d_arity;
413
  api::Sort d_sort;
414
415
 public:
416
  DeclareSortCommand(const std::string& id, size_t arity, api::Sort sort);
417
418
  size_t getArity() const;
419
  api::Sort getSort() const;
420
421
  void invoke(api::Solver* solver, SymbolManager* sm) override;
422
  Command* clone() const override;
423
  std::string getCommandName() const override;
424
  void toStream(
425
      std::ostream& out,
426
      int toDepth = -1,
427
      size_t dag = 1,
428
      OutputLanguage language = language::output::LANG_AUTO) const override;
429
}; /* class DeclareSortCommand */
430
431
422
class CVC4_EXPORT DefineSortCommand : public DeclarationDefinitionCommand
432
{
433
 protected:
434
  std::vector<api::Sort> d_params;
435
  api::Sort d_sort;
436
437
 public:
438
  DefineSortCommand(const std::string& id, api::Sort sort);
439
  DefineSortCommand(const std::string& id,
440
                    const std::vector<api::Sort>& params,
441
                    api::Sort sort);
442
443
  const std::vector<api::Sort>& getParameters() const;
444
  api::Sort getSort() const;
445
446
  void invoke(api::Solver* solver, SymbolManager* sm) override;
447
  Command* clone() const override;
448
  std::string getCommandName() const override;
449
  void toStream(
450
      std::ostream& out,
451
      int toDepth = -1,
452
      size_t dag = 1,
453
      OutputLanguage language = language::output::LANG_AUTO) const override;
454
}; /* class DefineSortCommand */
455
456
4634
class CVC4_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
457
{
458
 public:
459
  DefineFunctionCommand(const std::string& id,
460
                        api::Term func,
461
                        api::Term formula,
462
                        bool global);
463
  DefineFunctionCommand(const std::string& id,
464
                        api::Term func,
465
                        const std::vector<api::Term>& formals,
466
                        api::Term formula,
467
                        bool global);
468
469
  api::Term getFunction() const;
470
  const std::vector<api::Term>& getFormals() const;
471
  api::Term getFormula() const;
472
473
  void invoke(api::Solver* solver, SymbolManager* sm) override;
474
  Command* clone() const override;
475
  std::string getCommandName() const override;
476
  void toStream(
477
      std::ostream& out,
478
      int toDepth = -1,
479
      size_t dag = 1,
480
      OutputLanguage language = language::output::LANG_AUTO) const override;
481
482
 protected:
483
  /** The function we are defining */
484
  api::Term d_func;
485
  /** The formal arguments for the function we are defining */
486
  std::vector<api::Term> d_formals;
487
  /** The formula corresponding to the body of the function we are defining */
488
  api::Term d_formula;
489
  /**
490
   * Stores whether this definition is global (i.e. should persist when
491
   * popping the user context.
492
   */
493
  bool d_global;
494
}; /* class DefineFunctionCommand */
495
496
/**
497
 * The command when parsing define-fun-rec or define-funs-rec.
498
 * This command will assert a set of quantified formulas that specify
499
 * the (mutually recursive) function definitions provided to it.
500
 */
501
234
class CVC4_EXPORT DefineFunctionRecCommand : public Command
502
{
503
 public:
504
  DefineFunctionRecCommand(api::Term func,
505
                           const std::vector<api::Term>& formals,
506
                           api::Term formula,
507
                           bool global);
508
  DefineFunctionRecCommand(const std::vector<api::Term>& funcs,
509
                           const std::vector<std::vector<api::Term> >& formals,
510
                           const std::vector<api::Term>& formula,
511
                           bool global);
512
513
  const std::vector<api::Term>& getFunctions() const;
514
  const std::vector<std::vector<api::Term> >& getFormals() const;
515
  const std::vector<api::Term>& getFormulas() const;
516
517
  void invoke(api::Solver* solver, SymbolManager* sm) override;
518
  Command* clone() const override;
519
  std::string getCommandName() const override;
520
  void toStream(
521
      std::ostream& out,
522
      int toDepth = -1,
523
      size_t dag = 1,
524
      OutputLanguage language = language::output::LANG_AUTO) const override;
525
526
 protected:
527
  /** functions we are defining */
528
  std::vector<api::Term> d_funcs;
529
  /** formal arguments for each of the functions we are defining */
530
  std::vector<std::vector<api::Term> > d_formals;
531
  /** formulas corresponding to the bodies of the functions we are defining */
532
  std::vector<api::Term> d_formulas;
533
  /**
534
   * Stores whether this definition is global (i.e. should persist when
535
   * popping the user context.
536
   */
537
  bool d_global;
538
}; /* class DefineFunctionRecCommand */
539
540
/**
541
 * In separation logic inputs, which is an extension of smt2 inputs, this
542
 * corresponds to the command:
543
 *   (declare-heap (T U))
544
 * where T is the location sort and U is the data sort.
545
 */
546
174
class CVC4_EXPORT DeclareHeapCommand : public Command
547
{
548
 public:
549
  DeclareHeapCommand(api::Sort locSort, api::Sort dataSort);
550
  api::Sort getLocationSort() const;
551
  api::Sort getDataSort() const;
552
  void invoke(api::Solver* solver, SymbolManager* sm) override;
553
  Command* clone() const override;
554
  std::string getCommandName() const override;
555
  void toStream(
556
      std::ostream& out,
557
      int toDepth = -1,
558
      size_t dag = 1,
559
      OutputLanguage language = language::output::LANG_AUTO) const override;
560
561
 protected:
562
  /** The location sort */
563
  api::Sort d_locSort;
564
  /** The data sort */
565
  api::Sort d_dataSort;
566
};
567
568
/**
569
 * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
570
 *  via the syntax (! expr :attr)
571
 */
572
158
class CVC4_EXPORT SetUserAttributeCommand : public Command
573
{
574
 public:
575
  SetUserAttributeCommand(const std::string& attr, api::Term term);
576
  SetUserAttributeCommand(const std::string& attr,
577
                          api::Term term,
578
                          const std::vector<api::Term>& values);
579
  SetUserAttributeCommand(const std::string& attr,
580
                          api::Term term,
581
                          const std::string& value);
582
583
  void invoke(api::Solver* solver, SymbolManager* sm) override;
584
  Command* clone() const override;
585
  std::string getCommandName() const override;
586
  void toStream(
587
      std::ostream& out,
588
      int toDepth = -1,
589
      size_t dag = 1,
590
      OutputLanguage language = language::output::LANG_AUTO) const override;
591
592
 private:
593
  SetUserAttributeCommand(const std::string& attr,
594
                          api::Term term,
595
                          const std::vector<api::Term>& termValues,
596
                          const std::string& strValue);
597
598
  const std::string d_attr;
599
  const api::Term d_term;
600
  const std::vector<api::Term> d_termValues;
601
  const std::string d_strValue;
602
}; /* class SetUserAttributeCommand */
603
604
/**
605
 * The command when parsing check-sat.
606
 * This command will check satisfiability of the input formula.
607
 */
608
14928
class CVC4_EXPORT CheckSatCommand : public Command
609
{
610
 public:
611
  CheckSatCommand();
612
  CheckSatCommand(const api::Term& term);
613
614
  api::Term getTerm() const;
615
  api::Result getResult() const;
616
  void invoke(api::Solver* solver, SymbolManager* sm) override;
617
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
618
  Command* clone() const override;
619
  std::string getCommandName() const override;
620
  void toStream(
621
      std::ostream& out,
622
      int toDepth = -1,
623
      size_t dag = 1,
624
      OutputLanguage language = language::output::LANG_AUTO) const override;
625
626
 private:
627
  api::Term d_term;
628
  api::Result d_result;
629
}; /* class CheckSatCommand */
630
631
/**
632
 * The command when parsing check-sat-assuming.
633
 * This command will assume a set of formulas and check satisfiability of the
634
 * input formula under these assumptions.
635
 */
636
1960
class CVC4_EXPORT CheckSatAssumingCommand : public Command
637
{
638
 public:
639
  CheckSatAssumingCommand(api::Term term);
640
  CheckSatAssumingCommand(const std::vector<api::Term>& terms);
641
642
  const std::vector<api::Term>& getTerms() const;
643
  api::Result getResult() const;
644
  void invoke(api::Solver* solver, SymbolManager* sm) override;
645
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
646
  Command* clone() const override;
647
  std::string getCommandName() const override;
648
  void toStream(
649
      std::ostream& out,
650
      int toDepth = -1,
651
      size_t dag = 1,
652
      OutputLanguage language = language::output::LANG_AUTO) const override;
653
654
 private:
655
  std::vector<api::Term> d_terms;
656
  api::Result d_result;
657
}; /* class CheckSatAssumingCommand */
658
659
458
class CVC4_EXPORT QueryCommand : public Command
660
{
661
 protected:
662
  api::Term d_term;
663
  api::Result d_result;
664
  bool d_inUnsatCore;
665
666
 public:
667
  QueryCommand(const api::Term& t, bool inUnsatCore = true);
668
669
  api::Term getTerm() const;
670
  api::Result getResult() const;
671
  void invoke(api::Solver* solver, SymbolManager* sm) override;
672
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
673
  Command* clone() const override;
674
  std::string getCommandName() const override;
675
  void toStream(
676
      std::ostream& out,
677
      int toDepth = -1,
678
      size_t dag = 1,
679
      OutputLanguage language = language::output::LANG_AUTO) const override;
680
}; /* class QueryCommand */
681
682
/* ------------------- sygus commands  ------------------ */
683
684
/** Declares a sygus universal variable */
685
1144
class CVC4_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand
686
{
687
 public:
688
  DeclareSygusVarCommand(const std::string& id, api::Term var, api::Sort sort);
689
  /** returns the declared variable */
690
  api::Term getVar() const;
691
  /** returns the declared variable's sort */
692
  api::Sort getSort() const;
693
  /** invokes this command
694
   *
695
   * The declared sygus variable is communicated to the SMT engine in case a
696
   * synthesis conjecture is built later on.
697
   */
698
  void invoke(api::Solver* solver, SymbolManager* sm) override;
699
  /** creates a copy of this command */
700
  Command* clone() const override;
701
  /** returns this command's name */
702
  std::string getCommandName() const override;
703
  /** prints this command */
704
  void toStream(
705
      std::ostream& out,
706
      int toDepth = -1,
707
      size_t dag = 1,
708
      OutputLanguage language = language::output::LANG_AUTO) const override;
709
710
 protected:
711
  /** the declared variable */
712
  api::Term d_var;
713
  /** the declared variable's sort */
714
  api::Sort d_sort;
715
};
716
717
/** Declares a sygus function-to-synthesize
718
 *
719
 * This command is also used for the special case in which we are declaring an
720
 * invariant-to-synthesize
721
 */
722
1078
class CVC4_EXPORT SynthFunCommand : public DeclarationDefinitionCommand
723
{
724
 public:
725
  SynthFunCommand(const std::string& id,
726
                  api::Term fun,
727
                  const std::vector<api::Term>& vars,
728
                  api::Sort sort,
729
                  bool isInv,
730
                  api::Grammar* g);
731
  /** returns the function-to-synthesize */
732
  api::Term getFunction() const;
733
  /** returns the input variables of the function-to-synthesize */
734
  const std::vector<api::Term>& getVars() const;
735
  /** returns the sygus sort of the function-to-synthesize */
736
  api::Sort getSort() const;
737
  /** returns whether the function-to-synthesize should be an invariant */
738
  bool isInv() const;
739
  /** Get the sygus grammar given for the synth fun command */
740
  const api::Grammar* getGrammar() const;
741
742
  /** invokes this command
743
   *
744
   * The declared function-to-synthesize is communicated to the SMT engine in
745
   * case a synthesis conjecture is built later on.
746
   */
747
  void invoke(api::Solver* solver, SymbolManager* sm) override;
748
  /** creates a copy of this command */
749
  Command* clone() const override;
750
  /** returns this command's name */
751
  std::string getCommandName() const override;
752
  /** prints this command */
753
  void toStream(
754
      std::ostream& out,
755
      int toDepth = -1,
756
      size_t dag = 1,
757
      OutputLanguage language = language::output::LANG_AUTO) const override;
758
759
 protected:
760
  /** the function-to-synthesize */
761
  api::Term d_fun;
762
  /** the input variables of the function-to-synthesize */
763
  std::vector<api::Term> d_vars;
764
  /** sort of the function-to-synthesize */
765
  api::Sort d_sort;
766
  /** whether the function-to-synthesize should be an invariant */
767
  bool d_isInv;
768
  /** optional grammar for the possible values of the function-to-sytnhesize */
769
  api::Grammar* d_grammar;
770
};
771
772
/** Declares a sygus constraint */
773
2378
class CVC4_EXPORT SygusConstraintCommand : public Command
774
{
775
 public:
776
  SygusConstraintCommand(const api::Term& t);
777
  /** returns the declared constraint */
778
  api::Term getTerm() const;
779
  /** invokes this command
780
   *
781
   * The declared constraint is communicated to the SMT engine in case a
782
   * synthesis conjecture is built later on.
783
   */
784
  void invoke(api::Solver* solver, SymbolManager* sm) override;
785
  /** creates a copy of this command */
786
  Command* clone() const override;
787
  /** returns this command's name */
788
  std::string getCommandName() const override;
789
  /** prints this command */
790
  void toStream(
791
      std::ostream& out,
792
      int toDepth = -1,
793
      size_t dag = 1,
794
      OutputLanguage language = language::output::LANG_AUTO) const override;
795
796
 protected:
797
  /** the declared constraint */
798
  api::Term d_term;
799
};
800
801
/** Declares a sygus invariant constraint
802
 *
803
 * Invarint constraints are declared in a somewhat implicit manner in the SyGuS
804
 * language: they are declared in terms of the previously declared
805
 * invariant-to-synthesize, precondition, transition relation and condition.
806
 *
807
 * The actual constraint must be built such that the invariant is not stronger
808
 * than the precondition, not weaker than the postcondition and inductive
809
 * w.r.t. the transition relation.
810
 */
811
54
class CVC4_EXPORT SygusInvConstraintCommand : public Command
812
{
813
 public:
814
  SygusInvConstraintCommand(const std::vector<api::Term>& predicates);
815
  SygusInvConstraintCommand(const api::Term& inv,
816
                            const api::Term& pre,
817
                            const api::Term& trans,
818
                            const api::Term& post);
819
  /** returns the place holder predicates */
820
  const std::vector<api::Term>& getPredicates() const;
821
  /** invokes this command
822
   *
823
   * The place holders are communicated to the SMT engine and the actual
824
   * invariant constraint is built, in case an actual synthesis conjecture is
825
   * built later on.
826
   */
827
  void invoke(api::Solver* solver, SymbolManager* sm) override;
828
  /** creates a copy of this command */
829
  Command* clone() const override;
830
  /** returns this command's name */
831
  std::string getCommandName() const override;
832
  /** prints this command */
833
  void toStream(
834
      std::ostream& out,
835
      int toDepth = -1,
836
      size_t dag = 1,
837
      OutputLanguage language = language::output::LANG_AUTO) const override;
838
839
 protected:
840
  /** the place holder predicates with which to build the actual constraint
841
   * (i.e. the invariant, precondition, transition relation and postcondition)
842
   */
843
  std::vector<api::Term> d_predicates;
844
};
845
846
/** Declares a synthesis conjecture */
847
716
class CVC4_EXPORT CheckSynthCommand : public Command
848
{
849
 public:
850
358
  CheckSynthCommand(){};
851
  /** returns the result of the check-synth call */
852
  api::Result getResult() const;
853
  /** prints the result of the check-synth-call */
854
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
855
  /** invokes this command
856
   *
857
   * This invocation makes the SMT engine build a synthesis conjecture based on
858
   * previously declared information (such as universal variables,
859
   * functions-to-synthesize and so on), set up attributes to guide the solving,
860
   * and then perform a satisfiability check, whose result is stored in
861
   * d_result.
862
   */
863
  void invoke(api::Solver* solver, SymbolManager* sm) override;
864
  /** creates a copy of this command */
865
  Command* clone() const override;
866
  /** returns this command's name */
867
  std::string getCommandName() const override;
868
  /** prints this command */
869
  void toStream(
870
      std::ostream& out,
871
      int toDepth = -1,
872
      size_t dag = 1,
873
      OutputLanguage language = language::output::LANG_AUTO) const override;
874
875
 protected:
876
  /** result of the check-synth call */
877
  api::Result d_result;
878
  /** string stream that stores the output of the solution */
879
  std::stringstream d_solution;
880
};
881
882
/* ------------------- sygus commands  ------------------ */
883
884
// this is TRANSFORM in the CVC presentation language
885
class CVC4_EXPORT SimplifyCommand : public Command
886
{
887
 protected:
888
  api::Term d_term;
889
  api::Term d_result;
890
891
 public:
892
  SimplifyCommand(api::Term term);
893
894
  api::Term getTerm() const;
895
  api::Term getResult() const;
896
  void invoke(api::Solver* solver, SymbolManager* sm) override;
897
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
898
  Command* clone() const override;
899
  std::string getCommandName() const override;
900
  void toStream(
901
      std::ostream& out,
902
      int toDepth = -1,
903
      size_t dag = 1,
904
      OutputLanguage language = language::output::LANG_AUTO) const override;
905
}; /* class SimplifyCommand */
906
907
120
class CVC4_EXPORT GetValueCommand : public Command
908
{
909
 protected:
910
  std::vector<api::Term> d_terms;
911
  api::Term d_result;
912
913
 public:
914
  GetValueCommand(api::Term term);
915
  GetValueCommand(const std::vector<api::Term>& terms);
916
917
  const std::vector<api::Term>& getTerms() const;
918
  api::Term getResult() const;
919
  void invoke(api::Solver* solver, SymbolManager* sm) override;
920
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
921
  Command* clone() const override;
922
  std::string getCommandName() const override;
923
  void toStream(
924
      std::ostream& out,
925
      int toDepth = -1,
926
      size_t dag = 1,
927
      OutputLanguage language = language::output::LANG_AUTO) const override;
928
}; /* class GetValueCommand */
929
930
16
class CVC4_EXPORT GetAssignmentCommand : public Command
931
{
932
 protected:
933
  api::Term d_result;
934
935
 public:
936
  GetAssignmentCommand();
937
938
  api::Term getResult() const;
939
  void invoke(api::Solver* solver, SymbolManager* sm) override;
940
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
941
  Command* clone() const override;
942
  std::string getCommandName() const override;
943
  void toStream(
944
      std::ostream& out,
945
      int toDepth = -1,
946
      size_t dag = 1,
947
      OutputLanguage language = language::output::LANG_AUTO) const override;
948
}; /* class GetAssignmentCommand */
949
950
56
class CVC4_EXPORT GetModelCommand : public Command
951
{
952
 public:
953
  GetModelCommand();
954
955
  // Model is private to the library -- for now
956
  // Model* getResult() const ;
957
  void invoke(api::Solver* solver, SymbolManager* sm) override;
958
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
959
  Command* clone() const override;
960
  std::string getCommandName() const override;
961
  void toStream(
962
      std::ostream& out,
963
      int toDepth = -1,
964
      size_t dag = 1,
965
      OutputLanguage language = language::output::LANG_AUTO) const override;
966
967
 protected:
968
  smt::Model* d_result;
969
}; /* class GetModelCommand */
970
971
/** The command to block models. */
972
20
class CVC4_EXPORT BlockModelCommand : public Command
973
{
974
 public:
975
  BlockModelCommand();
976
977
  void invoke(api::Solver* solver, SymbolManager* sm) override;
978
  Command* clone() const override;
979
  std::string getCommandName() const override;
980
  void toStream(
981
      std::ostream& out,
982
      int toDepth = -1,
983
      size_t dag = 1,
984
      OutputLanguage language = language::output::LANG_AUTO) const override;
985
}; /* class BlockModelCommand */
986
987
/** The command to block model values. */
988
12
class CVC4_EXPORT BlockModelValuesCommand : public Command
989
{
990
 public:
991
  BlockModelValuesCommand(const std::vector<api::Term>& terms);
992
993
  const std::vector<api::Term>& getTerms() const;
994
  void invoke(api::Solver* solver, SymbolManager* sm) override;
995
  Command* clone() const override;
996
  std::string getCommandName() const override;
997
  void toStream(
998
      std::ostream& out,
999
      int toDepth = -1,
1000
      size_t dag = 1,
1001
      OutputLanguage language = language::output::LANG_AUTO) const override;
1002
1003
 protected:
1004
  /** The terms we are blocking */
1005
  std::vector<api::Term> d_terms;
1006
}; /* class BlockModelValuesCommand */
1007
1008
class CVC4_EXPORT GetProofCommand : public Command
1009
{
1010
 public:
1011
  GetProofCommand();
1012
1013
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1014
1015
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1016
1017
  Command* clone() const override;
1018
  std::string getCommandName() const override;
1019
  void toStream(
1020
      std::ostream& out,
1021
      int toDepth = -1,
1022
      size_t dag = 1,
1023
      OutputLanguage language = language::output::LANG_AUTO) const override;
1024
1025
 private:
1026
  /** the result of the getProof call */
1027
  std::string d_result;
1028
}; /* class GetProofCommand */
1029
1030
20
class CVC4_EXPORT GetInstantiationsCommand : public Command
1031
{
1032
 public:
1033
  GetInstantiationsCommand();
1034
1035
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1036
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1037
  Command* clone() const override;
1038
  std::string getCommandName() const override;
1039
  void toStream(
1040
      std::ostream& out,
1041
      int toDepth = -1,
1042
      size_t dag = 1,
1043
      OutputLanguage language = language::output::LANG_AUTO) const override;
1044
1045
 protected:
1046
  api::Solver* d_solver;
1047
}; /* class GetInstantiationsCommand */
1048
1049
class CVC4_EXPORT GetSynthSolutionCommand : public Command
1050
{
1051
 public:
1052
  GetSynthSolutionCommand();
1053
1054
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1055
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1056
  Command* clone() const override;
1057
  std::string getCommandName() const override;
1058
  void toStream(
1059
      std::ostream& out,
1060
      int toDepth = -1,
1061
      size_t dag = 1,
1062
      OutputLanguage language = language::output::LANG_AUTO) const override;
1063
1064
 protected:
1065
  api::Solver* d_solver;
1066
}; /* class GetSynthSolutionCommand */
1067
1068
/** The command (get-interpol s B (G)?)
1069
 *
1070
 * This command asks for an interpolant from the current set of assertions and
1071
 * conjecture (goal) B.
1072
 *
1073
 * The symbol s is the name for the interpolation predicate. If we successfully
1074
 * find a predicate P, then the output response of this command is: (define-fun
1075
 * s () Bool P)
1076
 */
1077
16
class CVC4_EXPORT GetInterpolCommand : public Command
1078
{
1079
 public:
1080
  GetInterpolCommand(const std::string& name, api::Term conj);
1081
  /** The argument g is the grammar of the interpolation query */
1082
  GetInterpolCommand(const std::string& name, api::Term conj, api::Grammar* g);
1083
1084
  /** Get the conjecture of the interpolation query */
1085
  api::Term getConjecture() const;
1086
  /** Get the sygus grammar given for the interpolation query */
1087
  const api::Grammar* getGrammar() const;
1088
  /** Get the result of the query, which is the solution to the interpolation
1089
   * query. */
1090
  api::Term getResult() const;
1091
1092
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1093
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1094
  Command* clone() const override;
1095
  std::string getCommandName() const override;
1096
  void toStream(
1097
      std::ostream& out,
1098
      int toDepth = -1,
1099
      size_t dag = 1,
1100
      OutputLanguage language = language::output::LANG_AUTO) const override;
1101
1102
 protected:
1103
  /** The name of the interpolation predicate */
1104
  std::string d_name;
1105
  /** The conjecture of the interpolation query */
1106
  api::Term d_conj;
1107
  /** The (optional) grammar of the interpolation query */
1108
  api::Grammar* d_sygus_grammar;
1109
  /** the return status of the command */
1110
  bool d_resultStatus;
1111
  /** the return expression of the command */
1112
  api::Term d_result;
1113
}; /* class GetInterpolCommand */
1114
1115
/** The command (get-abduct s B (G)?)
1116
 *
1117
 * This command asks for an abduct from the current set of assertions and
1118
 * conjecture (goal) given by the argument B.
1119
 *
1120
 * The symbol s is the name for the abduction predicate. If we successfully
1121
 * find a predicate P, then the output response of this command is:
1122
 *   (define-fun s () Bool P)
1123
 *
1124
 * A grammar G can be optionally provided to indicate the syntactic restrictions
1125
 * on the possible solutions returned.
1126
 */
1127
44
class CVC4_EXPORT GetAbductCommand : public Command
1128
{
1129
 public:
1130
  GetAbductCommand(const std::string& name, api::Term conj);
1131
  GetAbductCommand(const std::string& name, api::Term conj, api::Grammar* g);
1132
1133
  /** Get the conjecture of the abduction query */
1134
  api::Term getConjecture() const;
1135
  /** Get the grammar given for the abduction query */
1136
  const api::Grammar* getGrammar() const;
1137
  /** Get the name of the abduction predicate for the abduction query */
1138
  std::string getAbductName() const;
1139
  /** Get the result of the query, which is the solution to the abduction query.
1140
   */
1141
  api::Term getResult() const;
1142
1143
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1144
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1145
  Command* clone() const override;
1146
  std::string getCommandName() const override;
1147
  void toStream(
1148
      std::ostream& out,
1149
      int toDepth = -1,
1150
      size_t dag = 1,
1151
      OutputLanguage language = language::output::LANG_AUTO) const override;
1152
1153
 protected:
1154
  /** The name of the abduction predicate */
1155
  std::string d_name;
1156
  /** The conjecture of the abduction query */
1157
  api::Term d_conj;
1158
  /** The (optional) grammar of the abduction query */
1159
  api::Grammar* d_sygus_grammar;
1160
  /** the return status of the command */
1161
  bool d_resultStatus;
1162
  /** the return expression of the command */
1163
  api::Term d_result;
1164
}; /* class GetAbductCommand */
1165
1166
14
class CVC4_EXPORT GetQuantifierEliminationCommand : public Command
1167
{
1168
 protected:
1169
  api::Term d_term;
1170
  bool d_doFull;
1171
  api::Term d_result;
1172
1173
 public:
1174
  GetQuantifierEliminationCommand();
1175
  GetQuantifierEliminationCommand(const api::Term& term, bool doFull);
1176
1177
  api::Term getTerm() const;
1178
  bool getDoFull() const;
1179
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1180
  api::Term getResult() const;
1181
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1182
1183
  Command* clone() const override;
1184
  std::string getCommandName() const override;
1185
  void toStream(
1186
      std::ostream& out,
1187
      int toDepth = -1,
1188
      size_t dag = 1,
1189
      OutputLanguage language = language::output::LANG_AUTO) const override;
1190
}; /* class GetQuantifierEliminationCommand */
1191
1192
16
class CVC4_EXPORT GetUnsatAssumptionsCommand : public Command
1193
{
1194
 public:
1195
  GetUnsatAssumptionsCommand();
1196
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1197
  std::vector<api::Term> getResult() const;
1198
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1199
  Command* clone() const override;
1200
  std::string getCommandName() const override;
1201
  void toStream(
1202
      std::ostream& out,
1203
      int toDepth = -1,
1204
      size_t dag = 1,
1205
      OutputLanguage language = language::output::LANG_AUTO) const override;
1206
1207
 protected:
1208
  std::vector<api::Term> d_result;
1209
}; /* class GetUnsatAssumptionsCommand */
1210
1211
24
class CVC4_EXPORT GetUnsatCoreCommand : public Command
1212
{
1213
 public:
1214
  GetUnsatCoreCommand();
1215
  const std::vector<api::Term>& getUnsatCore() const;
1216
1217
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1218
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1219
1220
  Command* clone() const override;
1221
  std::string getCommandName() const override;
1222
  void toStream(
1223
      std::ostream& out,
1224
      int toDepth = -1,
1225
      size_t dag = 1,
1226
      OutputLanguage language = language::output::LANG_AUTO) const override;
1227
1228
 protected:
1229
  /** The symbol manager we were invoked with */
1230
  SymbolManager* d_sm;
1231
  /** the result of the unsat core call */
1232
  std::vector<api::Term> d_result;
1233
}; /* class GetUnsatCoreCommand */
1234
1235
class CVC4_EXPORT GetAssertionsCommand : public Command
1236
{
1237
 protected:
1238
  std::string d_result;
1239
1240
 public:
1241
  GetAssertionsCommand();
1242
1243
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1244
  std::string getResult() const;
1245
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1246
  Command* clone() const override;
1247
  std::string getCommandName() const override;
1248
  void toStream(
1249
      std::ostream& out,
1250
      int toDepth = -1,
1251
      size_t dag = 1,
1252
      OutputLanguage language = language::output::LANG_AUTO) const override;
1253
}; /* class GetAssertionsCommand */
1254
1255
class CVC4_EXPORT SetBenchmarkStatusCommand : public Command
1256
{
1257
 protected:
1258
  BenchmarkStatus d_status;
1259
1260
 public:
1261
  SetBenchmarkStatusCommand(BenchmarkStatus status);
1262
1263
  BenchmarkStatus getStatus() const;
1264
1265
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1266
  Command* clone() const override;
1267
  std::string getCommandName() const override;
1268
  void toStream(
1269
      std::ostream& out,
1270
      int toDepth = -1,
1271
      size_t dag = 1,
1272
      OutputLanguage language = language::output::LANG_AUTO) const override;
1273
}; /* class SetBenchmarkStatusCommand */
1274
1275
10428
class CVC4_EXPORT SetBenchmarkLogicCommand : public Command
1276
{
1277
 protected:
1278
  std::string d_logic;
1279
1280
 public:
1281
  SetBenchmarkLogicCommand(std::string logic);
1282
1283
  std::string getLogic() const;
1284
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1285
  Command* clone() const override;
1286
  std::string getCommandName() const override;
1287
  void toStream(
1288
      std::ostream& out,
1289
      int toDepth = -1,
1290
      size_t dag = 1,
1291
      OutputLanguage language = language::output::LANG_AUTO) const override;
1292
}; /* class SetBenchmarkLogicCommand */
1293
1294
10746
class CVC4_EXPORT SetInfoCommand : public Command
1295
{
1296
 protected:
1297
  std::string d_flag;
1298
  std::string d_value;
1299
1300
 public:
1301
  SetInfoCommand(const std::string& flag, const std::string& value);
1302
1303
  const std::string& getFlag() const;
1304
  const std::string& getValue() const;
1305
1306
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1307
  Command* clone() const override;
1308
  std::string getCommandName() const override;
1309
  void toStream(
1310
      std::ostream& out,
1311
      int toDepth = -1,
1312
      size_t dag = 1,
1313
      OutputLanguage language = language::output::LANG_AUTO) const override;
1314
}; /* class SetInfoCommand */
1315
1316
38
class CVC4_EXPORT GetInfoCommand : public Command
1317
{
1318
 protected:
1319
  std::string d_flag;
1320
  std::string d_result;
1321
1322
 public:
1323
  GetInfoCommand(std::string flag);
1324
1325
  std::string getFlag() const;
1326
  std::string getResult() const;
1327
1328
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1329
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1330
  Command* clone() const override;
1331
  std::string getCommandName() const override;
1332
  void toStream(
1333
      std::ostream& out,
1334
      int toDepth = -1,
1335
      size_t dag = 1,
1336
      OutputLanguage language = language::output::LANG_AUTO) const override;
1337
}; /* class GetInfoCommand */
1338
1339
13616
class CVC4_EXPORT SetOptionCommand : public Command
1340
{
1341
 protected:
1342
  std::string d_flag;
1343
  std::string d_value;
1344
1345
 public:
1346
  SetOptionCommand(const std::string& flag, const std::string& value);
1347
1348
  const std::string& getFlag() const;
1349
  const std::string& getValue() const;
1350
1351
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1352
  Command* clone() const override;
1353
  std::string getCommandName() const override;
1354
  void toStream(
1355
      std::ostream& out,
1356
      int toDepth = -1,
1357
      size_t dag = 1,
1358
      OutputLanguage language = language::output::LANG_AUTO) const override;
1359
}; /* class SetOptionCommand */
1360
1361
20
class CVC4_EXPORT GetOptionCommand : public Command
1362
{
1363
 protected:
1364
  std::string d_flag;
1365
  std::string d_result;
1366
1367
 public:
1368
  GetOptionCommand(std::string flag);
1369
1370
  std::string getFlag() const;
1371
  std::string getResult() const;
1372
1373
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1374
  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
1375
  Command* clone() const override;
1376
  std::string getCommandName() const override;
1377
  void toStream(
1378
      std::ostream& out,
1379
      int toDepth = -1,
1380
      size_t dag = 1,
1381
      OutputLanguage language = language::output::LANG_AUTO) const override;
1382
}; /* class GetOptionCommand */
1383
1384
1764
class CVC4_EXPORT DatatypeDeclarationCommand : public Command
1385
{
1386
 private:
1387
  std::vector<api::Sort> d_datatypes;
1388
1389
 public:
1390
  DatatypeDeclarationCommand(const api::Sort& datatype);
1391
1392
  DatatypeDeclarationCommand(const std::vector<api::Sort>& datatypes);
1393
  const std::vector<api::Sort>& getDatatypes() const;
1394
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1395
  Command* clone() const override;
1396
  std::string getCommandName() const override;
1397
  void toStream(
1398
      std::ostream& out,
1399
      int toDepth = -1,
1400
      size_t dag = 1,
1401
      OutputLanguage language = language::output::LANG_AUTO) const override;
1402
}; /* class DatatypeDeclarationCommand */
1403
1404
94
class CVC4_EXPORT ResetCommand : public Command
1405
{
1406
 public:
1407
47
  ResetCommand() {}
1408
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1409
  Command* clone() const override;
1410
  std::string getCommandName() const override;
1411
  void toStream(
1412
      std::ostream& out,
1413
      int toDepth = -1,
1414
      size_t dag = 1,
1415
      OutputLanguage language = language::output::LANG_AUTO) const override;
1416
}; /* class ResetCommand */
1417
1418
62
class CVC4_EXPORT ResetAssertionsCommand : public Command
1419
{
1420
 public:
1421
31
  ResetAssertionsCommand() {}
1422
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1423
  Command* clone() const override;
1424
  std::string getCommandName() const override;
1425
  void toStream(
1426
      std::ostream& out,
1427
      int toDepth = -1,
1428
      size_t dag = 1,
1429
      OutputLanguage language = language::output::LANG_AUTO) const override;
1430
}; /* class ResetAssertionsCommand */
1431
1432
1346
class CVC4_EXPORT QuitCommand : public Command
1433
{
1434
 public:
1435
673
  QuitCommand() {}
1436
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1437
  Command* clone() const override;
1438
  std::string getCommandName() const override;
1439
  void toStream(
1440
      std::ostream& out,
1441
      int toDepth = -1,
1442
      size_t dag = 1,
1443
      OutputLanguage language = language::output::LANG_AUTO) const override;
1444
}; /* class QuitCommand */
1445
1446
class CVC4_EXPORT CommentCommand : public Command
1447
{
1448
  std::string d_comment;
1449
1450
 public:
1451
  CommentCommand(std::string comment);
1452
1453
  std::string getComment() const;
1454
1455
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1456
  Command* clone() const override;
1457
  std::string getCommandName() const override;
1458
  void toStream(
1459
      std::ostream& out,
1460
      int toDepth = -1,
1461
      size_t dag = 1,
1462
      OutputLanguage language = language::output::LANG_AUTO) const override;
1463
}; /* class CommentCommand */
1464
1465
class CVC4_EXPORT CommandSequence : public Command
1466
{
1467
 protected:
1468
  /** All the commands to be executed (in sequence) */
1469
  std::vector<Command*> d_commandSequence;
1470
  /** Next command to be executed */
1471
  unsigned int d_index;
1472
1473
 public:
1474
  CommandSequence();
1475
  ~CommandSequence();
1476
1477
  void addCommand(Command* cmd);
1478
  void clear();
1479
1480
  void invoke(api::Solver* solver, SymbolManager* sm) override;
1481
  void invoke(api::Solver* solver,
1482
              SymbolManager* sm,
1483
              std::ostream& out) override;
1484
1485
  typedef std::vector<Command*>::iterator iterator;
1486
  typedef std::vector<Command*>::const_iterator const_iterator;
1487
1488
  const_iterator begin() const;
1489
  const_iterator end() const;
1490
1491
  iterator begin();
1492
  iterator end();
1493
1494
  Command* clone() const override;
1495
  std::string getCommandName() const override;
1496
  void toStream(
1497
      std::ostream& out,
1498
      int toDepth = -1,
1499
      size_t dag = 1,
1500
      OutputLanguage language = language::output::LANG_AUTO) const override;
1501
}; /* class CommandSequence */
1502
1503
10560
class CVC4_EXPORT DeclarationSequence : public CommandSequence
1504
{
1505
  void toStream(
1506
      std::ostream& out,
1507
      int toDepth = -1,
1508
      size_t dag = 1,
1509
      OutputLanguage language = language::output::LANG_AUTO) const override;
1510
};
1511
1512
}  // namespace CVC4
1513
1514
#endif /* CVC4__COMMAND_H */