We now preserve types when rewriting. This means that we no longer need to use operators that store the type of terms to construct in the cases of bags, sets, and sequences.
theory/assertion.h
theory/atom_requests.cpp
theory/atom_requests.h
- theory/bags/bag_make_op.cpp
- theory/bags/bag_make_op.h
theory/bags/bags_rewriter.cpp
theory/bags/bags_rewriter.h
theory/bags/bag_solver.cpp
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
theory/sets/skolem_cache.cpp
theory/sets/skolem_cache.h
theory/sets/solver_state.cpp
theory/strings/regexp_solver.h
theory/strings/rewrites.cpp
theory/strings/rewrites.h
- theory/strings/seq_unit_op.cpp
- theory/strings/seq_unit_op.h
theory/strings/sequences_rewriter.cpp
theory/strings/sequences_rewriter.h
theory/strings/sequences_stats.cpp
{
// default case, same as above
checkMkTerm(kind, children.size());
- if (kind == SET_SINGLETON)
- {
- // the type of the term is the same as the type of the internal node
- // see Term::getSort()
- internal::TypeNode type = children[0].d_node->getType();
- // Internally NodeManager::mkSingleton needs a type argument
- // to construct a singleton, since there is no difference between
- // integers and reals (both are Rationals).
- // At the API, mkReal and mkInteger are different and therefore the
- // element type can be used safely here.
- res = getNodeManager()->mkSingleton(type, *children[0].d_node);
- }
- else if (kind == BAG_MAKE)
- {
- // the type of the term is the same as the type of the internal node
- // see Term::getSort()
- internal::TypeNode type = children[0].d_node->getType();
- // Internally NodeManager::mkBag needs a type argument
- // to construct a bag, since there is no difference between
- // integers and reals (both are Rationals).
- // At the API, mkReal and mkInteger are different and therefore the
- // element type can be used safely here.
- res = getNodeManager()->mkBag(
- type, *children[0].d_node, *children[1].d_node);
- }
- else if (kind == SEQ_UNIT)
- {
- // the type of the term is the same as the type of the internal node
- // see Term::getSort()
- internal::TypeNode type = children[0].d_node->getType();
- res = getNodeManager()->mkSeqUnit(type, *children[0].d_node);
- }
- else
- {
- res = d_nodeMgr->mkNode(k, echildren);
- }
+ // make the term
+ res = d_nodeMgr->mkNode(k, echildren);
}
(void)res.getType(true); /* kick off type checking */
#include "expr/skolem_manager.h"
#include "expr/type_checker.h"
#include "expr/type_properties.h"
-#include "theory/bags/bag_make_op.h"
-#include "theory/sets/singleton_op.h"
-#include "theory/strings/seq_unit_op.h"
#include "util/bitvector.h"
#include "util/poly_util.h"
#include "util/rational.h"
}
}
-Node NodeManager::mkSeqUnit(const TypeNode& t, const TNode n)
-{
- Assert(n.getType().isSubtypeOf(t))
- << "Invalid operands for mkSeqUnit. The type '" << n.getType()
- << "' of node '" << n << "' is not a subtype of '" << t << "'."
- << std::endl;
- Node op = mkConst(SeqUnitOp(t));
- Node sunit = mkNode(kind::SEQ_UNIT, op, n);
- return sunit;
-}
-
-Node NodeManager::mkSingleton(const TypeNode& t, const TNode n)
-{
- Assert(n.getType().isSubtypeOf(t))
- << "Invalid operands for mkSingleton. The type '" << n.getType()
- << "' of node '" << n << "' is not a subtype of '" << t << "'."
- << std::endl;
- Node op = mkConst(SetSingletonOp(t));
- Node singleton = mkNode(kind::SET_SINGLETON, op, n);
- return singleton;
-}
-
-Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m)
-{
- Assert(n.getType().isSubtypeOf(t))
- << "Invalid operands for mkBag. The type '" << n.getType()
- << "' of node '" << n << "' is not a subtype of '" << t << "'."
- << std::endl;
- Node op = mkConst(BagMakeOp(t));
- Node bag = mkNode(kind::BAG_MAKE, op, n, m);
- return bag;
-}
-
bool NodeManager::hasOperator(Kind k)
{
switch (kind::MetaKind mk = kind::metaKindOf(k))
/** make unique (per Type,Kind) variable. */
Node mkNullaryOperator(const TypeNode& type, Kind k);
- /**
- * Create a sequence unit from the given element n.
- * @param t the element type of the returned sequence.
- * Note that the type of n needs to be a subtype of t.
- * @param n the single element in the sequence.
- * @return a sequence unit constructed from the element n.
- */
- Node mkSeqUnit(const TypeNode& t, const TNode n);
-
- /**
- * Create a singleton set from the given element n.
- * @param t the element type of the returned set.
- * Note that the type of n needs to be a subtype of t.
- * @param n the single element in the singleton.
- * @return a singleton set constructed from the element n.
- */
- Node mkSingleton(const TypeNode& t, const TNode n);
-
- /**
- * Create a bag from the given element n along with its multiplicity m.
- * @param t the element type of the returned bag.
- * Note that the type of n needs to be a subtype of t.
- * @param n the element that is used to to construct the bag
- * @param m the multiplicity of the element n
- * @return a bag that contains m occurrences of n.
- */
- Node mkBag(const TypeNode& t, const TNode n, const TNode m);
-
/**
* Create a constant of type T. It will have the appropriate
* CONST_* kind defined for T.
std::vector<Node> vecu;
for (size_t i = 0, size = charVec.size(); i < size; i++)
{
- Node u = nm->mkSeqUnit(tn.getSequenceElementType(),
- postConvert(charVec[size - (i + 1)]));
+ Node u = nm->mkNode(SEQ_UNIT, postConvert(charVec[size - (i + 1)]));
if (size == 1)
{
// singleton case
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Mudathir Mohamed, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class for BAG_MAKE operator.
- */
-
-#include "bag_make_op.h"
-
-#include <iostream>
-
-#include "expr/type_node.h"
-
-namespace cvc5::internal {
-
-std::ostream& operator<<(std::ostream& out, const BagMakeOp& op)
-{
- return out << "(BagMakeOp " << op.getType() << ')';
-}
-
-size_t BagMakeOpHashFunction::operator()(const BagMakeOp& op) const
-{
- return std::hash<TypeNode>()(op.getType());
-}
-
-BagMakeOp::BagMakeOp(const TypeNode& elementType)
- : d_type(new TypeNode(elementType))
-{
-}
-
-BagMakeOp::BagMakeOp(const BagMakeOp& op) : d_type(new TypeNode(op.getType()))
-{
-}
-
-const TypeNode& BagMakeOp::getType() const { return *d_type; }
-
-bool BagMakeOp::operator==(const BagMakeOp& op) const
-{
- return getType() == op.getType();
-}
-
-} // namespace cvc5::internal
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Mudathir Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class for BAG_MAKE operator.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__BAG_MAKE_OP_H
-#define CVC5__BAG_MAKE_OP_H
-
-#include <memory>
-
-namespace cvc5::internal {
-
-class TypeNode;
-
-/**
- * The class is an operator for kind BAG_MAKE used to construct bags.
- * It specifies the type of the element especially when it is a constant.
- * e.g. the type of rational 1 is Int, however
- * (bag (BagMakeOp Real) 1) is of type (Bag Real), not (Bag Int).
- * Note that the type passed to the constructor is the element's type, not the
- * bag type.
- */
-class BagMakeOp
-{
- public:
- explicit BagMakeOp(const TypeNode& elementType);
- BagMakeOp(const BagMakeOp& op);
-
- /** return the type of the current object */
- const TypeNode& getType() const;
-
- bool operator==(const BagMakeOp& op) const;
-
- private:
- /** a pointer to the type of the bag element */
- std::unique_ptr<TypeNode> d_type;
-}; /* class BagMakeOp */
-
-std::ostream& operator<<(std::ostream& out, const BagMakeOp& op);
-
-/**
- * Hash function for the BagMakeOpHashFunction objects.
- */
-struct BagMakeOpHashFunction
-{
- size_t operator()(const BagMakeOp& op) const;
-}; /* struct BagMakeOpHashFunction */
-
-} // namespace cvc5::internal
-
-#endif /* CVC5__BAG_MAKE_OP_H */
combine_i.eqNode(nm->mkNode(APPLY_UF, f, uf_i, combine_iMinusOne));
Node unionDisjoint_0_equal =
unionDisjoint_0.eqNode(nm->mkConst(EmptyBag(bagType)));
- Node singleton = nm->mkBag(elementType, uf_i, one);
+ Node singleton = nm->mkNode(BAG_MAKE, uf_i, one);
Node unionDisjoint_i_equal = unionDisjoint_i.eqNode(
nm->mkNode(BAG_UNION_DISJOINT, singleton, unionDisjoint_iMinusOne));
nm->mkNode(ADD, uf_i_multiplicity, cardinality_iMinusOne));
Node unionDisjoint_0_equal =
unionDisjoint_0.eqNode(nm->mkConst(EmptyBag(bagType)));
- Node bag = nm->mkBag(elementType, uf_i, uf_i_multiplicity);
+ Node bag = nm->mkNode(BAG_MAKE, uf_i, uf_i_multiplicity);
Node unionDisjoint_i_equal = unionDisjoint_i.eqNode(
nm->mkNode(BAG_UNION_DISJOINT, bag, unionDisjoint_iMinusOne));
{
// (bag.duplicate_removal (bag x n)) = (bag x 1)
// where n is a positive constant
- Node bag = d_nm->mkBag(n[0][0].getType(), n[0][0], d_one);
+ Node bag = d_nm->mkNode(BAG_MAKE, n[0][0], d_one);
return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_BAG_MAKE);
}
return BagsRewriteResponse(n, Rewrite::NONE);
Assert(n.getKind() == BAG_FROM_SET);
if (n[0].getKind() == SET_SINGLETON)
{
- // (bag.from_set (set.singleton (SetSingletonOp Int) x)) = (bag x 1)
- TypeNode type = n[0].getType().getSetElementType();
- Node bag = d_nm->mkBag(type, n[0][0], d_one);
+ // (bag.from_set (set.singleton x)) = (bag x 1)
+ Node bag = d_nm->mkNode(BAG_MAKE, n[0][0], d_one);
return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON);
}
return BagsRewriteResponse(n, Rewrite::NONE);
if (n[0].getKind() == BAG_MAKE && n[0][1].isConst()
&& n[0][1].getConst<Rational>().sgn() == 1)
{
- // (bag.to_set (bag x n)) = (set.singleton (SetSingletonOp T) x)
+ // (bag.to_set (bag x n)) = (set.singleton x)
// where n is a positive constant and T is the type of the bag's elements
- Node set = d_nm->mkSingleton(n[0][0].getType(), n[0][0]);
+ Node set = d_nm->mkNode(SET_SINGLETON, n[0][0]);
return BagsRewriteResponse(set, Rewrite::TO_SINGLETON);
}
return BagsRewriteResponse(n, Rewrite::NONE);
{
// (bag.map f (bag x y)) = (bag (apply f x) y)
Node mappedElement = d_nm->mkNode(APPLY_UF, n[0], n[1][0]);
- Node ret =
- d_nm->mkBag(n[0].getType().getRangeType(), mappedElement, n[1][1]);
+ Node ret = d_nm->mkNode(BAG_MAKE, mappedElement, n[1][1]);
return BagsRewriteResponse(ret, Rewrite::MAP_BAG_MAKE);
}
/**
* rewrites for n include:
- * - (bag.from_set (singleton (SetSingletonOp Int) x)) = (bag x 1)
+ * - (bag.from_set (set.singleton x)) = (bag x 1)
*/
BagsRewriteResponse rewriteFromSet(const TNode& n) const;
/**
* rewrites for n include:
- * - (bag.to_set (bag x n)) = (singleton (SetSingletonOp T) x)
+ * - (bag.to_set (bag x n)) = (set.singleton x)
* where n is a positive constant and T is the type of the bag's elements
*/
BagsRewriteResponse rewriteToSet(const TNode& n) const;
}
TypeNode elementType = t.getBagElementType();
std::map<Node, Rational>::const_reverse_iterator it = elements.rbegin();
- Node bag = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second));
+ Node bag = nm->mkNode(BAG_MAKE, it->first, nm->mkConstInt(it->second));
while (++it != elements.rend())
{
- Node n = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second));
+ Node n = nm->mkNode(BAG_MAKE, it->first, nm->mkConstInt(it->second));
bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag);
}
return bag;
}
TypeNode elementType = t.getBagElementType();
std::map<Node, Node>::const_reverse_iterator it = elements.rbegin();
- Node bag = nm->mkBag(elementType, it->first, it->second);
+ Node bag = nm->mkNode(BAG_MAKE, it->first, it->second);
while (++it != elements.rend())
{
- Node n = nm->mkBag(elementType, it->first, it->second);
+ Node n = nm->mkNode(BAG_MAKE, it->first, it->second);
bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag);
}
return bag;
for (const auto& [e, count] : elements)
{
Node multiplicity = nm->mkConstInt(count);
- Node bag = nm->mkBag(bagType.getBagElementType(), e, multiplicity);
+ Node bag = nm->mkNode(BAG_MAKE, e, multiplicity);
Node pOfe = nm->mkNode(APPLY_UF, P, e);
Node ite = nm->mkNode(ITE, pOfe, bag, empty);
bags.push_back(ite);
std::vector<Node> bags;
for (const Node& node : eqc)
{
- Node bag = nm->mkBag(
- bagType.getBagElementType(), node, nm->mkConstInt(elements[node]));
+ Node bag = nm->mkNode(BAG_MAKE, node, nm->mkConstInt(elements[node]));
bags.push_back(bag);
}
Node part = computeDisjointUnion(bagType, bags);
operator BAG_MEMBER 2 "bag membership predicate; is first parameter a member of second?"
operator BAG_DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)"
-constant BAG_MAKE_OP \
- class \
- BagMakeOp \
- ::cvc5::internal::BagMakeOpHashFunction \
- "theory/bags/bag_make_op.h" \
- "operator for BAG_MAKE; payload is an instance of the cvc5::internal::BagMakeOp class"
-parameterized BAG_MAKE BAG_MAKE_OP 2 \
-"constructs a bag from one element along with its multiplicity"
+operator BAG_MAKE 2 "constructs a bag from one element along with its multiplicity"
# The operator bag-is-singleton returns whether the given bag is a singleton
operator BAG_IS_SINGLETON 1 "return whether the given bag is a singleton"
typerule BAG_COUNT ::cvc5::internal::theory::bags::CountTypeRule
typerule BAG_MEMBER ::cvc5::internal::theory::bags::MemberTypeRule
typerule BAG_DUPLICATE_REMOVAL ::cvc5::internal::theory::bags::DuplicateRemovalTypeRule
-typerule BAG_MAKE_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BAG_MAKE ::cvc5::internal::theory::bags::BagMakeTypeRule
typerule BAG_EMPTY ::cvc5::internal::theory::bags::EmptyBagTypeRule
typerule BAG_CARD ::cvc5::internal::theory::bags::CardTypeRule
Trace("bags-model") << "newElement is " << newElement << std::endl;
Rational difference = rCardRational - constructedRational;
Node multiplicity = nm->mkConstInt(difference);
- Node slackBag = nm->mkBag(elementType, newElement, multiplicity);
+ Node slackBag = nm->mkNode(BAG_MAKE, newElement, multiplicity);
constructedBag =
nm->mkNode(kind::BAG_UNION_DISJOINT, constructedBag, slackBag);
constructedBag = rewrite(constructedBag);
// return (bag d_element 1)
Node one = d_nodeManager->mkConstInt(Rational(1));
TypeNode elementType = d_elementTypeEnumerator.getType();
- Node singleton = d_nodeManager->mkBag(elementType, d_element, one);
+ Node singleton = d_nodeManager->mkNode(BAG_MAKE, d_element, one);
d_currentBag = singleton;
}
else
#include "expr/dtype_cons.h"
#include "expr/emptybag.h"
#include "table_project_op.h"
-#include "theory/bags/bag_make_op.h"
#include "theory/bags/bags_utils.h"
#include "theory/datatypes/tuple_project_op.h"
#include "theory/datatypes/tuple_utils.h"
TypeNode BagMakeTypeRule::computeType(NodeManager* nm, TNode n, bool check)
{
- Assert(n.getKind() == kind::BAG_MAKE && n.hasOperator()
- && n.getOperator().getKind() == kind::BAG_MAKE_OP);
- BagMakeOp op = n.getOperator().getConst<BagMakeOp>();
- TypeNode expectedElementType = op.getType();
+ Assert(n.getKind() == kind::BAG_MAKE);
+ TypeNode actualElementType = n[0].getType(check);
if (check)
{
if (n.getNumChildren() != 2)
ss << "BAG_MAKE expects an integer for " << n[1] << ". Found" << type1;
throw TypeCheckingExceptionPrivate(n, ss.str());
}
-
- TypeNode actualElementType = n[0].getType(check);
- // the type of the element should be a subtype of the type of the operator
- // e.g. (bag (bag_op Real) 1 1) where 1 is an Int
- if (actualElementType != expectedElementType)
- {
- std::stringstream ss;
- ss << "The type '" << actualElementType
- << "' of the element is not type of '" << expectedElementType
- << "' in term : " << n;
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
}
- return nm->mkBagType(expectedElementType);
+ return nm->mkBagType(actualElementType);
}
bool BagMakeTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
Assert(i < d_setm_choice[sro].size());
choice_i = d_setm_choice[sro][i];
choices.push_back(choice_i);
- Node sChoiceI = nm->mkSingleton(choice_i.getType(), choice_i);
+ Node sChoiceI = nm->mkNode(SET_SINGLETON, choice_i);
if (nsr.isNull())
{
nsr = sChoiceI;
Trace("sygus-grammar-def") << "...add for seq.unit" << std::endl;
std::vector<TypeNode> cargsSeqUnit;
cargsSeqUnit.push_back(unresElemType);
- // lambda x . (seq.unit (seq_unit_op T) x) where T = x.getType()
- Node x = nm->mkBoundVar(etype);
- Node vars = nm->mkNode(BOUND_VAR_LIST, x);
- Node seqUnit = nm->mkSeqUnit(etype, x);
- Node lambda = nm->mkNode(LAMBDA, vars, seqUnit);
- sdts[i].addConstructor(lambda, "seq.unit", cargsSeqUnit);
+ sdts[i].addConstructor(SEQ_UNIT, cargsSeqUnit);
}
}
else if (types[i].isArray())
Trace("sygus-grammar-def") << "...add for singleton" << std::endl;
std::vector<TypeNode> cargsSingleton;
cargsSingleton.push_back(unresElemType);
-
- // lambda x . (singleton (singleton_op T) x) where T = x.getType()
- Node x = nm->mkBoundVar(etype);
- Node vars = nm->mkNode(BOUND_VAR_LIST, x);
- Node singleton = nm->mkSingleton(etype, x);
- Node lambda = nm->mkNode(LAMBDA,vars, singleton);
- sdts[i].addConstructor(lambda, "singleton", cargsSingleton);
+ sdts[i].addConstructor(SET_SINGLETON, cargsSingleton);
// add for union, difference, intersection
std::vector<Kind> bin_kinds = {SET_UNION, SET_INTER, SET_MINUS};
{
NodeManager* nm = NodeManager::currentNM();
// (SEP_LABEL (sep.pto x y) L) => L = (set.singleton x)
- Node s = nm->mkSingleton(slbl.getType().getSetElementType(), satom[0]);
+ Node s = nm->mkNode(SET_SINGLETON, satom[0]);
Node eq = slbl.eqNode(s);
TrustNode trn =
d_im.mkLemmaExp(eq, PfRule::THEORY_INFERENCE, {fact}, {fact}, {eq});
}
else if (satom.getKind() == SEP_PTO)
{
- // TODO(project##230): Find a safe type for the singleton operator
- Node ss = nm->mkSingleton(satom[0].getType(), satom[0]);
+ Node ss = nm->mkNode(SET_SINGLETON, satom[0]);
if (slbl != ss)
{
conc = slbl.eqNode(ss);
for( unsigned i=0; i<locs.size(); i++ ){
Node s = locs[i];
Assert(!s.isNull());
- s = NodeManager::currentNM()->mkSingleton(tn, s);
+ s = NodeManager::currentNM()->mkNode(SET_SINGLETON, s);
if( u.isNull() ){
u = s;
}else{
std::map<Node, bool>& active_lbl,
unsigned ind)
{
+ NodeManager* nm = NodeManager::currentNM();
Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl;
if (options().sep.sepMinimalRefine && lbl != o_lbl
&& active_lbl.find(lbl) != active_lbl.end())
//check if this pto reference is in the base label, if not, then it does not need to be added as an assumption
Assert(d_label_model.find(o_lbl) != d_label_model.end());
Node vr = d_valuation.getModel()->getRepresentative( n[0] );
- // TODO(project##230): Find a safe type for the singleton operator
- Node svr = NodeManager::currentNM()->mkSingleton(vr.getType(), vr);
+ Node svr = nm->mkNode(SET_SINGLETON, vr);
bool inBaseHeap = std::find( d_label_model[o_lbl].d_heap_locs_model.begin(), d_label_model[o_lbl].d_heap_locs_model.end(), svr )!=d_label_model[o_lbl].d_heap_locs_model.end();
Trace("sep-inst-debug") << "Is in base (non-instantiating) heap : " << inBaseHeap << " for value ref " << vr << " in " << o_lbl << std::endl;
std::vector< Node > children;
if( inBaseHeap ){
- // TODO(project##230): Find a safe type for the singleton operator
- Node s = NodeManager::currentNM()->mkSingleton(n[0].getType(), n[0]);
+ Node s = nm->mkNode(SET_SINGLETON, n[0]);
children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, n[0], n[1] ), s ) );
}else{
//look up value of data
Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl;
}
}
- // TODO(project##230): Find a safe type for the singleton operator
- Node singleton = NodeManager::currentNM()->mkSingleton(n[0].getType(), n[0]);
+ Node singleton = nm->mkNode(SET_SINGLETON, n[0]);
children.push_back(singleton.eqNode(lbl_v));
Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) );
Trace("sep-inst-debug") << "Return " << ret << std::endl;
void TheorySep::computeLabelModel( Node lbl ) {
if( !d_label_model[lbl].d_computed ){
d_label_model[lbl].d_computed = true;
-
+ NodeManager* nm = NodeManager::currentNM();
//we must get the value of lbl from the model: this is being run at last call, after the model is constructed
//Assert(...); TODO
Node v_val = d_valuation.getModel()->getRepresentative( lbl );
}else{
tt = itm->second;
}
- // TODO(project##230): Find a safe type for the singleton operator
- Node stt = NodeManager::currentNM()->mkSingleton(tt.getType(), tt);
+ Node stt = nm->mkNode(SET_SINGLETON, tt);
Trace("sep-process-debug") << "...model : add " << tt << " for " << u << " in lbl " << lbl << std::endl;
d_label_model[lbl].d_heap_locs.push_back( stt );
}
// the current members of this finite type.
Node slack = sm->mkDummySkolem("slack", elementType);
- Node singleton = nm->mkSingleton(elementType, slack);
+ Node singleton = nm->mkNode(SET_SINGLETON, slack);
els.push_back(singleton);
d_finite_type_slack_elements[elementType].push_back(slack);
Trace("sets-model") << "Added slack element " << slack << " to set "
}
else
{
- els.push_back(nm->mkSingleton(
- elementType, sm->mkDummySkolem("msde", elementType)));
+ els.push_back(nm->mkNode(SET_SINGLETON,
+ sm->mkDummySkolem("msde", elementType)));
}
}
}
operator SET_SUBSET 2 "subset predicate; first parameter a subset of second"
operator SET_MEMBER 2 "set membership predicate; first parameter a member of second"
-constant SET_SINGLETON_OP \
- class \
- SetSingletonOp \
- ::cvc5::internal::SetSingletonOpHashFunction \
- "theory/sets/singleton_op.h" \
- "operator for singletons; payload is an instance of the cvc5::internal::SingletonOp class"
-parameterized SET_SINGLETON SET_SINGLETON_OP 1 \
-"constructs a set of a single element. First parameter is a SingletonOp. Second is a term"
+operator SET_SINGLETON 1 "constructs a set of a single element. First parameter is a term"
operator SET_INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
operator SET_CARD 1 "set cardinality operator"
typerule SET_MINUS ::cvc5::internal::theory::sets::SetsBinaryOperatorTypeRule
typerule SET_SUBSET ::cvc5::internal::theory::sets::SubsetTypeRule
typerule SET_MEMBER ::cvc5::internal::theory::sets::MemberTypeRule
-typerule SET_SINGLETON_OP "SimpleTypeRule<RBuiltinOperator>"
typerule SET_SINGLETON ::cvc5::internal::theory::sets::SingletonTypeRule
typerule SET_EMPTY ::cvc5::internal::theory::sets::EmptySetTypeRule
typerule SET_INSERT ::cvc5::internal::theory::sets::InsertTypeRule
}
else
{
- TypeNode elementType = setType.getSetElementType();
ElementsIterator it = elements.begin();
- Node cur = nm->mkSingleton(elementType, *it);
+ Node cur = nm->mkNode(kind::SET_SINGLETON, *it);
while (++it != elements.end())
{
- Node singleton = nm->mkSingleton(elementType, *it);
+ Node singleton = nm->mkNode(kind::SET_SINGLETON, *it);
cur = nm->mkNode(kind::SET_UNION, singleton, cur);
}
return cur;
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Mudathir Mohamed, Aina Niemetz, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class for singleton operator for sets.
- */
-
-#include "theory/sets/singleton_op.h"
-
-#include <iostream>
-
-#include "expr/type_node.h"
-
-namespace cvc5::internal {
-
-std::ostream& operator<<(std::ostream& out, const SetSingletonOp& op)
-{
- return out << "(SetSingletonOp " << op.getType() << ')';
-}
-
-size_t SetSingletonOpHashFunction::operator()(const SetSingletonOp& op) const
-{
- return std::hash<TypeNode>()(op.getType());
-}
-
-SetSingletonOp::SetSingletonOp(const TypeNode& elementType)
- : d_type(new TypeNode(elementType))
-{
-}
-
-SetSingletonOp::SetSingletonOp(const SetSingletonOp& op)
- : d_type(new TypeNode(op.getType()))
-{
-}
-
-const TypeNode& SetSingletonOp::getType() const { return *d_type; }
-
-bool SetSingletonOp::operator==(const SetSingletonOp& op) const
-{
- return getType() == op.getType();
-}
-
-} // namespace cvc5::internal
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class for singleton operator for sets.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__THEORY__SETS__SINGLETON_OP_H
-#define CVC5__THEORY__SETS__SINGLETON_OP_H
-
-#include <memory>
-
-namespace cvc5::internal {
-
-class TypeNode;
-
-/**
- * The class is an operator for kind SET_SINGLETON used to construct singleton
- * sets. It specifies the type of the single element especially when it is a
- * constant. e.g. the type of rational 1 is Int, however (singleton
- * (singleton_op Real) 1) is of type (Set Real), not (Set Int). Note that the
- * type passed to the constructor is the element's type, not the set type.
- */
-class SetSingletonOp
-{
- public:
- SetSingletonOp(const TypeNode& elementType);
- SetSingletonOp(const SetSingletonOp& op);
-
- /** return the type of the current object */
- const TypeNode& getType() const;
-
- bool operator==(const SetSingletonOp& op) const;
-
- private:
- SetSingletonOp();
- /** a pointer to the type of the singleton element */
- std::unique_ptr<TypeNode> d_type;
-}; /* class SetSingletonOp */
-
-std::ostream& operator<<(std::ostream& out, const SetSingletonOp& op);
-
-/**
- * Hash function for the SetSingletonOp objects.
- */
-struct SetSingletonOpHashFunction
-{
- size_t operator()(const SetSingletonOp& op) const;
-}; /* struct SetSingletonOpHashFunction */
-
-} // namespace cvc5::internal
-
-#endif /* CVC5__THEORY__SETS__SINGLETON_OP_H */
const std::map<Node, Node>& emems = d_state.getMembers(eqc);
if (!emems.empty())
{
- TypeNode elementType = eqc.getType().getSetElementType();
for (const std::pair<const Node, Node>& itmm : emems)
{
// when we have y -> (set.member x S) where rep(x)=y, we use x
// in the model here. Using y may not be legal with respect to
// subtyping, since y may be real where x is an int.
- Node t = nm->mkSingleton(elementType, itmm.second[0]);
+ Node t = nm->mkNode(SET_SINGLETON, itmm.second[0]);
els.push_back(t);
}
}
TypeNode setType = set.getType();
ensureFirstClassSetType(setType);
Node boundVar = nm->mkBoundVar(setType.getSetElementType());
- Node singleton = nm->mkSingleton(setType.getSetElementType(), boundVar);
+ Node singleton = nm->mkNode(SET_SINGLETON, boundVar);
Node equal = set.eqNode(singleton);
std::vector<Node> variables = {boundVar};
Node boundVars = nm->mkNode(BOUND_VAR_LIST, variables);
Node element = TupleUtils::nthElementOfTuple(eqc_node, i);
if (!element.isConst())
{
- makeSharedTerm(element, tupleTypes[i]);
+ makeSharedTerm(element);
}
}
}
fact =
NodeManager::currentNM()->mkNode(kind::SET_MEMBER, mem2, join_rel[1]);
sendInfer(fact, InferenceId::SETS_RELS_JOIN_SPLIT_2, reason);
- makeSharedTerm(shared_x, shared_type);
+ makeSharedTerm(shared_x);
}
/*
// 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.
- makeSharedTerm(r1_rmost, r1_rmost.getType());
- makeSharedTerm(r2_lmost, r2_lmost.getType());
+ makeSharedTerm(r1_rmost);
+ makeSharedTerm(r2_lmost);
Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost
<< " of type " << r1_rmost.getType() << std::endl;
}
else if (!atn.isBoolean())
{
- // TODO(project##230): Find a safe type for the singleton operator
- makeSharedTerm(a, atn);
- makeSharedTerm(b, b.getType());
+ makeSharedTerm(a);
+ makeSharedTerm(b);
}
return false;
}
return false;
}
- void TheorySetsRels::makeSharedTerm(Node n, TypeNode t)
+ void TheorySetsRels::makeSharedTerm(Node n)
{
if (d_shared_terms.find(n) != d_shared_terms.end())
{
}
Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl;
// force a proxy lemma to be sent for the singleton containing n
- Node ss = NodeManager::currentNM()->mkSingleton(t, n);
+ Node ss = NodeManager::currentNM()->mkNode(SET_SINGLETON, n);
d_treg.getProxy(ss);
d_shared_terms.insert(n);
}
for (unsigned int i = 0; i < n[0].getType().getTupleLength(); i++)
{
Node element = TupleUtils::nthElementOfTuple(n[0], i);
- makeSharedTerm(element, tupleTypes[i]);
+ makeSharedTerm(element);
tuple_elements.push_back(element);
}
Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
/** Helper functions */
bool hasTerm( Node a );
- void makeSharedTerm(Node, TypeNode t);
+ void makeSharedTerm(Node a);
void reduceTupleVar( Node );
bool hasMember( Node, Node );
void computeTupleReps( Node );
else if (k == kind::SET_INSERT)
{
size_t setNodeIndex = node.getNumChildren()-1;
- TypeNode elementType = node[setNodeIndex].getType().getSetElementType();
- Node insertedElements = nm->mkSingleton(elementType, node[0]);
+ Node insertedElements = nm->mkNode(SET_SINGLETON, node[0]);
for (size_t i = 1; i < setNodeIndex; ++i)
{
- Node singleton = nm->mkSingleton(elementType, node[i]);
+ Node singleton = nm->mkNode(SET_SINGLETON, node[i]);
insertedElements =
nm->mkNode(kind::SET_UNION, insertedElements, singleton);
}
Assert(n.getKind() == kind::SET_MAP);
NodeManager* nm = NodeManager::currentNM();
Kind k = n[1].getKind();
- TypeNode rangeType = n[0].getType().getRangeType();
switch (k)
{
case SET_EMPTY:
{
+ TypeNode rangeType = n[0].getType().getRangeType();
// (set.map f (as set.empty (Set T1)) = (as set.empty (Set T2))
Node ret = nm->mkConst(EmptySet(nm->mkSetType(rangeType)));
return RewriteResponse(REWRITE_DONE, ret);
{
// (set.map f (set.singleton x)) = (set.singleton (f x))
Node mappedElement = nm->mkNode(APPLY_UF, n[0], n[1][0]);
- Node ret = nm->mkSingleton(rangeType, mappedElement);
+ Node ret = nm->mkNode(SET_SINGLETON, mappedElement);
return RewriteResponse(REWRITE_AGAIN_FULL, ret);
}
case SET_UNION:
// get a new element and return it as a singleton set
Node element = *d_elementEnumerator;
d_elementsSoFar.push_back(element);
- TypeNode elementType = d_elementEnumerator.getType();
- d_currentSet = d_nodeManager->mkSingleton(elementType, element);
+ d_currentSet = d_nodeManager->mkNode(kind::SET_SINGLETON, element);
d_elementEnumerator++;
}
else
#include <sstream>
#include "theory/sets/normal_form.h"
-#include "theory/sets/singleton_op.h"
#include "util/cardinality.h"
namespace cvc5::internal {
TNode n,
bool check)
{
- Assert(n.getKind() == kind::SET_SINGLETON && n.hasOperator()
- && n.getOperator().getKind() == kind::SET_SINGLETON_OP);
-
- const SetSingletonOp& op = n.getOperator().getConst<SetSingletonOp>();
- TypeNode type1 = op.getType();
- if (check)
- {
- TypeNode type2 = n[0].getType(check);
- // the type of the element should be a subtype of the type of the operator
- // e.g. (set.singleton (SetSingletonOp Real) 1) where 1 is an Int
- if (type1 != type2)
- {
- std::stringstream ss;
- ss << "The type '" << type2 << "' of the element is not a type of '"
- << type1 << "' in term : " << n;
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- }
+ Assert(n.getKind() == kind::SET_SINGLETON);
+ TypeNode type1 = n[0].getType(check);
return nodeManager->mkSetType(type1);
}
};
/**
- * Type rule for (set.singleton (SetSingletonOp t) x) to check the sort of x
+ * Type rule for (set.singleton x) to check the sort of x
* matches the sort t.
*/
struct SingletonTypeRule
Node cond1 = nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), n[1]);
Node cond2 = nm->mkNode(LT, n[1], nm->mkNode(STRING_LENGTH, n[0]));
Node cond = nm->mkNode(AND, cond1, cond2);
- TypeNode etn = n.getType().getSequenceElementType();
Node body1 = nm->mkNode(
- EQUAL, n, nm->mkSeqUnit(etn, nm->mkNode(SEQ_NTH, n[0], n[1])));
+ EQUAL, n, nm->mkNode(SEQ_UNIT, nm->mkNode(SEQ_NTH, n[0], n[1])));
Node body2 = nm->mkNode(EQUAL, n, Word::mkEmptyWord(n.getType()));
Node lem = nm->mkNode(ITE, cond, body1, body2);
sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_EXTRACT);
"expr/sequence.h" \
"a sequence of characters"
-constant SEQ_UNIT_OP \
- class \
- SeqUnitOp \
- ::cvc5::internal::SeqUnitOpHashFunction \
- "theory/strings/seq_unit_op.h" \
- "operator for sequence units; payload is an instance of the cvc5::internal::SeqUnitOp class"
-parameterized SEQ_UNIT SEQ_UNIT_OP 1 \
-"a sequence of length one. First parameter is a SeqUnitOp. Second is a term"
-
+operator SEQ_UNIT 1 "a sequence of length one. First parameter is a term"
operator SEQ_NTH 2 "The nth element of a sequence"
# equal equal / less than / output
### sequence specific operators
typerule CONST_SEQUENCE ::cvc5::internal::theory::strings::ConstSequenceTypeRule
-typerule SEQ_UNIT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule SEQ_UNIT ::cvc5::internal::theory::strings::SeqUnitTypeRule
typerule SEQ_NTH ::cvc5::internal::theory::strings::SeqNthTypeRule
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class for sequence unit
- */
-
-#include "theory/strings/seq_unit_op.h"
-
-#include <iostream>
-
-#include "expr/type_node.h"
-
-namespace cvc5::internal {
-
-std::ostream& operator<<(std::ostream& out, const SeqUnitOp& op)
-{
- return out << "(SeqUnitOp " << op.getType() << ')';
-}
-
-size_t SeqUnitOpHashFunction::operator()(const SeqUnitOp& op) const
-{
- return std::hash<TypeNode>()(op.getType());
-}
-
-SeqUnitOp::SeqUnitOp(const TypeNode& elementType)
- : d_type(new TypeNode(elementType))
-{
-}
-
-SeqUnitOp::SeqUnitOp(const SeqUnitOp& op) : d_type(new TypeNode(op.getType()))
-{
-}
-
-const TypeNode& SeqUnitOp::getType() const { return *d_type; }
-
-bool SeqUnitOp::operator==(const SeqUnitOp& op) const
-{
- return getType() == op.getType();
-}
-
-} // namespace cvc5::internal
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Mudathir Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class for sequence unit
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H
-#define CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H
-
-#include <memory>
-
-namespace cvc5::internal {
-
-class TypeNode;
-
-/**
- * The class is an operator for kind SEQ_UNIT used to construct sequences
- * of length one. It specifies the type of the single element especially when it
- * is a constant. e.g. the type of rational 1 is Int, however (seq.unit
- * (seq_unit_op Real) 1) is of type (Seq Real), not (Seq Int). Note that the
- * type passed to the constructor is the element's type, not the sequence type.
- */
-class SeqUnitOp
-{
- public:
- SeqUnitOp(const TypeNode& elementType);
- SeqUnitOp(const SeqUnitOp& op);
-
- /** return the type of the current object */
- const TypeNode& getType() const;
-
- bool operator==(const SeqUnitOp& op) const;
-
- private:
- SeqUnitOp();
- /** a pointer to the type of the singleton element */
- std::unique_ptr<TypeNode> d_type;
-}; /* class SeqUnitOp */
-
-std::ostream& operator<<(std::ostream& out, const SeqUnitOp& op);
-
-/**
- * Hash function for the SeqUnitOp objects.
- */
-struct SeqUnitOpHashFunction
-{
- size_t operator()(const SeqUnitOp& op) const;
-}; /* struct SeqUnitOpHashFunction */
-
-} // namespace cvc5::internal
-
-#endif /* CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H */
argVal = nfe.d_nf[0][0];
}
Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0];
- assignedValue = rewrite(
- nm->mkSeqUnit(eqc.getType().getSequenceElementType(), argVal));
+ assignedValue = rewrite(nm->mkNode(SEQ_UNIT, argVal));
Trace("strings-model")
<< "-> assign via seq.unit: " << assignedValue << std::endl;
}
continue;
}
usedWrites.insert(ivalue);
- Node wsunit = nm->mkSeqUnit(etype, w.second);
+ Node wsunit = nm->mkNode(SEQ_UNIT, w.second);
writes.emplace_back(ivalue, wsunit);
}
// sort based on index value
Node v = bvm->mkBoundVar<SeqModelVarAttribute>(snv, etn);
// use a skolem, not a bound variable
Node kv = sm->mkPurifySkolem(v, "smv");
- skChildren.push_back(nm->mkSeqUnit(etn, kv));
+ skChildren.push_back(nm->mkNode(SEQ_UNIT, kv));
}
return utils::mkConcat(skChildren, c.getType());
}
cacheVals.push_back(nm->mkConstInt(Rational(currIndex)));
Node kv = sm->mkSkolemFunction(
SkolemFunId::SEQ_MODEL_BASE_ELEMENT, etn, cacheVals);
- skChildren.push_back(nm->mkSeqUnit(etn, kv));
+ skChildren.push_back(nm->mkNode(SEQ_UNIT, kv));
cacheVals.pop_back();
}
return utils::mkConcat(skChildren, r.getType());
// nodes for the case where `seq.nth` is defined.
Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre");
Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
- Node unit = nm->mkSeqUnit(t.getType(), skt);
+ Node unit = nm->mkNode(SEQ_UNIT, skt);
Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, unit, sk2));
// length of first skolem is second argument
Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
#include "expr/node_manager.h"
#include "expr/sequence.h"
#include "options/strings_options.h"
-#include "theory/strings/seq_unit_op.h"
#include "util/cardinality.h"
namespace cvc5::internal {
TNode n,
bool check)
{
- Assert(n.getKind() == kind::SEQ_UNIT && n.hasOperator()
- && n.getOperator().getKind() == kind::SEQ_UNIT_OP);
-
- const SeqUnitOp& op = n.getOperator().getConst<SeqUnitOp>();
- TypeNode otype = op.getType();
- if (check)
- {
- TypeNode argType = n[0].getType(check);
- // the type of the element should be a subtype of the type of the operator
- // e.g. (seq.unit (SeqUnitOp Real) 1) where 1 is an Int
- if (argType != otype)
- {
- std::stringstream ss;
- ss << "The type '" << argType << "' of the element is not the type of '"
- << otype << "' in term : " << n;
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- }
- return nodeManager->mkSequenceType(otype);
+ Assert(n.getKind() == kind::SEQ_UNIT);
+ TypeNode argType = n[0].getType(check);
+ return nodeManager->mkSequenceType(argType);
}
TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager,
return nm->mkNode(STRING_UNIT, n);
}
Assert(tn.isSequence());
- TypeNode etn = tn.getSequenceElementType();
- return nm->mkSeqUnit(etn, n);
+ return nm->mkNode(SEQ_UNIT, n);
}
Node getConstantComponent(Node t)
static_cast<uint64_t>(std::numeric_limits<uint32_t>::max()) + 1);
Node s01 = d_nodeManager->mkConst(Sequence(intType, {zero, one}));
- Node sx = d_nodeManager->mkSeqUnit(intType, x);
- Node sy = d_nodeManager->mkSeqUnit(intType, y);
- Node sz = d_nodeManager->mkSeqUnit(intType, z);
- Node sw = d_nodeManager->mkSeqUnit(intType, w);
- Node sv = d_nodeManager->mkSeqUnit(intType, v);
+ Node sx = d_nodeManager->mkNode(SEQ_UNIT, x);
+ Node sy = d_nodeManager->mkNode(SEQ_UNIT, y);
+ Node sz = d_nodeManager->mkNode(SEQ_UNIT, z);
+ Node sw = d_nodeManager->mkNode(SEQ_UNIT, w);
+ Node sv = d_nodeManager->mkNode(SEQ_UNIT, v);
Node xyz = d_nodeManager->mkNode(STRING_CONCAT, sx, sy, sz);
Node wv = d_nodeManager->mkNode(STRING_CONCAT, sw, sv);
Node one = d_nodeManager->mkConstInt(1);
Node three = d_nodeManager->mkConstInt(3);
- Node sx = d_nodeManager->mkSeqUnit(intType, x);
- Node sy = d_nodeManager->mkSeqUnit(intType, y);
- Node sz = d_nodeManager->mkSeqUnit(intType, z);
- Node sw = d_nodeManager->mkSeqUnit(intType, w);
- Node sv = d_nodeManager->mkSeqUnit(intType, v);
+ Node sx = d_nodeManager->mkNode(SEQ_UNIT, x);
+ Node sy = d_nodeManager->mkNode(SEQ_UNIT, y);
+ Node sz = d_nodeManager->mkNode(SEQ_UNIT, z);
+ Node sw = d_nodeManager->mkNode(SEQ_UNIT, w);
+ Node sv = d_nodeManager->mkNode(SEQ_UNIT, v);
Node xyz = d_nodeManager->mkNode(STRING_CONCAT, sx, sy, sz);
Node wv = d_nodeManager->mkNode(STRING_CONCAT, sw, sv);
TEST_F(TestTheoryWhiteBagsNormalForm, mkBag_constant_element)
{
std::vector<Node> elements = getNStrings(1);
- Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(-1)));
- Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(0)));
- Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(1)));
+ Node negative = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(-1)));
+ Node zero = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(0)));
+ Node positive = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(1)));
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node y_5 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5)));
- Node z_5 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(5)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node y_5 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(5)));
+ Node z_5 = d_nodeManager->mkNode(
+ BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(5)));
Node input1 = d_nodeManager->mkNode(BAG_COUNT, x, empty);
Node output1 = zero;
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_1 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node y_5 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node y_5 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(5)));
Node input2 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, x_4);
Node output2 = x_1;
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node x_3 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3)));
+ Node x_7 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7)));
+ Node z_2 = d_nodeManager->mkNode(
+ BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
std::vector<Node> elements = getNStrings(3);
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(2)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConstInt(Rational(3)));
- Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[2],
- d_nodeManager->mkConstInt(Rational(4)));
+ Node A = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(2)));
+ Node B = d_nodeManager->mkNode(
+ BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(3)));
+ Node C = d_nodeManager->mkNode(
+ BAG_MAKE, elements[2], d_nodeManager->mkConstInt(Rational(4)));
Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
// unionDisjointAB is already in a normal form
ASSERT_EQ(unionDisjointA_BC, rewrite(unionDisjointAB_C));
Node unionDisjointAA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, A);
- Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(4)));
+ Node AA = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(4)));
ASSERT_FALSE(unionDisjointAA.isConst());
ASSERT_TRUE(AA.isConst());
ASSERT_EQ(AA, rewrite(unionDisjointAA));
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node x_3 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3)));
+ Node x_7 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7)));
+ Node z_2 = d_nodeManager->mkNode(
+ BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node x_3 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3)));
+ Node x_7 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7)));
+ Node z_2 = d_nodeManager->mkNode(
+ BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_1 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node x_3 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3)));
+ Node x_7 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7)));
+ Node z_2 = d_nodeManager->mkNode(
+ BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_1 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node x_3 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3)));
+ Node x_7 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7)));
+ Node z_2 = d_nodeManager->mkNode(
+ BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
Node input1 = d_nodeManager->mkNode(BAG_CARD, empty);
Node output1 = d_nodeManager->mkConstInt(Rational(0));
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_1 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
Node input1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, empty);
Node output1 = falseNode;
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
- Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
- Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y);
+ Node xSingleton = d_nodeManager->mkNode(SET_SINGLETON, x);
+ Node ySingleton = d_nodeManager->mkNode(SET_SINGLETON, y);
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+ Node x_1 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1)));
+ Node y_1 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1)));
Node input2 = d_nodeManager->mkNode(BAG_FROM_SET, xSingleton);
Node output2 = x_1;
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
- Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
- Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y);
+ Node xSingleton = d_nodeManager->mkNode(SET_SINGLETON, x);
+ Node ySingleton = d_nodeManager->mkNode(SET_SINGLETON, y);
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
- Node y_5 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5)));
+ Node x_4 = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4)));
+ Node y_5 = d_nodeManager->mkNode(
+ BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(5)));
Node input2 = d_nodeManager->mkNode(BAG_TO_SET, x_4);
Node output2 = xSingleton;
Node y = elements[1];
Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->integerType());
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), y, d);
+ Node A = d_nodeManager->mkNode(BAG_MAKE, x, c);
+ Node B = d_nodeManager->mkNode(BAG_MAKE, y, d);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
Node emptyString = d_nodeManager->mkConst(String(""));
- Node constantBag =
- d_nodeManager->mkBag(d_nodeManager->stringType(),
- emptyString,
- d_nodeManager->mkConstInt(Rational(1)));
+ Node constantBag = d_nodeManager->mkNode(
+ BAG_MAKE, emptyString, d_nodeManager->mkConstInt(Rational(1)));
// (= A A) = true where A is a bag
Node n1 = A.eqNode(A);
TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element)
{
std::vector<Node> elements = getNStrings(1);
- Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(-1)));
- Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(0)));
- Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(1)));
+ Node negative = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(-1)));
+ Node zero = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(0)));
+ Node positive = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(1)));
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
{
Node skolem =
d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
- Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(),
- skolem,
- d_nodeManager->mkConstInt(Rational(-1)));
- Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
- skolem,
- d_nodeManager->mkConstInt(Rational(-1)));
- Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
- skolem,
- d_nodeManager->mkConstInt(Rational(0)));
- Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
- skolem,
- d_nodeManager->mkConstInt(Rational(1)));
+ Node variable = d_nodeManager->mkNode(
+ BAG_MAKE, skolem, d_nodeManager->mkConstInt(Rational(-1)));
+ Node negative = d_nodeManager->mkNode(
+ BAG_MAKE, skolem, d_nodeManager->mkConstInt(Rational(-1)));
+ Node zero = d_nodeManager->mkNode(
+ BAG_MAKE, skolem, d_nodeManager->mkConstInt(Rational(0)));
+ Node positive = d_nodeManager->mkNode(
+ BAG_MAKE, skolem, d_nodeManager->mkConstInt(Rational(1)));
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
&& response1.d_node == zero);
// (bag.count x (bag x c) = c, c > 0 is a constant
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, three);
+ Node bag = d_nodeManager->mkNode(BAG_MAKE, skolem, three);
Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag);
RewriteResponse response2 = d_rewriter->postRewrite(n2);
TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)
{
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
- Node bag = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(5)));
+ Node bag = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(5)));
// (bag.duplicate_removal (bag x n)) = (bag x 1)
Node n = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag);
RewriteResponse response = d_rewriter->postRewrite(n);
- Node noDuplicate = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
+ Node noDuplicate = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1)));
ASSERT_TRUE(response.d_node == noDuplicate
&& response.d_status == REWRITE_AGAIN_FULL);
}
std::vector<Node> elements = getNStrings(2);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConstInt(Rational(n + 1)));
+ Node A = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n)));
+ Node B = d_nodeManager->mkNode(
+ BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(n + 1)));
Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
std::vector<Node> elements = getNStrings(3);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConstInt(Rational(n + 1)));
- Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[2],
- d_nodeManager->mkConstInt(Rational(n + 2)));
+ Node A = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n)));
+ Node B = d_nodeManager->mkNode(
+ BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(n + 1)));
+ Node C = d_nodeManager->mkNode(
+ BAG_MAKE, elements[2], d_nodeManager->mkConstInt(Rational(n + 2)));
Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A);
std::vector<Node> elements = getNStrings(2);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConstInt(Rational(n + 1)));
+ Node A = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n)));
+ Node B = d_nodeManager->mkNode(
+ BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(n + 1)));
Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
std::vector<Node> elements = getNStrings(2);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConstInt(Rational(n + 1)));
+ Node A = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n)));
+ Node B = d_nodeManager->mkNode(
+ BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(n + 1)));
Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
std::vector<Node> elements = getNStrings(2);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConstInt(Rational(n + 1)));
+ Node A = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n)));
+ Node B = d_nodeManager->mkNode(
+ BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(n + 1)));
Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
{
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node c = d_nodeManager->mkConstInt(Rational(3));
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
+ Node bag = d_nodeManager->mkNode(BAG_MAKE, x, c);
// (bag.choose (bag x c)) = x where c is a constant > 0
Node n1 = d_nodeManager->mkNode(BAG_CHOOSE, bag);
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
Node zero = d_nodeManager->mkConstInt(Rational(0));
Node c = d_nodeManager->mkConstInt(Rational(3));
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
+ Node bag = d_nodeManager->mkNode(BAG_MAKE, x, c);
std::vector<Node> elements = getNStrings(2);
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(4)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConstInt(Rational(5)));
+ Node A = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(4)));
+ Node B = d_nodeManager->mkNode(
+ BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(5)));
Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
// (bag.card (as bag.empty (Bag String)) = 0
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
+ Node bag = d_nodeManager->mkNode(BAG_MAKE, x, c);
// (bag.is_singleton (as bag.empty (Bag String)) = false
Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag);
TEST_F(TestTheoryWhiteBagsRewriter, from_set)
{
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
- Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
+ Node singleton = d_nodeManager->mkNode(SET_SINGLETON, x);
// (bag.from_set (set.singleton (set.singleton_op Int) x)) = (bag x 1)
Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton);
RewriteResponse response = d_rewriter->postRewrite(n);
Node one = d_nodeManager->mkConstInt(Rational(1));
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, one);
+ Node bag = d_nodeManager->mkNode(BAG_MAKE, x, one);
ASSERT_TRUE(response.d_node == bag
&& response.d_status == REWRITE_AGAIN_FULL);
}
TEST_F(TestTheoryWhiteBagsRewriter, to_set)
{
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
- Node bag = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(5)));
+ Node bag = d_nodeManager->mkNode(
+ BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(5)));
// (bag.to_set (bag x n)) = (set.singleton (set.singleton_op T) x)
Node n = d_nodeManager->mkNode(BAG_TO_SET, bag);
RewriteResponse response = d_rewriter->postRewrite(n);
- Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
+ Node singleton = d_nodeManager->mkNode(SET_SINGLETON, x);
ASSERT_TRUE(response.d_node == singleton
&& response.d_status == REWRITE_AGAIN_FULL);
}
std::vector<Node> elements = getNStrings(2);
Node a = d_nodeManager->mkConst(String("a"));
Node b = d_nodeManager->mkConst(String("b"));
- Node A = d_nodeManager->mkBag(
- d_nodeManager->stringType(), a, d_nodeManager->mkConstInt(Rational(3)));
- Node B = d_nodeManager->mkBag(
- d_nodeManager->stringType(), b, d_nodeManager->mkConstInt(Rational(4)));
+ Node A = d_nodeManager->mkNode(
+ BAG_MAKE, a, d_nodeManager->mkConstInt(Rational(3)));
+ Node B = d_nodeManager->mkNode(
+ BAG_MAKE, b, d_nodeManager->mkConstInt(Rational(4)));
Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
ASSERT_TRUE(unionDisjointAB.isConst());
// (bag "" 7))
Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB);
Node rewritten = Rewriter::rewrite(n2);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- empty,
- d_nodeManager->mkConstInt(Rational(7)));
+ Node bag = d_nodeManager->mkNode(
+ BAG_MAKE, empty, d_nodeManager->mkConstInt(Rational(7)));
// - (bag.map f (bag.union_disjoint K1 K2)) =
// (bag.union_disjoint (bag.map f K1) (bag.map f K2))
Node k1 = d_skolemManager->mkDummySkolem("K1", A.getType());
f = d_nodeManager->mkNode(LAMBDA, xy, sum);
Node xSkolem = d_nodeManager->getSkolemManager()->mkDummySkolem(
"x", d_nodeManager->integerType());
- Node bag = d_nodeManager->mkBag(d_nodeManager->integerType(), xSkolem, n);
+ Node bag = d_nodeManager->mkNode(BAG_MAKE, xSkolem, n);
Node node2 = d_nodeManager->mkNode(BAG_FOLD, f, one, bag);
Node apply_f_once = d_nodeManager->mkNode(APPLY_UF, f, xSkolem, one);
Node apply_f_twice =
&& response2.d_status == REWRITE_AGAIN_FULL);
// (bag.fold (lambda ((x Int)(y Int)) (+ x y)) 1 (bag 10 2)) = 21
- bag = d_nodeManager->mkBag(d_nodeManager->integerType(), ten, n);
+ bag = d_nodeManager->mkNode(BAG_MAKE, ten, n);
Node node3 = d_nodeManager->mkNode(BAG_FOLD, f, one, bag);
Node result3 = d_nodeManager->mkConstInt(Rational(21));
Node response3 = Rewriter::rewrite(node3);
TEST_F(TestTheoryWhiteBagsTypeRule, count_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(100)));
+ Node bag = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(100)));
Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag);
Node node = d_nodeManager->mkConstInt(Rational(10));
TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(10)));
+ Node bag = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(10)));
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag));
ASSERT_EQ(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag).getType(),
bag.getType());
TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(-1)));
- Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(0)));
- Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(1)));
+ Node negative = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(-1)));
+ Node zero = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(0)));
+ Node positive = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(1)));
// only positive multiplicity are constants
ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, negative));
TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node set =
- d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]);
+ Node set = d_nodeManager->mkNode(SET_SINGLETON, elements[0]);
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_FROM_SET, set));
ASSERT_TRUE(d_nodeManager->mkNode(BAG_FROM_SET, set).getType().isBag());
}
TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(10)));
+ Node bag = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(10)));
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag));
ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet());
}
TEST_F(TestTheoryWhiteBagsTypeRule, map_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConstInt(Rational(10)));
- Node set =
- d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]);
+ Node bag = d_nodeManager->mkNode(
+ BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(10)));
+ Node set = d_nodeManager->mkNode(SET_SINGLETON, elements[0]);
Node x1 = d_nodeManager->mkBoundVar("x", d_nodeManager->stringType());
Node length = d_nodeManager->mkNode(STRING_LENGTH, x1);
Node a = d_nodeManager->mkConst(String("a"));
Node b = d_nodeManager->mkConst(String("b"));
- Node A = d_nodeManager->mkSingleton(d_nodeManager->stringType(), a);
- Node B = d_nodeManager->mkSingleton(d_nodeManager->stringType(), b);
+ Node A = d_nodeManager->mkNode(SET_SINGLETON, a);
+ Node B = d_nodeManager->mkNode(SET_SINGLETON, b);
Node unionAB = d_nodeManager->mkNode(SET_UNION, A, B);
// (set.map
// (set.union (set.singleton "a") (set.singleton "b"))) = (set.singleton 1))
Node n2 = d_nodeManager->mkNode(SET_MAP, lambda, unionAB);
Node rewritten2 = Rewriter::rewrite(n2);
- Node bag = d_nodeManager->mkSingleton(d_nodeManager->integerType(), one);
+ Node bag = d_nodeManager->mkNode(SET_SINGLETON, one);
ASSERT_TRUE(rewritten2 == bag);
// - (set.map f (set.union K1 K2)) =
#include "expr/dtype.h"
#include "test_api.h"
#include "test_node.h"
-#include "theory/sets/singleton_op.h"
#include "util/rational.h"
using namespace cvc5;
TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node)
{
- Node singletonInt =
- d_nodeManager->mkConst(SetSingletonOp(d_nodeManager->integerType()));
- Node singletonReal =
- d_nodeManager->mkConst(SetSingletonOp(d_nodeManager->realType()));
- Node intConstant = d_nodeManager->mkConst(kind::CONST_RATIONAL, Rational(1));
- Node realConstant =
- d_nodeManager->mkConst(kind::CONST_RATIONAL, Rational(1, 5));
+ Node intConstant = d_nodeManager->mkConstReal(Rational(1));
+ Node realConstant = d_nodeManager->mkConstReal(Rational(1, 5));
// (singleton (singleton_op Real) 1)
- ASSERT_NO_THROW(
- d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant));
- // (singleton (singleton_op Int) (/ 1 5))
- ASSERT_DEATH(
- d_nodeManager->mkSingleton(d_nodeManager->integerType(), realConstant),
- "Invalid operands for mkSingleton");
+ ASSERT_NO_THROW(d_nodeManager->mkNode(kind::SET_SINGLETON, intConstant));
- Node n = d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant);
+ Node n = d_nodeManager->mkNode(kind::SET_SINGLETON, intConstant);
// the type of (singleton (singleton_op Real) 1) is (Set Real)
ASSERT_TRUE(n.getType()
== d_nodeManager->mkSetType(d_nodeManager->realType()));
projects / cvc5.git / commitdiff