dReal4
command.h
1 #pragma once
2 
3 #include <memory>
4 #include <ostream>
5 #include <string>
6 #include <utility>
7 
8 #include "dreal/smt2/logic.h"
10 
11 namespace dreal {
12 
13 class CommandCell;
14 
15 /** Command class in smt2lib. It only includes a shared_ptr to
16  * CommandCell.*/
17 class Command {
18  public:
19  explicit Command(std::shared_ptr<CommandCell> ptr) : ptr_{std::move(ptr)} {}
20 
21  private:
22  std::shared_ptr<CommandCell> ptr_;
23 
24  friend std::ostream& operator<<(std::ostream& os, const Command& c);
25 };
26 std::ostream& operator<<(std::ostream& os, const Command& c);
27 
28 Command assert_command(const Formula& f);
29 Command check_sat_command();
30 Command exit_command();
31 Command pop_command(int level);
32 Command push_command(int level);
33 Command reset_command();
34 Command set_info_command(const std::string& key, const std::string& val);
35 Command set_logic_command(Logic logic);
36 Command set_option_command(const std::string& key, const std::string& val);
37 
38 } // namespace dreal
Sum type of symbolic::Expression and symbolic::Formula.
Definition: api.cc:9
Command class in smt2lib.
Definition: command.h:17
This is the header file that we consolidate Drake&#39;s symbolic classes and expose them inside of dreal ...
Represents a symbolic form of a first-order logic formula.
Definition: symbolic_formula.h:101