diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/dtype.h | 3 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 10 |
2 files changed, 0 insertions, 13 deletions
diff --git a/src/expr/dtype.h b/src/expr/dtype.h index b2399472a..08fe9965b 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -243,9 +243,6 @@ class DType /** is this a tuple datatype? */ bool isTuple() const; - /** get the record representation for this datatype */ - Record* getRecord() const; - /** * Return the cardinality of this datatype. * The DType must be resolved. diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index e11ac67f1..0779fdc58 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -24,19 +24,9 @@ #include "theory/datatypes/theory_datatypes_utils.h" namespace CVC4 { - -namespace expr { -namespace attr { -struct DatatypeConstructorTypeGroundTermTag {}; -} /* CVC4::expr::attr namespace */ -} /* CVC4::expr namespace */ - namespace theory { namespace datatypes { -typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> - GroundTermAttr; - struct DatatypeConstructorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { |