Add nullary operator metakind.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 470a6eeca0d02be4fb05e30dfd4b25e55f85565d..82cabbd3e84ad230a490e74cd4637a23faff307f 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -946,9 +946,9 @@ Expr ExprManager::mkBoundVar(Type type) {
   return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
 }
 
-Expr ExprManager::mkUniqueVar(Type type, Kind k){
+Expr ExprManager::mkNullaryOperator(Type type, Kind k){
   NodeManagerScope nms(d_nodeManager);
-  Node n = d_nodeManager->mkUniqueVar(*type.d_typeNode, k); 
+  Node n = d_nodeManager->mkNullaryOperator(*type.d_typeNode, k); 
   return n.toExpr();
 }
 

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index ed9247e5e843de7b7751e6c52716a6e533f75f7f..9e962d970715ad354a89d28d09df6c071d3b38b8 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -549,7 +549,7 @@ public:
   /**
    * Create unique variable of type 
    */
-  Expr mkUniqueVar( Type type, Kind k);
+  Expr mkNullaryOperator( Type type, Kind k);
 
   /** Get a reference to the statistics registry for this ExprManager */
   Statistics getStatistics() const throw();

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 1c03cf4074d7163c24341538d13b8d072bb17c79..2dcf24b095d17f97be4a6cd7a3eeaa290964a201 100644 (file)
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -98,7 +98,8 @@ enum MetaKind_t {
   VARIABLE, /**< special node kinds: no operator */
   OPERATOR, /**< operators that get "inlined" */
   PARAMETERIZED, /**< parameterized ops (like APPLYs) that carry extra data */
-  CONSTANT /**< constants */
+  CONSTANT, /**< constants */
+  NULLARY_OPERATOR /**< nullary operator */
 };/* enum MetaKind_t */
 
 }/* CVC4::kind::metakind namespace */
@@ -338,7 +339,7 @@ ${metakind_operatorKinds}
 
 }/* CVC4::kind namespace */
 
