diff options
Diffstat (limited to 'src/prop/cnf_stream.h')
| -rw-r--r-- | src/prop/cnf_stream.h | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 264e26777..2959ae726 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -191,16 +191,16 @@ class CnfStream { */ SatLiteral toCNF(TNode node, bool negated = false); - /** Specific clausifiers, based on the formula kinds, that clausify a formula, - * by calling toCNF into each of the formula's children under the respective - * kind, and introduce a literal definitionally equal to it. */ - SatLiteral handleNot(TNode node); - SatLiteral handleXor(TNode node); - SatLiteral handleImplies(TNode node); - SatLiteral handleIff(TNode node); - SatLiteral handleIte(TNode node); - SatLiteral handleAnd(TNode node); - SatLiteral handleOr(TNode node); + /** + * Specific clausifiers that clausify a formula based on the given formula + * kind and introduce a literal definitionally equal to it. + */ + void handleXor(TNode node); + void handleImplies(TNode node); + void handleIff(TNode node); + void handleIte(TNode node); + void handleAnd(TNode node); + void handleOr(TNode node); /** Stores the literal of the given node in d_literalToNodeMap. * |