This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
two = slv.mkReal(2)
three = slv.mkReal(3)
- singleton_one = slv.mkTerm(kinds.Singleton, one)
- singleton_two = slv.mkTerm(kinds.Singleton, two)
- singleton_three = slv.mkTerm(kinds.Singleton, three)
+ singleton_one = slv.mkSingleton(integer, one)
+ singleton_two = slv.mkSingleton(integer, two)
+ singleton_three = slv.mkSingleton(integer, three)
one_two = slv.mkTerm(kinds.Union, singleton_one, singleton_two)
two_three = slv.mkTerm(kinds.Union, singleton_two, singleton_three)
intersection = slv.mkTerm(kinds.Intersection, one_two, two_three)
Term two = slv.mkReal(2);
Term three = slv.mkReal(3);
- Term singleton_one = slv.mkTerm(SINGLETON, one);
- Term singleton_two = slv.mkTerm(SINGLETON, two);
- Term singleton_three = slv.mkTerm(SINGLETON, three);
+ Term singleton_one = slv.mkSingleton(integer, one);
+ Term singleton_two = slv.mkSingleton(integer, two);
+ Term singleton_three = slv.mkSingleton(integer, three);
Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two);
Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
theory/sets/inference_manager.h
theory/sets/normal_form.h
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
CVC4_API_SOLVER_TRY_CATCH_END;
}
+Term Solver::mkSingleton(Sort s, Term t) const
+{
+ NodeManagerScope scope(getNodeManager());
+
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_ARG_CHECK_EXPECTED(!t.isNull(), t) << "non-null term";
+ CVC4_API_SOLVER_CHECK_TERM(t);
+ checkMkTerm(SINGLETON, 1);
+
+ TypeNode typeNode = TypeNode::fromType(*s.d_type);
+ Node res = getNodeManager()->mkSingleton(typeNode, *t.d_node);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
+
+ CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
Term Solver::mkEmptyBag(Sort s) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
*/
Term mkEmptySet(Sort s) const;
+ /**
+ * Create a singleton set from the given element t.
+ * @param s the element sort of the returned set.
+ * Note that the sort of t needs to be a subtype of s.
+ * @param t the single element in the singleton.
+ * @return a singleton set constructed from the element t.
+ */
+ Term mkSingleton(Sort s, Term t) const;
+
/**
* Create a constant representing an empty bag of the given sort.
* @param s the sort of the bag elements.
Term mkRegexpEmpty() except +
Term mkRegexpSigma() except +
Term mkEmptySet(Sort s) except +
+ Term mkSingleton(Sort s, Term t) except +
Term mkSepNil(Sort sort) except +
Term mkString(const string& s) except +
Term mkString(const vector[unsigned]& s) except +
term.cterm = self.csolver.mkEmptySet(s.csort)
return term
+ def mkSingleton(self, Sort s, Term t):
+ cdef Term term = Term(self)
+ term.cterm = self.csolver.mkSingleton(s.csort, t.cterm)
+ return term
+
def mkSepNil(self, Sort sort):
cdef Term term = Term(self)
term.cterm = self.csolver.mkSepNil(sort.csort)
}
}
+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(SingletonOp(t));
+ Node singleton = mkNode(kind::SINGLETON, op, n);
+ return singleton;
+}
+
Node NodeManager::mkAbstractValue(const TypeNode& type) {
Node n = mkConst(AbstractValue(++d_abstractValueCount));
n.setAttribute(TypeAttr(), type);
/** make unique (per Type,Kind) variable. */
Node mkNullaryOperator(const TypeNode& type, Kind k);
+ /**
+ * 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 constant of type T. It will have the appropriate
* CONST_* kind defined for T.
/* finite set literal */
| LBRACE formula[f] { args.push_back(f); }
( COMMA formula[f] { args.push_back(f); } )* RBRACE
- { f = MK_TERM(api::SINGLETON, args[0]);
+ { f = SOLVER->mkSingleton(args[0].getSort(), args[0]);
for(size_t i = 1; i < args.size(); ++i) {
- f = MK_TERM(api::UNION, f, MK_TERM(api::SINGLETON, args[i]));
+ f = MK_TERM(api::UNION, f, SOLVER->mkSingleton(args[i].getSort(), args[i]));
}
}
parseError(
"eqrange predicate requires option --arrays-exp to be enabled.");
}
+ if (kind == api::SINGLETON && args.size() == 1)
+ {
+ api::Sort sort = args[0].getSort();
+ api::Term ret = d_solver->mkSingleton(sort, args[0]);
+ Debug("parser") << "applyParseOp: return singleton " << ret << std::endl;
+ return ret;
+ }
api::Term ret = d_solver->mkTerm(kind, args);
Debug("parser") << "applyParseOp: return default builtin " << ret
<< std::endl;
out << smtKindString(k, d_variant) << " ";
break;
case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break;
+ case kind::SINGLETON: stillNeedToPrintParams = false; CVC4_FALLTHROUGH;
case kind::MEMBER: typeChildren = true; CVC4_FALLTHROUGH;
case kind::INSERT:
case kind::SET_TYPE:
- case kind::SINGLETON:
case kind::COMPLEMENT:
case kind::CHOOSE:
case kind::IS_SINGLETON: out << smtKindString(k, d_variant) << " "; break;
TypeNode elemType = TypeNode::leastCommonTypeNode( n[0].getType(), n[1].getType().getSetElementType() );
force_child_type[0] = elemType;
force_child_type[1] = NodeManager::currentNM()->mkSetType( elemType );
- }else{
+ }
+ else if (n.getKind() == kind::SINGLETON)
+ {
+ force_child_type[0] = n.getType().getSetElementType();
+ }
+ else{
// APPLY_UF, APPLY_CONSTRUCTOR, etc.
Assert(n.hasOperator());
TypeNode opt = n.getOperator().getType();
Assert(i < d_setm_choice[sro].size());
choice_i = d_setm_choice[sro][i];
choices.push_back(choice_i);
- Node sChoiceI = nm->mkNode(SINGLETON, choice_i);
+ Node sChoiceI = nm->mkSingleton(choice_i.getType(), choice_i);
if (nsr.isNull())
{
nsr = sChoiceI;
Trace("sygus-grammar-def") << "...add for singleton" << std::endl;
std::vector<TypeNode> cargsSingleton;
cargsSingleton.push_back(unresElemType);
- sdts[i].addConstructor(SINGLETON, cargsSingleton);
+
+ // 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);
// add for union, difference, intersection
std::vector<Kind> bin_kinds = {UNION, INTERSECTION, SETMINUS};
}
else if (satom.getKind() == SEP_PTO)
{
- Node ss = nm->mkNode(SINGLETON, satom[0]);
+ // TODO(project##230): Find a safe type for the singleton operator
+ Node ss = nm->mkSingleton(satom[0].getType(), 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()->mkNode( kind::SINGLETON, s );
+ s = NodeManager::currentNM()->mkSingleton(tn, s);
if( u.isNull() ){
u = s;
}else{
//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] );
- Node svr = NodeManager::currentNM()->mkNode( kind::SINGLETON, vr );
+ // TODO(project##230): Find a safe type for the singleton operator
+ Node svr = NodeManager::currentNM()->mkSingleton(vr.getType(), 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 ){
- Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] );
+ // TODO(project##230): Find a safe type for the singleton operator
+ Node s = NodeManager::currentNM()->mkSingleton(n[0].getType(), 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
}else{
Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl;
}
- }
- children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] ), lbl_v ) );
+ }
+ // TODO(project##230): Find a safe type for the singleton operator
+ Node singleton = NodeManager::currentNM()->mkSingleton(n[0].getType(), 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;
return ret;
}else{
tt = itm->second;
}
- Node stt = NodeManager::currentNM()->mkNode( kind::SINGLETON, tt );
+ // TODO(project##230): Find a safe type for the singleton operator
+ Node stt = NodeManager::currentNM()->mkSingleton(tt.getType(), 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 );
}
switch (node.getKind()) {
case kind::SEP_LABEL: {
if( node[0].getKind()==kind::SEP_PTO ){
- Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, node[0][0] );
+ // TODO(project##230): Find a safe type for the singleton operator
+ Node s = NodeManager::currentNM()->mkSingleton(node[0][0].getType(),
+ node[0][0]);
if( node[1]!=s ){
Node c1 = node[1].eqNode( s );
Node c2 = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, node[0][0], node[0][1] ), s );
// the current members of this finite type.
Node slack = nm->mkSkolem("slack", elementType);
- Node singleton = nm->mkNode(SINGLETON, slack);
+ Node singleton = nm->mkSingleton(elementType, 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->mkNode(SINGLETON, nm->mkSkolem("msde", elementType)));
+ nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType)));
}
}
}
"theory/sets/theory_sets_type_enumerator.h"
# operators
-operator UNION 2 "set union"
-operator INTERSECTION 2 "set intersection"
-operator SETMINUS 2 "set subtraction"
-operator SUBSET 2 "subset predicate; first parameter a subset of second"
-operator MEMBER 2 "set membership predicate; first parameter a member of second"
-operator SINGLETON 1 "the set of the single element given as a parameter"
-operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
-operator CARD 1 "set cardinality operator"
-operator COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)"
+operator UNION 2 "set union"
+operator INTERSECTION 2 "set intersection"
+operator SETMINUS 2 "set subtraction"
+operator SUBSET 2 "subset predicate; first parameter a subset of second"
+operator MEMBER 2 "set membership predicate; first parameter a member of second"
+
+constant SINGLETON_OP \
+ ::CVC4::SingletonOp \
+ ::CVC4::SingletonOpHashFunction \
+ "theory/sets/singleton_op.h" \
+ "operator for singletons; payload is an instance of the CVC4::SingletonOp class"
+parameterized SINGLETON SINGLETON_OP 1 \
+"constructs a set of a single element. First parameter is a SingletonOp. Second is a term"
+
+operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
+operator CARD 1 "set cardinality operator"
+operator COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)"
nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it."
# A set comprehension is specified by:
typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SUBSET ::CVC4::theory::sets::SubsetTypeRule
typerule MEMBER ::CVC4::theory::sets::MemberTypeRule
+typerule SINGLETON_OP "SimpleTypeRule<RBuiltinOperator>"
typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
typerule INSERT ::CVC4::theory::sets::InsertTypeRule
}
else
{
+ TypeNode elementType = setType.getSetElementType();
ElementsIterator it = elements.begin();
- Node cur = nm->mkNode(kind::SINGLETON, *it);
+ Node cur = nm->mkSingleton(elementType, *it);
while (++it != elements.end())
{
- cur = nm->mkNode(kind::UNION, nm->mkNode(kind::SINGLETON, *it), cur);
+ Node singleton = nm->mkSingleton(elementType, *it);
+ cur = nm->mkNode(kind::UNION, singleton, cur);
}
return cur;
}
--- /dev/null
+/********************* */
+/*! \file singleton_op.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief a class for singleton operator for sets
+ **/
+
+#include "singleton_op.h"
+
+#include <iostream>
+
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const SingletonOp& op)
+{
+ return out << "(singleton_op " << op.getType() << ')';
+}
+
+size_t SingletonOpHashFunction::operator()(const SingletonOp& op) const
+{
+ return TypeNodeHashFunction()(op.getType());
+}
+
+SingletonOp::SingletonOp(const TypeNode& elementType)
+ : d_type(new TypeNode(elementType))
+{
+}
+
+SingletonOp::SingletonOp(const SingletonOp& op)
+ : d_type(new TypeNode(op.getType()))
+{
+}
+
+const TypeNode& SingletonOp::getType() const { return *d_type; }
+
+bool SingletonOp::operator==(const SingletonOp& op) const
+{
+ return getType() == op.getType();
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file singleton_op.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief a class for singleton operator for sets
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__SINGLETON_OP_H
+#define CVC4__SINGLETON_OP_H
+
+#include <memory>
+
+namespace CVC4 {
+
+class TypeNode;
+
+/**
+ * The class is an operator for kind 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 SingletonOp
+{
+ public:
+ SingletonOp(const TypeNode& elementType);
+ SingletonOp(const SingletonOp& op);
+
+ /** return the type of the current object */
+ const TypeNode& getType() const;
+
+ bool operator==(const SingletonOp& op) const;
+
+ private:
+ SingletonOp();
+ /** a pointer to the type of the singleton element */
+ std::unique_ptr<TypeNode> d_type;
+}; /* class Singleton */
+
+std::ostream& operator<<(std::ostream& out, const SingletonOp& op);
+
+/**
+ * Hash function for the SingletonHashFunction objects.
+ */
+struct CVC4_PUBLIC SingletonOpHashFunction
+{
+ size_t operator()(const SingletonOp& op) const;
+}; /* struct SingletonOpHashFunction */
+
+} // namespace CVC4
+
+#endif /* CVC4__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)
{
- Node t = nm->mkNode(kind::SINGLETON, itmm.first);
+ Node t = nm->mkSingleton(elementType, itmm.first);
els.push_back(t);
}
}
TypeNode setType = set.getType();
Node boundVar = nm->mkBoundVar(setType.getSetElementType());
- Node singleton = nm->mkNode(kind::SINGLETON, boundVar);
+ Node singleton = nm->mkSingleton(setType.getSetElementType(), boundVar);
Node equal = set.eqNode(singleton);
std::vector<Node> variables = {boundVar};
Node boundVars = nm->mkNode(BOUND_VAR_LIST, variables);
}
else if (erType.isTuple() && !eqc_node.isConst() && !eqc_node.isVar())
{
+ std::vector<TypeNode> tupleTypes = erType.getTupleTypes();
for (unsigned i = 0, tlen = erType.getTupleLength(); i < tlen; i++)
{
- Node element = RelsUtils::nthElementOfTuple( eqc_node, i );
-
- if( !element.isConst() ) {
- makeSharedTerm( element );
+ Node element = RelsUtils::nthElementOfTuple(eqc_node, i);
+ if (!element.isConst())
+ {
+ makeSharedTerm(element, tupleTypes[i]);
}
}
}
sendInfer(fact, reason, "JOIN-Split-1");
fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]);
sendInfer(fact, reason, "JOIN-Split-2");
- makeSharedTerm( shared_x );
+ makeSharedTerm(shared_x, shared_type);
}
/*
}
return equal;
} else if(!a.getType().isBoolean()){
- makeSharedTerm(a);
- makeSharedTerm(b);
+ // TODO(project##230): Find a safe type for the singleton operator
+ makeSharedTerm(a, a.getType());
+ makeSharedTerm(b, b.getType());
}
return false;
}
return false;
}
- void TheorySetsRels::makeSharedTerm( Node n ) {
+ void TheorySetsRels::makeSharedTerm(Node n, TypeNode t)
+ {
if (d_shared_terms.find(n) != d_shared_terms.end())
{
return;
}
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()->mkNode(SINGLETON, n);
+ Node ss = NodeManager::currentNM()->mkSingleton(t, n);
d_treg.getProxy(ss);
d_shared_terms.insert(n);
}
Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl;
std::vector<Node> tuple_elements;
tuple_elements.push_back((n[0].getType().getDType())[0].getConstructor());
- for(unsigned int i = 0; i < n[0].getType().getTupleLength(); 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);
- makeSharedTerm(element);
+ makeSharedTerm(element, tupleTypes[i]);
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 );
+ void makeSharedTerm(Node, TypeNode t);
void reduceTupleVar( Node );
bool hasMember( Node, Node );
void computeTupleReps( Node );
std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
std::inserter(newSet, newSet.begin()));
Node newNode = NormalForm::elementsToSet(newSet, node.getType());
- Assert(newNode.isConst());
+ Assert(newNode.isConst() && newNode.getType() == node.getType());
Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
return RewriteResponse(REWRITE_DONE, newNode);
}
}
else if (k == kind::INSERT)
{
- Node insertedElements = nm->mkNode(kind::SINGLETON, node[0]);
size_t setNodeIndex = node.getNumChildren()-1;
- for(size_t i = 1; i < setNodeIndex; ++i) {
- insertedElements = nm->mkNode(kind::UNION,
- insertedElements,
- nm->mkNode(kind::SINGLETON, node[i]));
+ TypeNode elementType = node[setNodeIndex].getType().getSetElementType();
+ Node insertedElements = nm->mkSingleton(elementType, node[0]);
+
+ for (size_t i = 1; i < setNodeIndex; ++i)
+ {
+ Node singleton = nm->mkSingleton(elementType, node[i]);
+ insertedElements = nm->mkNode(kind::UNION, insertedElements, singleton);
}
return RewriteResponse(REWRITE_AGAIN,
nm->mkNode(kind::UNION,
// get a new element and return it as a singleton set
Node element = *d_elementEnumerator;
d_elementsSoFar.push_back(element);
- d_currentSet = d_nodeManager->mkNode(kind::SINGLETON, element);
+ TypeNode elementType = d_elementEnumerator.getType();
+ d_currentSet = d_nodeManager->mkSingleton(elementType, element);
d_elementEnumerator++;
}
else
TNode n,
bool check)
{
- Assert(n.getKind() == kind::UNION ||
- n.getKind() == kind::INTERSECTION ||
- n.getKind() == kind::SETMINUS);
+ Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION
+ || n.getKind() == kind::SETMINUS);
TypeNode setType = n[0].getType(check);
if (check)
{
TypeNode secondSetType = n[1].getType(check);
if (secondSetType != setType)
{
- if (n.getKind() == kind::INTERSECTION)
- {
- setType = TypeNode::mostCommonTypeNode(secondSetType, setType);
- }
- else
- {
- setType = TypeNode::leastCommonTypeNode(secondSetType, setType);
- }
- if (setType.isNull())
- {
- throw TypeCheckingExceptionPrivate(
- n, "operator expects two sets of comparable types");
- }
+ std::stringstream ss;
+ ss << "Operator " << n.getKind()
+ << " expects two sets of the same type. Found types '" << setType
+ << "' and '" << secondSetType << "'.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
}
}
return setType;
}
};/* struct MemberTypeRule */
-struct SingletonTypeRule {
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+struct SingletonTypeRule
+{
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
{
- Assert(n.getKind() == kind::SINGLETON);
- return nodeManager->mkSetType(n[0].getType(check));
+ Assert(n.getKind() == kind::SINGLETON && n.hasOperator()
+ && n.getOperator().getKind() == kind::SINGLETON_OP);
+
+ SingletonOp op = n.getOperator().getConst<SingletonOp>();
+ TypeNode type1 = op.getType();
+ if (check)
+ {
+ TypeNode type2 = n[0].getType(check);
+ TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2);
+ // the type of the element should be a subtype of the type of the operator
+ // e.g. (singleton (singleton_op Real) 1) where 1 is an Int
+ if (leastCommonType.isNull() || leastCommonType != type1)
+ {
+ std::stringstream ss;
+ ss << "The type '" << type2 << "' of the element is not a subtype of '"
+ << type1 << "' in term : " << n;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ return nodeManager->mkSetType(type1);
}
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
+ {
Assert(n.getKind() == kind::SINGLETON);
return n[0].isConst();
}
-};/* struct SingletonTypeRule */
+}; /* struct SingletonTypeRule */
struct EmptySetTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
(declare-fun t1 () (Set Real))
(declare-fun t2 () (Set Real))
(declare-fun t3 () (Set Real))
-(declare-fun r1 () (Set Int))
-(declare-fun r2 () (Set Int))
-(declare-fun r3 () (Set Int))
-(assert (and (member 1.5 s) (member 0 s)))
+(declare-fun r1 () (Set Real))
+(declare-fun r2 () (Set Real))
+(declare-fun r3 () (Set Real))
+(assert (and (member 1.5 s) (member 0.0 s)))
(assert (= t1 (union s (singleton 2.5))))
-(assert (= t2 (union s (singleton 2))))
+(assert (= t2 (union s (singleton 2.0))))
(assert (= t3 (union r3 (singleton 2.5))))
-(assert (= (intersection r1 r2) (intersection s (singleton 0))))
+(assert (= (intersection r1 r2) (intersection s (singleton 0.0))))
(assert (not (= r1 (as emptyset (Set Real)))))
(check-sat)
cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
+cvc4_add_unit_test_white(theory_sets_type_rules_white theory)
cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory)
cvc4_add_unit_test_white(theory_strings_word_white theory)
cvc4_add_unit_test_white(theory_white theory)
Node node = d_nm->mkConst(Rational(10));
// node of type Int is not compatible with bag of type (Bag String)
- TS_ASSERT_THROWS(d_nm->mkNode(BAG_COUNT, node, bag),
+ TS_ASSERT_THROWS(d_nm->mkNode(BAG_COUNT, node, bag).getType(true),
TypeCheckingExceptionPrivate&);
}
--- /dev/null
+/********************* */
+/*! \file theory_sets_type_rules_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of sets typing rules
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+#include "expr/dtype.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+using namespace CVC4::api;
+
+class SetsTypeRuleWhite : public CxxTest::TestSuite
+{
+ public:
+ void setUp() override
+ {
+ d_slv.reset(new Solver());
+ d_em.reset(new ExprManager());
+ d_smt.reset(new SmtEngine(d_em.get()));
+ d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+ d_smt->finishInit();
+ }
+
+ void tearDown() override
+ {
+ d_slv.reset();
+ d_smt.reset();
+ d_nm.release();
+ d_em.reset();
+ }
+
+ void testSingletonTerm()
+ {
+ Sort realSort = d_slv->getRealSort();
+ Sort intSort = d_slv->getIntegerSort();
+ Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort));
+ Term one = d_slv->mkReal(1);
+ Term singletonInt = d_slv->mkSingleton(intSort, one);
+ Term singletonReal = d_slv->mkSingleton(realSort, one);
+ // (union
+ // (singleton (singleton_op Int) 1)
+ // (as emptyset (Set Real)))
+ TS_ASSERT_THROWS(d_slv->mkTerm(UNION, singletonInt, emptyReal),
+ CVC4ApiException);
+ // (union
+ // (singleton (singleton_op Real) 1)
+ // (as emptyset (Set Real)))
+ TS_ASSERT_THROWS_NOTHING(d_slv->mkTerm(UNION, singletonReal, emptyReal));
+ }
+
+ void testSingletonNode()
+ {
+ Node singletonInt = d_nm->mkConst(SingletonOp(d_nm->integerType()));
+ Node singletonReal = d_nm->mkConst(SingletonOp(d_nm->realType()));
+ Node intConstant = d_nm->mkConst(Rational(1));
+ Node realConstant = d_nm->mkConst(Rational(1, 5));
+ // (singleton (singleton_op Real) 1)
+ TS_ASSERT_THROWS_NOTHING(
+ d_nm->mkSingleton(d_nm->realType(), intConstant));
+ // (singleton (singleton_op Int) (/ 1 5))
+ // This fails now with the assertions. cxxtest does not catch that.
+ // TS_ASSERT_THROWS(d_nm->mkSingleton(d_nm->integerType(), realConstant),
+ // Exception);
+
+ Node n = d_nm->mkSingleton(d_nm->realType(), intConstant);
+ // the type of (singleton (singleton_op Real) 1) is (Set Real)
+ TS_ASSERT(n.getType() == d_nm->mkSetType(d_nm->realType()));
+ // (singleton (singleton_op Real) 1) is a constant in normal form
+ TS_ASSERT(n.isConst());
+ }
+
+ private:
+ std::unique_ptr<Solver> d_slv;
+ std::unique_ptr<ExprManager> d_em;
+ std::unique_ptr<SmtEngine> d_smt;
+ std::unique_ptr<NodeManager> d_nm;
+}; /* class SetsTypeRuleWhite */
projects / cvc5.git / commitdiff