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
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
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
#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"
case FLOATINGPOINT_TO_FP_FROM_UBV: size = 2; break;
case REGEXP_LOOP: size = 2; break;
case TUPLE_PROJECT:
- size = d_node->getConst<internal::TupleProjectOp>().getIndices().size();
- break;
+ case TABLE_AGGREGATE:
+ case TABLE_GROUP:
+ case TABLE_JOIN:
case TABLE_PROJECT:
- size = d_node->getConst<internal::TableProjectOp>().getIndices().size();
+ {
+ size = d_node->getConst<internal::ProjectOp>().getIndices().size();
break;
+ }
default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k);
}
return size;
break;
}
-
case TUPLE_PROJECT:
+ case TABLE_AGGREGATE:
+ case TABLE_GROUP:
+ case TABLE_JOIN:
+ case TABLE_PROJECT:
{
const std::vector<uint32_t>& projectionIndices =
- d_node->getConst<internal::TupleProjectOp>().getIndices();
+ d_node->getConst<internal::ProjectOp>().getIndices();
t = d_solver->mkRationalValHelper(projectionIndices[index]);
break;
}
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)
{
#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"
}
case kind::TUPLE_PROJECT:
{
- TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
if (op.getIndices().empty())
{
// e.g. (tuple.project tuple)
}
case kind::TABLE_PROJECT:
{
- TableProjectOp op = n.getOperator().getConst<TableProjectOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
if (op.getIndices().empty())
{
// e.g. (table.project A)
}
case kind::TABLE_AGGREGATE:
{
- TableAggregateOp op = n.getOperator().getConst<TableAggregateOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
if (op.getIndices().empty())
{
// e.g. (table.project function initial_value bag)
}
case kind::TABLE_JOIN:
{
- TableJoinOp op = n.getOperator().getConst<TableJoinOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
if (op.getIndices().empty())
{
// e.g. (table.join A B)
}
case kind::TABLE_GROUP:
{
- TableGroupOp op = n.getOperator().getConst<TableGroupOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
if (op.getIndices().empty())
{
// e.g. (table.group A)
#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"
TypeNode elementType = function.getType().getArgTypes()[0];
Node initialValue = node[1];
Node A = node[2];
- const std::vector<uint32_t>& indices =
- node.getOperator().getConst<TableAggregateOp>().getIndices();
+ ProjectOp op = node.getOperator().getConst<ProjectOp>();
- 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<FirstIndexVarAttribute>(
#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"
}
std::vector<uint32_t> indices =
- n.getOperator().getConst<TableGroupOp>().getIndices();
+ n.getOperator().getConst<ProjectOp>().getIndices();
std::map<Node, Rational> elements = BagsUtils::getBagElements(A);
Trace("bags-group") << "elements: " << elements << std::endl;
std::map<Node, Rational> elements;
std::vector<uint32_t> indices =
- n.getOperator().getConst<TableProjectOp>().getIndices();
+ n.getOperator().getConst<ProjectOp>().getIndices();
for (const auto& [a, countA] : elementsA)
{
{
Assert(n.getKind() == kind::TABLE_JOIN && n.hasOperator()
&& n.getOperator().getKind() == kind::TABLE_JOIN_OP);
- TableJoinOp op = n.getOperator().getConst<TableJoinOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
const std::vector<uint32_t>& indices = op.getIndices();
size_t joinSize = indices.size() / 2;
std::vector<uint32_t> indices1(joinSize), indices2(joinSize);
#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"
std::vector<Node> aElements = TupleUtils::getTupleElements(e1);
std::vector<Node> bElements = TupleUtils::getTupleElements(e2);
const std::vector<uint32_t>& indices =
- n.getOperator().getConst<TableJoinOp>().getIndices();
+ n.getOperator().getConst<ProjectOp>().getIndices();
InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_UP);
Node multiply = d_nm->mkNode(MULT, countA, countB);
Node multiplicityConstraint = count.eqNode(multiply);
const std::vector<uint32_t>& indices =
- n.getOperator().getConst<TableJoinOp>().getIndices();
+ n.getOperator().getConst<ProjectOp>().getIndices();
Node joinConstraints = d_true;
for (size_t i = 0; i < indices.size(); i += 2)
{
# 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"
+++ /dev/null
-/******************************************************************************
- * 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<uint32_t> indices)
- : ProjectOp(std::move(indices))
-{
-}
-
-TableAggregateOp::TableAggregateOp(std::vector<uint32_t> indices)
- : ProjectOp(std::move(indices))
-{
-}
-
-TableJoinOp::TableJoinOp(std::vector<uint32_t> indices)
- : ProjectOp(std::move(indices))
-{
-}
-
-TableGroupOp::TableGroupOp(std::vector<uint32_t> indices)
- : ProjectOp(std::move(indices))
-{
-}
-
-} // namespace cvc5::internal
+++ /dev/null
-/******************************************************************************
- * 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<uint32_t> 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<uint32_t> 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<uint32_t> 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<uint32_t> 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 */
#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"
{
Assert(n.getKind() == kind::TABLE_PROJECT && n.hasOperator()
&& n.getOperator().getKind() == kind::TABLE_PROJECT_OP);
- TableProjectOp op = n.getOperator().getConst<TableProjectOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
const std::vector<uint32_t>& indices = op.getIndices();
TypeNode bagType = n[0].getType(check);
if (check)
{
Assert(n.getKind() == kind::TABLE_AGGREGATE && n.hasOperator()
&& n.getOperator().getKind() == kind::TABLE_AGGREGATE_OP);
- TableAggregateOp op = n.getOperator().getConst<TableAggregateOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
const std::vector<uint32_t>& indices = op.getIndices();
TypeNode functionType = n[0].getType(check);
{
Assert(n.getKind() == kind::TABLE_JOIN && n.hasOperator()
&& n.getOperator().getKind() == kind::TABLE_JOIN_OP);
- TableJoinOp op = n.getOperator().getConst<TableJoinOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
const std::vector<uint32_t>& indices = op.getIndices();
Node A = n[0];
Node B = n[1];
{
Assert(n.getKind() == kind::TABLE_GROUP && n.hasOperator()
&& n.getOperator().getKind() == kind::TABLE_GROUP_OP);
- TableGroupOp op = n.getOperator().getConst<TableGroupOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
const std::vector<uint32_t>& indices = op.getIndices();
TypeNode bagType = n[0].getType(check);
#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"
Trace("dt-rewrite-project") << "Rewrite project: " << in << std::endl;
- TupleProjectOp op = in.getOperator().getConst<TupleProjectOp>();
+ ProjectOp op = in.getOperator().getConst<ProjectOp>();
std::vector<uint32_t> indices = op.getIndices();
Node tuple = in[0];
Node ret = TupleUtils::getTupleProjection(indices, tuple);
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"
--- /dev/null
+/******************************************************************************
+ * 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 <iostream>
+
+#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<uint32_t> indices)
+ : d_indices(std::move(indices))
+{
+}
+
+const std::vector<uint32_t>& ProjectOp::getIndices() const { return d_indices; }
+
+bool ProjectOp::operator==(const ProjectOp& op) const
+{
+ return d_indices == op.d_indices;
+}
+
+} // namespace cvc5::internal
--- /dev/null
+/******************************************************************************
+ * 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 <ostream>
+#include <vector>
+
+namespace cvc5::internal {
+
+class TypeNode;
+
+/**
+ * class for projection operators
+ */
+class ProjectOp
+{
+ public:
+ explicit ProjectOp(std::vector<uint32_t> indices);
+ ProjectOp(const ProjectOp& op) = default;
+
+ /** return the indices of the projection */
+ const std::vector<uint32_t>& getIndices() const;
+
+ bool operator==(const ProjectOp& op) const;
+
+ private:
+ std::vector<uint32_t> 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 */
#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"
{
Assert(n.getKind() == kind::TUPLE_PROJECT && n.hasOperator()
&& n.getOperator().getKind() == kind::TUPLE_PROJECT_OP);
- TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
const std::vector<uint32_t>& indices = op.getIndices();
if (check)
{
+++ /dev/null
-/******************************************************************************
- * 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 <iostream>
-
-#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<uint32_t> indices)
- : d_indices(std::move(indices))
-{
-}
-
-const std::vector<uint32_t>& ProjectOp::getIndices() const { return d_indices; }
-
-bool ProjectOp::operator==(const ProjectOp& op) const
-{
- return d_indices == op.d_indices;
-}
-
-TupleProjectOp::TupleProjectOp(std::vector<uint32_t> indices)
- : ProjectOp(std::move(indices))
-{
-}
-
-} // namespace cvc5::internal
+++ /dev/null
-/******************************************************************************
- * 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 <ostream>
-#include <vector>
-
-namespace cvc5::internal {
-
-class TypeNode;
-
-/**
- * base class for TupleProjectOp, TupleProjectOp
- */
-class ProjectOp
-{
- public:
- explicit ProjectOp(std::vector<uint32_t> indices);
- ProjectOp(const ProjectOp& op) = default;
-
- /** return the indices of the projection */
- const std::vector<uint32_t>& getIndices() const;
-
- bool operator==(const ProjectOp& op) const;
-
- private:
- std::vector<uint32_t> 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<uint32_t> 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 */
projects / cvc5.git / commitdiff