Built foundation for activation literal management in PDR by michael-zhang-lambda · Pull Request #52 · cucapra/patronus

michael-zhang-lambda · 2026-08-25T15:20:28Z

This PR is essentially #50, but all activation literal usage that was not present before (including in PDR and BMC) are removed.

Thus, YICES2 will run all tests without (check-sat-assuming) and (get-unsat-assumptions).

Changes

Added new supports_check_assuming_exprs flag to mark solvers that can accept compound expression query assumptions
Removed create_act_lit from BasePdr
Implemented the ActLitScope struct that contains activation literals active in a given scope, which can then be permanently deactivated (i.e. assert $\neg \text{act}$ in solver) with the release method
Implemented the ActLitPool struct which provides helper methods to create activation literal implications (i.e. $\text{act} \Rightarrow \text{expr}$) in a ActLitScope, with an additional cache and special helper method (step_lit_act) to reuse activation literals for stepped cube literals (which are valid throughout the whole PDR run)
Added with_act_scope helper function to execute a closure with an activation literal scope, automatically disabling the relevant activation literals (i.e. those that are not associated with stepped cube literals)
Cleaned up stale documentation

…and added proxy variables to BMC

…ssumptions; made YICES2 skip some (get-unsat-assumptions) tests

…ivation literals from scope during cleanup

…fore

… literals for compound expressions in pdr

ekiwi · 2026-08-25T15:41:49Z

    fn name(&self) -> &str;
    fn supports_check_assuming(&self) -> bool;
+    /// Indicates whether `(check-sat-assuming ...)` accepts arbitrary Boolean-valued expressions
+    fn supports_check_assuming_exprs(&self) -> bool {


Please don't define this here. I would rather have each implementation of the trait provide their own explicit definition.

Understood. I'll make the change.

…erMetaData trait

ekiwi

There is new code that is never used. It also looks like you removed some activation literal cleanups without replacement.

ekiwi · 2026-08-28T14:44:17Z

+}
+
+/// Execute closure with a fresh [`ActLitScope`] and clean up all used activation literals in the end
+fn with_act_scope<S: SolverContext, T>(


Where is this used?

In the meantime, we don't have any activation literals that we want to permanently disable yet. This will be necessary once we get activation literals for compound formulas that we would only use once for a query (e.g. compound expressions in a relative inductiveness query).

Currently, all activation literals are coupled with formulas that are used throughout the program (such as the FROM_STEP bad states, TO_STEP constraints, and various stepped cube literals). To throw these away would mean wasting more solver time to redefine them when we need them. Therefore, their activation literals are permanently asserted in the solver and are cached to be used again as needed.

I can remove this helper function in this PR if you want to keep things clean for this PR.

ekiwi · 2026-08-28T14:45:16Z

+
+    /// Create a temporary activation literal that is coupled with `body` (i.e. `act => body`)
+    /// and registered into `scope`
+    fn imply(


Where is this used?

Currently, the only activation literals that we create should persist throughout the entire PDR run. imply is only used when we want an activation literal to be active for some scope (connecting back the the reason why we have no usages for with_act_scope).

In a sense, we can say that imply is always coupled with a call to with_act_scope. Thus, it is not used in the current PDR implementation.

ekiwi · 2026-08-28T14:45:58Z


            if check_res.0 && first_iter {
-                // Clean up activation literals
-                for &act in lit_map.keys() {


How does this cleanup happen now?

Since the activation literals are associated with stepped literals (instead of compound formulas), they could be used in a different context. Therefore, to prevent redefinition of activation literals, step_lit_act will cache the activation literal for the particular stepped literal.

If we were to deactivate these activation literals here, we may get a solver error in the future since the cache will still return the cached activation literal (which was already deactivated).

Even if these literals are removed from the cube, that does not necessarily mean that the literal does not exist elsewhere. For example, let's say that some literal was truly dropped in the fix_gen_cube subroutine. However, the same literal could exist in a CTI in block_cube. Just because we stopped using the literal in one instance doesn't mean it's useless in another! In this case, it would better to reuse the same activation literal, instead of creating a new one.

ekiwi · 2026-08-28T14:46:07Z


-            // Permanently disable literals that were removed
-            for &act in &prev_acts {
-                if !lit_map.contains_key(&act) {


How does this cleanup happen now?

Same reasoning as before.

ekiwi · 2026-08-28T14:46:13Z

                fin_lits.extend(lit_map.values().copied());
-
-                // Clean up activation literals
-                for &act in lit_map.keys() {


Same reasoning as before.

ekiwi · 2026-08-28T14:46:21Z

-        };
-
-        // Disable all created activation literals as cleanup
-        for &act in lit_map.keys() {


Same reasoning as before.

ekiwi · 2026-08-28T14:46:38Z

                smt_ctx.restart()?;

+                // Clear the stepped literal cache
+                state.pool.step_lit_cache.clear();


Why do you clear the cache here?

Also, since you clear the cache, should you also disable the associated activation literals?

This is a little bit of vestigial code from earlier. This code just wants to highlight that the cache for the pool is invalid (because the solver was previously cleared). Technically, this doesn't provide that much safety for the program because we still have stale solver formulas in the PdrEncodingWrapper, frame trace, etc. because the solver was restarted.

However, since PDR will subsequently call BMC and return, this is not an issue for now. I'm removing this to keep the code clean.

…Pdr::init

michael-zhang-lambda added 12 commits August 23, 2026 15:23

added proxies variables for PDR compound expressions

70e4e08

cleaned up proxy variables in PDR, enabled YICES2 UNSAT assumptions, …

3c83838

…and added proxy variables to BMC

added check_assuming_expr flag for solvers that can accept compound a…

fb1871a

…ssumptions; made YICES2 skip some (get-unsat-assumptions) tests

fixed formatting

e99a049

prototype of activation literal pool and scope

feae238

segment/nest with_act_scope calls to prevent bloat and clear used act…

4dd60f4

…ivation literals from scope during cleanup

remove broken links from pdr docs

faa196e

removed stale comment about YICES2 unsat assumptions incompatability

8772d02

remove activation literal usage from places where it did not exist be…

e79ffac

…fore

remove unsat assumptions support for yices2 due to loss of activation…

30b1059

… literals for compound expressions in pdr

disabled check-assuming calls for yices2

ac4337f

restore original bmc code

8f3c3d0

michael-zhang-lambda requested a review from ekiwi August 25, 2026 15:20

ekiwi reviewed Aug 25, 2026

View reviewed changes

michael-zhang-lambda mentioned this pull request Aug 25, 2026

Add activation literals for compound expressions #53

Closed

remove default definition for supports_check_assuming_exprs from Solv…

6024fbf

…erMetaData trait

michael-zhang-lambda requested a review from ekiwi August 25, 2026 20:12

ekiwi requested changes Aug 28, 2026

View reviewed changes

replaced manual activation literal creation with step_lit_act in Base…

b341c83

…Pdr::init

Uh oh!

Conversation

michael-zhang-lambda commented Aug 25, 2026

Changes

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ekiwi left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

michael-zhang-lambda Aug 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

michael-zhang-lambda Aug 28, 2026 •

edited

Loading