What library should I use for efficient symbolic boolean formulas?

Learn
#1

In my code, I have some data structures like this

data Guard = 
      GTriv
    | GFalse
    | GPos Int
    | GNeg Int
    | GAnd Guard Guard
    | GOr Guard Guard

gAnd :: Guard -> Guard -> Guard
gAnd = undefined

gOr :: Guard -> Guard -> Guard
gOr = undefined

sat :: Guard -> Bool
sat = undefined

taut :: Guard -> Bool
taut = undefined

simplifyGuard :: Guard -> Guard
simplifyGuard = undefined

type Valuation = [Bool]

checkGuard :: Valuation -> Guard -> Bool
checkGuard = undefined

instance (Show Guard) where
    show = undefined

Since Guard is essentially a symbolic boolean expression, I figured there must be some library which I can use, which does all this efficiently, instead of trying to roll my own. What should I use?

1 Like
#2

There’s a bunch of stuff on hackage, depending on what you want. Here’s an old thing I worked on for attempting to produce computation-efficient simplifications of boolean expressions: Data.BoolSimplifier

Here’s something else that has evaluation as well as some of the more standard normal forms: Data.BoolExpr

1 Like
#3

This sounds like you could put the hegg equality saturation library to use! Seems like a perfect use case.

I would appreciate it if you could try hegg and its documentation and tutorial to implement your goal of symbolic simplification. I’d be happy to clarify any questions and improve documentation while you try to employ it in your use case.

Do let me know how it goes/what you didn’t understand, if you do try that route.

1 Like
#4

It might be a bit overkill for your use case, depending on where you would go from here… but I got enthusiastic about the symbolic simplification :slight_smile:

In re-reading the tutorial I feel like there’s too much going on. I’d like to improve it a bit overall.

Still, it might be just what you are looking for, and I can help you jump through the hoops — just ask away all the questions.

1 Like
#5

Thanks for these suggestions. For now, I have decided I will just use my handrolled implementation because the use-case does not seem to require very complex simplifications

1 Like