diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 23:01:16 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 23:01:16 +0000 |
commit | 1ca8427a5c79e2e0425a55bc83fe8572055e1660 (patch) | |
tree | c9431983b76c3884a4e34a95c7a94476b95efc51 /src/prop/cnf_stream.h | |
parent | c5872ac197a68ea0686c90f3a8bd1e7cc993532d (diff) |
Merging from branch branches/Liana r241
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index d7bb3c265..83a6aa68f 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -81,14 +81,14 @@ protected: * @param node the node * @return true if the node has been cached */ - bool isCached(const Node& node) const; + bool isCached(const TNode& node) const; /** * Returns the cashed literal corresponding to the given node. * @param node the node to lookup * @return returns the corresponding literal */ - SatLiteral lookupInCache(const Node& n) const; + SatLiteral lookupInCache(const TNode& n) const; /** * Caches the pair of the node and the literal corresponding to the @@ -96,7 +96,7 @@ protected: * @param node node * @param lit */ - void cacheTranslation(const Node& node, SatLiteral lit); + void cacheTranslation(const TNode& node, SatLiteral lit); /** * Acquires a new variable from the SAT solver to represent the node and @@ -104,7 +104,7 @@ protected: * @param node a formula * @return the literal corresponding to the formula */ - SatLiteral newLiteral(const Node& node); + SatLiteral newLiteral(const TNode& node); public: @@ -128,7 +128,7 @@ public: * @param node node to convert and assert * @param whether the sat solver can choose to remove this clause */ - virtual void convertAndAssert(const Node& node) = 0; + virtual void convertAndAssert(const TNode& node) = 0; }; /* class CnfStream */ @@ -150,7 +150,7 @@ public: * Convert a given formula to CNF and assert it to the SAT solver. * @param node the formula to assert */ - void convertAndAssert(const Node& node); + void convertAndAssert(const TNode& node); /** * Constructs the stream to use the given sat solver. @@ -170,21 +170,21 @@ private: // - returning l // // handleX( n ) can assume that n is not in d_translationCache - SatLiteral handleAtom(const Node& node); - SatLiteral handleNot(const Node& node); - SatLiteral handleXor(const Node& node); - SatLiteral handleImplies(const Node& node); - SatLiteral handleIff(const Node& node); - SatLiteral handleIte(const Node& node); - SatLiteral handleAnd(const Node& node); - SatLiteral handleOr(const Node& node); + SatLiteral handleAtom(const TNode& node); + SatLiteral handleNot(const TNode& node); + SatLiteral handleXor(const TNode& node); + SatLiteral handleImplies(const TNode& node); + SatLiteral handleIff(const TNode& node); + SatLiteral handleIte(const TNode& node); + SatLiteral handleAnd(const TNode& node); + SatLiteral handleOr(const TNode& node); /** * Transforms the node into CNF recursively. * @param node the formula to transform * @return the literal representing the root of the formula */ - SatLiteral toCNF(const Node& node); + SatLiteral toCNF(const TNode& node); }; /* class TseitinCnfStream */ |