# 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
"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
"util/bitvector.h" \
"bit-vector type"
-
\ No newline at end of file
+
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);
*/
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 <class T>
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
check_theory_seen
}
-function nonatomic_operator {
- # nonatomic_operator K #children ["comment"]
-
- lineno=${BASH_LINENO[0]}
-
- check_theory_seen
-}
-
function parameterized {
# parameterized K #children ["comment"]
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"]
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"]
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 */
";
b=$(basename $(dirname "$kf"))
metakind_kinds="${metakind_kinds}
/* from $b */
-"
- metakind_canbeatomic="${metakind_canbeatomic}
- /* from $b */
"
metakind_operatorKinds="${metakind_operatorKinds}
/* from $b */
for var in \
metakind_includes \
metakind_kinds \
- metakind_canbeatomic \
metakind_constantMaps \
metakind_compares \
metakind_constHashes \
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
template <bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
-template <bool ref_count>
-inline bool NodeTemplate<ref_count>::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
// attribute tags
struct TypeTag {};
- struct AtomicTag {};
// NodeManager's attributes. These aren't exposed outside of this
// class; use the getters.
typedef expr::Attribute<TypeTag, TypeNode> TypeAttr;
- typedef expr::Attribute<AtomicTag, bool> 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:
* 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);
- }
};
/**
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) {
}
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);
return lookupInCache(node);
}
- // Atomic nodes are treated specially
- if(node.isAtomic()) {
- return handleAtom(node);
- }
-
// Handle each Boolean operator case
switch(node.getKind()) {
case NOT:
default:
{
Node atomic = handleNonAtomicNode(node);
- AlwaysAssert(isCached(atomic) || atomic.isAtomic());
- return toCNF(atomic);
+ return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
}
}
}
"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"
do_theoryof "$1"
}
-function nonatomic_operator {
- # nonatomic_operator K #children ["comment"]
-
- lineno=${BASH_LINENO[0]}
-
- do_theoryof "$1"
-}
-
function parameterized {
# parameterized K #children ["comment"]
TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
lastId = attr::LastAttributeId<bool, false>::s_id;
- TS_ASSERT_LESS_THAN(NodeManager::AtomicAttr::s_id, lastId);
TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag4::s_id, lastId);
TS_ASSERT_LESS_THAN(TestFlag5::s_id, lastId);
- TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id,
- theory::Theory::PreRegisteredAttr::s_id);
- TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag1::s_id);
- TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag2::s_id);
- TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag3::s_id);
- TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag4::s_id);
- TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag5::s_id);
TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag1::s_id);
TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag2::s_id);
TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag3::s_id);
TS_ASSERT(!null->isConst());
}
- void testIsAtomic() {
- /* bool isAtomic() const; */
-
- TS_ASSERT(a_bool->isAtomic());
- TS_ASSERT(b_bool->isAtomic());
- TS_ASSERT(c_bool_mult->isAtomic());
- TS_ASSERT(mult_op->isAtomic());
- TS_ASSERT(plus_op->isAtomic());
- TS_ASSERT(d_apply_fun_bool->isAtomic());
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS(null->isAtomic(), IllegalArgumentException);
-#endif /* CVC4_ASSERTIONS */
-
- TS_ASSERT(i1->isAtomic());
- TS_ASSERT(i2->isAtomic());
- TS_ASSERT(r1->isAtomic());
- TS_ASSERT(r2->isAtomic());
-
- Expr x = d_em->mkExpr(AND, *a_bool, *b_bool);
- Expr y = d_em->mkExpr(ITE, *a_bool, *b_bool, *c_bool_mult);
- Expr z = d_em->mkExpr(IFF, x, y);
-
- TS_ASSERT(!x.isAtomic());
- TS_ASSERT(!y.isAtomic());
- TS_ASSERT(!z.isAtomic());
-
- Expr w1 = d_em->mkExpr(PLUS, d_em->mkExpr(ITE, z, *i1, *i2), *i2);
- Expr w2 = d_em->mkExpr(PLUS, d_em->mkExpr(MULT, *i1, *i2), *i2);
-
- TS_ASSERT(!w1.isAtomic());
- TS_ASSERT(w2.isAtomic());
- }
-
void testGetConst() {
/* template <class T>
const T& getConst() const; */
projects / cvc5.git / commitdiff