Skip to content

add new minimizer and fix bug #44

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

Perro2110
Copy link
Member

Update on Logical Minimizers and Bug Fix

I started by adding two new logical minimizers, boom and abc. While working on this, I noticed a bug in the conversion functions between PLA and formulas. This led me to investigate further.

Specifically, I was testing the correctness of the two core functions:

  • _formula_to_pla
  • _pla_to_formula

Both are located in the SoleData/src/scalar-pla.jl file under the SoleData module.

Here’s a minimal reproducible test case:

using SoleData, SoleLogics
using SoleData: PLA

f = @scalarformula(
    ((V1 < 5.85)  (V1  5.65)  (V2 < 2.85)  (V3 < 4.55)  (V3  4.45)  (V4 < 0.35)) 
    ((V1 < 5.3)  (V2  2.85)  (V3 < 5.05)  (V3  4.85)  (V4 < 0.35))
)

pla_str, args, kwargs = PLA._formula_to_pla(f, false, false)

featvaltype = Float64

result = PLA._pla_to_formula(pla_str, false, args...; featvaltype=featvaltype, kwargs...)

For most formulas, the result is logically equivalent to the original formula f, as expected. However, in this particular case, it’s not.


Root Cause

I believe I found the issue:

The original implementation had a critical bug: it always overwrote values in pla_row without checking if they were already set, potentially causing logical conflicts.


Fix

Key Improvement:

  • Added proper conflict checks and state management during the conversion process.

These two functions are extremely important — not just for Lumen, but also for a major feature I’ve been working on and was planning to demo in SoleData.

fix scalar-pla convert
@Perro2110 Perro2110 changed the title add new minimizer add new minimizer and fix bug Jun 28, 2025
Copy link

codecov bot commented Jun 28, 2025

Codecov Report

Attention: Patch coverage is 11.59420% with 183 lines in your changes missing coverage. Please review.

Project coverage is 50.23%. Comparing base (6629d91) to head (adb2a1b).

Files with missing lines Patch % Lines
src/minimize.jl 0.00% 177 Missing ⚠️
src/scalar-pla.jl 80.00% 6 Missing ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##             main      #44      +/-   ##
==========================================
- Coverage   52.84%   50.23%   -2.61%     
==========================================
  Files          51       51              
  Lines        3151     3354     +203     
==========================================
+ Hits         1665     1685      +20     
- Misses       1486     1669     +183     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@Perro2110 Perro2110 self-assigned this Jun 28, 2025
@Perro2110 Perro2110 added bug Something isn't working documentation Improvements or additions to documentation labels Jun 28, 2025
@Perro2110 Perro2110 added this to SOLE Jun 28, 2025
@@ -1,4 +1,5 @@
"""
by https://jackhack96.github.io/logic-synthesis/espresso.html.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Docstrings should start with the function signature, not anything else. Let's could cite the reference in the docstring text body

Comment on lines +7 to +10
src/espresso.linux
src/abc
src/boom.exe
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Either we make these part of the package (but let's ensure we can and there are no licensing issues), or we introduce some logic for downloading them automatically. If the executable are not too large (< 5MB) I would lean towards the first choice. Btw they should be executable on linux machines surely (idk about that exe file?). Also what's the .linux extension? Is it an executable?

- The function assumes that either the main condition or its dual exists in the conditions vector
- Warnings are issued when logical conflicts are detected during encoding
- The resulting PLA row uses "-" for don't-care positions that are not constrained by any literal
"""
function encode_disjunct(disjunct::LeftmostConjunctiveForm, features::AbstractVector, conditions::AbstractVector, includes, excludes, feat_condindxss)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This function is a bit of a mess (my bad, sorry, I've rushed a bit while writing it). It's difficult for me atm to understand what's going on and whether the fix is correct. Do all the tests pass?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working documentation Improvements or additions to documentation
Projects
Status: No status
Development

Successfully merging this pull request may close these issues.

2 participants