GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/node_command.h Lines: 5 5 100.0 %
Date: 2021-03-23 Branches: 3 32 9.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_command.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Abdalrhman Mohamed
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 Datastructures used for printing commands internally.
13
 **
14
 ** Datastructures used for printing commands internally.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__SMT__NODE_COMMAND_H
20
#define CVC4__SMT__NODE_COMMAND_H
21
22
#include <string>
23
24
#include "expr/node.h"
25
#include "expr/type_node.h"
26
#include "options/language.h"
27
28
namespace CVC4 {
29
30
/**
31
 * A node version of Command. DO NOT use this version unless there is a need
32
 * to buffer commands for later use (e.g., printing models).
33
 */
34
283359
class NodeCommand
35
{
36
 public:
37
  /** Destructor */
38
  virtual ~NodeCommand();
39
40
  /** Print this NodeCommand to output stream */
41
  virtual void toStream(
42
      std::ostream& out,
43
      int toDepth = -1,
44
      size_t dag = 1,
45
      OutputLanguage language = language::output::LANG_AUTO) const = 0;
46
47
  /** Get a string representation of this NodeCommand */
48
  std::string toString() const;
49
50
  /** Clone this NodeCommand (make a shallow copy). */
51
  virtual NodeCommand* clone() const = 0;
52
};
53
54
std::ostream& operator<<(std::ostream& out, const NodeCommand& nc);
55
56
/**
57
 * Declare n-ary function symbol.
58
 * SMT-LIB: ( declare-fun <id> ( <type.getArgTypes()> ) <type.getRangeType()> )
59
 */
60
268641
class DeclareFunctionNodeCommand : public NodeCommand
61
{
62
 public:
63
  DeclareFunctionNodeCommand(const std::string& id, Node fun, TypeNode type);
64
  void toStream(
65
      std::ostream& out,
66
      int toDepth = -1,
67
      size_t dag = 1,
68
      OutputLanguage language = language::output::LANG_AUTO) const override;
69
  NodeCommand* clone() const override;
70
  const Node& getFunction() const;
71
72
 private:
73
  std::string d_id;
74
  Node d_fun;
75
  TypeNode d_type;
76
};
77
78
/**
79
 * Create datatype sort.
80
 * SMT-LIB: ( declare-datatypes ( <datatype decls>{n+1} ) ( <datatypes>{n+1} ) )
81
 */
82
2856
class DeclareDatatypeNodeCommand : public NodeCommand
83
{
84
 public:
85
  DeclareDatatypeNodeCommand(const std::vector<TypeNode>& datatypes);
86
  void toStream(
87
      std::ostream& out,
88
      int toDepth = -1,
89
      size_t dag = 1,
90
      OutputLanguage language = language::output::LANG_AUTO) const override;
91
  NodeCommand* clone() const override;
92
93
 private:
94
  std::vector<TypeNode> d_datatypes;
95
};
96
97
/**
98
 * Declare uninterpreted sort.
99
 * SMT-LIB: ( declare-sort <id> <arity> )
100
 */
101
9170
class DeclareTypeNodeCommand : public NodeCommand
102
{
103
 public:
104
  DeclareTypeNodeCommand(const std::string& id, size_t arity, TypeNode type);
105
  void toStream(
106
      std::ostream& out,
107
      int toDepth = -1,
108
      size_t dag = 1,
109
      OutputLanguage language = language::output::LANG_AUTO) const override;
110
  NodeCommand* clone() const override;
111
  const std::string getSymbol() const;
112
  const TypeNode& getType() const;
113
114
 private:
115
  std::string d_id;
116
  size_t d_arity;
117
  TypeNode d_type;
118
};
119
120
/**
121
 * Define n-ary function.
122
 * SMT-LIB: ( define-fun <id> ( <formals> ) <fun.getType()> <formula> )
123
 */
124
2873
class DefineFunctionNodeCommand : public NodeCommand
125
{
126
 public:
127
  DefineFunctionNodeCommand(const std::string& id,
128
                            Node fun,
129
                            const std::vector<Node>& formals,
130
                            Node formula);
131
  void toStream(
132
      std::ostream& out,
133
      int toDepth = -1,
134
      size_t dag = 1,
135
      OutputLanguage language = language::output::LANG_AUTO) const override;
136
  NodeCommand* clone() const override;
137
138
 private:
139
  std::string d_id;
140
  Node d_fun;
141
  std::vector<Node> d_formals;
142
  Node d_formula;
143
};
144
145
}  // namespace CVC4
146
147
#endif /* CVC4__SMT__NODE_COMMAND_H */