Fix nullary operator printers, minor.

6 files changed, 49 insertions, 35 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 6d98b940b..bd1b5e63c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -457,14 +457,21 @@ public:
   bool isConst() const;
 
   /**
-   * Returns true if this node represents a constant
-   * @return true if const
+   * Returns true if this node represents a variable
    */
   inline bool isVar() const {
     assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::VARIABLE;
   }
-
+  
+  /**
+   * Returns true if this node represents a nullary operator
+   */
+  inline bool isNullaryOp() const {
+    assertTNodeNotExpired();
+    return getMetaKind() == kind::metakind::NULLARY_OPERATOR;
+  }
+  
   inline bool isClosure() const {
     assertTNodeNotExpired();
     return getKind() == kind::LAMBDA ||
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 2a819935d..7cf228403 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -412,8 +412,9 @@ TypeNode NodeManager::getType(TNode n, bool check)
   bool hasType = getAttribute(n, TypeAttr(), typeNode);
   bool needsCheck = check && !getAttribute(n, TypeCheckedAttr());
 
-  Debug("getType") << "getting type for " << n << endl;
 
+  Debug("getType") << this << " getting type for " << &n << " " << n << ", check=" << check << ", needsCheck = " << needsCheck << ", hasType = " << hasType << endl;
+  
   if(needsCheck && !(*d_options)[options::earlyTypeChecking]) {
     /* Iterate and compute the children bottom up. This avoids stack
        overflows in computeType() when the Node graph is really deep,
@@ -437,6 +438,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
       }
 
       if( readyToCompute ) {
+        Assert( check || m.getMetaKind()!=kind::metakind::NULLARY_OPERATOR );
         /* All the children have types, time to compute */
         typeNode = TypeChecker::computeType(this, m, check);
         worklist.pop();
@@ -448,6 +450,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
   } else if( !hasType || needsCheck ) {
     /* We can compute the type top-down, without worrying about
        deep recursion. */
+    Assert( check || n.getMetaKind()!=kind::metakind::NULLARY_OPERATOR );
     typeNode = TypeChecker::computeType(this, n, check);
   }
 
@@ -788,16 +791,18 @@ Node NodeManager::mkBooleanTermVariable() {
 }
 
 Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
+  //FIXME : this is not correct for multitheading
   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);
-    //should type check it
-    //n.setAttribute(TypeCheckedAttr(), true);
+    Node n = NodeBuilder<0>(this, k).constructNode();
+    setAttribute(n, TypeAttr(), type);
+    //setAttribute(n, TypeCheckedAttr(), true);
     d_unique_vars[k][type] = n;
     Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR );
+    Trace("ajr-temp") << this << "...made nullary operator " << n << std::endl;
     return n;
   }else{
+    Trace("ajr-temp") << this << "...reuse nullary operator " << it->second << std::endl;
     return it->second;
   }
 }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 7b0ccdb8a..6b42d4e74 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -90,8 +90,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     string s;
     if(n.getAttribute(expr::VarNameAttr(), s)) {
       out << s;
-    }else if( n.getKind() == kind::UNIVERSE_SET ){
-      out << "UNIVERSE :: " << n.getType();
     } else {
       if(n.getKind() == kind::VARIABLE) {
         out << "var_";
@@ -107,6 +105,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     }
     return;
   }
+  if(n.isNullaryOp()) {
+    if( n.getKind() == kind::UNIVERSE_SET ){
+      out << "UNIVERSE :: " << n.getType();
+    }else{
+      //unknown printer
+      out << n.getKind();
+    }
+    return;
+  }
 
   // constants
   if(n.getMetaKind() == kind::metakind::CONSTANT) {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index fcb6be366..57c02f3c7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -117,29 +117,21 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
 
   // variable
   if(n.isVar()) {
-    if( n.getKind() == kind::SEP_NIL ){
-      out << "(as sep.nil " << n.getType() << ")";
-      return;
-    }else if( n.getKind() == kind::UNIVERSE_SET ){
-      out << "(as univset " << n.getType() << ")";
-      return;
-    }else{
-      string s;
-      if(n.getAttribute(expr::VarNameAttr(), s)) {
-        out << maybeQuoteSymbol(s);
+    string s;
+    if(n.getAttribute(expr::VarNameAttr(), s)) {
+      out << maybeQuoteSymbol(s);
+    } else {
+      if(n.getKind() == kind::VARIABLE) {
+        out << "var_";
       } else {
-        if(n.getKind() == kind::VARIABLE) {
-          out << "var_";
-        } else {
-          out << n.getKind() << '_';
-        }
-        out << n.getId();
-      }
-      if(types) {
-        // print the whole type, but not *its* type
-        out << ":";
-        n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
+        out << n.getKind() << '_';
       }
+      out << n.getId();
+    }
+    if(types) {
+      // print the whole type, but not *its* type
+      out << ":";
+      n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
     }
 
     return;
@@ -520,7 +512,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::SET_TYPE:
   case kind::SINGLETON: 
   case kind::COMPLEMENT:out << smtKindString(k) << " "; break;
-
+  case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
+  
     // fp theory
   case kind::FLOATINGPOINT_FP:
   case kind::FLOATINGPOINT_EQ:
@@ -594,12 +587,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::PARAMETRIC_DATATYPE:
     break;
     
-  //separation
+  //separation logic
   case kind::SEP_EMP:
   case kind::SEP_PTO:
   case kind::SEP_STAR:
   case kind::SEP_WAND:out << smtKindString(k) << " "; break;
 
+  case kind::SEP_NIL:out << "(as sep.nil " << n.getType() << ")";break;
+
     // quantifiers
   case kind::FORALL:
   case kind::EXISTS:
diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index 25166ca8e..0eae782c8 100644
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -104,7 +104,7 @@ struct SepNilTypeRule {
     throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::SEP_NIL);
     Assert(check);
-    TypeNode type = n.getType(false);
+    TypeNode type = n.getType();
     return type;
   }
 };/* struct SepLabelTypeRule */
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 541835980..25ca63c28 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -180,7 +180,7 @@ struct UniverseSetTypeRule {
     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);
+    TypeNode setType = n.getType();
     if(!setType.isSet()) {
       throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found");
     }