namespace CVC4 {
-class Node;
+template<bool ref_count>
+ class NodeTemplate;
+typedef NodeTemplate<true> Node;
+typedef NodeTemplate<false> TNode;
inline std::ostream& operator<<(std::ostream&, const Node&);
class Type;
namespace expr {
- class NodeValue;
+class NodeValue;
}/* CVC4::expr namespace */
using CVC4::expr::NodeValue;
* Encapsulation of an NodeValue pointer. The reference count is
* maintained in the NodeValue.
*/
-class Node {
+template<bool ref_count>
+ class NodeTemplate {
friend class NodeValue;
- /** A convenient null-valued encapsulated pointer */
- static Node s_null;
-
- /** The referenced NodeValue */
- NodeValue* d_ev;
-
- /** This constructor is reserved for use by the Node package; one
- * must construct an Node using one of the build mechanisms of the
- * Node package.
- *
- * Increments the reference count.
- *
- * FIXME: there's a type-system escape here to cast away the const,
- * since the refcount needs to be updated. But conceptually Nodes
- * don't change their arguments, and it's nice to have
- * const_iterators over them. See notes in .cpp file for
- * details. */
- // this really does needs to be explicit to avoid hard to track
- // errors with Nodes implicitly wrapping NodeValues
- explicit Node(const NodeValue*);
-
- template <unsigned> friend class NodeBuilder;
- friend class NodeManager;
+ /** A convenient null-valued encapsulated pointer */
+ static NodeTemplate s_null;
- /**
- * Assigns the expression value and does reference counting. No assumptions
- * are made on the expression, and should only be used if we know what we are
- * doing.
- *
- * @param ev the expression value to assign
- */
- void assignNodeValue(NodeValue* ev);
+ /** The referenced NodeValue */
+ NodeValue* d_ev;
+
+ bool d_count_ref;
+
+ /** This constructor is reserved for use by the NodeTemplate package; one
+ * must construct an NodeTemplate using one of the build mechanisms of the
+ * NodeTemplate package.
+ *
+ * Increments the reference count.
+ *
+ * FIXME: there's a type-system escape here to cast away the const,
+ * since the refcount needs to be updated. But conceptually Nodes
+ * don't change their arguments, and it's nice to have
+ * const_iterators over them. See notes in .cpp file for
+ * details. */
+ // this really does needs to be explicit to avoid hard to track
+ // errors with Nodes implicitly wrapping NodeValues
+ explicit NodeTemplate(const NodeValue*);
- typedef NodeValue::ev_iterator ev_iterator;
- typedef NodeValue::const_ev_iterator const_ev_iterator;
+ template<unsigned>
+ friend class NodeBuilder;
- inline ev_iterator ev_begin();
- inline ev_iterator ev_end();
- inline const_ev_iterator ev_begin() const;
- inline const_ev_iterator ev_end() const;
+ friend class NodeTemplate<true>;
+ friend class NodeTemplate<false>;
-public:
+ friend class NodeManager;
- /** Default constructor, makes a null expression. */
- Node();
+ /**
+ * Assigns the expression value and does reference counting. No assumptions
+ * are made on the expression, and should only be used if we know what we are
+ * doing.
+ *
+ * @param ev the expression value to assign
+ */
+ void assignNodeValue(NodeValue* ev);
- Node(const Node&);
+ typedef NodeValue::ev_iterator ev_iterator;
+ typedef NodeValue::const_ev_iterator const_ev_iterator;
- /** Destructor. Decrements the reference count and, if zero,
- * collects the NodeValue. */
- ~Node();
+ inline ev_iterator ev_begin();
+ inline ev_iterator ev_end();
+ inline const_ev_iterator ev_begin() const;
+ inline const_ev_iterator ev_end() const;
- bool operator==(const Node& e) const { return d_ev == e.d_ev; }
- bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
+ public:
+ /** Default constructor, makes a null expression. */
+ NodeTemplate();
+
+<<<<<<< .working
Node operator[](int i) const {
Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
return Node(d_ev->d_children[i]);
}
+=======
+ template <bool ref_count_1>
+ NodeTemplate(const NodeTemplate<ref_count_1>&);
+>>>>>>> .merge-right.r241
- /**
- * We compare by expression ids so, keeping things deterministic and having
- * that subexpressions have to be smaller than the enclosing expressions.
- */
- inline bool operator<(const Node& e) const;
+ /** Destructor. Decrements the reference count and, if zero,
+ * collects the NodeValue. */
+ ~NodeTemplate();
- Node& operator=(const Node&);
+ bool operator==(const NodeTemplate& e) const {
+ return d_ev == e.d_ev;
+ }
+ bool operator!=(const NodeTemplate& e) const {
+ return d_ev != e.d_ev;
+ }
- size_t hash() const { return d_ev->getId(); }
- uint64_t getId() const { return d_ev->getId(); }
+ NodeTemplate operator[](int i) const {
+ Assert(i >= 0 && i < d_ev->d_nchildren);
+ return NodeTemplate(d_ev->d_children[i]);
+ }
- Node eqExpr(const Node& right) const;
- Node notExpr() const;
- Node andExpr(const Node& right) const;
- Node orExpr(const Node& right) const;
- Node iteExpr(const Node& thenpart, const Node& elsepart) const;
- Node iffExpr(const Node& right) const;
- Node impExpr(const Node& right) const;
- Node xorExpr(const Node& right) const;
+ /**
+ * We compare by expression ids so, keeping things deterministic and having
+ * that subexpressions have to be smaller than the enclosing expressions.
+ */
+ inline bool operator<(const NodeTemplate& e) const;
+<<<<<<< .working
/*
Node plusExpr(const Node& right) const;
Node uMinusExpr() const;
Node multExpr(const Node& right) const;
+=======
+ NodeTemplate& operator=(const NodeTemplate&);
+>>>>>>> .merge-right.r241
*/
- inline Kind getKind() const;
+ size_t hash() const {
+ return d_ev->getId();
+ }
- inline size_t getNumChildren() const;
+ uint64_t getId() const {
+ return d_ev->getId();
+ }
const Type* getType() const;
- static Node null();
+ const Type* getType() const;
- typedef NodeValue::node_iterator iterator;
- typedef NodeValue::node_iterator const_iterator;
+ NodeTemplate eqExpr(const NodeTemplate& right) const;
+ NodeTemplate notExpr() const;
+ NodeTemplate andExpr(const NodeTemplate& right) const;
+ NodeTemplate orExpr(const NodeTemplate& right) const;
+ NodeTemplate iteExpr(const NodeTemplate& thenpart,
+ const NodeTemplate& elsepart) const;
+ NodeTemplate iffExpr(const NodeTemplate& right) const;
+ NodeTemplate impExpr(const NodeTemplate& right) const;
+ NodeTemplate xorExpr(const NodeTemplate& right) const;
- inline iterator begin();
- inline iterator end();
- inline const_iterator begin() const;
- inline const_iterator end() const;
+ NodeTemplate plusExpr(const NodeTemplate& right) const;
+ NodeTemplate uMinusExpr() const;
+ NodeTemplate multExpr(const NodeTemplate& right) const;
- inline std::string toString() const;
- inline void toStream(std::ostream&) const;
+ inline Kind getKind() const;
- bool isNull() const;
- bool isAtomic() const;
+ inline size_t getNumChildren() const;
+<<<<<<< .working
template <class AttrKind>
inline typename AttrKind::value_type getAttribute(const AttrKind&) const;
+=======
+ static NodeTemplate null();
+>>>>>>> .merge-right.r241
+<<<<<<< .working
template <class AttrKind>
inline bool hasAttribute(const AttrKind&,
typename AttrKind::value_type* = NULL) const;
+=======
+ typedef typename NodeValue::iterator<ref_count> iterator;
+ typedef typename NodeValue::iterator<ref_count> const_iterator;
+>>>>>>> .merge-right.r241
- template <class AttrKind>
- inline void setAttribute(const AttrKind&,
- const typename AttrKind::value_type& value);
+ inline iterator begin();
+ inline iterator end();
+ inline const_iterator begin() const;
+ inline const_iterator end() const;
+
+ template <class AttrKind>
+ inline typename AttrKind::value_type getAttribute(const AttrKind&) const;
+
+ template <class AttrKind>
+ inline bool hasAttribute(const AttrKind&, typename AttrKind::value_type* = NULL) const;
+
+ inline std::string toString() const;
+ inline void toStream(std::ostream&) const;
+
+
+ bool isNull() const;
+ bool isAtomic() const;
/**
* Very basic pretty printer for Node.
*/
void debugPrint();
-};/* class Node */
+ template<class AttrKind>
+ inline void setAttribute(
+ const AttrKind&, const typename AttrKind::value_type& value);
+
+ static void indent(std::ostream & o, int indent) {
+ for(int i = 0; i < indent; i++)
+ o << ' ';
+ }
+
+ };/* class NodeTemplate */
}/* CVC4 namespace */
// for hashtables
namespace __gnu_cxx {
- template <>
+template<>
struct hash<CVC4::Node> {
size_t operator()(const CVC4::Node& node) const {
- return (size_t)node.hash();
+ return (size_t) node.hash();
}
};
}/* __gnu_cxx namespace */
namespace CVC4 {
-inline bool Node::operator<(const Node& e) const {
- return d_ev->d_id < e.d_ev->d_id;
-}
+template<bool ref_count>
+ inline bool NodeTemplate<ref_count>::operator<(const NodeTemplate& e) const {
+ return d_ev->d_id < e.d_ev->d_id;
+ }
inline std::ostream& operator<<(std::ostream& out, const Node& e) {
e.toStream(out);
return out;
}
-inline Kind Node::getKind() const {
- return Kind(d_ev->d_kind);
-}
+template<bool ref_count>
+ inline Kind NodeTemplate<ref_count>::getKind() const {
+ return Kind(d_ev->d_kind);
+ }
-inline std::string Node::toString() const {
- return d_ev->toString();
-}
+template<bool ref_count>
+ inline std::string NodeTemplate<ref_count>::toString() const {
+ return d_ev->toString();
+ }
-inline void Node::toStream(std::ostream& out) const {
- d_ev->toStream(out);
-}
+template<bool ref_count>
+ inline void NodeTemplate<ref_count>::toStream(std::ostream& out) const {
+ d_ev->toStream(out);
+ }
-inline Node::ev_iterator Node::ev_begin() {
- return d_ev->ev_begin();
-}
+template<bool ref_count>
+ inline typename NodeTemplate<ref_count>::ev_iterator NodeTemplate<ref_count>::ev_begin() {
+ return d_ev->ev_begin();
+ }
-inline Node::ev_iterator Node::ev_end() {
- return d_ev->ev_end();
-}
+template<bool ref_count>
+ inline typename NodeTemplate<ref_count>::ev_iterator NodeTemplate<ref_count>::ev_end() {
+ return d_ev->ev_end();
+ }
-inline Node::const_ev_iterator Node::ev_begin() const {
- return d_ev->ev_begin();
-}
+template<bool ref_count>
+ inline typename NodeTemplate<ref_count>::const_ev_iterator NodeTemplate<
+ ref_count>::ev_begin() const {
+ return d_ev->ev_begin();
+ }
-inline Node::const_ev_iterator Node::ev_end() const {
- return d_ev->ev_end();
-}
+template<bool ref_count>
+ inline typename NodeTemplate<ref_count>::const_ev_iterator NodeTemplate<
+ ref_count>::ev_end() const {
+ return d_ev->ev_end();
+ }
-inline Node::iterator Node::begin() {
- return d_ev->begin();
-}
+template<bool ref_count>
+ inline typename NodeTemplate<ref_count>::iterator NodeTemplate<ref_count>::begin() {
+ return d_ev->begin<ref_count> ();
+ }
-inline Node::iterator Node::end() {
- return d_ev->end();
-}
+template<bool ref_count>
+ inline typename NodeTemplate<ref_count>::iterator NodeTemplate<ref_count>::end() {
+ return d_ev->end<ref_count> ();
+ }
-inline Node::const_iterator Node::begin() const {
- return d_ev->begin();
-}
+template<bool ref_count>
+ inline typename NodeTemplate<ref_count>::const_iterator NodeTemplate<
+ ref_count>::begin() const {
+ return d_ev->begin<ref_count> ();
+ }
-inline Node::const_iterator Node::end() const {
- return d_ev->end();
-}
+template<bool ref_count>
+ inline typename NodeTemplate<ref_count>::const_iterator NodeTemplate<
+ ref_count>::end() const {
+ return d_ev->end<ref_count> ();
+ }
-inline size_t Node::getNumChildren() const {
- return d_ev->d_nchildren;
-}
+template<bool ref_count>
+ inline size_t NodeTemplate<ref_count>::getNumChildren() const {
+ return d_ev->d_nchildren;
+ }
+template <bool ref_count>
template <class AttrKind>
+<<<<<<< .working
inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) const {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
"Perhaps a public-facing function is missing a NodeManagerScope ?" );
+=======
+inline typename AttrKind::value_type NodeTemplate<ref_count>::getAttribute(const AttrKind&) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
+>>>>>>> .merge-right.r241
return NodeManager::currentNM()->getAttribute(*this, AttrKind());
}
+template <bool ref_count>
template <class AttrKind>
+<<<<<<< .working
inline bool Node::hasAttribute(const AttrKind&,
typename AttrKind::value_type* ret) const {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
"Perhaps a public-facing function is missing a NodeManagerScope ?" );
+=======
+inline bool NodeTemplate<ref_count>::hasAttribute(const AttrKind&,
+ typename AttrKind::value_type* ret) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
+>>>>>>> .merge-right.r241
return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
}
+template <bool ref_count>
template <class AttrKind>
-inline void Node::setAttribute(const AttrKind&,
+inline void NodeTemplate<ref_count>::setAttribute(const AttrKind&,
const typename AttrKind::value_type& value) {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
}
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&NodeValue::s_null);
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::null() {
+ return s_null;
+ }
+
+template<bool ref_count>
+ bool NodeTemplate<ref_count>::isNull() const {
+ return d_ev == &NodeValue::s_null;
+ }
+
+////FIXME: This function is a major hack! Should be changed ASAP
+////TODO: Should use positive definition, i.e. what kinds are atomic.
+template<bool ref_count>
+ bool NodeTemplate<ref_count>::isAtomic() const {
+ switch(getKind()) {
+ case NOT:
+ case XOR:
+ case ITE:
+ case IFF:
+ case IMPLIES:
+ case OR:
+ case AND:
+ return false;
+ default:
+ return true;
+ }
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count>::NodeTemplate() :
+ d_ev(&NodeValue::s_null) {
+ // No refcount needed
+ }
+
+// 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
+// support node_iterators over const NodeValue*. So.... hm.
+template<bool ref_count>
+ NodeTemplate<ref_count>::NodeTemplate(const NodeValue* ev) :
+ d_ev(const_cast<NodeValue*> (ev)) {
+ Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+ if(ref_count)
+ d_ev->inc();
+ }
+
+template<bool ref_count>
+template<bool ref_count_1>
+ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count_1>& e) {
+ Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
+ d_ev = e.d_ev;
+ if(ref_count)
+ d_ev->inc();
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count>::~NodeTemplate() {
+ Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+ if(ref_count)
+ d_ev->dec();
+ Assert(ref_count || d_ev->d_rc > 0,
+ "Temporary node pointing to an expired node");
+ }
+
+template<bool ref_count>
+ void NodeTemplate<ref_count>::assignNodeValue(NodeValue* ev) {
+ d_ev = ev;
+ if(ref_count)
+ d_ev->inc();
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count>& NodeTemplate<ref_count>::operator=
+ (const NodeTemplate<ref_count>& e) {
+ Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+ Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!");
+ if(EXPECT_TRUE( d_ev != e.d_ev )) {
+ if(ref_count)
+ d_ev->dec();
+ d_ev = e.d_ev;
+ if(ref_count)
+ d_ev->inc();
+ }
+ return *this;
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::eqExpr(const NodeTemplate<
+ ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::notExpr() const {
+ return NodeManager::currentNM()->mkNode(NOT, *this);
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::andExpr(
+ const NodeTemplate<ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(AND, *this, right);
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::orExpr(
+ const NodeTemplate<ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(OR, *this, right);
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::iteExpr(
+ const NodeTemplate<ref_count>& thenpart,
+ const NodeTemplate<ref_count>& elsepart) const {
+ return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::iffExpr(
+ const NodeTemplate<ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(IFF, *this, right);
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::impExpr(
+ const NodeTemplate<ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
+ }
+
+template<bool ref_count>
+ NodeTemplate<ref_count> NodeTemplate<ref_count>::xorExpr(
+ const NodeTemplate<ref_count>& right) const {
+ return NodeManager::currentNM()->mkNode(XOR, *this, right);
+ }
+
+
+template<bool ref_count>
+ void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
+ indent(out, ind);
+ out << '(';
+ out << getKind();
+ if(getKind() == VARIABLE) {
+ out << ' ' << getId();
+
+ } else if(getNumChildren() >= 1) {
+ for(const_iterator child = begin(); child != end(); ++child) {
+ out << std::endl;
+ NodeTemplate((*child)).printAst(out, ind + 1);
+ }
+ out << std::endl;
+ indent(out, ind);
+ }
+ out << ')';
+ }
+
+template<bool ref_count>
+ void NodeTemplate<ref_count>::debugPrint() {
+ printAst(Warning(), 0);
+ Warning().flush();
+ }
+
+template<bool ref_count>
+const Type* NodeTemplate<ref_count>::getType() const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ return NodeManager::currentNM()->getType(*this);
+}
+
}/* CVC4 namespace */
#endif /* __CVC4__NODE_H */
assertClause(clause);
}
-bool CnfStream::isCached(const Node& n) const {
+bool CnfStream::isCached(const TNode& n) const {
return d_translationCache.find(n) != d_translationCache.end();
}
-SatLiteral CnfStream::lookupInCache(const Node& n) const {
+SatLiteral CnfStream::lookupInCache(const TNode& n) const {
Assert(isCached(n), "Node is not in CNF translation cache");
return d_translationCache.find(n)->second;
}
-void CnfStream::cacheTranslation(const Node& node, SatLiteral lit) {
+void CnfStream::cacheTranslation(const TNode& node, SatLiteral lit) {
Debug("cnf") << "caching translation " << node << " to " << lit << endl;
- d_translationCache.insert(make_pair(node, lit));
+ d_translationCache[node] = lit;
}
-SatLiteral CnfStream::newLiteral(const Node& node) {
+SatLiteral CnfStream::newLiteral(const TNode& node) {
SatLiteral lit = SatLiteral(d_satSolver->newVar());
cacheTranslation(node, lit);
return lit;
}
-SatLiteral TseitinCnfStream::handleAtom(const Node& node) {
+SatLiteral TseitinCnfStream::handleAtom(const TNode& node) {
Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom");
Assert(!isCached(node), "atom already mapped!");
return lit;
}
-SatLiteral TseitinCnfStream::handleXor(const Node& xorNode) {
+SatLiteral TseitinCnfStream::handleXor(const TNode& xorNode) {
Assert(!isCached(xorNode), "Atom already mapped!");
Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
return xorLit;
}
-SatLiteral TseitinCnfStream::handleOr(const Node& orNode) {
+SatLiteral TseitinCnfStream::handleOr(const TNode& orNode) {
Assert(!isCached(orNode), "Atom already mapped!");
Assert(orNode.getKind() == OR, "Expecting an OR expression!");
Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
unsigned n_children = orNode.getNumChildren();
// Transform all the children first
- Node::iterator node_it = orNode.begin();
- Node::iterator node_it_end = orNode.end();
+ TNode::const_iterator node_it = orNode.begin();
+ TNode::const_iterator node_it_end = orNode.end();
SatClause clause(n_children + 1);
for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
clause[i] = toCNF(*node_it);
return orLit;
}
-SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) {
+SatLiteral TseitinCnfStream::handleAnd(const TNode& andNode) {
Assert(!isCached(andNode), "Atom already mapped!");
Assert(andNode.getKind() == AND, "Expecting an AND expression!");
Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
unsigned n_children = andNode.getNumChildren();
// Transform all the children first (remembering the negation)
- Node::iterator node_it = andNode.begin();
- Node::iterator node_it_end = andNode.end();
+ TNode::const_iterator node_it = andNode.begin();
+ TNode::const_iterator node_it_end = andNode.end();
SatClause clause(n_children + 1);
for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
clause[i] = ~toCNF(*node_it);
return andLit;
}
-SatLiteral TseitinCnfStream::handleImplies(const Node& impliesNode) {
+SatLiteral TseitinCnfStream::handleImplies(const TNode& impliesNode) {
Assert(!isCached(impliesNode), "Atom already mapped!");
Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
}
-SatLiteral TseitinCnfStream::handleIff(const Node& iffNode) {
+SatLiteral TseitinCnfStream::handleIff(const TNode& iffNode) {
Assert(!isCached(iffNode), "Atom already mapped!");
Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
}
-SatLiteral TseitinCnfStream::handleNot(const Node& notNode) {
+SatLiteral TseitinCnfStream::handleNot(const TNode& notNode) {
Assert(!isCached(notNode), "Atom already mapped!");
Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!");
return notLit;
}
-SatLiteral TseitinCnfStream::handleIte(const Node& iteNode) {
+SatLiteral TseitinCnfStream::handleIte(const TNode& iteNode) {
Assert(iteNode.getKind() == ITE);
Assert(iteNode.getNumChildren() == 3);
return iteLit;
}
-SatLiteral TseitinCnfStream::toCNF(const Node& node) {
+SatLiteral TseitinCnfStream::toCNF(const TNode& node) {
// If the node has already been translated, return the previous translation
if(isCached(node)) {
}
}
-void TseitinCnfStream::convertAndAssert(const Node& node) {
+void TseitinCnfStream::convertAndAssert(const TNode& node) {
Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
// If the node is a conjuntion, we handle each conjunct separatelu
if (node.getKind() == AND) {
- Node::iterator conjunct = node.begin();
- Node::iterator node_end = node.end();
+ TNode::const_iterator conjunct = node.begin();
+ TNode::const_iterator node_end = node.end();
while (conjunct != node_end) {
convertAndAssert(*conjunct);
++ conjunct;
if (node.getKind() == OR) {
int nChildren = node.getNumChildren();
SatClause clause(nChildren);
- Node::iterator disjunct = node.begin();
+ TNode::const_iterator disjunct = node.begin();
for (int i = 0; i < nChildren; ++ disjunct, ++ i) {
clause[i] = toCNF(*disjunct);
}
projects / cvc5.git / commitdiff