KIND_ENUM(RELATION_IDEN, internal::Kind::RELATION_IDEN),
KIND_ENUM(RELATION_GROUP, internal::Kind::RELATION_GROUP),
KIND_ENUM(RELATION_AGGREGATE, internal::Kind::RELATION_AGGREGATE),
+ KIND_ENUM(RELATION_PROJECT, internal::Kind::RELATION_PROJECT),
/* Bags ------------------------------------------------------------- */
KIND_ENUM(BAG_UNION_MAX, internal::Kind::BAG_UNION_MAX),
KIND_ENUM(BAG_UNION_DISJOINT, internal::Kind::BAG_UNION_DISJOINT),
{internal::Kind::RELATION_GROUP, RELATION_GROUP},
{internal::Kind::RELATION_AGGREGATE_OP, RELATION_AGGREGATE},
{internal::Kind::RELATION_AGGREGATE, RELATION_AGGREGATE},
+ {internal::Kind::RELATION_PROJECT_OP, RELATION_PROJECT},
+ {internal::Kind::RELATION_PROJECT, RELATION_PROJECT},
/* Bags ------------------------------------------------------------ */
{internal::Kind::BAG_UNION_MAX, BAG_UNION_MAX},
{internal::Kind::BAG_UNION_DISJOINT, BAG_UNION_DISJOINT},
{TUPLE_PROJECT, internal::Kind::TUPLE_PROJECT_OP},
{RELATION_AGGREGATE, internal::Kind::RELATION_AGGREGATE_OP},
{RELATION_GROUP, internal::Kind::RELATION_GROUP_OP},
+ {RELATION_PROJECT, internal::Kind::RELATION_PROJECT_OP},
{TABLE_PROJECT, internal::Kind::TABLE_PROJECT_OP},
{TABLE_AGGREGATE, internal::Kind::TABLE_AGGREGATE_OP},
{TABLE_JOIN, internal::Kind::TABLE_JOIN_OP},
case TUPLE_PROJECT:
case RELATION_AGGREGATE:
case RELATION_GROUP:
+ case RELATION_PROJECT:
case TABLE_AGGREGATE:
case TABLE_GROUP:
case TABLE_JOIN:
case TUPLE_PROJECT:
case RELATION_AGGREGATE:
case RELATION_GROUP:
+ case RELATION_PROJECT:
case TABLE_AGGREGATE:
case TABLE_GROUP:
case TABLE_JOIN:
case TUPLE_PROJECT:
case RELATION_AGGREGATE:
case RELATION_GROUP:
+ case RELATION_PROJECT:
case TABLE_AGGREGATE:
case TABLE_GROUP:
case TABLE_JOIN:
* \endrst
*/
RELATION_AGGREGATE,
+ /**
+ * Relation projection operator extends tuple projection operator to sets.
+ *
+ * - Arity: ``1``
+ * - ``1:`` Term of relation Sort
+ *
+ * - Indices: ``n``
+ * - ``1..n:`` Indices of the projection
+ *
+ * - Create Term of this Kind with:
+ * - Solver::mkTerm(const Op&, const std::vector<Term>&) const
+ *
+ * - Create Op of this kind with:
+ * - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
+ */
+ RELATION_PROJECT,
/* Bags ------------------------------------------------------------------ */
cvc5::Op op = SOLVER->mkOp(cvc5::RELATION_AGGREGATE, indices);
expr = SOLVER->mkTerm(op, {expr});
}
+ | LPAREN_TOK RELATION_PROJECT_TOK term[expr,expr2] RPAREN_TOK
+ {
+ std::vector<uint32_t> indices;
+ cvc5::Op op = SOLVER->mkOp(cvc5::RELATION_PROJECT, indices);
+ expr = SOLVER->mkTerm(op, {expr});
+ }
| /* an atomic term (a term with no subterms) */
termAtomic[atomTerm] { expr = atomTerm; }
;
p.d_kind = cvc5::RELATION_AGGREGATE;
p.d_op = SOLVER->mkOp(cvc5::RELATION_AGGREGATE, numerals);
}
+ | RELATION_PROJECT_TOK nonemptyNumeralList[numerals]
+ {
+ // we adopt a special syntax (_ rel.project i_1 ... i_n) where
+ // i_1, ..., i_n are numerals
+ p.d_kind = cvc5::RELATION_PROJECT;
+ p.d_op = SOLVER->mkOp(cvc5::RELATION_PROJECT, numerals);
+ }
| functionName[opName, CHECK_NONE] nonemptyNumeralList[numerals]
{
cvc5::Kind k = PARSER_STATE->getIndexedOpKind(opName);
TABLE_GROUP_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_BAGS) }? 'table.group';
RELATION_GROUP_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_SETS) }? 'rel.group';
RELATION_AGGREGATE_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_SETS) }? 'rel.aggr';
+RELATION_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_SETS) }? 'rel.project';
FMF_CARD_TOK: { !PARSER_STATE->strictModeEnabled() && PARSER_STATE->hasCardinalityConstraints() }? 'fmf.card';
HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
void Smt2::addCoreSymbols()
{
defineType("Bool", d_solver->getBooleanSort(), true);
- defineType("Table", d_solver->mkBagSort(d_solver->mkTupleSort({})), true);
+ Sort tupleSort = d_solver->mkTupleSort({});
+ defineType("Relation", d_solver->mkSetSort(tupleSort), true);
+ defineType("Table", d_solver->mkBagSort(tupleSort), true);
defineVar("true", d_solver->mkTrue(), true);
defineVar("false", d_solver->mkFalse(), true);
addOperator(cvc5::AND, "and");
else if (p.d_kind == cvc5::TUPLE_PROJECT || p.d_kind == cvc5::TABLE_PROJECT
|| p.d_kind == cvc5::TABLE_AGGREGATE || p.d_kind == cvc5::TABLE_JOIN
|| p.d_kind == cvc5::TABLE_GROUP || p.d_kind == cvc5::RELATION_GROUP
- || p.d_kind == cvc5::RELATION_AGGREGATE)
+ || p.d_kind == cvc5::RELATION_AGGREGATE
+ || p.d_kind == cvc5::RELATION_PROJECT)
{
cvc5::Term ret = d_solver->mkTerm(p.d_op, args);
Trace("parser") << "applyParseOp: return projection " << ret << std::endl;
}
return;
}
+ case kind::RELATION_PROJECT:
+ {
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
+ if (op.getIndices().empty())
+ {
+ // e.g. (rel.project A)
+ out << "rel.project " << n[0] << ")";
+ }
+ else
+ {
+ // e.g. ((_ rel.project 2 4 4) A)
+ out << "(_ rel.project" << op << ") " << n[0] << ")";
+ }
+ return;
+ }
case kind::CONSTRUCTOR_TYPE:
{
out << n[n.getNumChildren()-1];
case kind::RELATION_JOIN_IMAGE: return "rel.join_image";
case kind::RELATION_GROUP: return "rel.group";
case kind::RELATION_AGGREGATE: return "rel.aggr";
+ case kind::RELATION_PROJECT: return "rel.project";
// bag theory
case kind::BAG_TYPE: return "Bag";
return map;
}
+Node BagReduction::reduceProjectOperator(Node n)
+{
+ Assert(n.getKind() == TABLE_PROJECT);
+ NodeManager* nm = NodeManager::currentNM();
+ Node A = n[0];
+ TypeNode elementType = A.getType().getBagElementType();
+ ProjectOp projectOp = n.getOperator().getConst<ProjectOp>();
+ Node op = nm->mkConst(TUPLE_PROJECT_OP, projectOp);
+ Node t = nm->mkBoundVar("t", elementType);
+ Node projection = nm->mkNode(TUPLE_PROJECT, op, t);
+ Node lambda = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, t), projection);
+ Node setMap = nm->mkNode(BAG_MAP, lambda, A);
+ return setMap;
+}
+
} // namespace bags
} // namespace theory
} // namespace cvc5::internal
* ((_ table.group n1 ... nk) A))
*/
static Node reduceAggregateOperator(Node node);
+ /**
+ * @param n has the form ((table.project n1 ... nk) A) where A has type
+ * (Bag T)
+ * @return (bag.map (lambda ((t T)) ((_ tuple.project n1 ... nk) t)) A)
+ */
+ static Node reduceProjectOperator(Node n);
};
} // namespace bags
Node BagsUtils::evaluateTableProject(TNode n)
{
Assert(n.getKind() == TABLE_PROJECT);
- // Examples
- // --------
- // - ((_ table.project 1) (bag (tuple true "a") 4)) = (bag (tuple "a") 4)
- // - (table.project (bag.union_disjoint
- // (bag (tuple "a") 4)
- // (bag (tuple "b") 3))) = (bag tuple 7)
-
- Node A = n[0];
-
- std::map<Node, Rational> elementsA = BagsUtils::getBagElements(A);
-
- std::map<Node, Rational> elements;
- std::vector<uint32_t> indices =
- n.getOperator().getConst<ProjectOp>().getIndices();
-
- for (const auto& [a, countA] : elementsA)
- {
- Node element = TupleUtils::getTupleProjection(indices, a);
- // multiple elements could be projected to the same tuple.
- // Zero is the default value for Rational values.
- elements[element] += countA;
- }
-
- Node ret = BagsUtils::constructConstantBagFromElements(n.getType(), elements);
+ Node bagMap = BagReduction::reduceProjectOperator(n);
+ Node ret = evaluateBagMap(bagMap);
return ret;
}
Trace("bags::ppr") << "reduce(" << atom << ") = " << ret << std::endl;
return TrustNode::mkTrustRewrite(atom, ret, nullptr);
}
+ case kind::TABLE_PROJECT:
+ {
+ Node ret = BagReduction::reduceProjectOperator(atom);
+ Trace("bags::ppr") << "reduce(" << atom << ") = " << ret << std::endl;
+ return TrustNode::mkTrustRewrite(atom, ret, nullptr);
+ }
default: return TrustNode::null();
}
}
case BAG_TO_SET:
case BAG_IS_SINGLETON:
case BAG_PARTITION:
- case TABLE_PROJECT:
{
std::stringstream ss;
ss << "Term of kind " << n.getKind() << " is not supported yet";
/**
* Table project is indexed by a list of indices (n_1, ..., n_m). It ensures
* that the argument is a bag of tuples whose arity k is greater than each n_i
- * for i = 1, ..., m. If the argument is of type (Bag (Tuple T_1 ... T_k)), then
- * the returned type is (Bag (Tuple T_{n_1} ... T_{n_m})).
+ * for i = 1, ..., m. If the argument is of type (Table T_1 ... T_k), then
+ * the returned type is (Table T_{n_1} ... T_{n_m}).
*/
struct TableProjectTypeRule
{
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
-}; /* struct BagFoldTypeRule */
+}; /* struct TableProjectTypeRule */
/**
* Table aggregate operator is indexed by a list of indices (n_1, ..., n_k).
parameterized RELATION_AGGREGATE RELATION_AGGREGATE_OP 3 "relation aggregate"
+# rel.project operator extends datatypes tuple_project operator to a set of tuples
+constant RELATION_PROJECT_OP \
+ class \
+ ProjectOp+ \
+ ::cvc5::internal::ProjectOpHashFunction \
+ "theory/datatypes/project_op.h" \
+ "operator for RELATION_PROJECT; payload is an instance of the cvc5::internal::ProjectOp class"
+
+parameterized RELATION_PROJECT RELATION_PROJECT_OP 1 "relation projection"
+
operator RELATION_JOIN 2 "relation join"
operator RELATION_PRODUCT 2 "relation cartesian product"
operator RELATION_TRANSPOSE 1 "relation transpose"
typerule RELATION_JOIN ::cvc5::internal::theory::sets::RelBinaryOperatorTypeRule
typerule RELATION_PRODUCT ::cvc5::internal::theory::sets::RelBinaryOperatorTypeRule
-typerule RELATION_TRANSPOSE ::cvc5::internal::theory::sets::RelTransposeTypeRule
+typerule RELATION_TRANSPOSE ::cvc5::internal::theory::sets::RelTransposeTypeRule
typerule RELATION_TCLOSURE ::cvc5::internal::theory::sets::RelTransClosureTypeRule
-typerule RELATION_JOIN_IMAGE ::cvc5::internal::theory::sets::JoinImageTypeRule
+typerule RELATION_JOIN_IMAGE ::cvc5::internal::theory::sets::JoinImageTypeRule
typerule RELATION_IDEN ::cvc5::internal::theory::sets::RelIdenTypeRule
typerule RELATION_GROUP_OP "SimpleTypeRule<RBuiltinOperator>"
typerule RELATION_GROUP ::cvc5::internal::theory::sets::RelationGroupTypeRule
typerule RELATION_AGGREGATE_OP "SimpleTypeRule<RBuiltinOperator>"
typerule RELATION_AGGREGATE ::cvc5::internal::theory::sets::RelationAggregateTypeRule
+typerule RELATION_PROJECT_OP "SimpleTypeRule<RBuiltinOperator>"
+typerule RELATION_PROJECT ::cvc5::internal::theory::sets::RelationProjectTypeRule
construle SET_UNION ::cvc5::internal::theory::sets::SetsBinaryOperatorTypeRule
construle SET_SINGLETON ::cvc5::internal::theory::sets::SingletonTypeRule
return map;
}
+Node SetReduction::reduceProjectOperator(Node n)
+{
+ Assert(n.getKind() == RELATION_PROJECT);
+ NodeManager* nm = NodeManager::currentNM();
+ Node A = n[0];
+ TypeNode elementType = A.getType().getSetElementType();
+ ProjectOp projectOp = n.getOperator().getConst<ProjectOp>();
+ Node op = nm->mkConst(TUPLE_PROJECT_OP, projectOp);
+ Node t = nm->mkBoundVar("t", elementType);
+ Node projection = nm->mkNode(TUPLE_PROJECT, op, t);
+ Node lambda = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, t), projection);
+ Node setMap = nm->mkNode(SET_MAP, lambda, A);
+ return setMap;
+}
+
} // namespace sets
} // namespace theory
} // namespace cvc5::internal
* ((_ rel.group n1 ... nk) A))
*/
static Node reduceAggregateOperator(Node node);
+ /**
+ * @param n has the form ((rel.project n1 ... nk) A) where A has type (Set T)
+ * @return (set.map (lambda ((t T)) ((_ tuple.project n1 ... nk) t)) A)
+ */
+ static Node reduceProjectOperator(Node n);
};
} // namespace sets
d_im.lemma(andNode, InferenceId::BAGS_FOLD);
return TrustNode::mkTrustRewrite(n, ret, nullptr);
}
- if (nk == TABLE_AGGREGATE)
+ if (nk == RELATION_AGGREGATE)
{
Node ret = SetReduction::reduceAggregateOperator(n);
return TrustNode::mkTrustRewrite(ret, ret, nullptr);
}
+ if (nk == RELATION_PROJECT)
+ {
+ Node ret = SetReduction::reduceProjectOperator(n);
+ return TrustNode::mkTrustRewrite(ret, ret, nullptr);
+ }
return d_internal->ppRewrite(n, lems);
}
#include "theory/datatypes/tuple_utils.h"
#include "theory/sets/normal_form.h"
#include "theory/sets/rels_utils.h"
+#include "theory/sets/set_reduction.h"
#include "util/rational.h"
using namespace cvc5::internal::kind;
case RELATION_GROUP: return postRewriteGroup(node);
case RELATION_AGGREGATE: return postRewriteAggregate(node);
+ case RELATION_PROJECT: return postRewriteProject(node);
default: break;
}
return RewriteResponse(REWRITE_DONE, n);
}
+RewriteResponse TheorySetsRewriter::postRewriteProject(TNode n)
+{
+ Assert(n.getKind() == RELATION_PROJECT);
+ Node ret = SetReduction::reduceProjectOperator(n);
+ if (ret != n)
+ {
+ return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+ }
+ return RewriteResponse(REWRITE_DONE, n);
+}
+
} // namespace sets
} // namespace theory
} // namespace cvc5::internal
* @return the aggregation result.
*/
RewriteResponse postRewriteAggregate(TNode n);
+ /**
+ * If A has type (Set T), then rewrite ((rel.project n1 ... nk) A) as
+ * (set.map (lambda ((t T)) ((_ tuple.project n1 ... nk) t)) A)
+ */
+ RewriteResponse postRewriteProject(TNode n);
}; /* class TheorySetsRewriter */
} // namespace sets
#include "theory/sets/theory_sets_type_rules.h"
-#include <climits>
#include <sstream>
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
#include "theory/sets/normal_form.h"
#include "util/cardinality.h"
#include "theory/datatypes/project_op.h"
if (!setType.isSet())
{
std::stringstream ss;
- ss << "RELATION_PROJECT operator expects a table. Found '" << n[2]
+ ss << "RELATION_AGGREGATE operator expects a set. Found '" << n[2]
<< "' of type '" << setType << "'.";
throw TypeCheckingExceptionPrivate(n, ss.str());
}
if (!tupleType.isTuple())
{
std::stringstream ss;
- ss << "TABLE_PROJECT operator expects a table. Found '" << n[2]
+ ss << "RELATION_AGGREGATE operator expects a relation. Found '" << n[2]
<< "' of type '" << setType << "'.";
throw TypeCheckingExceptionPrivate(n, ss.str());
}
return nm->mkSetType(functionType.getRangeType());
}
+TypeNode RelationProjectTypeRule::computeType(NodeManager* nm,
+ TNode n,
+ bool check)
+{
+ Assert(n.getKind() == kind::RELATION_PROJECT && n.hasOperator()
+ && n.getOperator().getKind() == kind::RELATION_PROJECT_OP);
+ ProjectOp op = n.getOperator().getConst<ProjectOp>();
+ const std::vector<uint32_t>& indices = op.getIndices();
+ TypeNode setType = n[0].getType(check);
+ if (check)
+ {
+ if (n.getNumChildren() != 1)
+ {
+ std::stringstream ss;
+ ss << "operands in term " << n << " are " << n.getNumChildren()
+ << ", but RELATION_PROJECT expects 1 operand.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+
+ if (!setType.isSet())
+ {
+ std::stringstream ss;
+ ss << "RELATION_PROJECT operator expects a set. Found '" << n[0]
+ << "' of type '" << setType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+
+ TypeNode tupleType = setType.getSetElementType();
+ if (!tupleType.isTuple())
+ {
+ std::stringstream ss;
+ ss << "RELATION_PROJECT operator expects a relation. Found '" << n[0]
+ << "' of type '" << setType << "'.";
+ 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 << "Index " << index << " in term " << n << " is >= " << numArgs
+ << " which is the number of columns in " << n[0] << ".";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ }
+ TypeNode tupleType = setType.getSetElementType();
+ TypeNode retTupleType =
+ TupleUtils::getTupleProjectionType(indices, tupleType);
+ return nm->mkSetType(retTupleType);
+}
+
Cardinality SetsProperties::computeCardinality(TypeNode type)
{
Assert(type.getKind() == kind::SET_TYPE);
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
}; /* struct RelationGroupTypeRule */
+/**
+ * Relation project is indexed by a list of indices (n_1, ..., n_m). It ensures
+ * that the argument is a set of tuples whose arity k is greater than each n_i
+ * for i = 1, ..., m. If the argument is of type (Relation T_1 ... T_k), then
+ * the returned type is (Relation T_{n_1} ... T_{n_m}).
+ */
+struct RelationProjectTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+}; /* struct RelationProjectTypeRule */
+
/**
* Relation aggregate operator is indexed by a list of indices (n_1, ..., n_k).
* It ensures that it has 3 arguments:
regress1/bags/table_join2.smt2
regress1/bags/table_join3.smt2
regress1/bags/table_project1.smt2
+ regress1/bags/table_project2.smt2
regress1/bags/union_disjoint.smt2
regress1/bags/union_max1.smt2
regress1/bags/union_max2.smt2
regress1/sets/relation_group3.smt2
regress1/sets/relation_group4.smt2
regress1/sets/relation_group5.smt2
+ regress1/sets/relation_project1.smt2
+ regress1/sets/relation_project2.smt2
regress1/sets/remove_check_free_31_6.smt2
regress1/sets/sets-disequal.smt2
regress1/sets/sets-tuple-poly.cvc.smt2
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(set-option :uf-lazy-ll true)
+
+(declare-fun A () (Table String String))
+(declare-fun B () (Table String String))
+
+(assert (= B ((_ table.project 1 0) A)))
+(assert (bag.member (tuple "y" "x") B))
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+
+(set-info :status sat)
+
+(declare-fun A () (Relation String Int String Bool))
+(declare-fun B () (Relation Int Bool String String))
+(declare-fun C () (Relation String String))
+(declare-fun D () Relation)
+
+(assert
+ (= A
+ (set.union
+ (set.singleton (tuple "x" 0 "y" false))
+ (set.singleton (tuple "x" 1 "z" true)))))
+
+
+; (set.union (set.singleton (tuple 0 false "x" "y")) (set.singleton (tuple 1 true "x" "z")))
+(assert (= B ((_ rel.project 1 3 0 2) A)))
+
+; (set.singleton (tuple "x" "x"))
+(assert (= C ((_ rel.project 0 0) A)))
+
+; (set.singleton tuple)
+(assert (= D (rel.project A)))
+
+(check-sat)
--- /dev/null
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :uf-lazy-ll true)
+
+(declare-fun A () (Relation String String))
+(declare-fun B () (Relation String String))
+
+(assert (= B ((_ rel.project 1 0) A)))
+(assert (set.member (tuple "y" "x") B))
+(check-sat)
Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
ASSERT_EQ(indices.size(), tupleProject.getNumIndices());
+ Op relationProject = d_solver.mkOp(RELATION_PROJECT, indices);
+ ASSERT_EQ(indices.size(), relationProject.getNumIndices());
+
Op tableProject = d_solver.mkOp(TABLE_PROJECT, indices);
ASSERT_EQ(indices.size(), tableProject.getNumIndices());
}
Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
assertEquals(6, tupleProject.getNumIndices());
+ Op relationProject = d_solver.mkOp(RELATION_PROJECT, indices);
+ assertEquals(6, relationProject.getNumIndices());
+
Op tableProject = d_solver.mkOp(TABLE_PROJECT, indices);
assertEquals(6, tableProject.getNumIndices());
}
tuple_project_op = solver.mkOp(Kind.TUPLE_PROJECT, *indices)
assert len(indices) == tuple_project_op.getNumIndices()
+ relation_project_op = solver.mkOp(Kind.RELATION_PROJECT, *indices)
+ assert len(indices) == relation_project_op.getNumIndices()
+
table_project_op = solver.mkOp(Kind.TABLE_PROJECT, *indices)
assert len(indices) == table_project_op.getNumIndices()
projects / cvc5.git / commitdiff