diff options
Diffstat (limited to 'src/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 493dbfe01..f7561d945 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -145,9 +145,8 @@ class PropEngine * * @param trn the trust node storing the formula to assert * @param p the properties of the lemma - * @return the (preprocessed) lemma */ - Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p); + void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p); /** * If ever n is decided upon, it must be in the given phase. This @@ -209,6 +208,20 @@ class PropEngine * if preprocessing n involves introducing new skolems. */ Node getPreprocessedTerm(TNode n); + /** + * Same as above, but also compute the skolems in n and in the lemmas + * corresponding to their definition. + * + * Note this will include skolems that occur in the definition lemma + * for all skolems in sks. This is run until a fixed point is reached. + * For example, if k1 has definition (ite A (= k1 k2) (= k1 x)) where k2 is + * 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. + */ + Node getPreprocessedTerm(TNode n, + std::vector<Node>& skAsserts, + std::vector<Node>& sks); /** * Push the context level. |