✨ Add advanced power encoding

[FeldmeierMichael]

Added support for Pseudo boolean Cardinalty constraints using CUDD
This pull request introduces significant enhancements to the exact synthesis functionality, focusing on improved data structures, integration of the CUDD BDD library, and the addition of new synthesis methods. The changes make the codebase more extensible and ready for advanced synthesis techniques, especially those leveraging BDDs for power optimization.

Summary by CodeRabbit

• New Features

  • New CLI option to select among multiple exact‑synthesis search modes (including a step‑size mode) and updated usage text.

• Enhancements

  • Added an alternate BDD-based synthesis pathway with improved encoding for activity and cardinality constraints.
  • Extended cleanup to free additional resources for more reliable long runs.

• Bug Fixes

  • Fixed indexing, allocation and initialization issues that could cause crashes.

• Behavior Changes

  • Synthesis now dispatches to different backends based on the selected search mode.

[coderabbitai]

Actionable comments posted: 1

🧹 Nitpick comments (1)

pexact.c (1)

1401-1401: Consider using bit shifts for integer powers of 2.

Throughout the code, pow(2, k-1) and similar expressions are used for computing powers of 2. Since these are always integer operations, using bit shifts would be more efficient and clearer:

// Instead of: int np = pow(2, p->nVars - 1) + 1;
int np = (1 << (p->nVars - 1)) + 1;

This applies to multiple locations (lines 1188, 1280, 1324, 1370, 1401, 1587, 1638, etc.). Given nVars is restricted to 2–4, there's no overflow concern.

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In `@pexact.c` at line 1401, The code uses pow(2, k) for integer powers of two
(e.g., the expression initializing np as pow(2, p->nVars - 1) + 1) which is
inefficient and unnecessary; replace occurrences of pow(2, ...) with bit shifts
using 1 << (...) (for example compute np from p->nVars as (1 << (p->nVars - 1))
+ 1) and apply the same replacement for the other pow(2, ...) sites in pexact.c
so all integer power-of-two computations use shifts rather than pow.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@pexact.c`:
- Around line 2573-2605: The code wrongly compares possibly-complemented CUDD
pointers (nodeE from Cudd_E(node)) against regularized entries in col->nodes and
against Cudd_ReadLogicZero/Cudd_ReadOne, causing missed matches and invalid
child values passed to AddMuxEncodingCudd; fix by regularizing children with
Cudd_Regular(nodeT)/Cudd_Regular(nodeE) and detecting complements with
Cudd_IsComplement so comparisons use the regular pointers (compare col->nodes[j]
to Cudd_Regular(nodeT/E)) and handle complemented flags by swapping/inverting
child0/child1 or mapping to the correct litConst values before calling
AddMuxEncodingCudd; also update the constant checks to compare
Cudd_Regular(child) to Cudd_ReadLogicZero/Cudd_ReadOne and apply the complement
flag when assigning child0/child1.

---

Nitpick comments:
In `@pexact.c`:
- Line 1401: The code uses pow(2, k) for integer powers of two (e.g., the
expression initializing np as pow(2, p->nVars - 1) + 1) which is inefficient and
unnecessary; replace occurrences of pow(2, ...) with bit shifts using 1 << (...)
(for example compute np from p->nVars as (1 << (p->nVars - 1)) + 1) and apply
the same replacement for the other pow(2, ...) sites in pexact.c so all integer
power-of-two computations use shifts rather than pow.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 2360965f-6ca0-47c8-8edf-6f81413ad524

📥 Commits

Reviewing files that changed from the base of the PR and between c25855b and 35d20e0.

📒 Files selected for processing (2)

• init.cpp
• pexact.c

🚧 Files skipped from review as they are similar to previous changes (1)

• init.cpp

[Copilot]

Pull request overview

Copilot reviewed 3 out of 3 changed files in this pull request and generated 11 comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[coderabbitai]

Actionable comments posted: 4

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@init.cpp`:
- Around line 75-87: The parsing of the -M option using strtol is not validating
partial parses or errors; update the block that uses strtol (where searchMode is
set) to check errno (clear it before call), ensure pEnd is not equal to
argv[globalUtilOptind] (i.e. at least one digit was consumed) and that *pEnd ==
'\0' (no trailing garbage), and detect ERANGE via errno; if any of these checks
fail or the value is out of range (searchMode < 0 || searchMode > 2) print the
existing invalid-switch message and goto usage; only increment globalUtilOptind
after all validation passes.

