From: mudathirmahgoub Date: Sat, 18 Jun 2022 17:31:08 +0000 (-0500) Subject: Remove redundant projection operators (#8889) X-Git-Tag: cvc5-1.0.1~48 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=72fe8a98d6f794a03727c6ec24af53cf75204275;p=cvc5.git 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 --- 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/project_op.cpp b/src/theory/datatypes/project_op.cpp new file mode 100644 index 000000000..23973fec4 --- /dev/null +++ b/src/theory/datatypes/project_op.cpp @@ -0,0 +1,57 @@ +/****************************************************************************** + * 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 ProjectOp operator. + */ + +#include "project_op.h" + +#include + +#include "expr/type_node.h" + +namespace cvc5::internal { + +std::ostream& operator<<(std::ostream& out, const ProjectOp& op) +{ + for (const uint32_t& index : op.getIndices()) + { + out << " " << index; + } + return out; +} + +size_t ProjectOpHashFunction::operator()(const ProjectOp& op) const +{ + // we expect most tuples to have length < 10. + // Therefore we can implement a simple hash function + size_t hash = 0; + for (uint32_t index : op.getIndices()) + { + hash = hash * 10 + index; + } + return hash; +} + +ProjectOp::ProjectOp(std::vector indices) + : d_indices(std::move(indices)) +{ +} + +const std::vector& ProjectOp::getIndices() const { return d_indices; } + +bool ProjectOp::operator==(const ProjectOp& op) const +{ + return d_indices == op.d_indices; +} + +} // namespace cvc5::internal diff --git a/src/theory/datatypes/project_op.h b/src/theory/datatypes/project_op.h new file mode 100644 index 000000000..5fa1f1d07 --- /dev/null +++ b/src/theory/datatypes/project_op.h @@ -0,0 +1,58 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, Aina Niemetz, Mathias Preiner + * + * 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 ProjectOp operator. + */ + +#include "cvc5_public.h" + +#ifndef CVC5__PROJECT_OP_H +#define CVC5__PROJECT_OP_H + +#include +#include + +namespace cvc5::internal { + +class TypeNode; + +/** + * class for projection operators + */ +class ProjectOp +{ + public: + explicit ProjectOp(std::vector indices); + ProjectOp(const ProjectOp& op) = default; + + /** return the indices of the projection */ + const std::vector& getIndices() const; + + bool operator==(const ProjectOp& op) const; + + private: + std::vector d_indices; +}; /* class ProjectOp */ + +std::ostream& operator<<(std::ostream& out, const ProjectOp& op); + +/** + * Hash function for the ProjectOpHashFunction objects. + */ +struct ProjectOpHashFunction +{ + size_t operator()(const ProjectOp& op) const; +}; /* struct ProjectOpHashFunction */ + +} // 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) { diff --git a/src/theory/datatypes/tuple_project_op.cpp b/src/theory/datatypes/tuple_project_op.cpp deleted file mode 100644 index 28027528f..000000000 --- a/src/theory/datatypes/tuple_project_op.cpp +++ /dev/null @@ -1,62 +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 ProjectOp operator. - */ - -#include "tuple_project_op.h" - -#include - -#include "expr/type_node.h" - -namespace cvc5::internal { - -std::ostream& operator<<(std::ostream& out, const ProjectOp& op) -{ - for (const uint32_t& index : op.getIndices()) - { - out << " " << index; - } - return out; -} - -size_t ProjectOpHashFunction::operator()(const ProjectOp& op) const -{ - // we expect most tuples to have length < 10. - // Therefore we can implement a simple hash function - size_t hash = 0; - for (uint32_t index : op.getIndices()) - { - hash = hash * 10 + index; - } - return hash; -} - -ProjectOp::ProjectOp(std::vector indices) - : d_indices(std::move(indices)) -{ -} - -const std::vector& ProjectOp::getIndices() const { return d_indices; } - -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/tuple_project_op.h deleted file mode 100644 index 7d1b46ff9..000000000 --- a/src/theory/datatypes/tuple_project_op.h +++ /dev/null @@ -1,76 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed, Aina Niemetz, Mathias Preiner - * - * 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 TupleProjectOp operator. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__PROJECT_OP_H -#define CVC5__PROJECT_OP_H - -#include -#include - -namespace cvc5::internal { - -class TypeNode; - -/** - * base class for TupleProjectOp, TupleProjectOp - */ -class ProjectOp -{ - public: - explicit ProjectOp(std::vector indices); - ProjectOp(const ProjectOp& op) = default; - - /** return the indices of the projection */ - const std::vector& getIndices() const; - - bool operator==(const ProjectOp& op) const; - - private: - std::vector d_indices; -}; /* class ProjectOp */ - -std::ostream& operator<<(std::ostream& out, const ProjectOp& op); - -/** - * Hash function for the ProjectOpHashFunction objects. - */ -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 */