diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-31 15:26:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-31 15:26:19 +0000 |
commit | 39031822cf3f9faab7b5b9e6cbce46a5194503b1 (patch) | |
tree | 7f95265819554a20a2ef4637a4a8a6a83a7cfc0b /src/prop/cnf_stream.h | |
parent | d4bfaa103d56d5c0172bf1457343a75ddea8a9b5 (diff) |
enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some documentation, and make it possible to "make doc" on a clean source tree (post-configure)
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 42 |
1 files changed, 25 insertions, 17 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 919214f9b..e307732f4 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -24,8 +24,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__CNF_STREAM_H -#define __CVC4__CNF_STREAM_H +#ifndef __CVC4__PROP__CNF_STREAM_H +#define __CVC4__PROP__CNF_STREAM_H #include "expr/node.h" #include "prop/sat.h" @@ -35,6 +35,7 @@ namespace CVC4 { namespace prop { + class PropEngine; /** @@ -70,18 +71,21 @@ protected: /** * Asserts the given clause to the sat solver. + * @param node the node giving rise to this clause * @param clause the clasue to assert */ void assertClause(TNode node, SatClause& clause); /** * Asserts the unit clause to the sat solver. + * @param node the node giving rise to this clause * @param a the unit literal of the clause */ void assertClause(TNode node, SatLiteral a); /** * Asserts the binary clause to the sat solver. + * @param node the node giving rise to this clause * @param a the first literal in the clause * @param b the second literal in the clause */ @@ -89,6 +93,7 @@ protected: /** * Asserts the ternary clause to the sat solver. + * @param node the node giving rise to this clause * @param a the first literal in the clause * @param b the second literal in the clause * @param c the thirs literal in the clause @@ -96,33 +101,33 @@ protected: void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); /** - * Returns true if the node has been cashed in the translation cache. + * Returns true if the node has been cached in the translation cache. * @param node the node * @return true if the node has been cached */ bool isCached(TNode node) const; /** - * Returns the cashed literal corresponding to the given node. + * Returns the cached literal corresponding to the given node. * @param node the node to lookup * @return returns the corresponding literal */ - SatLiteral lookupInCache(TNode n) const; + SatLiteral lookupInCache(TNode node) const; /** * Caches the pair of the node and the literal corresponding to the * translation. - * @param node node - * @param lit + * @param node the node + * @param lit the literal */ void cacheTranslation(TNode node, SatLiteral lit); /** - * Acquires a new variable from the SAT solver to represent the node and - * inserts the necessary data it into the mapping tables. + * Acquires a new variable from the SAT solver to represent the node + * and inserts the necessary data it into the mapping tables. * @param node a formula - * @param theoryLiteral is this literal a theory literal (i.e. theory to be - * informed when set to true/false + * @param theoryLiteral whether this literal a theory literal (and + * therefore the theory is to be informed when set to true/false) * @return the literal corresponding to the formula */ SatLiteral newLiteral(TNode node, bool theoryLiteral = false); @@ -140,8 +145,8 @@ protected: public: /** - * Constructs a CnfStream that sends constructs an equi-satisfiable set of clauses - * and sends them to the given sat solver. + * Constructs a CnfStream that sends constructs an equi-satisfiable + * set of clauses and sends them to the given sat solver. * @param satSolver the sat solver to use */ CnfStream(SatInputInterface* satSolver); @@ -157,7 +162,7 @@ public: /** * Converts and asserts a formula. * @param node node to convert and assert - * @param whether the sat solver can choose to remove the clauses + * @param lemma whether the sat solver can choose to remove the clauses * @param negated wheather we are asserting the node negated */ virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0; @@ -184,8 +189,10 @@ public: const NodeCache& getNodeCache() const { return d_nodeCache; } + };/* class CnfStream */ + /** * TseitinCnfStream is based on the following recursive algorithm * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf @@ -249,9 +256,10 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); -}; /* class TseitinCnfStream */ +};/* class TseitinCnfStream */ + -}/* prop namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__CNF_STREAM_H */ +#endif /* __CVC4__PROP__CNF_STREAM_H */ |