In `@pexact.c`:
- Around line 3144-3149: Allocate the replacement manager into a temporary
pointer first (call PexaManAlloc with pPars, pTruth into a temp like newpm),
check if newpm is NULL and only on success call PexaManFree(*p) and set *p =
newpm; if allocation fails, leave *p unchanged and return the error (do not free
*p). This uses PexaManAlloc, PexaManFree and the existing *p/pPars/pTruth
symbols to avoid leaving *p NULL when allocation fails.
- Around line 2287-2293: The inner function CalculateBddCuddSmallerThanMinInner
currently calls Cudd_RecursiveDeref(dd, *orNode) on its error path, but it never
owned that reference (caller retains ownership) which leads to a double-deref
when the caller also frees *orNode; remove the Cudd_RecursiveDeref(dd, *orNode)
call from the error path(s) in CalculateBddCuddSmallerThanMinInner (the sections
that handle tmp == Cudd_ReadLogicZero(dd) for DdNode *tmp from BddNOutofROptCudd
and the analogous block around lines shown), leaving only
Cudd_RecursiveDeref(dd, andNode) before returning 0 so each acquired reference
is released exactly once.
- Around line 2743-2764: The root unit clause ignores the complement of the
original root pointer: after locating rootIdx using Cudd_Regular(r) you must
preserve the root's polarity by using Cudd_IsComplement(r) when building the
literal; construct rootLit with Abc_Var2Lit(nodeVar[rootIdx],
Cudd_IsComplement(r) ? 1 : 0) and then add that single-literal clause to the
solver via sat_solver_addclause using the rootLit pointer/range as done
elsewhere. Ensure you reference rootIdx, Cudd_Regular, Cudd_IsComplement,
rootLit, Abc_Var2Lit and sat_solver_addclause when making the change.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 2b49fbad-f4da-4847-b2d8-8464aece9f2e

📥 Commits

Reviewing files that changed from the base of the PR and between 35d20e0 and 4d6e5ec.

📒 Files selected for processing (3)

• init.cpp
• pexact.c
• pexact.h

🚧 Files skipped from review as they are similar to previous changes (1)

• pexact.h

[marcelwa]

Many thanks for the additions! 🙏 The PR looks really good already. Just a few minor questions and suggestions.

[marcelwa]

Btw, as you can see by GitHub's warning at the top, avoid emojis in the branch names.

[coderabbitai]

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

init.cpp (1)

63-90: ⚠️ Potential issue | 🟡 Minor

Validate -M on a long before assigning to int.

strtol() returns long, but line 84 stores it in int searchMode before the range check. Values outside int but within long range can overflow implementation-definedly when converted, and the resulting int value could silently pass the subsequent range check if it wraps to 0, 1, or 2. Parse into a long, validate the bounds, then cast after acceptance.

Suggested fix

-    int searchMode = 0;  // Default search mode
+    int searchMode = 0;  // Default search mode
+    long parsedSearchMode = 0;
...
-            searchMode = strtol( argv[globalUtilOptind], &pEnd, DECIMAL_BASE );
-            if ( pEnd == argv[globalUtilOptind] || *pEnd != '\0' || errno == ERANGE || searchMode < 0 || searchMode > 2 )
+            parsedSearchMode = strtol( argv[globalUtilOptind], &pEnd, DECIMAL_BASE );
+            if ( pEnd == argv[globalUtilOptind] || *pEnd != '\0' || errno == ERANGE || parsedSearchMode < 0 || parsedSearchMode > 2 )
             {
                 Abc_Print( -1, "Invalid search mode. Valid values are 0 (queue search), 1 (free search), and 2 (binary search).\n" );
                 goto usage;
             }
