diff options
Diffstat (limited to 'src')
25 files changed, 296 insertions, 70 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3ca20e8dc..65223f3c5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -773,6 +773,8 @@ libcvc4_add_sources( 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 diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 6ed8855e4..179eb672e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3701,6 +3701,23 @@ Term Solver::mkEmptySet(Sort s) const 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; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 31ff13ba0..c53d6f828 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2600,6 +2600,15 @@ class CVC4_PUBLIC Solver 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. * @return the empty bag constant diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 76dcc5317..987db9363 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -177,6 +177,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": 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 + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index daff390b4..bf135dca2 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -691,6 +691,11 @@ cdef class Solver: 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) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 3c3d6df4a..f8057006c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -950,6 +950,17 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) { } } +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); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index ef22101f0..5427c3b6a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -576,6 +576,15 @@ class NodeManager { 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. */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 5f959c660..6eb0924ac 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2158,9 +2158,9 @@ simpleTerm[CVC4::api::Term& f] /* 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])); } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e7bb8795c..c154db399 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1216,6 +1216,13 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) 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; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9350111c7..6d75279e5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -740,10 +740,10 @@ void Smt2Printer::toStream(std::ostream& out, 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; @@ -976,7 +976,12 @@ void Smt2Printer::toStream(std::ostream& out, 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(); diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 28731b371..2d6af9a63 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -676,7 +676,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { 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; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 1b86afb85..ba9962bd9 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -965,7 +965,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( 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}; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 578d5faba..b18ae5b95 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -412,7 +412,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) } 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); @@ -1341,7 +1342,7 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { 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{ @@ -1512,12 +1513,14 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: //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 @@ -1529,8 +1532,10 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: }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; @@ -1650,7 +1655,8 @@ void TheorySep::computeLabelModel( Node lbl ) { }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 ); } diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 87a849a78..78837508e 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -102,7 +102,9 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) { 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 ); diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 07672605d..21344ee73 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -1028,7 +1028,7 @@ void CardinalityExtension::mkModelValueElementsFor( // 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 " @@ -1037,7 +1037,7 @@ void CardinalityExtension::mkModelValueElementsFor( else { els.push_back( - nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType))); + nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType))); } } } diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index fd941ab29..57120e42e 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -35,15 +35,23 @@ enumerator SET_TYPE \ "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: @@ -82,6 +90,7 @@ typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule 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 diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 8989fbc15..2654344f3 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -44,11 +44,13 @@ class NormalForm { } 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; } diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp new file mode 100644 index 000000000..d7f318314 --- /dev/null +++ b/src/theory/sets/singleton_op.cpp @@ -0,0 +1,50 @@ +/********************* */ +/*! \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 diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h new file mode 100644 index 000000000..57118999a --- /dev/null +++ b/src/theory/sets/singleton_op.h @@ -0,0 +1,63 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 51f49ad1d..18df43e9f 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1143,9 +1143,10 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m, 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); } } @@ -1357,7 +1358,7 @@ TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node) 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); diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index ebbc24d12..617b458c9 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -247,12 +247,13 @@ void TheorySetsRels::check(Theory::Effort level) } 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]); } } } @@ -863,7 +864,7 @@ void TheorySetsRels::check(Theory::Effort level) 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); } /* @@ -1153,8 +1154,9 @@ void TheorySetsRels::check(Theory::Effort level) } 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; } @@ -1183,14 +1185,15 @@ void TheorySetsRels::check(Theory::Effort level) 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); } @@ -1216,9 +1219,11 @@ void TheorySetsRels::check(Theory::Effort level) 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); diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 9b8fd0cb7..95a13f4d5 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -176,7 +176,7 @@ private: /** Helper functions */ bool hasTerm( Node a ); - void makeSharedTerm( Node ); + void makeSharedTerm(Node, TypeNode t); void reduceTupleVar( Node ); bool hasMember( Node, Node ); void computeTupleReps( Node ); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index d821a0059..847bf34eb 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -161,7 +161,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode 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); } @@ -488,12 +488,14 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { } 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, diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp index 321b9ffcd..1d932b590 100644 --- a/src/theory/sets/theory_sets_type_enumerator.cpp +++ b/src/theory/sets/theory_sets_type_enumerator.cpp @@ -89,7 +89,8 @@ SetEnumerator& SetEnumerator::operator++() // 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 diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 3e2834aaf..20e5e57e2 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -31,9 +31,8 @@ struct SetsBinaryOperatorTypeRule 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) { @@ -45,19 +44,11 @@ struct SetsBinaryOperatorTypeRule 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; @@ -132,18 +123,40 @@ struct MemberTypeRule { } };/* 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) |