From 72fe8a98d6f794a03727c6ec24af53cf75204275 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Sat, 18 Jun 2022 12:31:08 -0500 Subject: [PATCH] Remove redundant projection operators (#8889) This removes all projection operators for tuples and tables except a generic one `ProjectOp`. It also updates the number of indices and other issues in cvc5.cpp --- src/CMakeLists.txt | 6 +- src/api/cpp/cvc5.cpp | 35 ++++---- src/printer/smt2/smt2_printer.cpp | 13 ++- src/theory/bags/bag_reduction.cpp | 7 +- src/theory/bags/bags_utils.cpp | 8 +- src/theory/bags/inference_generator.cpp | 6 +- src/theory/bags/kinds | 32 +++---- src/theory/bags/table_project_op.cpp | 40 --------- src/theory/bags/table_project_op.h | 87 ------------------- src/theory/bags/theory_bags_type_rules.cpp | 11 ++- src/theory/datatypes/datatypes_rewriter.cpp | 4 +- src/theory/datatypes/kinds | 8 +- .../{tuple_project_op.cpp => project_op.cpp} | 7 +- .../{tuple_project_op.h => project_op.h} | 22 +---- .../datatypes/theory_datatypes_type_rules.cpp | 4 +- 15 files changed, 67 insertions(+), 223 deletions(-) delete mode 100644 src/theory/bags/table_project_op.cpp delete mode 100644 src/theory/bags/table_project_op.h rename src/theory/datatypes/{tuple_project_op.cpp => project_op.cpp} (91%) rename src/theory/datatypes/{tuple_project_op.h => project_op.h} (69%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1a46f4b74..995f15c85 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -567,8 +567,6 @@ libcvc5_add_sources( theory/bags/solver_state.h theory/bags/strategy.cpp theory/bags/strategy.h - theory/bags/table_project_op.cpp - theory/bags/table_project_op.h theory/bags/term_registry.cpp theory/bags/term_registry.h theory/bags/theory_bags.cpp @@ -662,8 +660,8 @@ libcvc5_add_sources( theory/datatypes/theory_datatypes_type_rules.h theory/datatypes/theory_datatypes_utils.cpp theory/datatypes/theory_datatypes_utils.h - theory/datatypes/tuple_project_op.cpp - theory/datatypes/tuple_project_op.h + theory/datatypes/project_op.cpp + theory/datatypes/project_op.h theory/datatypes/tuple_utils.cpp theory/datatypes/tuple_utils.h theory/datatypes/type_enumerator.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 92f791d51..ed46fa3ed 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -69,8 +69,7 @@ #include "smt/model.h" #include "smt/smt_mode.h" #include "smt/solver_engine.h" -#include "theory/bags/table_project_op.h" -#include "theory/datatypes/tuple_project_op.h" +#include "theory/datatypes/project_op.h" #include "theory/logic_info.h" #include "theory/theory_model.h" #include "util/bitvector.h" @@ -1949,11 +1948,14 @@ size_t Op::getNumIndicesHelper() const case FLOATINGPOINT_TO_FP_FROM_UBV: size = 2; break; case REGEXP_LOOP: size = 2; break; case TUPLE_PROJECT: - size = d_node->getConst().getIndices().size(); - break; + case TABLE_AGGREGATE: + case TABLE_GROUP: + case TABLE_JOIN: case TABLE_PROJECT: - size = d_node->getConst().getIndices().size(); + { + size = d_node->getConst().getIndices().size(); break; + } default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k); } return size; @@ -2105,11 +2107,14 @@ Term Op::getIndexHelper(size_t index) const break; } - case TUPLE_PROJECT: + case TABLE_AGGREGATE: + case TABLE_GROUP: + case TABLE_JOIN: + case TABLE_PROJECT: { const std::vector& projectionIndices = - d_node->getConst().getIndices(); + d_node->getConst().getIndices(); t = d_solver->mkRationalValHelper(projectionIndices[index]); break; } @@ -6144,20 +6149,14 @@ Op Solver::mkOp(Kind kind, const std::vector& args) const res = mkOpHelper(kind, internal::RegExpLoop(args[0], args[1])); break; case TUPLE_PROJECT: - res = mkOpHelper(kind, internal::TupleProjectOp(args)); - break; - case TABLE_PROJECT: - res = mkOpHelper(kind, internal::TableProjectOp(args)); - break; case TABLE_AGGREGATE: - res = mkOpHelper(kind, internal::TableAggregateOp(args)); - break; - case TABLE_JOIN: - res = mkOpHelper(kind, internal::TableJoinOp(args)); - break; case TABLE_GROUP: - res = mkOpHelper(kind, internal::TableGroupOp(args)); + case TABLE_JOIN: + case TABLE_PROJECT: + { + res = mkOpHelper(kind, internal::ProjectOp(args)); break; + } default: if (nargs == 0) { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5908e82e7..c49bd202f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -40,9 +40,8 @@ #include "proof/unsat_core.h" #include "smt/command.h" #include "theory/arrays/theory_arrays_rewriter.h" -#include "theory/bags/table_project_op.h" +#include "theory/datatypes/project_op.h" #include "theory/datatypes/sygus_datatype_utils.h" -#include "theory/datatypes/tuple_project_op.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/theory_model.h" #include "theory/uf/function_const.h" @@ -747,7 +746,7 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::TUPLE_PROJECT: { - TupleProjectOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); if (op.getIndices().empty()) { // e.g. (tuple.project tuple) @@ -762,7 +761,7 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::TABLE_PROJECT: { - TableProjectOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); if (op.getIndices().empty()) { // e.g. (table.project A) @@ -777,7 +776,7 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::TABLE_AGGREGATE: { - TableAggregateOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); if (op.getIndices().empty()) { // e.g. (table.project function initial_value bag) @@ -793,7 +792,7 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::TABLE_JOIN: { - TableJoinOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); if (op.getIndices().empty()) { // e.g. (table.join A B) @@ -808,7 +807,7 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::TABLE_GROUP: { - TableGroupOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); if (op.getIndices().empty()) { // e.g. (table.group A) diff --git a/src/theory/bags/bag_reduction.cpp b/src/theory/bags/bag_reduction.cpp index e7ccba325..b2713f882 100644 --- a/src/theory/bags/bag_reduction.cpp +++ b/src/theory/bags/bag_reduction.cpp @@ -18,7 +18,7 @@ #include "expr/bound_var_manager.h" #include "expr/emptybag.h" #include "expr/skolem_manager.h" -#include "table_project_op.h" +#include "theory/datatypes/project_op.h" #include "theory/datatypes/tuple_utils.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "util/rational.h" @@ -211,10 +211,9 @@ Node BagReduction::reduceAggregateOperator(Node node) TypeNode elementType = function.getType().getArgTypes()[0]; Node initialValue = node[1]; Node A = node[2]; - const std::vector& indices = - node.getOperator().getConst().getIndices(); + ProjectOp op = node.getOperator().getConst(); - Node groupOp = nm->mkConst(TableGroupOp(indices)); + Node groupOp = nm->mkConst(TABLE_GROUP_OP, op); Node group = nm->mkNode(TABLE_GROUP, {groupOp, A}); Node bag = bvm->mkBoundVar( diff --git a/src/theory/bags/bags_utils.cpp b/src/theory/bags/bags_utils.cpp index 4935a24d4..83be57a5e 100644 --- a/src/theory/bags/bags_utils.cpp +++ b/src/theory/bags/bags_utils.cpp @@ -18,8 +18,8 @@ #include "expr/dtype_cons.h" #include "expr/emptybag.h" #include "smt/logic_exception.h" -#include "table_project_op.h" #include "theory/bags/bag_reduction.h" +#include "theory/datatypes/project_op.h" #include "theory/datatypes/tuple_utils.h" #include "theory/rewriter.h" #include "theory/sets/normal_form.h" @@ -992,7 +992,7 @@ Node BagsUtils::evaluateGroup(Rewriter* rewriter, TNode n) } std::vector indices = - n.getOperator().getConst().getIndices(); + n.getOperator().getConst().getIndices(); std::map elements = BagsUtils::getBagElements(A); Trace("bags-group") << "elements: " << elements << std::endl; @@ -1069,7 +1069,7 @@ Node BagsUtils::evaluateTableProject(TNode n) std::map elements; std::vector indices = - n.getOperator().getConst().getIndices(); + n.getOperator().getConst().getIndices(); for (const auto& [a, countA] : elementsA) { @@ -1088,7 +1088,7 @@ BagsUtils::splitTableJoinIndices(Node n) { Assert(n.getKind() == kind::TABLE_JOIN && n.hasOperator() && n.getOperator().getKind() == kind::TABLE_JOIN_OP); - TableJoinOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); const std::vector& indices = op.getIndices(); size_t joinSize = indices.size() / 2; std::vector indices1(joinSize), indices2(joinSize); diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 31509fa9c..dd560b8f3 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -23,7 +23,7 @@ #include "theory/bags/bags_utils.h" #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" -#include "theory/bags/table_project_op.h" +#include "theory/datatypes/project_op.h" #include "theory/datatypes/tuple_utils.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/uf/equality_engine.h" @@ -647,7 +647,7 @@ InferInfo InferenceGenerator::joinUp(Node n, Node e1, Node e2) std::vector aElements = TupleUtils::getTupleElements(e1); std::vector bElements = TupleUtils::getTupleElements(e2); const std::vector& indices = - n.getOperator().getConst().getIndices(); + n.getOperator().getConst().getIndices(); InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_UP); @@ -704,7 +704,7 @@ InferInfo InferenceGenerator::joinDown(Node n, Node e) Node multiply = d_nm->mkNode(MULT, countA, countB); Node multiplicityConstraint = count.eqNode(multiply); const std::vector& indices = - n.getOperator().getConst().getIndices(); + n.getOperator().getConst().getIndices(); Node joinConstraints = d_true; for (size_t i = 0; i < indices.size(); i += 2) { diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index 9961b5864..cf91ec318 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -117,40 +117,40 @@ operator TABLE_PRODUCT 2 "table cross product" # table.project operator extends datatypes tuple_project operator to a bag of tuples constant TABLE_PROJECT_OP \ class \ - TableProjectOp \ - ::cvc5::internal::TableProjectOpHashFunction \ - "theory/bags/table_project_op.h" \ - "operator for TABLE_PROJECT; payload is an instance of the cvc5::internal::TableProjectOp class" + ProjectOp+ \ + ::cvc5::internal::ProjectOpHashFunction \ + "theory/datatypes/project_op.h" \ + "operator for TABLE_PROJECT; payload is an instance of the cvc5::internal::ProjectOp class" parameterized TABLE_PROJECT TABLE_PROJECT_OP 1 "table projection" # table.aggregate operator constant TABLE_AGGREGATE_OP \ class \ - TableAggregateOp \ - ::cvc5::internal::TableAggregateOpHashFunction \ - "theory/bags/table_project_op.h" \ - "operator for TABLE_AGGREGATE; payload is an instance of the cvc5::internal::TableAggregateOp class" + ProjectOp+ \ + ::cvc5::internal::ProjectOpHashFunction \ + "theory/datatypes/project_op.h" \ + "operator for TABLE_AGGREGATE; payload is an instance of the cvc5::internal::ProjectOp class" parameterized TABLE_AGGREGATE TABLE_AGGREGATE_OP 3 "table aggregate" # table.join operator constant TABLE_JOIN_OP \ class \ - TableJoinOp \ - ::cvc5::internal::TableJoinOpHashFunction \ - "theory/bags/table_project_op.h" \ - "operator for TABLE_JOIN; payload is an instance of the cvc5::internal::TableJoinOp class" + ProjectOp+ \ + ::cvc5::internal::ProjectOpHashFunction \ + "theory/datatypes/project_op.h" \ + "operator for TABLE_JOIN; payload is an instance of the cvc5::internal::ProjectOp class" parameterized TABLE_JOIN TABLE_JOIN_OP 2 "table join" # table.group operator constant TABLE_GROUP_OP \ class \ - TableGroupOp \ - ::cvc5::internal::TableGroupOpHashFunction \ - "theory/bags/table_project_op.h" \ - "operator for TABLE_GROUP; payload is an instance of the cvc5::internal::TableGroupOp class" + ProjectOp+ \ + ::cvc5::internal::ProjectOpHashFunction \ + "theory/datatypes/project_op.h" \ + "operator for TABLE_GROUP; payload is an instance of the cvc5::internal::ProjectOp class" parameterized TABLE_GROUP TABLE_GROUP_OP 1 "table group" diff --git a/src/theory/bags/table_project_op.cpp b/src/theory/bags/table_project_op.cpp deleted file mode 100644 index 9c19cdba7..000000000 --- a/src/theory/bags/table_project_op.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class for TableProjectOp operator. - */ - -#include "table_project_op.h" - -namespace cvc5::internal { - -TableProjectOp::TableProjectOp(std::vector indices) - : ProjectOp(std::move(indices)) -{ -} - -TableAggregateOp::TableAggregateOp(std::vector indices) - : ProjectOp(std::move(indices)) -{ -} - -TableJoinOp::TableJoinOp(std::vector indices) - : ProjectOp(std::move(indices)) -{ -} - -TableGroupOp::TableGroupOp(std::vector indices) - : ProjectOp(std::move(indices)) -{ -} - -} // namespace cvc5::internal diff --git a/src/theory/bags/table_project_op.h b/src/theory/bags/table_project_op.h deleted file mode 100644 index 03f2f5561..000000000 --- a/src/theory/bags/table_project_op.h +++ /dev/null @@ -1,87 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class for TableProjectOp operator. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__TABLE_PROJECT_OP_H -#define CVC5__TABLE_PROJECT_OP_H - -#include "theory/datatypes/tuple_project_op.h" - -namespace cvc5::internal { - -/** - * The class is an operator for kind project used to project elements in a - * table. It stores the indices of projected elements - */ -class TableProjectOp : public ProjectOp -{ - public: - explicit TableProjectOp(std::vector indices); - TableProjectOp(const TableProjectOp& op) = default; -}; /* class TableProjectOp */ - -/** - * Hash function for the TableProjectOpHashFunction objects. - */ -struct TableProjectOpHashFunction : public ProjectOpHashFunction -{ -}; /* struct TableProjectOpHashFunction */ - -class TableAggregateOp : public ProjectOp -{ - public: - explicit TableAggregateOp(std::vector indices); - TableAggregateOp(const TableAggregateOp& op) = default; -}; /* class TableAggregateOp */ - -/** - * Hash function for the TableAggregateOpHashFunction objects. - */ -struct TableAggregateOpHashFunction : public ProjectOpHashFunction -{ -}; /* struct TableAggregateOpHashFunction */ - -class TableJoinOp : public ProjectOp -{ - public: - explicit TableJoinOp(std::vector indices); - TableJoinOp(const TableJoinOp& op) = default; -}; /* class TableJoinOp */ - -/** - * Hash function for the TableJoinOpHashFunction objects. - */ -struct TableJoinOpHashFunction : public ProjectOpHashFunction -{ -}; /* struct TableJoinOpHashFunction */ - -class TableGroupOp : public ProjectOp -{ - public: - explicit TableGroupOp(std::vector indices); - TableGroupOp(const TableGroupOp& op) = default; -}; /* class TableGroupOp */ - -/** - * Hash function for the TableGroupOpHashFunction objects. - */ -struct TableGroupOpHashFunction : public ProjectOpHashFunction -{ -}; /* struct TableGroupOpHashFunction */ - -} // namespace cvc5::internal - -#endif /* CVC5__TABLE_PROJECT_OP_H */ diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 0bcf95612..a5ac9c1e2 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -21,9 +21,8 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/emptybag.h" -#include "table_project_op.h" #include "theory/bags/bags_utils.h" -#include "theory/datatypes/tuple_project_op.h" +#include "theory/datatypes/project_op.h" #include "theory/datatypes/tuple_utils.h" #include "util/cardinality.h" #include "util/rational.h" @@ -523,7 +522,7 @@ TypeNode TableProjectTypeRule::computeType(NodeManager* nm, TNode n, bool check) { Assert(n.getKind() == kind::TABLE_PROJECT && n.hasOperator() && n.getOperator().getKind() == kind::TABLE_PROJECT_OP); - TableProjectOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); const std::vector& indices = op.getIndices(); TypeNode bagType = n[0].getType(check); if (check) @@ -580,7 +579,7 @@ TypeNode TableAggregateTypeRule::computeType(NodeManager* nm, { Assert(n.getKind() == kind::TABLE_AGGREGATE && n.hasOperator() && n.getOperator().getKind() == kind::TABLE_AGGREGATE_OP); - TableAggregateOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); const std::vector& indices = op.getIndices(); TypeNode functionType = n[0].getType(check); @@ -644,7 +643,7 @@ TypeNode TableJoinTypeRule::computeType(NodeManager* nm, TNode n, bool check) { Assert(n.getKind() == kind::TABLE_JOIN && n.hasOperator() && n.getOperator().getKind() == kind::TABLE_JOIN_OP); - TableJoinOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); const std::vector& indices = op.getIndices(); Node A = n[0]; Node B = n[1]; @@ -711,7 +710,7 @@ TypeNode TableGroupTypeRule::computeType(NodeManager* nm, TNode n, bool check) { Assert(n.getKind() == kind::TABLE_GROUP && n.hasOperator() && n.getOperator().getKind() == kind::TABLE_GROUP_OP); - TableGroupOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); const std::vector& indices = op.getIndices(); TypeNode bagType = n[0].getType(check); diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 928b6d1e4..17061532c 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -23,9 +23,9 @@ #include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" #include "options/datatypes_options.h" +#include "theory/datatypes/project_op.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" -#include "theory/datatypes/tuple_project_op.h" #include "tuple_utils.h" #include "util/rational.h" #include "util/uninterpreted_sort_value.h" @@ -167,7 +167,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) Trace("dt-rewrite-project") << "Rewrite project: " << in << std::endl; - TupleProjectOp op = in.getOperator().getConst(); + ProjectOp op = in.getOperator().getConst(); std::vector indices = op.getIndices(); Node tuple = in[0]; Node ret = TupleUtils::getTupleProjection(indices, tuple); diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index dee4fe4be..9e0f5de47 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -141,10 +141,10 @@ typerule MATCH_BIND_CASE ::cvc5::internal::theory::datatypes::MatchBindCaseTypeR constant TUPLE_PROJECT_OP \ class \ - TupleProjectOp \ - ::cvc5::internal::TupleProjectOpHashFunction \ - "theory/datatypes/tuple_project_op.h" \ - "operator for TUPLE_PROJECT; payload is an instance of the cvc5::internal::TupleProjectOp class" + ProjectOp+ \ + ::cvc5::internal::ProjectOpHashFunction \ + "theory/datatypes/project_op.h" \ + "operator for TUPLE_PROJECT; payload is an instance of the cvc5::internal::ProjectOp class" parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \ "projects a tuple from an existing tuple using indices passed in TupleProjectOp" diff --git a/src/theory/datatypes/tuple_project_op.cpp b/src/theory/datatypes/project_op.cpp similarity index 91% rename from src/theory/datatypes/tuple_project_op.cpp rename to src/theory/datatypes/project_op.cpp index 28027528f..23973fec4 100644 --- a/src/theory/datatypes/tuple_project_op.cpp +++ b/src/theory/datatypes/project_op.cpp @@ -13,7 +13,7 @@ * A class for ProjectOp operator. */ -#include "tuple_project_op.h" +#include "project_op.h" #include @@ -54,9 +54,4 @@ bool ProjectOp::operator==(const ProjectOp& op) const return d_indices == op.d_indices; } -TupleProjectOp::TupleProjectOp(std::vector indices) - : ProjectOp(std::move(indices)) -{ -} - } // namespace cvc5::internal diff --git a/src/theory/datatypes/tuple_project_op.h b/src/theory/datatypes/project_op.h similarity index 69% rename from src/theory/datatypes/tuple_project_op.h rename to src/theory/datatypes/project_op.h index 7d1b46ff9..5fa1f1d07 100644 --- a/src/theory/datatypes/tuple_project_op.h +++ b/src/theory/datatypes/project_op.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A class for TupleProjectOp operator. + * A class for ProjectOp operator. */ #include "cvc5_public.h" @@ -26,7 +26,7 @@ namespace cvc5::internal { class TypeNode; /** - * base class for TupleProjectOp, TupleProjectOp + * class for projection operators */ class ProjectOp { @@ -53,24 +53,6 @@ struct ProjectOpHashFunction size_t operator()(const ProjectOp& op) const; }; /* struct ProjectOpHashFunction */ -/** - * The class is an operator for kind project used to project elements in a - * table. It stores the indices of projected elements - */ -class TupleProjectOp : public ProjectOp -{ - public: - explicit TupleProjectOp(std::vector indices); - TupleProjectOp(const TupleProjectOp& op) = default; -}; /* class TupleProjectOp */ - -/** - * Hash function for the TupleProjectOpHashFunction objects. - */ -struct TupleProjectOpHashFunction : public ProjectOpHashFunction -{ -}; /* struct TupleProjectOpHashFunction */ - } // namespace cvc5::internal #endif /* CVC5__PROJECT_OP_H */ diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 1a8c62225..be96741d4 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -22,8 +22,8 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/type_matcher.h" +#include "theory/datatypes/project_op.h" #include "theory/datatypes/theory_datatypes_utils.h" -#include "theory/datatypes/tuple_project_op.h" #include "theory/datatypes/tuple_utils.h" #include "util/rational.h" @@ -519,7 +519,7 @@ TypeNode TupleProjectTypeRule::computeType(NodeManager* nm, TNode n, bool check) { Assert(n.getKind() == kind::TUPLE_PROJECT && n.hasOperator() && n.getOperator().getKind() == kind::TUPLE_PROJECT_OP); - TupleProjectOp op = n.getOperator().getConst(); + ProjectOp op = n.getOperator().getConst(); const std::vector& indices = op.getIndices(); if (check) { -- 2.30.2