Skip to content
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

BaseEq should probably always sort its operands #280

Open
langston-barrett opened this issue Feb 4, 2025 · 1 comment
Open

BaseEq should probably always sort its operands #280

langston-barrett opened this issue Feb 4, 2025 · 1 comment
Labels
good first issue Good for newcomers

Comments

@langston-barrett
Copy link
Contributor

Many instances of BaseEq in What4.Expr.Builder sort their operands:

sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min xr yr) (max xr yr)

sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min x y) (max x y)

_ -> sbMakeExpr sym $ BaseEq BaseBoolRepr (min x y) (max x y)

sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min xr yr) (max xr yr)

-> sbMakeExpr sym $ BaseEq (BaseBVRepr (bvWidth x)) (min x y) (max x y)

But some don't:

= sbMakeExpr sym $ BaseEq (BaseStringRepr (stringInfo x)) x y

sbMakeExpr sym $! BaseEq (exprType x) x y

| otherwise = floatIEEELogicBinOp (BaseEq (exprType x)) sym x y

The latter probably should too. In fact, we should probably have a helper

baseEq :: BaseTypeRepr t -> Expr t -> Expr t -> Expr t
baseEq t x y = BaseEq t (min x y) (max x y)

with some Haddocks about why this is generally a good idea.

@langston-barrett
Copy link
Contributor Author

This baseEq helper should also probably encapsulate the following common rewrite:

| x == y
= return (truePred sym)

@langston-barrett langston-barrett added the good first issue Good for newcomers label Feb 4, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
good first issue Good for newcomers
Projects
None yet
Development

No branches or pull requests

1 participant