+            searchMode = (int)parsedSearchMode;

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In `@init.cpp` around lines 63 - 90, The code currently stores strtol() directly
into int searchMode, which can overflow; change searchMode to be parsed into a
long (e.g., long tmpMode = strtol(...)) using the same pEnd and errno checks,
verify tmpMode is within the valid logical range (0..2) and also within int
bounds (INT_MIN..INT_MAX), only then assign searchMode = (int)tmpMode and
increment globalUtilOptind; update all references to searchMode accordingly and
keep the existing error messages/usage handling when checks fail.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Outside diff comments:
In `@init.cpp`:
- Around line 63-90: The code currently stores strtol() directly into int
searchMode, which can overflow; change searchMode to be parsed into a long
(e.g., long tmpMode = strtol(...)) using the same pEnd and errno checks, verify
tmpMode is within the valid logical range (0..2) and also within int bounds
(INT_MIN..INT_MAX), only then assign searchMode = (int)tmpMode and increment
globalUtilOptind; update all references to searchMode accordingly and keep the
existing error messages/usage handling when checks fail.

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 906cb983-a6a6-434b-a098-920deae8a983

📥 Commits

Reviewing files that changed from the base of the PR and between 4d6e5ec and 9edc1e0.

📒 Files selected for processing (2)

• init.cpp
• pexact.c

✅ Files skipped from review due to trivial changes (1)

• pexact.c

[marcelwa]

Looking good now! Just one minor clarification regarding an older comment of mine.

[coderabbitai]

🧹 Nitpick comments (1)

pexact.c (1)

2854-2864: Consider using consistent "allocate then free" pattern.

This uses the "free then allocate" pattern, whereas PexaManExactPowerSynthesisBasePowerBDDBinaryInner uses the safer "allocate then free" pattern. While the current code handles the NULL case correctly, using the same pattern consistently would improve maintainability and safety.

♻️ Suggested refactor for consistency

-            PexaManFree( p );
-            p = PexaManAlloc( pPars, pTruth );
-            if ( p == NULL )
+            PexaMan_t * next = PexaManAlloc( pPars, pTruth );
+            if ( next == NULL )
             {
                 printf( "Error: memory allocation failed for PexaMan_t.\n" );
                 free( node->combi );
                 free( node );
                 FreeCombList( list );
                 free( list );
                 return 1;
             }
+            PexaManFree( p );
+            p = next;

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In `@pexact.c` around lines 2854 - 2864, The current code frees p via
PexaManFree(p) before calling PexaManAlloc(pPars, pTruth), which is the "free
then allocate" pattern; instead follow the safer "allocate then free" approach
used in PexaManExactPowerSynthesisBasePowerBDDBinaryInner by first calling
PexaManAlloc into a temporary pointer (e.g., new_p), check new_p for NULL and
handle the error if allocation fails, and only after successful allocation call
PexaManFree(p) and assign p = new_p; update the block that currently calls
PexaManFree, PexaManAlloc and the NULL check to use this allocate-then-free flow
referencing PexaManAlloc, PexaManFree and the variable p.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Nitpick comments:
In `@pexact.c`:
- Around line 2854-2864: The current code frees p via PexaManFree(p) before
calling PexaManAlloc(pPars, pTruth), which is the "free then allocate" pattern;
instead follow the safer "allocate then free" approach used in
PexaManExactPowerSynthesisBasePowerBDDBinaryInner by first calling PexaManAlloc
into a temporary pointer (e.g., new_p), check new_p for NULL and handle the
error if allocation fails, and only after successful allocation call
PexaManFree(p) and assign p = new_p; update the block that currently calls
PexaManFree, PexaManAlloc and the NULL check to use this allocate-then-free flow
referencing PexaManAlloc, PexaManFree and the variable p.

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 69a9ae1c-6bba-4f22-ae41-b8f314cf4eec

📥 Commits

Reviewing files that changed from the base of the PR and between 9edc1e0 and 7914a17.

📒 Files selected for processing (2)

• init.cpp
• pexact.c

✅ Files skipped from review due to trivial changes (1)

• init.cpp