Currently we can easily do polymorph definitions of problems like:
problem :: (Orderable (Expr t), Num (Expr t)) => ... -> Expr BoolSort
problem = ...
main :: IO ()
main = do
solveWith @SMT (solver z3) $ problem @RealSort
solveWith @SMT (solver z3) $ problem @IntSort ...
solveWith @SMT (solver z3) $ problem @(BvSort Unsigned 8) ...
This works fine for IntSort and RealSort.
However one needs to deal with overflow for fixed size bv of size n: BvSort _ n.
Currently in use cases I encode extra overflow contraints via checking t with KnownSMTSort t inside problem.
That is bad.
Add an overflow-safe BitVec type.
Ideally some wrapper and not a new sort.
Currently we can easily do polymorph definitions of problems like:
This works fine for
IntSortandRealSort.However one needs to deal with overflow for fixed size bv of size n:
BvSort _ n.Currently in use cases I encode extra overflow contraints via checking
twithKnownSMTSort tinsideproblem.That is bad.
Add an overflow-safe BitVec type.
Ideally some wrapper and not a new sort.