From 6ac90a806f563981bc25fe06bb0dde35d62da7a9 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 27 May 2010 21:19:36 +0000 Subject: Remove isAtomic() as per 4/27/2010 meeting. Add comments about its potential design for later. Resolves bug 113, invalidates bugs 93 and 94. --- src/expr/builtin_kinds | 7 ++-- src/expr/expr_template.cpp | 6 ---- src/expr/expr_template.h | 18 +++++++--- src/expr/metakind_template.h | 16 --------- src/expr/mkexpr | 8 ----- src/expr/mkkind | 9 ----- src/expr/mkmetakind | 23 ------------- src/expr/node.h | 25 +++++++------- src/expr/node_manager.h | 79 ++++++++------------------------------------ src/prop/cnf_stream.cpp | 11 ++---- src/theory/booleans/kinds | 16 ++++----- src/theory/mktheoryof | 8 ----- 12 files changed, 49 insertions(+), 177 deletions(-) (limited to 'src') diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index 5ce38f5fd..50b858b31 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -17,13 +17,10 @@ # SKOLEM. # # operator K #children ["comment"] -# nonatomic_operator K #children ["comment"] # # Declares a "built-in" operator kind K. Really this is the same # as "variable" except that it has an operator (automatically -# generated by NodeManager). These two commands are identical, -# except that kinds declared with nonatomic_operator answer false -# to Node::isAtomic(). +# generated by NodeManager). # # You can specify an exact # of children required as the second # argument to the operator command. In debug mode, assertions are @@ -134,4 +131,4 @@ constant BITVECTOR_TYPE \ "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \ "util/bitvector.h" \ "bit-vector type" - \ No newline at end of file + diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 876b400fe..5c4e30a0c 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -182,12 +182,6 @@ bool Expr::isConst() const { return d_node->isConst(); } -bool Expr::isAtomic() const { - ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - return d_node->isAtomic(); -} - void Expr::toStream(std::ostream& out) const { ExprManagerScope ems(*this); d_node->toStream(out); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 99b57b0c2..08dd1d25f 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -211,11 +211,19 @@ public: */ bool isConst() const; - /** - * Check if this is an expression representing a constant. - * @return true if a constant expression - */ - bool isAtomic() const; + /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. + * + * It has been decided for now to hold off on implementations of + * these functions, as they may only be needed in CNF conversion, + * where it's pointless to do a lazy isAtomic determination by + * searching through the DAG, and storing it, since the result will + * only be used once. For more details see the 4/27/2010 CVC4 + * developer's meeting notes at: + * + * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 + */ + // bool containsDecision(); // is "atomic" + // bool properlyContainsDecision(); // maybe not atomic but all children are /** Extract a constant of type T */ template diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 5b0ac150b..3c17507cf 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -126,22 +126,6 @@ ${metakind_kinds} return metaKinds[k]; }/* metaKindOf(k) */ -/** - * Determine if a particular kind can be atomic or not. Some kinds - * are never atomic (OR, NOT, ITE...), some can be atomic depending on - * their children (PLUS might have an ITE under it, for instance). - */ -static inline bool kindCanBeAtomic(Kind k) { - static const bool canBeAtomic[] = { - false, /* NULL_EXPR */ -${metakind_canbeatomic} - false /* LAST_KIND */ - };/* canBeAtomic[] */ - - return canBeAtomic[k]; -}/* kindCanBeAtomic(k) */ - - /** * Map a kind of the operator to the kind of the enclosing expression. For * example, since the kind of functions is just VARIABLE, it should map diff --git a/src/expr/mkexpr b/src/expr/mkexpr index f59388def..35a245a84 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -104,14 +104,6 @@ function operator { check_theory_seen } -function nonatomic_operator { - # nonatomic_operator K #children ["comment"] - - lineno=${BASH_LINENO[0]} - - check_theory_seen -} - function parameterized { # parameterized K #children ["comment"] diff --git a/src/expr/mkkind b/src/expr/mkkind index d9c64b660..a417b7871 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -83,15 +83,6 @@ function operator { register_kind "$1" "$2" "$3" } -function nonatomic_operator { - # nonatomic_operator K #children ["comment"] - - lineno=${BASH_LINENO[0]} - - check_theory_seen - register_kind "$1" "$2" "$3" -} - function parameterized { # parameterized K1 K2 #children ["comment"] diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 4915a17ec..cf3fb1e97 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -99,15 +99,6 @@ function operator { register_metakind OPERATOR "$1" "$2" } -function nonatomic_operator { - # nonatomic_operator K #children ["comment"] - - lineno=${BASH_LINENO[0]} - - check_theory_seen - register_metakind NONATOMIC_OPERATOR "$1" "$2" -} - function parameterized { # parameterized K1 K2 #children ["comment"] @@ -217,16 +208,6 @@ function register_metakind { k=$2 nc=$3 - - if [ $mk = NONATOMIC_OPERATOR ]; then - metakind_canbeatomic="${metakind_canbeatomic} false, /* $k */ -"; - mk=OPERATOR - else - metakind_canbeatomic="${metakind_canbeatomic} true, /* $k */ -"; - fi - metakind_kinds="${metakind_kinds} metakind::$mk, /* $k */ "; @@ -296,9 +277,6 @@ while [ $# -gt 0 ]; do b=$(basename $(dirname "$kf")) metakind_kinds="${metakind_kinds} /* from $b */ -" - metakind_canbeatomic="${metakind_canbeatomic} - /* from $b */ " metakind_operatorKinds="${metakind_operatorKinds} /* from $b */ @@ -315,7 +293,6 @@ text=$(cat "$template") for var in \ metakind_includes \ metakind_kinds \ - metakind_canbeatomic \ metakind_constantMaps \ metakind_compares \ metakind_constHashes \ diff --git a/src/expr/node.h b/src/expr/node.h index 2abe762ed..0daa3f58c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -253,11 +253,19 @@ public: return NodeTemplate(d_nv->getChild(i)); } - /** - * Returns true if this node is atomic (has no more Boolean structure) - * @return true if atomic + /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. + * + * It has been decided for now to hold off on implementations of + * these functions, as they may only be needed in CNF conversion, + * where it's pointless to do a lazy isAtomic determination by + * searching through the DAG, and storing it, since the result will + * only be used once. For more details see the 4/27/2010 CVC4 + * developer's meeting notes at: + * + * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 */ - inline bool isAtomic() const; + // bool containsDecision(); // is "atomic" + // bool properlyContainsDecision(); // maybe not atomic but all children are /** * Returns true if this node represents a constant @@ -686,15 +694,6 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { template NodeTemplate NodeTemplate::s_null(&expr::NodeValue::s_null); -template -inline bool NodeTemplate::isAtomic() const { - if(!ref_count) { - Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); - } - - return NodeManager::currentNM()->isAtomic(*this); -} - // FIXME: escape from type system convenient but is there a better // way? Nodes conceptually don't change their expr values but of // course they do modify the refcount. But it's nice to be able to diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 35e73842e..098694c3d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -211,39 +211,24 @@ class NodeManager { // attribute tags struct TypeTag {}; - struct AtomicTag {}; // NodeManager's attributes. These aren't exposed outside of this // class; use the getters. typedef expr::Attribute TypeAttr; - typedef expr::Attribute AtomicAttr; - /** - * Returns true if this node is atomic (has no more Boolean - * structure). This is the NodeValue version for NodeManager's - * internal use. There's a public version of this function below - * that takes a TNode. - * @param nv the node to check for atomicity - * @return true if atomic - */ - inline bool isAtomic(expr::NodeValue* nv) const { - // The kindCanBeAtomic() and metakind checking are just optimizations - // (to avoid the hashtable lookup). We assume that all nodes have - // the atomic attribute pre-computed and set at their time of - // creation. This is because: - // (1) it's super cheap to do it bottom-up. - // (2) if we computed it lazily, we'd need a second attribute to - // tell us whether we had computed it yet or not. - // The pre-computation and registration occurs in poolInsert(). - AssertArgument(nv->getMetaKind() != kind::metakind::INVALID, *nv, - "NodeManager::isAtomic() called on INVALID node (%s)", - kind::kindToString(nv->getKind()).c_str()); - return - nv->getMetaKind() == kind::metakind::VARIABLE || - nv->getMetaKind() == kind::metakind::CONSTANT || - ( kind::kindCanBeAtomic(nv->getKind()) && - getAttribute(nv, AtomicAttr()) ); - } + /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. + * + * It has been decided for now to hold off on implementations of + * these functions, as they may only be needed in CNF conversion, + * where it's pointless to do a lazy isAtomic determination by + * searching through the DAG, and storing it, since the result will + * only be used once. For more details see the 4/27/2010 CVC4 + * developer's meeting notes at: + * + * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 + */ + // bool containsDecision(TNode); // is "atomic" + // bool properlyContainsDecision(TNode); // all children are atomic public: @@ -529,15 +514,6 @@ public: * Get the type for the given node. */ TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate); - - /** - * Returns true if this node is atomic (has no more Boolean structure) - * @param n the node to check for atomicity - * @return true if atomic - */ - inline bool isAtomic(TNode n) const { - return isAtomic(n.d_nv); - } }; /** @@ -707,35 +683,6 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) { Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), "NodeValue already in the pool!"); d_nodeValuePool.insert(nv);// FIXME multithreading - - switch(nv->getMetaKind()) { - case kind::metakind::INVALID: - case kind::metakind::VARIABLE: - case kind::metakind::CONSTANT: - // nothing to do (don't bother setting the attribute, isAtomic() - // on VARIABLEs and CONSTANTs is always true) - break; - - case kind::metakind::OPERATOR: - case kind::metakind::PARAMETERIZED: - { - // register this NodeValue as atomic or not; use nv_begin/end - // because we need to consider the operator too in the case of - // PARAMETERIZED-metakinded nodes (i.e. APPLYs); they could have a - // buried ITE. - - // assume it's atomic if its kind can be atomic, check children - // to see if that is actually true - bool atomic = kind::kindCanBeAtomic(nv->getKind()); - for(expr::NodeValue::nv_iterator i = nv->nv_begin(); - atomic && i != nv->nv_end(); - ++i) { - atomic = isAtomic(*i); - } - - setAttribute(nv, AtomicAttr(), atomic); - } - } } inline void NodeManager::poolRemove(expr::NodeValue* nv) { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index a245eb469..219c25399 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -115,11 +115,10 @@ const CnfStream::TranslationCache& CnfStream::getTranslationCache() const { } SatLiteral TseitinCnfStream::handleAtom(TNode node) { - Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom"); Assert(!isCached(node), "atom already mapped!"); Debug("cnf") << "handleAtom(" << node << ")" << endl; - + bool theoryLiteral = node.getKind() != kind::VARIABLE; SatLiteral lit = newLiteral(node, theoryLiteral); @@ -378,11 +377,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) { return lookupInCache(node); } - // Atomic nodes are treated specially - if(node.isAtomic()) { - return handleAtom(node); - } - // Handle each Boolean operator case switch(node.getKind()) { case NOT: @@ -402,8 +396,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) { default: { Node atomic = handleNonAtomicNode(node); - AlwaysAssert(isCached(atomic) || atomic.isAtomic()); - return toCNF(atomic); + return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic); } } } diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index bd85af69d..43c37f4b7 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -12,12 +12,10 @@ constant CONST_BOOLEAN \ "util/bool.h" \ "truth and falsity" -# these are nonatomic because they have boolean structure. -# i.e. nodes n with this kind return false for n.isAtomic() -nonatomic_operator NOT 1 "logical not" -nonatomic_operator AND 2: "logical and" -nonatomic_operator IFF 2 "logical equivalence" -nonatomic_operator IMPLIES 2 "logical implication" -nonatomic_operator OR 2: "logical or" -nonatomic_operator XOR 2 "exclusive or" -nonatomic_operator ITE 3 "if-then-else" +operator NOT 1 "logical not" +operator AND 2: "logical and" +operator IFF 2 "logical equivalence" +operator IMPLIES 2 "logical implication" +operator OR 2: "logical or" +operator XOR 2 "exclusive or" +operator ITE 3 "if-then-else" diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof index 842e02a07..227831451 100755 --- a/src/theory/mktheoryof +++ b/src/theory/mktheoryof @@ -84,14 +84,6 @@ function operator { do_theoryof "$1" } -function nonatomic_operator { - # nonatomic_operator K #children ["comment"] - - lineno=${BASH_LINENO[0]} - - do_theoryof "$1" -} - function parameterized { # parameterized K #children ["comment"] -- cgit v1.2.3