diff options
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/kinds | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 14 |
4 files changed, 17 insertions, 5 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index ab0ca3428..cfe7eb632 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -44,6 +44,7 @@ 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)" +nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it." operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" @@ -60,14 +61,13 @@ typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule typerule INSERT ::CVC4::theory::sets::InsertTypeRule typerule CARD ::CVC4::theory::sets::CardTypeRule typerule COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule +typerule UNIVERSE_SET ::CVC4::theory::sets::UniverseSetTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule -variable UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it." - construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 5b9f4bf03..57ab8c0cf 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1531,7 +1531,7 @@ Node TheorySetsPrivate::getEmptySet( TypeNode tn ) { Node TheorySetsPrivate::getUnivSet( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_univset.find( tn ); if( it==d_univset.end() ){ - Node n = NodeManager::currentNM()->mkUniqueVar(tn, kind::UNIVERSE_SET); + Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET); d_univset[tn] = n; return n; }else{ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 9669561a6..8facf1f48 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -306,7 +306,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { break; }//kind::UNION case kind::COMPLEMENT: { - Node univ = NodeManager::currentNM()->mkUniqueVar( node[0].getType(), kind::UNIVERSE_SET ); + Node univ = NodeManager::currentNM()->mkNullaryOperator( node[0].getType(), kind::UNIVERSE_SET ); return RewriteResponse( REWRITE_AGAIN, NodeManager::currentNM()->mkNode( kind::SETMINUS, univ, node[0] ) ); } break; diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 11f375d5b..541835980 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -174,7 +174,19 @@ struct ComplementTypeRule { } };/* struct ComplementTypeRule */ - +struct UniverseSetTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::UNIVERSE_SET); + // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation + Assert(check); + TypeNode setType = n.getType(false); + if(!setType.isSet()) { + throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found"); + } + return setType; + } +};/* struct ComplementTypeRule */ struct InsertTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) |