theory/datatypes/theory_datatypes_utils.h
theory/datatypes/tuple_project_op.cpp
theory/datatypes/tuple_project_op.h
+ theory/datatypes/tuple_utils.cpp
+ theory/datatypes/tuple_utils.h
theory/datatypes/type_enumerator.cpp
theory/datatypes/type_enumerator.h
theory/decision_manager.cpp
theory/sets/inference_manager.cpp
theory/sets/inference_manager.h
theory/sets/normal_form.h
+ theory/sets/rels_utils.cpp
theory/sets/rels_utils.h
theory/sets/singleton_op.cpp
theory/sets/singleton_op.h
{BAG_MAP, cvc5::Kind::BAG_MAP},
{BAG_FILTER, cvc5::Kind::BAG_FILTER},
{BAG_FOLD, cvc5::Kind::BAG_FOLD},
+ {TABLE_PRODUCT, cvc5::Kind::TABLE_PRODUCT},
/* Strings ------------------------------------------------------------- */
{STRING_CONCAT, cvc5::Kind::STRING_CONCAT},
{STRING_IN_REGEXP, cvc5::Kind::STRING_IN_REGEXP},
{cvc5::Kind::BAG_MAP, BAG_MAP},
{cvc5::Kind::BAG_FILTER, BAG_FILTER},
{cvc5::Kind::BAG_FOLD, BAG_FOLD},
+ {cvc5::Kind::TABLE_PRODUCT, TABLE_PRODUCT},
/* Strings --------------------------------------------------------- */
{cvc5::Kind::STRING_CONCAT, STRING_CONCAT},
{cvc5::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP},
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
BAG_FOLD,
+ /**
+ * Table cross product.
+ *
+ * Parameters:
+ * - 1..2: Terms of bag sort
+ *
+ * Create with:
+ * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
+ * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ */
+ TABLE_PRODUCT,
/* Strings --------------------------------------------------------------- */
addOperator(api::BAG_MAP, "bag.map");
addOperator(api::BAG_FILTER, "bag.filter");
addOperator(api::BAG_FOLD, "bag.fold");
+ addOperator(api::TABLE_PRODUCT, "table.product");
}
if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
defineType("String", d_solver->getStringSort(), true, true);
case kind::BAG_MAP: return "bag.map";
case kind::BAG_FILTER: return "bag.filter";
case kind::BAG_FOLD: return "bag.fold";
+ case kind::TABLE_PRODUCT: return "table.product";
// fp theory
case kind::FLOATINGPOINT_FP: return "fp";
case kind::BAG_DUPLICATE_REMOVAL: checkDuplicateRemoval(n); break;
case kind::BAG_FILTER: checkFilter(n); break;
case kind::BAG_MAP: checkMap(n); break;
+ case kind::TABLE_PRODUCT: checkProduct(n); break;
default: break;
}
it++;
}
}
+void BagSolver::checkProduct(Node n)
+{
+ Assert(n.getKind() == TABLE_PRODUCT);
+ const set<Node>& elementsA = d_state.getElements(n[0]);
+ const set<Node>& elementsB = d_state.getElements(n[1]);
+ for (const Node& e1 : elementsA)
+ {
+ for (const Node& e2 : elementsB)
+ {
+ InferInfo i = d_ig.productUp(
+ n, d_state.getRepresentative(e1), d_state.getRepresentative(e2));
+ d_im.lemmaTheoryInference(&i);
+ }
+ }
+
+ std::set<Node> elements = d_state.getElements(n);
+ for (const Node& e : elements)
+ {
+ InferInfo i = d_ig.productDown(n, d_state.getRepresentative(e));
+ d_im.lemmaTheoryInference(&i);
+ }
+}
+
} // namespace bags
} // namespace theory
} // namespace cvc5
void checkMap(Node n);
/** apply inference rules for filter operator */
void checkFilter(Node n);
+ /** apply inference rules for product operator */
+ void checkProduct(Node n);
/** The solver state object */
SolverState& d_state;
case BAG_MAP: response = postRewriteMap(n); break;
case BAG_FILTER: response = postRewriteFilter(n); break;
case BAG_FOLD: response = postRewriteFold(n); break;
+ case TABLE_PRODUCT: response = postRewriteProduct(n); break;
default: response = BagsRewriteResponse(n, Rewrite::NONE); break;
}
}
}
return BagsRewriteResponse(n, Rewrite::NONE);
}
+
+BagsRewriteResponse BagsRewriter::postRewriteProduct(const TNode& n) const
+{
+ Assert(n.getKind() == TABLE_PRODUCT);
+ TypeNode tableType = n.getType();
+ Node empty = d_nm->mkConst(EmptyBag(tableType));
+ if (n[0].getKind() == BAG_EMPTY || n[1].getKind() == BAG_EMPTY)
+ {
+ return BagsRewriteResponse(empty, Rewrite::PRODUCT_EMPTY);
+ }
+
+ return BagsRewriteResponse(n, Rewrite::NONE);
+}
+
} // namespace bags
} // namespace theory
} // namespace cvc5
* where f: T1 -> T2 -> T2
*/
BagsRewriteResponse postRewriteFold(const TNode& n) const;
+ /**
+ * rewrites for n include:
+ * - (bag.product A (as bag.empty T2)) = (as bag.empty T)
+ * - (bag.product (as bag.empty T2)) = (f t ... (f t (f t x))) n times, where n > 0
+ * - (bag.fold f t (bag.union_disjoint A B)) =
+ * (bag.fold f (bag.fold f t A) B) where A < B to break symmetry
+ * where f: T1 -> T2 -> T2
+ */
+ BagsRewriteResponse postRewriteProduct(const TNode& n)const;
private:
/** Reference to the rewriter statistics. */
*/
#include "bags_utils.h"
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
#include "expr/emptybag.h"
#include "smt/logic_exception.h"
+#include "theory/datatypes/tuple_utils.h"
#include "theory/sets/normal_form.h"
#include "theory/type_enumerator.h"
#include "util/rational.h"
using namespace cvc5::kind;
+using namespace cvc5::theory::datatypes;
namespace cvc5 {
namespace theory {
case BAG_MAP: return evaluateBagMap(n);
case BAG_FILTER: return evaluateBagFilter(n);
case BAG_FOLD: return evaluateBagFold(n);
+ case TABLE_PRODUCT: return evaluateProduct(n);
default: break;
}
Unhandled() << "Unexpected bag kind '" << n.getKind() << "' in node " << n
return ret;
}
+Node BagsUtils::constructProductTuple(TNode n, TNode e1, TNode e2)
+{
+ Assert(n.getKind() == TABLE_PRODUCT);
+ Node A = n[0];
+ Node B = n[1];
+ TypeNode typeA = A.getType().getBagElementType();
+ TypeNode typeB = B.getType().getBagElementType();
+ Assert(e1.getType().isSubtypeOf(typeA));
+ Assert(e2.getType().isSubtypeOf(typeB));
+
+ TypeNode productTupleType = n.getType().getBagElementType();
+ Node tuple = TupleUtils::concatTuples(productTupleType, e1, e2);
+ return tuple;
+}
+
+Node BagsUtils::evaluateProduct(TNode n)
+{
+ Assert(n.getKind() == TABLE_PRODUCT);
+
+ // Examples
+ // --------
+ //
+ // - (table.product (bag (tuple "a") 4) (bag (tuple true) 5)) =
+ // (bag (tuple "a" true) 20
+
+ Node A = n[0];
+ Node B = n[1];
+
+ std::map<Node, Rational> elementsA = BagsUtils::getBagElements(A);
+ std::map<Node, Rational> elementsB = BagsUtils::getBagElements(B);
+
+ std::map<Node, Rational> elements;
+
+ for (const auto& [a, countA] : elementsA)
+ {
+ for (const auto& [b, countB] : elementsB)
+ {
+ Node element = constructProductTuple(n, a, b);
+ elements[element] = countA * countB;
+ }
+ }
+
+ Node ret = BagsUtils::constructConstantBagFromElements(n.getType(), elements);
+ return ret;
+}
+
} // namespace bags
} // namespace theory
} // namespace cvc5
#include "cvc5_private.h"
-#ifndef CVC5__THEORY__BAGS__NORMAL_FORM_H
-#define CVC5__THEORY__BAGS__NORMAL_FORM_H
+#ifndef CVC5__THEORY__BAGS__UTILS_H
+#define CVC5__THEORY__BAGS__UTILS_H
namespace cvc5 {
namespace theory {
*/
static Node evaluateBagFilter(TNode n);
+ /**
+ * @param n of the form (table.product A B) where A , B of types (Bag T1),
+ * (Bag T2) respectively.
+ * @param e1 a tuple of type T1 of the form (tuple a1 ... an)
+ * @param e2 a tuple of type T2 of the form (tuple b1 ... bn)
+ * @return (tuple a1 ... an b1 ... bn)
+ */
+ static Node constructProductTuple(TNode n, TNode e1, TNode e2);
+
+ /**
+ * @param n of the form (table.product A B) where A, B are constants
+ * @return the evaluation of the cross product of A B
+ */
+ static Node evaluateProduct(TNode n);
+
private:
/**
* a high order helper function that return a constant bag that is the result
} // namespace theory
} // namespace cvc5
-#endif /* CVC5__THEORY__BAGS__NORMAL_FORM_H */
+#endif /* CVC5__THEORY__BAGS__UTILS_H */
#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
+#include "expr/dtype_cons.h"
#include "expr/emptybag.h"
#include "expr/skolem_manager.h"
+#include "theory/bags/bags_utils.h"
#include "theory/bags/inference_manager.h"
#include "theory/bags/solver_state.h"
+#include "theory/datatypes/tuple_utils.h"
#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/uf/equality_engine.h"
#include "util/rational.h"
using namespace cvc5::kind;
+using namespace cvc5::theory::datatypes;
namespace cvc5 {
namespace theory {
return inferInfo;
}
+InferInfo InferenceGenerator::productUp(Node n, Node e1, Node e2)
+{
+ Assert(n.getKind() == TABLE_PRODUCT);
+ Node A = n[0];
+ Node B = n[1];
+ Node tuple = BagsUtils::constructProductTuple(n, e1, e2);
+
+ InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_UP);
+
+ Node countA = getMultiplicityTerm(e1, A);
+ Node countB = getMultiplicityTerm(e2, B);
+
+ Node skolem = getSkolem(n, inferInfo);
+ Node count = getMultiplicityTerm(tuple, skolem);
+
+ Node multiply = d_nm->mkNode(MULT, countA, countB);
+ inferInfo.d_conclusion = count.eqNode(multiply);
+
+ return inferInfo;
+}
+
+InferInfo InferenceGenerator::productDown(Node n, Node e)
+{
+ Assert(n.getKind() == TABLE_PRODUCT);
+ Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
+
+ Node A = n[0];
+ Node B = n[1];
+
+ TypeNode tupleBType = B.getType().getBagElementType();
+ TypeNode tupleAType = A.getType().getBagElementType();
+ size_t tupleALength = tupleAType.getTupleLength();
+ size_t productTupleLength = n.getType().getBagElementType().getTupleLength();
+
+ std::vector<Node> elements = TupleUtils::getTupleElements(e);
+ Node a = TupleUtils::constructTupleFromElements(
+ tupleAType, elements, 0, tupleALength - 1);
+ Node b = TupleUtils::constructTupleFromElements(
+ tupleBType, elements, tupleALength, productTupleLength - 1);
+
+ InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_DOWN);
+
+ Node countA = getMultiplicityTerm(a, A);
+ Node countB = getMultiplicityTerm(b, B);
+
+ Node skolem = getSkolem(n, inferInfo);
+ Node count = getMultiplicityTerm(e, skolem);
+
+ Node multiply = d_nm->mkNode(MULT, countA, countB);
+ inferInfo.d_conclusion = count.eqNode(multiply);
+
+ return inferInfo;
+}
+
} // namespace bags
} // namespace theory
} // namespace cvc5
* (bag.member e skolem)
* (and
* (p e)
- * (= (bag.count e skolem) (bag.count A)))
+ * (= (bag.count e skolem) (bag.count e A)))
* where skolem is a variable equals (bag.filter p A)
*/
InferInfo filterDownwards(Node n, Node e);
*/
InferInfo filterUpwards(Node n, Node e);
+ /**
+ * @param n is a (table.product A B) where A, B are bags of tuples
+ * @param e1 an element of the form (tuple a1 ... am)
+ * @param e2 an element of the form (tuple b1 ... bn)
+ * @return an inference that represents the following
+ * (=
+ * (bag.count (tuple a1 ... am b1 ... bn) skolem)
+ * (* (bag.count e1 A) (bag.count e2 B)))
+ * where skolem is a variable equals (bag.product A B)
+ */
+ InferInfo productUp(Node n, Node e1, Node e2);
+
+ /**
+ * @param n is a (table.product A B) where A, B are bags of tuples
+ * @param e an element of the form (tuple a1 ... am b1 ... bn)
+ * @return an inference that represents the following
+ * (=
+ * (bag.count (tuple a1 ... am b1 ... bn) skolem)
+ * (* (bag.count (tuple a1 ... am A) (bag.count (tuple b1 ... bn) B)))
+ * where skolem is a variable equals (bag.product A B)
+ */
+ InferInfo productDown(Node n, Node e);
+
/**
* @param element of type T
* @param bag of type (bag T)
construle BAG_UNION_DISJOINT ::cvc5::theory::bags::BinaryOperatorTypeRule
construle BAG_MAKE ::cvc5::theory::bags::BagMakeTypeRule
+
+# bag.product operator returns the cross product of two tables
+operator TABLE_PRODUCT 2 "table cross product"
+
+typerule TABLE_PRODUCT ::cvc5::theory::bags::TableProductTypeRule
+
endtheory
case Rewrite::MAP_BAG_MAKE: return "MAP_BAG_MAKE";
case Rewrite::MAP_UNION_DISJOINT: return "MAP_UNION_DISJOINT";
case Rewrite::MEMBER: return "MEMBER";
+ case Rewrite::PRODUCT_EMPTY: return "PRODUCT_EMPTY";
case Rewrite::REMOVE_FROM_UNION: return "REMOVE_FROM_UNION";
case Rewrite::REMOVE_MIN: return "REMOVE_MIN";
case Rewrite::REMOVE_RETURN_LEFT: return "REMOVE_RETURN_LEFT";
MAP_BAG_MAKE,
MAP_UNION_DISJOINT,
MEMBER,
+ PRODUCT_EMPTY,
REMOVE_FROM_UNION,
REMOVE_MIN,
REMOVE_RETURN_LEFT,
return retType;
}
+TypeNode TableProductTypeRule::computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+{
+ Assert(n.getKind() == kind::TABLE_PRODUCT);
+ Node A = n[0];
+ Node B = n[1];
+ TypeNode typeA = n[0].getType(check);
+ TypeNode typeB = n[1].getType(check);
+
+ if (check && !(typeA.isBag() && typeB.isBag()))
+ {
+ std::stringstream ss;
+ ss << "Operator " << n.getKind() << " expects two bags. "
+ << "Found two terms of types '" << typeA << "' and '" << typeB
+ << "' respectively.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+
+ TypeNode elementAType = typeA.getBagElementType();
+ TypeNode elementBType = typeB.getBagElementType();
+
+ if (check && !(elementAType.isTuple() && elementBType.isTuple()))
+ {
+ std::stringstream ss;
+ ss << "Operator " << n.getKind() << " expects two tables (bags of tuples). "
+ << "Found two terms of types '" << typeA << "' and '" << typeB
+ << "' respectively.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+
+ std::vector<TypeNode> productTupleTypes;
+ std::vector<TypeNode> tupleATypes = elementAType.getTupleTypes();
+ std::vector<TypeNode> tupleBTypes = elementBType.getTupleTypes();
+
+ productTupleTypes.insert(
+ productTupleTypes.end(), tupleATypes.begin(), tupleATypes.end());
+ productTupleTypes.insert(
+ productTupleTypes.end(), tupleBTypes.begin(), tupleBTypes.end());
+
+ TypeNode retTupleType = nodeManager->mkTupleType(productTupleTypes);
+ TypeNode retType = nodeManager->mkBagType(retTupleType);
+ return retType;
+}
+
Cardinality BagsProperties::computeCardinality(TypeNode type)
{
return Cardinality::INTEGERS;
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
}; /* struct BagFoldTypeRule */
+/**
+ * Type rule for (table.product A B) to make sure A,B are bags of tuples,
+ * and get the type of the cross product
+ */
+struct TableProductTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+}; /* struct BagFoldTypeRule */
+
struct BagsProperties
{
static Cardinality computeCardinality(TypeNode type);
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Utility functions for data types.
+ */
+
+#include "tuple_utils.h"
+
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace datatypes {
+
+Node TupleUtils::nthElementOfTuple(Node tuple, int n_th)
+{
+ if (tuple.getKind() == APPLY_CONSTRUCTOR)
+ {
+ return tuple[n_th];
+ }
+ TypeNode tn = tuple.getType();
+ const DType& dt = tn.getDType();
+ return NodeManager::currentNM()->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple);
+}
+
+std::vector<Node> TupleUtils::getTupleElements(Node tuple)
+{
+ Assert(tuple.getType().isTuple());
+ size_t tupleLength = tuple.getType().getTupleLength();
+ std::vector<Node> elements;
+ for (size_t i = 0; i < tupleLength; i++)
+ {
+ elements.push_back(TupleUtils::nthElementOfTuple(tuple, i));
+ }
+ return elements;
+}
+
+std::vector<Node> TupleUtils::getTupleElements(Node tuple1, Node tuple2)
+{
+ std::vector<Node> elements;
+ std::vector<Node> elementsA = getTupleElements(tuple1);
+ size_t tuple1Length = tuple1.getType().getTupleLength();
+ for (size_t i = 0; i < tuple1Length; i++)
+ {
+ elements.push_back(TupleUtils::nthElementOfTuple(tuple1, i));
+ }
+
+ size_t tuple2Length = tuple2.getType().getTupleLength();
+ for (size_t i = 0; i < tuple2Length; i++)
+ {
+ elements.push_back(TupleUtils::nthElementOfTuple(tuple2, i));
+ }
+ return elements;
+}
+
+Node TupleUtils::constructTupleFromElements(TypeNode tupleType,
+ const std::vector<Node>& elements,
+ size_t start,
+ size_t end)
+{
+ std::vector<Node> tupleElements;
+ // add the constructor first
+ Node constructor = tupleType.getDType()[0].getConstructor();
+ tupleElements.push_back(constructor);
+ // add the elements of the tuple
+ for (size_t i = start; i <= end; i++)
+ {
+ tupleElements.push_back(elements[i]);
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ Node tuple = nm->mkNode(APPLY_CONSTRUCTOR, tupleElements);
+ return tuple;
+}
+
+Node TupleUtils::concatTuples(TypeNode tupleType, Node tuple1, Node tuple2)
+{
+ std::vector<Node> tupleElements;
+ // add the constructor first
+ Node constructor = tupleType.getDType()[0].getConstructor();
+ tupleElements.push_back(constructor);
+
+ // add the flattened concatenation of the two tuples e1, e2
+ std::vector<Node> elements = getTupleElements(tuple1, tuple2);
+ tupleElements.insert(tupleElements.end(), elements.begin(), elements.end());
+
+ // construct the returned tuple
+ NodeManager* nm = NodeManager::currentNM();
+ Node tuple = nm->mkNode(APPLY_CONSTRUCTOR, tupleElements);
+ return tuple;
+}
+
+Node TupleUtils::reverseTuple(Node tuple)
+{
+ Assert(tuple.getType().isTuple());
+ std::vector<Node> elements;
+ std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
+ std::reverse(tuple_types.begin(), tuple_types.end());
+ TypeNode tn = NodeManager::currentNM()->mkTupleType(tuple_types);
+ const DType& dt = tn.getDType();
+ elements.push_back(dt[0].getConstructor());
+ for (int i = tuple_types.size() - 1; i >= 0; --i)
+ {
+ elements.push_back(nthElementOfTuple(tuple, i));
+ }
+ return NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, elements);
+}
+
+} // namespace datatypes
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Utility functions for data types.
+ */
+
+#ifndef CVC5__THEORY__TUPLE__UTILS_H
+#define CVC5__THEORY__TUPLE__UTILS_H
+
+#include "expr/node.h"
+
+namespace cvc5 {
+namespace theory {
+namespace datatypes {
+
+class TupleUtils
+{
+ public:
+ /**
+ * @param tuple a node of tuple type
+ * @param n_th the index of the element to be extracted, and must satisfy the
+ * constraint 0 <= n_th < length of tuple.
+ * @return tuple element at index n_th
+ */
+ static Node nthElementOfTuple(Node tuple, int n_th);
+
+ /**
+ * @param tuple a tuple node of the form (tuple a_1 ... a_n)
+ * @return the vector [a_1, ... a_n]
+ */
+ static std::vector<Node> getTupleElements(Node tuple);
+
+ /**
+ * @param tuple1 a tuple node of the form (tuple a_1 ... a_n)
+ * @param tuple2 a tuple node of the form (tuple b_1 ... b_n)
+ * @return the vector [a_1, ... a_n, b_1, ... b_n]
+ */
+ static std::vector<Node> getTupleElements(Node tuple1, Node tuple2);
+
+ /**
+ * construct a tuple from a list of elements
+ * @param tupleType the type of the returned tuple
+ * @param elements the list of nodes
+ * @param start the index of the first element
+ * @param end the index of the last element
+ * @pre the elements from start to end should match the tuple type
+ * @return a tuple of constructed from elements from start to end
+ */
+ static Node constructTupleFromElements(TypeNode tupleType,
+ const std::vector<Node>& elements,
+ size_t start,
+ size_t end);
+
+ /**
+ * construct a flattened tuple from two tuples
+ * @param tupleType the type of the returned tuple
+ * @param tuple1 a tuple node of the form (tuple a_1 ... a_n)
+ * @param tuple2 a tuple node of the form (tuple b_1 ... b_n)
+ * @pre the elements of tuple1, tuple2 should match the tuple type
+ * @return (tuple a1 ... an b1 ... bn)
+ */
+ static Node concatTuples(TypeNode tupleType, Node tuple1, Node tuple2);
+
+ /**
+ * @param tuple a tuple node of the form (tuple e_1 ... e_n)
+ * @return the reverse of the argument, i.e., (tuple e_n ... e_1)
+ */
+ static Node reverseTuple(Node tuple);
+};
+} // namespace datatypes
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__TUPLE__UTILS_H */
case InferenceId::BAGS_FILTER_UP: return "BAGS_FILTER_UP";
case InferenceId::BAGS_FOLD: return "BAGS_FOLD";
case InferenceId::BAGS_CARD: return "BAGS_CARD";
+ case InferenceId::TABLES_PRODUCT_UP: return "TABLES_PRODUCT_UP";
+ case InferenceId::TABLES_PRODUCT_DOWN: return "TABLES_PRODUCT_DOWN";
case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT";
case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA:
BAGS_FILTER_UP,
BAGS_FOLD,
BAGS_CARD,
+ TABLES_PRODUCT_UP,
+ TABLES_PRODUCT_DOWN,
// ---------------------------------- end bags theory
// ---------------------------------- bitvector theory
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Utility functions for relations.
+ */
+
+#include "rels_utils.h"
+
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
+#include "theory/datatypes/tuple_utils.h"
+
+using namespace cvc5::theory::datatypes;
+
+namespace cvc5 {
+namespace theory {
+namespace sets {
+
+std::set<Node> RelsUtils::computeTC(const std::set<Node>& members, Node rel)
+{
+ std::set<Node>::iterator mem_it = members.begin();
+ std::map<Node, int> ele_num_map;
+ std::set<Node> tc_rel_mem;
+
+ while (mem_it != members.end())
+ {
+ Node fst = TupleUtils::nthElementOfTuple(*mem_it, 0);
+ Node snd = TupleUtils::nthElementOfTuple(*mem_it, 1);
+ std::set<Node> traversed;
+ traversed.insert(fst);
+ computeTC(rel, members, fst, snd, traversed, tc_rel_mem);
+ mem_it++;
+ }
+ return tc_rel_mem;
+}
+
+void RelsUtils::computeTC(Node rel,
+ const std::set<Node>& members,
+ Node a,
+ Node b,
+ std::set<Node>& traversed,
+ std::set<Node>& transitiveClosureMembers)
+{
+ transitiveClosureMembers.insert(constructPair(rel, a, b));
+ if (traversed.find(b) != traversed.end())
+ {
+ return;
+ }
+ traversed.insert(b);
+ std::set<Node>::iterator mem_it = members.begin();
+ while (mem_it != members.end())
+ {
+ Node new_fst = TupleUtils::nthElementOfTuple(*mem_it, 0);
+ Node new_snd = TupleUtils::nthElementOfTuple(*mem_it, 1);
+ if (b == new_fst)
+ {
+ computeTC(rel, members, a, new_snd, traversed, transitiveClosureMembers);
+ }
+ mem_it++;
+ }
+}
+
+Node RelsUtils::constructPair(Node rel, Node a, Node b)
+{
+ const DType& dt = rel.getType().getSetElementType().getDType();
+ return NodeManager::currentNM()->mkNode(
+ kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
+}
+
+} // namespace sets
+} // namespace theory
+} // namespace cvc5
* directory for licensing information.
* ****************************************************************************
*
- * Extension to Sets theory.
+ * Utility functions for relations.
*/
#ifndef SRC_THEORY_SETS_RELS_UTILS_H_
#define SRC_THEORY_SETS_RELS_UTILS_H_
-#include "expr/dtype.h"
-#include "expr/dtype_cons.h"
#include "expr/node.h"
namespace cvc5 {
namespace theory {
namespace sets {
-class RelsUtils {
+class RelsUtils
+{
+ public:
+ /**
+ * compute the transitive closure of a binary relation
+ * @param members constant nodes of type (Tuple E E) that are known to in the
+ * relation rel
+ * @param rel a binary relation of type (Set (Tuple E E))
+ * @pre all members need to be constants
+ * @return the transitive closure of the relation
+ */
+ static std::set<Node> computeTC(const std::set<Node>& members, Node rel);
-public:
+ /**
+ * add all pairs (a, c) to the transitive closures where c is reachable from b
+ * in the transitive relation in a depth first search manner.
+ * @param rel a binary relation of type (Set (Tuple E E))
+ * @param members constant nodes of type (Tuple E E) that are known to be in
+ * the relation rel
+ * @param a a node of type E where (a,b) is an element in the transitive
+ * closure
+ * @param b a node of type E where (a,b) is an element in the transitive
+ * closure
+ * @param traversed the set of members that have been visited so far
+ * @param transitiveClosureMembers members of the transitive closure computed
+ * so far
+ */
+ static void computeTC(Node rel,
+ const std::set<Node>& members,
+ Node a,
+ Node b,
+ std::set<Node>& traversed,
+ std::set<Node>& transitiveClosureMembers);
- // Assumption: the input rel_mem contains all constant pairs
- static std::set< Node > computeTC( std::set< Node > rel_mem, Node rel ) {
- std::set< Node >::iterator mem_it = rel_mem.begin();
- std::map< Node, int > ele_num_map;
- std::set< Node > tc_rel_mem;
-
- while( mem_it != rel_mem.end() ) {
- Node fst = nthElementOfTuple( *mem_it, 0 );
- Node snd = nthElementOfTuple( *mem_it, 1 );
- std::set< Node > traversed;
- traversed.insert(fst);
- computeTC(rel, rel_mem, fst, snd, traversed, tc_rel_mem);
- mem_it++;
- }
- return tc_rel_mem;
- }
-
- static void computeTC( Node rel, std::set< Node >& rel_mem, Node fst,
- Node snd, std::set< Node >& traversed, std::set< Node >& tc_rel_mem ) {
- tc_rel_mem.insert(constructPair(rel, fst, snd));
- if( traversed.find(snd) == traversed.end() ) {
- traversed.insert(snd);
- } else {
- return;
- }
-
- std::set< Node >::iterator mem_it = rel_mem.begin();
- while( mem_it != rel_mem.end() ) {
- Node new_fst = nthElementOfTuple( *mem_it, 0 );
- Node new_snd = nthElementOfTuple( *mem_it, 1 );
- if( snd == new_fst ) {
- computeTC(rel, rel_mem, fst, new_snd, traversed, tc_rel_mem);
- }
- mem_it++;
- }
- }
-
- static Node nthElementOfTuple( Node tuple, int n_th ) {
- if( tuple.getKind() == kind::APPLY_CONSTRUCTOR ) {
- return tuple[n_th];
- }
- TypeNode tn = tuple.getType();
- const DType& dt = tn.getDType();
- return NodeManager::currentNM()->mkNode(
- kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple);
- }
-
- static Node reverseTuple( Node tuple ) {
- Assert(tuple.getType().isTuple());
- std::vector<Node> elements;
- std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
- std::reverse( tuple_types.begin(), tuple_types.end() );
- TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
- const DType& dt = tn.getDType();
- elements.push_back(dt[0].getConstructor());
- for(int i = tuple_types.size() - 1; i >= 0; --i) {
- elements.push_back( nthElementOfTuple(tuple, i) );
- }
- return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
- }
- static Node constructPair(Node rel, Node a, Node b) {
- const DType& dt = rel.getType().getSetElementType().getDType();
- return NodeManager::currentNM()->mkNode(
- kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
- }
-
+ /**
+ * construct a pair from two elements
+ * @param rel a node of type (Set (Tuple E E))
+ * @param a a node of type E
+ * @param b a node of type E
+ * @return a tuple (tuple a b)
+ */
+ static Node constructPair(Node rel, Node a, Node b);
};
} // namespace sets
} // namespace theory
#include "theory/sets/theory_sets_rels.h"
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
#include "expr/skolem_manager.h"
+#include "theory/datatypes/tuple_utils.h"
#include "theory/sets/theory_sets.h"
#include "theory/sets/theory_sets_private.h"
#include "util/rational.h"
using namespace std;
using namespace cvc5::kind;
+using namespace cvc5::theory::datatypes;
namespace cvc5 {
namespace theory {
std::vector<TypeNode> tupleTypes = erType.getTupleTypes();
for (unsigned i = 0, tlen = erType.getTupleLength(); i < tlen; i++)
{
- Node element = RelsUtils::nthElementOfTuple(eqc_node, i);
+ Node element = TupleUtils::nthElementOfTuple(eqc_node, i);
if (!element.isConst())
{
makeSharedTerm(element, tupleTypes[i]);
unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
while( mem_rep_it != (*rel_mem_it).second.end() ) {
- Node fst_mem_rep = RelsUtils::nthElementOfTuple( *mem_rep_it, 0 );
+ Node fst_mem_rep = TupleUtils::nthElementOfTuple( *mem_rep_it, 0 );
if( hasChecked.find( fst_mem_rep ) != hasChecked.end() ) {
++mem_rep_it;
std::vector< Node >::iterator mem_rep_exp_it_snd = (*rel_mem_exp_it).second.begin();
while( mem_rep_exp_it_snd != (*rel_mem_exp_it).second.end() ) {
- Node fst_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 0 );
+ Node fst_element_snd_mem =
+ TupleUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 0 );
if( areEqual( fst_mem_rep, fst_element_snd_mem ) ) {
bool notExist = true;
std::vector< Node >::iterator existing_mem_it = existing_members.begin();
- Node snd_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 1 );
+ Node snd_element_snd_mem =
+ TupleUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 1 );
while( existing_mem_it != existing_members.end() ) {
if( areEqual( (*existing_mem_it), snd_element_snd_mem ) ) {
Node reason = exp;
Node conclusion = d_trueNode;
std::vector< Node > distinct_skolems;
- Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
+ Node fst_mem_element = TupleUtils::nthElementOfTuple( exp[0], 0 );
if( exp[1] != join_image_term ) {
reason =
d_rel_nodes.insert( iden_term );
}
Node reason = exp;
- Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
- Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
+ Node fst_mem = TupleUtils::nthElementOfTuple( exp[0], 0 );
+ Node snd_mem = TupleUtils::nthElementOfTuple( exp[0], 1 );
const DType& dt = iden_term[0].getType().getSetElementType().getDType();
Node fact = nm->mkNode(
SET_MEMBER,
while( mem_rep_exp_it != (*rel_mem_exp_it).second.end() ) {
Node reason = *mem_rep_exp_it;
- Node fst_exp_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it)[0], 0 );
+ Node fst_exp_mem = TupleUtils::nthElementOfTuple( (*mem_rep_exp_it)[0], 0 );
Node new_mem = RelsUtils::constructPair( iden_term, fst_exp_mem, fst_exp_mem );
if( (*mem_rep_exp_it)[1] != iden_term_rel ) {
// add mem_rep to d_tcrRep_tcGraph
TC_IT tc_it = d_tcr_tcGraph.find( tc_rel );
- Node mem_rep_fst = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 0 ) );
- Node mem_rep_snd = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 1 ) );
+ Node mem_rep_fst = getRepresentative(TupleUtils::nthElementOfTuple( mem_rep, 0 ) );
+ Node mem_rep_snd = getRepresentative(TupleUtils::nthElementOfTuple( mem_rep, 1 ) );
Node mem_rep_tup = RelsUtils::constructPair( tc_rel, mem_rep_fst, mem_rep_snd );
if( tc_it != d_tcr_tcGraph.end() ) {
exp_map[mem_rep_tup] = exp;
d_tcr_tcGraph_exps[tc_rel] = exp_map;
}
- Node fst_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
- Node snd_element = RelsUtils::nthElementOfTuple( exp[0], 1 );
+ Node fst_element = TupleUtils::nthElementOfTuple( exp[0], 0 );
+ Node snd_element = TupleUtils::nthElementOfTuple( exp[0], 1 );
Node sk_1 = d_skCache.mkTypedSkolemCached(fst_element.getType(),
exp[0],
tc_rel[0],
if( tc_it != d_rRep_tcGraph.end() ) {
bool isReachable = false;
std::unordered_set<Node> seen;
- isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ),
- getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
+ isTCReachable( getRepresentative(TupleUtils::nthElementOfTuple(mem_rep, 0) ),
+ getRepresentative(TupleUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
return isReachable;
}
return false;
for (size_t i = 0, msize = members.size(); i < msize; i++)
{
- Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
- Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
+ Node fst_element_rep = getRepresentative(TupleUtils::nthElementOfTuple( members[i], 0 ));
+ Node snd_element_rep = getRepresentative(TupleUtils::nthElementOfTuple( members[i], 1 ));
Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
std::map<Node, std::unordered_set<Node> >::iterator rel_tc_graph_it =
rel_tc_graph.find(fst_element_rep);
std::unordered_set<Node>& seen)
{
NodeManager* nm = NodeManager::currentNM();
- Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) );
+ Node tc_mem = RelsUtils::constructPair( tc_rel,
+ TupleUtils::nthElementOfTuple((reasons.front())[0], 0),
+ TupleUtils::nthElementOfTuple((reasons.back())[0], 1) );
std::vector< Node > all_reasons( reasons );
for( unsigned int i = 0 ; i < reasons.size()-1; i++ ) {
- Node fst_element_end = RelsUtils::nthElementOfTuple( reasons[i][0], 1 );
- Node snd_element_begin = RelsUtils::nthElementOfTuple( reasons[i+1][0], 0 );
+ Node fst_element_end = TupleUtils::nthElementOfTuple( reasons[i][0], 1 );
+ Node snd_element_begin =
+ TupleUtils::nthElementOfTuple( reasons[i+1][0], 0 );
if( fst_element_end != snd_element_begin ) {
all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, fst_element_end, snd_element_begin) );
}
unsigned int i = 0;
for(; i < s1_len; ++i) {
- r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
+ r1_element.push_back(TupleUtils::nthElementOfTuple(mem, i));
}
const DType& dt2 = pt_rel[1].getType().getSetElementType().getDType();
r2_element.push_back(dt2[0].getConstructor());
for(; i < tup_len; ++i) {
- r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
+ r2_element.push_back(TupleUtils::nthElementOfTuple(mem, i));
}
Node reason = exp;
Node mem1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
unsigned int i = 0;
r1_element.push_back(dt1[0].getConstructor());
for(; i < s1_len-1; ++i) {
- r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
+ r1_element.push_back(TupleUtils::nthElementOfTuple(mem, i));
}
r1_element.push_back(shared_x);
const DType& dt2 = join_rel[1].getType().getSetElementType().getDType();
r2_element.push_back(dt2[0].getConstructor());
r2_element.push_back(shared_x);
for(; i < tup_len; ++i) {
- r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
+ r2_element.push_back(TupleUtils::nthElementOfTuple(mem, i));
}
Node mem1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
Node mem2 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_element);
}
Node reason = exp;
- Node reversed_mem = RelsUtils::reverseTuple( exp[0] );
+ Node reversed_mem = TupleUtils::reverseTuple( exp[0] );
if( tp_rel != exp[1] ) {
reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tp_rel, exp[1]));
kind::AND, reason, nm->mkNode(kind::EQUAL, rel[0], exps[i][1]));
}
sendInfer(
- nm->mkNode(SET_MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel),
+ nm->mkNode(SET_MEMBER, TupleUtils::reverseTuple(exps[i][0]), rel),
InferenceId::SETS_RELS_TRANSPOSE_REV,
reason);
}
std::vector<Node> reasons;
if (rk == kind::RELATION_JOIN)
{
- Node r1_rmost =
- RelsUtils::nthElementOfTuple(r1_rep_exps[i][0], r1_tuple_len - 1);
- Node r2_lmost = RelsUtils::nthElementOfTuple(r2_rep_exps[j][0], 0);
+ Node r1_rmost = TupleUtils::nthElementOfTuple(r1_rep_exps[i][0], r1_tuple_len - 1);
+ Node r2_lmost = TupleUtils::nthElementOfTuple(r2_rep_exps[j][0], 0);
// Since we require notification r1_rmost and r2_lmost are equal,
// they must be shared terms of theory of sets. Hence, we make the
// following calls to makeSharedTerm to ensure this is the case.
unsigned int l = 1;
for( ; k < r1_tuple_len - 1; ++k ) {
- tuple_elements.push_back( RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) );
+ tuple_elements.push_back(
+ TupleUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) );
}
if(isProduct) {
- tuple_elements.push_back( RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) );
- tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 ) );
+ tuple_elements.push_back(
+ TupleUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) );
+ tuple_elements.push_back(
+ TupleUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 ) );
}
for( ; l < r2_tuple_len; ++l ) {
- tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], l ) );
+ tuple_elements.push_back(
+ TupleUtils::nthElementOfTuple( r2_rep_exps[j][0], l ) );
}
Node composed_tuple =
size_t tlen = atn.getTupleLength();
for (size_t i = 0; i < tlen; i++)
{
- if (!areEqual(RelsUtils::nthElementOfTuple(a, i),
- RelsUtils::nthElementOfTuple(b, i)))
+ if (!areEqual(TupleUtils::nthElementOfTuple(a, i),
+ TupleUtils::nthElementOfTuple(b, i)))
{
return false;
}
void TheorySetsRels::computeTupleReps( Node n ) {
if( d_tuple_reps.find( n ) == d_tuple_reps.end() ){
for( unsigned i = 0; i < n.getType().getTupleLength(); i++ ){
- d_tuple_reps[n].push_back( getRepresentative( RelsUtils::nthElementOfTuple(n, i) ) );
+ d_tuple_reps[n].push_back( getRepresentative(TupleUtils::nthElementOfTuple(n, i) ) );
}
}
}
std::vector<TypeNode> tupleTypes = n[0].getType().getTupleTypes();
for (unsigned int i = 0; i < n[0].getType().getTupleLength(); i++)
{
- Node element = RelsUtils::nthElementOfTuple(n[0], i);
+ Node element = TupleUtils::nthElementOfTuple(n[0], i);
makeSharedTerm(element, tupleTypes[i]);
tuple_elements.push_back(element);
}
#include "theory/sets/theory_sets_rewriter.h"
#include "expr/attribute.h"
+#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "options/sets_options.h"
+#include "theory/datatypes/tuple_utils.h"
#include "theory/sets/normal_form.h"
#include "theory/sets/rels_utils.h"
#include "util/rational.h"
using namespace cvc5::kind;
+using namespace cvc5::theory::datatypes;
namespace cvc5 {
namespace theory {
std::set<Node>::iterator tuple_it = tuple_set.begin();
while(tuple_it != tuple_set.end()) {
- new_tuple_set.insert(RelsUtils::reverseTuple(*tuple_it));
+ new_tuple_set.insert(TupleUtils::reverseTuple(*tuple_it));
++tuple_it;
}
Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType());
std::vector<Node> left_tuple;
left_tuple.push_back(tn.getDType()[0].getConstructor());
for(int i = 0; i < left_len; i++) {
- left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
+ left_tuple.push_back(TupleUtils::nthElementOfTuple(*left_it,i));
}
std::set<Node>::iterator right_it = right.begin();
int right_len = (*right_it).getType().getTupleLength();
Trace("rels-debug") << "Sets::postRewrite processing right_it = " << *right_it << std::endl;
std::vector<Node> right_tuple;
for(int j = 0; j < right_len; j++) {
- right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
+ right_tuple.push_back(TupleUtils::nthElementOfTuple(*right_it,j));
}
std::vector<Node> new_tuple;
new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end());
std::vector<Node> left_tuple;
left_tuple.push_back(tn.getDType()[0].getConstructor());
for(int i = 0; i < left_len - 1; i++) {
- left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
+ left_tuple.push_back(TupleUtils::nthElementOfTuple(*left_it,i));
}
std::set<Node>::iterator right_it = right.begin();
int right_len = (*right_it).getType().getTupleLength();
while(right_it != right.end()) {
- if(RelsUtils::nthElementOfTuple(*left_it,left_len-1) == RelsUtils::nthElementOfTuple(*right_it,0)) {
+ if(TupleUtils::nthElementOfTuple(*left_it,left_len-1) == TupleUtils::nthElementOfTuple(*right_it,0)) {
std::vector<Node> right_tuple;
for(int j = 1; j < right_len; j++) {
- right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
+ right_tuple.push_back(
+ TupleUtils::nthElementOfTuple(*right_it,j));
}
std::vector<Node> new_tuple;
new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end());
std::set<Node>::iterator rel_mems_it = rel_mems.begin();
while( rel_mems_it != rel_mems.end() ) {
- Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0);
+ Node fst_mem = TupleUtils::nthElementOfTuple( *rel_mems_it, 0);
iden_rel_mems.insert(RelsUtils::constructPair(node, fst_mem, fst_mem));
++rel_mems_it;
}
std::set<Node>::iterator rel_mems_it = rel_mems.begin();
while( rel_mems_it != rel_mems.end() ) {
- Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0);
+ Node fst_mem = TupleUtils::nthElementOfTuple( *rel_mems_it, 0);
if( has_checked.find( fst_mem ) != has_checked.end() ) {
++rel_mems_it;
continue;
std::set<Node> existing_mems;
std::set<Node>::iterator rel_mems_it_snd = rel_mems.begin();
while( rel_mems_it_snd != rel_mems.end() ) {
- Node fst_mem_snd = RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 0);
+ Node fst_mem_snd = TupleUtils::nthElementOfTuple( *rel_mems_it_snd, 0);
if( fst_mem == fst_mem_snd ) {
- existing_mems.insert( RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 1) );
+ existing_mems.insert(
+ TupleUtils::nthElementOfTuple( *rel_mems_it_snd, 1) );
}
++rel_mems_it_snd;
}
regress1/bags/murxla1.smt2
regress1/bags/murxla2.smt2
regress1/bags/murxla3.smt2
+ regress1/bags/product1.smt2
+ regress1/bags/product2.smt2
+ regress1/bags/product3.smt2
regress1/bags/subbag1.smt2
regress1/bags/subbag2.smt2
regress1/bags/union_disjoint.smt2
--- /dev/null
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun A () (Bag (Tuple String)))
+(declare-fun B () (Bag (Tuple Bool)))
+(declare-fun C () (Bag (Tuple String Bool)))
+(declare-fun x () (Tuple String))
+(declare-fun y () (Tuple Bool))
+(assert (= (bag.count x A) 5))
+(assert (= (bag.count y B) 4))
+(assert (= C (table.product A B)))
+(check-sat)
--- /dev/null
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun A () (Bag (Tuple Int Int Int)))
+(declare-fun B () (Bag (Tuple Int Int Int)))
+(declare-fun x () (Tuple Int Int Int))
+(assert (= x (tuple 1 2 3)))
+(declare-fun y () (Tuple Int Int Int))
+(assert (= y (tuple 3 2 1)))
+(declare-fun z () (Tuple Int Int Int Int Int Int))
+(assert (= z (tuple 1 2 3 3 2 1)))
+(assert (bag.member x A))
+(assert (bag.member y B))
+(assert (not (bag.member z (table.product A B))))
+(check-sat)
--- /dev/null
+(set-logic ALL)
+
+(set-info :status sat)
+
+(declare-fun A () (Bag (Tuple Int Int Int)))
+(declare-fun B () (Bag (Tuple Int Int Int)))
+(declare-fun C () (Bag (Tuple Int Int Int Int Int Int)))
+
+(assert (= C (table.product A B)))
+
+(declare-fun x () (Tuple Int Int Int))
+(declare-fun y () (Tuple Int Int Int))
+(declare-fun z () (Tuple Int Int Int Int Int Int))
+
+(assert (bag.member x A))
+(assert (bag.member y B))
+(assert (bag.member z C))
+
+(assert (distinct x y ((_ tuple_project 0 1 2) z) ((_ tuple_project 3 4 5) z)))
+
+(check-sat)
projects / cvc5.git / commitdiff