This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.
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
{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},
{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},
CVC4_API_SOLVER_TRY_CATCH_END;
}
+Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& 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>(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 */
/* -------------------------------------------------------------------------- */
*/
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<uint32_t>& args) const;
+
/* .................................................................... */
/* Create Constants */
/* .................................................................... */
* mkTerm(Kind kind, const std::vector<Term>& children)
*/
DT_SIZE,
+ /**
+ * Operator for tuple projection indices
+ * Parameters: 1
+ * -[1]: The tuple projection indices
+ * Create with:
+ * mkOp(Kind TUPLE_PROJECT, std::vector<uint32_t> 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<Term>& children)
+ */
+ TUPLE_PROJECT,
#if 0
/* datatypes height bound */
DT_HEIGHT_BOUND,
}
expr = SOLVER->mkTuple(sorts, terms);
}
+ | LPAREN_TOK TUPLE_PROJECT_TOK term[expr,expr2] RPAREN_TOK
+ {
+ std::vector<uint32_t> 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; }
;
// 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<uint32_t> 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);
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';
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
}
break;
}
+ case kind::TUPLE_PROJECT:
+ {
+ TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
+ 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];
class MakeBagOp
{
public:
- MakeBagOp(const TypeNode& elementType);
+ explicit MakeBagOp(const TypeNode& elementType);
MakeBagOp(const MakeBagOp& op);
/** return the type of the current object */
bool operator==(const MakeBagOp& op) const;
private:
- MakeBagOp();
/** a pointer to the type of the bag element */
std::unique_ptr<TypeNode> d_type;
}; /* class MakeBagOp */
<< "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<TupleProjectOp>();
+ std::vector<uint32_t> indices = op.getIndices();
+ Node tuple = in[0];
+ std::vector<TypeNode> tupleTypes = tuple.getType().getTupleTypes();
+ std::vector<TypeNode> types;
+ std::vector<Node> 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)
{
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<RBuiltinOperator>"
+typerule TUPLE_PROJECT ::CVC4::theory::datatypes::TupleProjectTypeRule
+
endtheory
}
}; /* 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<TupleProjectOp>();
+ const std::vector<uint32_t>& 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<TypeNode> 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 */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+#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<uint32_t> indices)
+ : d_indices(std::move(indices))
+{
+}
+
+const std::vector<uint32_t>& TupleProjectOp::getIndices() const { return d_indices; }
+
+bool TupleProjectOp::operator==(const TupleProjectOp& op) const
+{
+ return d_indices == op.d_indices;
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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 <ostream>
+#include <vector>
+
+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<uint32_t> indices);
+ TupleProjectOp(const TupleProjectOp& op) = default;
+
+ /** return the indices of the projection */
+ const std::vector<uint32_t>& getIndices() const;
+
+ bool operator==(const TupleProjectOp& op) const;
+
+ private:
+ std::vector<uint32_t> 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 */
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
--- /dev/null
+(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
// 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<uint32_t> args)
+ std::vector<uint32_t> args = {1, 2, 2};
+ ASSERT_NO_THROW(d_solver.mkOp(TUPLE_PROJECT, args));
}
TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
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)
ASSERT_THROW(slv.getSynthSolutions({x}), CVC4ApiException);
}
+TEST_F(TestApiBlackSolver, tupleProject)
+{
+ std::vector<Sort> sorts = {d_solver.getBooleanSort(),
+ d_solver.getIntegerSort(),
+ d_solver.getStringSort(),
+ d_solver.mkSetSort(d_solver.getStringSort())};
+ std::vector<Term> 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<uint32_t> indices1 = {};
+ std::vector<uint32_t> indices2 = {0};
+ std::vector<uint32_t> indices3 = {0, 1};
+ std::vector<uint32_t> indices4 = {0, 0, 2, 2, 3, 3, 0};
+ std::vector<uint32_t> indices5 = {4};
+ std::vector<uint32_t> 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<uint32_t> 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
projects / cvc5.git / commitdiff