Add skolem definition manager (#6187)

[cvc5.git] / src / prop / prop_engine.h

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d0810324ae1db44884e1d959e5de1fcf12d8e634..fe5d9412253732b729d17e537dfc231e047e2730 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -220,6 +220,10 @@ class PropEngine
    * another skolem introduced by term formula removal, then calling this
    * method on (P k1) will include both k1 and k2 in sks, and their definitions
    * in skAsserts.
+   *
+   * Notice that this method is not frequently used. It is used for algorithms
+   * that explicitly care about knowing which skolems occur in the preprocessed
+   * form of a term, recursively.
    */
   Node getPreprocessedTerm(TNode n,
                            std::vector<Node>& skAsserts,