diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-20 13:07:22 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-20 11:07:22 -0800 |
| commit | c780b1778e97afe15a0eb2522505b796cd5bbe71 (patch) | |
| tree | 62eb88e0f8180f2ae165c0669a724f9baa53755e | |
| parent | 92f5835e86e6741eb6b273047e0a003212a8b638 (diff) | |
Minor removals (#3786)
Found while working on parser migration of datatypes.
| -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) { |