diff options
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r-- | src/prop/prop_engine.h | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 631317c2d..a12816906 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -157,6 +157,22 @@ class PropEngine bool isDecision(Node lit) const; /** + * Return the current decision level of `lit`. + * + * @param lit: The node in question, must have an associated SAT literal. + * @return Decision level of the SAT variable of `lit` (phase is disregarded), + * or -1 if `lit` has not been assigned yet. + */ + int32_t getDecisionLevel(Node lit) const; + + /** + * Return the user-context level when `lit` was introduced.. + * + * @return User-context level or -1 if not yet introduced. + */ + int32_t getIntroLevel(Node lit) const; + + /** * Checks the current context for satisfiability. * */ |