From: mudathirmahgoub Date: Wed, 3 Mar 2021 08:16:32 +0000 (-0600) Subject: Add tuple projection operator (#5904) X-Git-Tag: cvc5-1.0.0~2166 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c4709cb01356dd73fdd767d19af85b36ffd566c4;p=cvc5.git Add tuple projection operator (#5904) This PR adds tuple projection operator to the theory of data types. It Also adds helper functions for selecting elements from a tuple. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 02cb26760..2b04bb40d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -584,6 +584,8 @@ libcvc4_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/type_enumerator.cpp theory/datatypes/type_enumerator.h theory/decision_manager.cpp diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e1c64b750..c3490938b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -232,6 +232,7 @@ const static std::unordered_map s_kinds{ {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE}, {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE}, {DT_SIZE, CVC4::Kind::DT_SIZE}, + {TUPLE_PROJECT, CVC4::Kind::TUPLE_PROJECT}, /* Separation Logic ---------------------------------------------------- */ {SEP_NIL, CVC4::Kind::SEP_NIL}, {SEP_EMP, CVC4::Kind::SEP_EMP}, @@ -538,6 +539,7 @@ const static std::unordered_map {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE}, {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE}, {CVC4::Kind::DT_SIZE, DT_SIZE}, + {CVC4::Kind::TUPLE_PROJECT, TUPLE_PROJECT}, /* Separation Logic ------------------------------------------------ */ {CVC4::Kind::SEP_NIL, SEP_NIL}, {CVC4::Kind::SEP_EMP, SEP_EMP}, @@ -4749,6 +4751,35 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const CVC4_API_SOLVER_TRY_CATCH_END; } +Op Solver::mkOp(Kind kind, const std::vector& args) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_KIND_CHECK(kind); + + Op res; + switch (kind) + { + case TUPLE_PROJECT: + { + res = Op(this, + kind, + *mkValHelper(CVC4::TupleProjectOp(args)) + .d_node); + } + break; + default: + { + std::string message = "operator kind with " + std::to_string(args.size()) + + " uint32_t arguments"; + CVC4_API_KIND_CHECK_EXPECTED(false, kind) << message; + } + } + Assert(!res.isNull()); + return res; + + CVC4_API_SOLVER_TRY_CATCH_END; +} + /* Non-SMT-LIB commands */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 60127d18b..d503a317e 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2620,6 +2620,14 @@ class CVC4_PUBLIC Solver */ Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const; + /** + * Create operator of Kind: + * - TUPLE_PROJECT + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + */ + Op mkOp(Kind kind, const std::vector& args) const; + /* .................................................................... */ /* Create Constants */ /* .................................................................... */ diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 3fb16abcb..b2413486e 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1715,6 +1715,22 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ DT_SIZE, + /** + * Operator for tuple projection indices + * Parameters: 1 + * -[1]: The tuple projection indices + * Create with: + * mkOp(Kind TUPLE_PROJECT, std::vector param) + * + * constructs a new tuple from an existing one using the elements at the + * given indices + * Parameters: 1 + * -[1]: a term of tuple sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector& children) + */ + TUPLE_PROJECT, #if 0 /* datatypes height bound */ DT_HEIGHT_BOUND, diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 11ccb4935..7ef7edbbe 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1549,6 +1549,12 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] } expr = SOLVER->mkTuple(sorts, terms); } + | LPAREN_TOK TUPLE_PROJECT_TOK term[expr,expr2] RPAREN_TOK + { + std::vector indices; + api::Op op = SOLVER->mkOp(api::TUPLE_PROJECT, indices); + expr = SOLVER->mkTerm(op, expr); + } | /* an atomic term (a term with no subterms) */ termAtomic[atomTerm] { expr = atomTerm; } ; @@ -1672,6 +1678,19 @@ identifier[CVC4::ParseOp& p] // put m in expr so that the caller can deal with this case p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m)); } + | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals] + { + // we adopt a special syntax (_ tuple_project i_1 ... i_n) where + // i_1, ..., i_n are numerals + p.d_kind = api::TUPLE_PROJECT; + std::vector indices(numerals.size()); + for(size_t i = 0; i < numerals.size(); ++i) + { + // convert uint64_t to uint32_t + indices[i] = numerals[i]; + } + p.d_op = SOLVER->mkOp(api::TUPLE_PROJECT, indices); + } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals); @@ -2279,6 +2298,7 @@ EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp'; CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple'; TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel'; +TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project'; HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->'; HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 4d75a982b..049bf8b4d 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1097,6 +1097,12 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) Debug("parser") << "applyParseOp: return selector " << ret << std::endl; return ret; } + else if (p.d_kind == api::TUPLE_PROJECT) + { + api::Term ret = d_solver->mkTerm(p.d_op, args[0]); + Debug("parser") << "applyParseOp: return projection " << ret << std::endl; + return ret; + } else if (p.d_kind != api::NULL_EXPR) { // it should not have an expression or type specified at this point diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index fd9d20e4b..8c122f26d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -903,6 +903,21 @@ void Smt2Printer::toStream(std::ostream& out, } break; } + case kind::TUPLE_PROJECT: + { + TupleProjectOp op = n.getOperator().getConst(); + if (op.getIndices().empty()) + { + // e.g. (tuple_project tuple) + out << "project " << n[0] << ")"; + } + else + { + // e.g. ((_ tuple_project 2 4 4) tuple) + out << "(_ tuple_project" << op << ") " << n[0] << ")"; + } + return; + } case kind::CONSTRUCTOR_TYPE: { out << n[n.getNumChildren()-1]; diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h index a53000651..36bd3f5df 100644 --- a/src/theory/bags/make_bag_op.h +++ b/src/theory/bags/make_bag_op.h @@ -34,7 +34,7 @@ class TypeNode; class MakeBagOp { public: - MakeBagOp(const TypeNode& elementType); + explicit MakeBagOp(const TypeNode& elementType); MakeBagOp(const MakeBagOp& op); /** return the type of the current object */ @@ -43,7 +43,6 @@ class MakeBagOp bool operator==(const MakeBagOp& op) const; private: - MakeBagOp(); /** a pointer to the type of the bag element */ std::unique_ptr d_type; }; /* class MakeBagOp */ diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 5334e76df..4bf745f16 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -224,6 +224,41 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) << "Rewrite match: " << in << " ... " << ret << std::endl; return RewriteResponse(REWRITE_AGAIN_FULL, ret); } + else if (kind == TUPLE_PROJECT) + { + // returns a tuple that represents + // (mkTuple ((_ tupSel i_1) t) ... ((_ tupSel i_n) t)) + // where each i_j is less than the length of t + + Trace("dt-rewrite-project") << "Rewrite project: " << in << std::endl; + TupleProjectOp op = in.getOperator().getConst(); + std::vector indices = op.getIndices(); + Node tuple = in[0]; + std::vector tupleTypes = tuple.getType().getTupleTypes(); + std::vector types; + std::vector elements; + for (uint32_t index : indices) + { + TypeNode type = tupleTypes[index]; + types.push_back(type); + } + TypeNode projectType = nm->mkTupleType(types); + const DType& dt = projectType.getDType(); + elements.push_back(dt[0].getConstructor()); + const DType& tupleDType = tuple.getType().getDType(); + const DTypeConstructor& constructor = tupleDType[0]; + for (uint32_t index : indices) + { + Node selector = constructor[index].getSelector(); + Node element = nm->mkNode(kind::APPLY_SELECTOR, selector, tuple); + elements.push_back(element); + } + Node ret = nm->mkNode(kind::APPLY_CONSTRUCTOR, elements); + + Trace("dt-rewrite-project") + << "Rewrite project: " << in << " ... " << ret << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, ret); + } if (kind == kind::EQUAL) { diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index ef8dd47f1..f3e5be5c7 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -138,4 +138,17 @@ typerule MATCH ::CVC4::theory::datatypes::MatchTypeRule typerule MATCH_CASE ::CVC4::theory::datatypes::MatchCaseTypeRule typerule MATCH_BIND_CASE ::CVC4::theory::datatypes::MatchBindCaseTypeRule + +constant TUPLE_PROJECT_OP \ + ::CVC4::TupleProjectOp \ + ::CVC4::TupleProjectOpHashFunction \ + "theory/datatypes/tuple_project_op.h" \ + "operator for TUPLE_PROJECT; payload is an instance of the CVC4::TupleProjectOp class" + +parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \ + "projects a tuple from an existing tuple using indices passed in TupleProjectOp" + +typerule TUPLE_PROJECT_OP "SimpleTypeRule" +typerule TUPLE_PROJECT ::CVC4::theory::datatypes::TupleProjectTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 73aef4dd7..d7fb984e0 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -572,6 +572,60 @@ class MatchBindCaseTypeRule } }; /* class MatchBindCaseTypeRule */ +class TupleProjectTypeRule +{ + public: + static TypeNode 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(); + const std::vector& indices = op.getIndices(); + if (check) + { + if (n.getNumChildren() != 1) + { + std::stringstream ss; + ss << "operands in term " << n << " are " << n.getNumChildren() + << ", but TUPLE_PROJECT expects 1 operand."; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + TypeNode tupleType = n[0].getType(check); + if (!tupleType.isTuple()) + { + std::stringstream ss; + ss << "TUPLE_PROJECT expects a tuple for " << n[0] << ". Found" << tupleType; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + + // make sure all indices are less than the length of the tuple type + DType dType = tupleType.getDType(); + DTypeConstructor constructor = dType[0]; + size_t numArgs = constructor.getNumArgs(); + for (uint32_t index : indices) + { + std::stringstream ss; + if (index >= numArgs) + { + ss << "Project index " << index << " in term " << n + << " is >= " << numArgs << " which is the length of tuple " << n[0] + << std::endl; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + } + TypeNode tupleType = n[0].getType(check); + std::vector types; + DType dType = tupleType.getDType(); + DTypeConstructor constructor = dType[0]; + for (uint32_t index : indices) + { + types.push_back(constructor.getArgType(index)); + } + return nm->mkTupleType(types); + } +}; /* class TupleProjectTypeRule */ + } /* CVC4::theory::datatypes namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/datatypes/tuple_project_op.cpp b/src/theory/datatypes/tuple_project_op.cpp new file mode 100644 index 000000000..d09d43317 --- /dev/null +++ b/src/theory/datatypes/tuple_project_op.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file tuple_project_op.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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.\endverbatim + **/ + +#include "tuple_project_op.h" + +#include + +#include "expr/type_node.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const TupleProjectOp& op) +{ + for (const uint32_t& index : op.getIndices()) + { + out << " " << index; + } + return out; +} + +size_t TupleProjectOpHashFunction::operator()(const TupleProjectOp& 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; +} + +TupleProjectOp::TupleProjectOp(std::vector indices) + : d_indices(std::move(indices)) +{ +} + +const std::vector& TupleProjectOp::getIndices() const { return d_indices; } + +bool TupleProjectOp::operator==(const TupleProjectOp& op) const +{ + return d_indices == op.d_indices; +} + +} // namespace CVC4 diff --git a/src/theory/datatypes/tuple_project_op.h b/src/theory/datatypes/tuple_project_op.h new file mode 100644 index 000000000..045f05cc2 --- /dev/null +++ b/src/theory/datatypes/tuple_project_op.h @@ -0,0 +1,58 @@ +/********************* */ +/*! \file tuple_project_op.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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.\endverbatim + ** + ** \brief a class for TupleProjectOp operator + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__PROJECT_OP_H +#define CVC4__PROJECT_OP_H + +#include +#include + +namespace CVC4 { + +class TypeNode; + +/** + * The class is an operator for kind project used to project elements in a tuple + * It stores the indices of projected elements + */ +class TupleProjectOp +{ + public: + explicit TupleProjectOp(std::vector indices); + TupleProjectOp(const TupleProjectOp& op) = default; + + /** return the indices of the projection */ + const std::vector& getIndices() const; + + bool operator==(const TupleProjectOp& op) const; + + private: + std::vector d_indices; +}; /* class TupleProjectOp */ + +std::ostream& operator<<(std::ostream& out, const TupleProjectOp& op); + +/** + * Hash function for the TupleProjectOpHashFunction objects. + */ +struct CVC4_PUBLIC TupleProjectOpHashFunction +{ + size_t operator()(const TupleProjectOp& op) const; +}; /* struct TupleProjectOpHashFunction */ + +} // namespace CVC4 + +#endif /* CVC4__PROJECT_OP_H */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1a43b0335..8da7cfb05 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1476,6 +1476,7 @@ set(regress_1_tests regress1/datatypes/non-simple-rec.smt2 regress1/datatypes/non-simple-rec-mut-unsat.smt2 regress1/datatypes/non-simple-rec-param.smt2 + regress1/datatypes/tuple_projection.smt2 regress1/decision/bug374a.smtv1.smt2 regress1/decision/error3.smtv1.smt2 regress1/decision/quant-Arrays_Q1-noinfer.smt2 diff --git a/test/regress/regress1/datatypes/tuple_projection.smt2 b/test/regress/regress1/datatypes/tuple_projection.smt2 new file mode 100644 index 000000000..bdd9d5458 --- /dev/null +++ b/test/regress/regress1/datatypes/tuple_projection.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun t () (Tuple String String String String)) +(declare-fun u () (Tuple String String)) +(declare-fun v () Tuple) +(declare-fun x () String) +(assert (= t (mkTuple "a" "b" "c" "d"))) +(assert (= x ((_ tupSel 0) t))) +(assert (= u ((_ tuple_project 2 3) t))) +(assert (= v (tuple_project t))) +(check-sat) \ No newline at end of file diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 2e285fcc7..528d697ae 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -554,6 +554,10 @@ TEST_F(TestApiBlackSolver, mkOp) // mkOp(Kind kind, uint32_t arg1, uint32_t arg2) ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1, 1)); ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC4ApiException); + + // mkOp(Kind kind, std::vector args) + std::vector args = {1, 2, 2}; + ASSERT_NO_THROW(d_solver.mkOp(TUPLE_PROJECT, args)); } TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); } @@ -975,7 +979,8 @@ TEST_F(TestApiBlackSolver, defineSort) Sort arraySort1 = d_solver.mkArraySort(sortVar0, sortVar1); // Now create instantiations of the defined sorts ASSERT_NO_THROW(arraySort0.substitute(sortVar0, intSort)); - ASSERT_NO_THROW(arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort})); + ASSERT_NO_THROW( + arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort})); } TEST_F(TestApiBlackSolver, defineFun) @@ -2292,5 +2297,62 @@ TEST_F(TestApiBlackSolver, getSynthSolutions) ASSERT_THROW(slv.getSynthSolutions({x}), CVC4ApiException); } +TEST_F(TestApiBlackSolver, tupleProject) +{ + std::vector sorts = {d_solver.getBooleanSort(), + d_solver.getIntegerSort(), + d_solver.getStringSort(), + d_solver.mkSetSort(d_solver.getStringSort())}; + std::vector elements = { + d_solver.mkBoolean(true), + d_solver.mkInteger(3), + d_solver.mkString("C"), + d_solver.mkTerm(SINGLETON, d_solver.mkString("Z"))}; + + Term tuple = d_solver.mkTuple(sorts, elements); + + std::vector indices1 = {}; + std::vector indices2 = {0}; + std::vector indices3 = {0, 1}; + std::vector indices4 = {0, 0, 2, 2, 3, 3, 0}; + std::vector indices5 = {4}; + std::vector indices6 = {0, 4}; + + ASSERT_NO_THROW( + d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices1), tuple)); + ASSERT_NO_THROW( + d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices2), tuple)); + ASSERT_NO_THROW( + d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices3), tuple)); + ASSERT_NO_THROW( + d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), tuple)); + + ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), tuple), + CVC4ApiException); + ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), tuple), + CVC4ApiException); + + std::vector indices = {0, 3, 2, 0, 1, 2}; + + Op op = d_solver.mkOp(TUPLE_PROJECT, indices); + Term projection = d_solver.mkTerm(op, tuple); + + Datatype datatype = tuple.getSort().getDatatype(); + DatatypeConstructor constructor = datatype[0]; + + for (size_t i = 0; i < indices.size(); i++) + { + Term selectorTerm = constructor[indices[i]].getSelectorTerm(); + Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, selectorTerm, tuple); + Term simplifiedTerm = d_solver.simplify(selectedTerm); + ASSERT_EQ(elements[indices[i]], simplifiedTerm); + } + + ASSERT_EQ( + "((_ tuple_project 0 3 2 0 1 2) (mkTuple true 3 \"C\" (singleton " + "\"Z\")))", + projection.toString()); +} + } // namespace test } // namespace CVC4