GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/sygus_datatype.h Lines: 3 3 100.0 %
Date: 2021-03-22 Branches: 3 10 30.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_datatype.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa
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 A class for constructing SyGuS datatypes.
13
 **/
14
#include "cvc4_private.h"
15
16
#ifndef CVC4__EXPR__SYGUS_DATATYPE_H
17
#define CVC4__EXPR__SYGUS_DATATYPE_H
18
19
#include <string>
20
#include <vector>
21
22
#include "expr/attribute.h"
23
#include "expr/dtype.h"
24
#include "expr/node.h"
25
#include "expr/type_node.h"
26
27
namespace CVC4 {
28
29
/** Attribute true for variables that represent any constant */
30
struct SygusAnyConstAttributeId
31
{
32
};
33
typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
34
35
/**
36
 * Information necessary to specify a sygus constructor. Further detail on these
37
 * fields can be found in SygusDatatype below.
38
 */
39
79353
class SygusDatatypeConstructor
40
{
41
 public:
42
  /** The operator that the constructor encodes. */
43
  Node d_op;
44
  /** Name of the constructor. */
45
  std::string d_name;
46
  /** List of argument types. */
47
  std::vector<TypeNode> d_argTypes;
48
  /** Weight of the constructor. */
49
  int d_weight;
50
};
51
52
/**
53
 * Keeps the necessary information for initializing a sygus datatype, which
54
 * includes the operators, names, print callbacks and list of argument types
55
 * for each constructor.
56
 *
57
 * It also maintains a datatype to represent the structure of the type node.
58
 *
59
 * Notice that this class is only responsible for setting SyGuS-related
60
 * information regarding the datatype. It is still required that the user
61
 * of this class construct the datatype type corresponding to the datatype
62
 * e.g. via a call to ExprManager::mkMutualDatatypeTypes().
63
 */
64
2427
class SygusDatatype
65
{
66
 public:
67
  /** constructor */
68
  SygusDatatype(const std::string& name);
69
4204
  ~SygusDatatype() {}
70
  /** get the name of this datatype */
71
  std::string getName() const;
72
  /**
73
   * Add constructor that encodes an application of builtin operator op.
74
   *
75
   * op: the builtin operator,
76
   * name: the name of the constructor,
77
   * argTypes: the argument types of the constructor (typically other sygus
78
   * datatype types).
79
   * spc: the print callback (for custom printing of this node),
80
   * weight: the weight of this constructor.
81
   *
82
   * It should be the case that argTypes are sygus datatype types (possibly
83
   * unresolved) that encode the arguments of the builtin operator. That is,
84
   * if op is the builtin PLUS operator, then argTypes could contain 2+
85
   * sygus datatype types that encode integer.
86
   */
87
  void addConstructor(Node op,
88
                      const std::string& name,
89
                      const std::vector<TypeNode>& argTypes,
90
                      int weight = -1);
91
  /**
92
   * Add constructor that encodes an application of builtin kind k. Like above,
93
   * the arguments argTypes should correspond to sygus datatypes that encode
94
   * the types of the arguments of the kind.
95
   */
96
  void addConstructor(Kind k,
97
                      const std::vector<TypeNode>& argTypes,
98
                      int weight = -1);
99
  /**
100
   * This adds a constructor that corresponds to the any constant constructor
101
   * for the given (builtin) type tn.
102
   */
103
  void addAnyConstantConstructor(TypeNode tn);
104
105
  /** Get the number of constructors added to this class so far */
106
  size_t getNumConstructors() const;
107
108
  /** Get constructor at index i */
109
  const SygusDatatypeConstructor& getConstructor(unsigned i) const;
110
111
  /** builds a datatype with the information in the type object
112
   *
113
   * sygusType: the builtin type that this datatype encodes,
114
   * sygusVars: the formal argument list of the function-to-synthesize,
115
   * allowConst: whether the grammar corresponding to this datatype allows
116
   * any constant,
117
   * allowAll: whether the grammar corresponding to this datatype allows
118
   * any term.
119
   */
120
  void initializeDatatype(TypeNode sygusType,
121
                          Node sygusVars,
122
                          bool allowConst,
123
                          bool allowAll);
124
  /** Get the sygus datatype initialized by this class */
125
  const DType& getDatatype() const;
126
127
  /** is initialized */
128
  bool isInitialized() const;
129
130
 private:
131
  /** Information for each constructor. */
132
  std::vector<SygusDatatypeConstructor> d_cons;
133
  /** Datatype to represent type's structure */
134
  DType d_dt;
135
};
136
137
}  // namespace CVC4
138
139
#endif