diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-30 02:29:00 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-30 02:29:00 +0000 |
commit | 5fad8e60577136632f12b05fc07336b77fbabe7b (patch) | |
tree | 4ff4c244ce0e7e16afee90e1b277183e272fa08d /src/prop/cnf_stream.h | |
parent | e664ad1de4d35f5e37055706390a3e0ee6d8219b (diff) |
fixes to incremental simplification, cnf routines, other stuff in preparation of user push/pop in SAT solver
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index ecb0fd2fb..3ef636811 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -215,12 +215,16 @@ public: TNode getNode(const SatLiteral& literal); /** - * Returns true if the node has an assigned literal (it might not be translated). - * Caches the pair of the node and the literal corresponding to the - * translation. + * Returns true iff the node has an assigned literal (it might not be translated). * @param node the node */ - bool hasLiteral(TNode node) const; + bool hasEverHadLiteral(TNode node) const; + + /** + * Returns true iff the node has an assigned literal and it's translated. + * @param node the node + */ + bool currentlyHasLiteral(TNode node) const; /** * Returns the literal that represents the given node in the SAT CNF |