mirror of
https://github.com/GaloisInc/what4.git
synced 2024-10-06 00:22:49 +03:00
update what4-abc with changes to the floating-point terms
This commit is contained in:
parent
a458a19192
commit
c2db803bb0
@ -218,6 +218,7 @@ eval _ (SemiRingLiteral SemiRingRealRepr r _) = return (GroundRat r)
|
||||
eval ntk (SemiRingLiteral (SemiRingBVRepr _ w) bv _) =
|
||||
return $ BV w $ AIG.bvFromInteger (gia ntk) (widthVal w) (BV.asUnsigned bv)
|
||||
eval _ (StringExpr s _) = return (GroundString s)
|
||||
eval _ e@FloatExpr{} = failTerm e "floating-point expression"
|
||||
|
||||
eval ntk (NonceAppExpr e) = do
|
||||
memoExprNonce ntk (nonceExprId e) $ do
|
||||
@ -475,11 +476,6 @@ bitblastExpr h ae = do
|
||||
------------------------------------------------------------------------
|
||||
-- Floating point operations
|
||||
|
||||
FloatPZero{} -> floatFail
|
||||
FloatNZero{} -> floatFail
|
||||
FloatNaN{} -> floatFail
|
||||
FloatPInf{} -> floatFail
|
||||
FloatNInf{} -> floatFail
|
||||
FloatNeg{} -> floatFail
|
||||
FloatAbs{} -> floatFail
|
||||
FloatSqrt{} -> floatFail
|
||||
@ -488,11 +484,8 @@ bitblastExpr h ae = do
|
||||
FloatMul{} -> floatFail
|
||||
FloatDiv{} -> floatFail
|
||||
FloatRem{} -> floatFail
|
||||
FloatMin{} -> floatFail
|
||||
FloatMax{} -> floatFail
|
||||
FloatFMA{} -> floatFail
|
||||
FloatFpEq{} -> floatFail
|
||||
FloatFpNe{} -> floatFail
|
||||
FloatLe{} -> floatFail
|
||||
FloatLt{} -> floatFail
|
||||
FloatIsNaN{} -> floatFail
|
||||
|
Loading…
Reference in New Issue
Block a user