From: ajreynol Date: Fri, 14 Apr 2017 21:34:59 +0000 (-0500) Subject: Fix nullary operator printers, minor. X-Git-Tag: cvc5-1.0.0~5836 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d7766ed1e41da53d59ad16e9ef8be8f522226df;p=cvc5.git Fix nullary operator printers, minor. --- 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"); }