-#line 342 "${template}"
+#line 343 "${template}"
 
 namespace theory {
 

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 963e297b491ca845e44d87d183562cd6d0ec7118..60ee758d87968ea67dcc4c277c204d372a1714b6 100755 (executable)
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -248,6 +248,12 @@ template <> $2 const & Expr::getConst() const {
   case $1: return to->mkConst(n.getConst< $2 >());"
 }
 
+function nullaryoperator {
+  # nullaryoperator K ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function check_theory_seen {
   if $seen_endtheory; then
     echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2

diff --git a/src/expr/mkkind b/src/expr/mkkind
index 271c8bc7a9597c46ed3c40ee612fa471e767fc8d..2b1901f5dd37dcb8373e587e3613193bcffdae3f 100755 (executable)
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -239,6 +239,15 @@ function constant {
   register_kind "$1" 0 "$5"
 }
 
+function nullaryoperator {
+  # nullaryoperator K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_kind "$1" 0 "$2"
+}
+
 function register_sort {
   id=$1
   cardinality=$2

diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 3e06a88a50323dbe6b770bffda22c9eb39db3649..19e6e224409dba333a88e2510e38fa6de658437e 100755 (executable)
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -302,6 +302,15 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 "
 }
 
+function nullaryoperator {
+  # nullaryoperator K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_metakind NULLARY_OPERATOR "$1" 0
+}
+
 function registerOperatorToKind {
   operatorKind=$1
   applyKind=$2

diff --git a/src/expr/node.h b/src/expr/node.h
index 31721b2ef1ce6df495811ebfd22a5f5b21555a8c..6d98b940bd759c120a1b2fdf94e826b43d2653ac 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -464,12 +464,6 @@ public:
     assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::VARIABLE;
   }
-  inline bool isUninterpretedVar() const {
-    assertTNodeNotExpired();
-    return getMetaKind() == kind::metakind::VARIABLE &&
-           getKind() != kind::UNIVERSE_SET && 
-           getKind() != kind::SEP_NIL;
-  }
 
   inline bool isClosure() const {
     assertTNodeNotExpired();
@@ -1259,6 +1253,9 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
   case kind::metakind::CONSTANT:
     IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind");
 
+  case kind::metakind::NULLARY_OPERATOR:
+    IllegalArgument(*this, "getOperator() called on Node with NULLARY_OPERATOR-kinded kind");
+
   default:
     Unhandled(mk);
   }

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index d92524a1962389232198d838a79895da731ae94d..7cb14ed5a02918eed211354459bb024820ea324d 100644 (file)
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -933,7 +933,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   // file comments at the top of this file.
 
   // Case 0: If a VARIABLE
-  if(getMetaKind() == kind::metakind::VARIABLE) {
+  if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) {
     /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
      * there are no children (no reference counts to reason about),
      * and we don't keep VARIABLE-kinded Nodes in the NodeManager
@@ -1123,7 +1123,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
   // file comments at the top of this file.
 
   // Case 0: If a VARIABLE
-  if(getMetaKind() == kind::metakind::VARIABLE) {
+  if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) {
     /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
      * there are no children (no reference counts to reason about),
      * and we don't keep VARIABLE-kinded Nodes in the NodeManager
@@ -1336,6 +1336,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
   if( d_nm->getOptions()[options::earlyTypeChecking] ) {
     kind::MetaKind mk = n.getMetaKind();
     if( mk != kind::metakind::VARIABLE
+        && mk != kind::metakind::NULLARY_OPERATOR
         && mk != kind::metakind::CONSTANT ) {
       d_nm->getType(n, true);
     }

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index ebf78f541ea8291b0fb43a9b7fe96c603400b14b..2a819935d9312cb08ed47b324ab5c59e49c8ef5d 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -315,7 +315,7 @@ void NodeManager::reclaimZombies() {
 
       // remove from the pool
       kind::MetaKind mk = nv->getMetaKind();
-      if(mk != kind::metakind::VARIABLE) {
+      if(mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR) {
         poolRemove(nv);
       }
 
@@ -787,14 +787,15 @@ Node NodeManager::mkBooleanTermVariable() {
   return n;
 }
 
-Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) {
+Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
   std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
   if( it==d_unique_vars[k].end() ){
     Node n = NodeBuilder<0>(this, k);
     n.setAttribute(TypeAttr(), type);
-    n.setAttribute(TypeCheckedAttr(), true);
+    //should type check it
+    //n.setAttribute(TypeCheckedAttr(), true);
     d_unique_vars[k][type] = n;
-    Assert( n.getMetaKind() == kind::metakind::VARIABLE );
+    Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR );
     return n;
   }else{
     return it->second;

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d2b45a6361dae7a226d0c155a7a9a490c11cc697..3aa826b499b2e550c808948f3c66387a8bdbc19e 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -536,7 +536,7 @@ public:
   Node mkAbstractValue(const TypeNode& type);
   
   /** make unique (per Type,Kind) variable. */
-  Node mkUniqueVar(const TypeNode& type, Kind k);
+  Node mkNullaryOperator(const TypeNode& type, Kind k);
 
   /**
    * Create a constant of type T.  It will have the appropriate
@@ -1240,6 +1240,7 @@ inline bool NodeManager::hasOperator(Kind k) {
 
   case kind::metakind::INVALID:
   case kind::metakind::VARIABLE:
+  case kind::metakind::NULLARY_OPERATOR:
     return false;
 
   case kind::metakind::OPERATOR:

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 40649ef2c690ea0f323afa761d98ef1da57ba02c..f8de8c0c8e7d0a638b32a93461f5c4f7256ad631 100644 (file)
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -60,7 +60,7 @@ void NodeValue::printAst(std::ostream& out, int ind) const {
   indent(out, ind);
   out << '(';
   out << getKind();
-  if (getMetaKind() == kind::metakind::VARIABLE) {
+  if (getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR ) {
     out << ' ' << getId();
   } else if (getMetaKind() == kind::metakind::CONSTANT) {
     out << ' ';

diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 8ed894a22637b10dcdc7704f272438c45e6d7cbc..757a32529619c423175746015448f76f07137fe4 100644 (file)
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -61,7 +61,7 @@ ${typerules}
 bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
   throw (AssertionException) {
 
-  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
 
   switch(n.getKind()) {
 ${construles}
@@ -78,7 +78,7 @@ ${construles}
 bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
   throw (AssertionException) {
 
-  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
 
   switch(n.getKind()) {
 ${neverconstrules}

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index a5d5febe93c9c71962d7919724ad01b851cdc211..2dc74afdbe6c76b5cd9d445d6bb3ffee5197e004 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1839,7 +1839,7 @@ postfixTerm[CVC4::Expr& f]
         } else if(f.getKind() == CVC4::kind::EMPTYSET && t.isSet()) {
           f = MK_CONST(CVC4::EmptySet(t));
         } else if(f.getKind() == CVC4::kind::UNIVERSE_SET && t.isSet()) {
-          f = EXPR_MANAGER->mkUniqueVar(t, kind::UNIVERSE_SET);
+          f = EXPR_MANAGER->mkNullaryOperator(t, kind::UNIVERSE_SET);
         } else {
           if(f.getType() != t) {
             PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -2075,7 +2075,7 @@ simpleTerm[CVC4::Expr& f]
     { f = MK_CONST(EmptySet(Type())); }
   | UNIVSET_TOK
     { //booleanType is placeholder
-      f = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET);
+      f = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET);
     }
 
     /* finite set literal */

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 33674770d184556910b592c4cb7619838a73cf23..740e35ba4f818469b397223f8a7b409a39c474fd 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1868,12 +1868,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
                           << f2 << " " << type <<  std::endl;
         expr = MK_CONST( ::CVC4::EmptySet(type) );
       } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) {
-        expr = EXPR_MANAGER->mkUniqueVar(type, kind::UNIVERSE_SET);
+        expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET);
       } else if(f.getKind() == CVC4::kind::SEP_NIL) {
         //We don't want the nil reference to be a constant: for instance, it
         //could be of type Int but is not a const rational. However, the
         //expression has 0 children. So we convert to a SEP_NIL variable.
-        expr = EXPR_MANAGER->mkUniqueVar(type, kind::SEP_NIL);
+        expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL);
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -2304,11 +2304,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
 
   | UNIVSET_TOK
     { //booleanType is placeholder here since we don't have type info without type annotation
-      expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); }
+      expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); }
 
   | NILREF_TOK
     { //booleanType is placeholder here since we don't have type info without type annotation
-      expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::SEP_NIL); }
+      expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::SEP_NIL); }
     // NOTE: Theory constants go here
   ;
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8ae432162c0e66662969c8ac788ebeb0c6dadff1..94ff5d9b3703f010a7c27bf851653250c15faa69 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -893,7 +893,8 @@ public:
     Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl;
 
     if(n.getMetaKind() == kind::metakind::CONSTANT ||
-       n.getMetaKind() == kind::metakind::VARIABLE)
+       n.getMetaKind() == kind::metakind::VARIABLE ||
+       n.getMetaKind() == kind::metakind::NULLARY_OPERATOR)
     {
       return n;
     }

diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index 358c63f550d33bdc0c6478e3bbd464d094ceeb37..b83515d388cf721edcb37666de63bf166c0bcdcd 100644 (file)
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -12,7 +12,7 @@ properties check propagate presolve getNextDecisionRequest
 
 rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h"
 
-variable SEP_NIL "separation nil"
+nullaryoperator SEP_NIL "separation nil"
 
 operator SEP_EMP 2 "separation empty heap"
 operator SEP_PTO 2 "points to relation"
@@ -25,5 +25,6 @@ typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule
 typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule
 typerule SEP_WAND ::CVC4::theory::sep::SepWandTypeRule
 typerule SEP_LABEL ::CVC4::theory::sep::SepLabelTypeRule
+typerule SEP_NIL ::CVC4::theory::sep::SepNilTypeRule
 
 endtheory

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index ce5c0217920a2cb3cf9c9b8099edf5780a240854..9d064d74d4a379fe559812e224407b3d2c946e76 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1226,7 +1226,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
 Node TheorySep::getNilRef( TypeNode tn ) {
   std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn );
   if( it==d_nil_ref.end() ){
-    Node nil = NodeManager::currentNM()->mkUniqueVar( tn, kind::SEP_NIL );
+    Node nil = NodeManager::currentNM()->mkNullaryOperator( tn, kind::SEP_NIL );
     setNilRef( tn, nil );
     return nil;
   }else{

diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index 23e725a25baef5ce14916515746653ff20fc8cbb..25166ca8e1c1e3e9fb763fdd6f83744cf905812b 100644 (file)
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -99,6 +99,17 @@ struct SepLabelTypeRule {
   }
 };/* struct SepLabelTypeRule */
 
+struct SepNilTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::SEP_NIL);
+    Assert(check);
+    TypeNode type = n.getType(false);
+    return type;
+  }
+};/* struct SepLabelTypeRule */
+
+
 }/* CVC4::theory::sep namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index ab0ca3428b7d7c3583436532c0e4786d294f4bc6..cfe7eb632a71e36a346559907df0b7d28cee3fd9 100644 (file)
--- 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 5b9f4bf0350ca9ee1c10aea8e14f221e01a0fb9f..57ab8c0cf93e17dbf3374c82bdb5f6f47755462b 100644 (file)
--- 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 9669561a6c6c952a414e50cb1f4b0bcad5fedd98..8facf1f48e01795308c1eb24f43dcd64c0aca91f 100644 (file)
--- 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 11f375d5bcc941712e9665e6260a3a98370075ff..541835980ce0cb0c048bb15d738cfbc2c0ef0de2 100644 (file)
--- 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)

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 2b2ebbf5e9d53dbf87d3344a6e29f3136520ed6b..37d65972e95e00acb7fcdbf1ce9264d08d247471 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -271,12 +271,12 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
     // 1) x is a variable
     // 2) x is not in the term t
     // 3) x : T and t : S, then S <: T
-    if (in[0].isUninterpretedVar() && !in[1].hasSubterm(in[0]) &&
+    if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
         (in[1].getType()).isSubtypeOf(in[0].getType()) ){
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[1].isUninterpretedVar() && !in[0].hasSubterm(in[1]) &&
+    if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
         (in[0].getType()).isSubtypeOf(in[1].getType())){
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;