summaryrefslogtreecommitdiff
path: root/src/prop/prop_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r--src/prop/prop_engine.h7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index bb8ed86e1..16cb34e04 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -127,6 +127,13 @@ public:
bool hasValue(TNode node, bool& value);
/**
+ * Ensure that the given node will have a designated SAT literal
+ * that is definitionally equal to it. The result of this function
+ * is that the Node can be queried via getSatValue().
+ */
+ void ensureLiteral(TNode n);
+
+ /**
* Push the context level.
*/
void push();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback