1----------------------------------------------------------------------------- 2-- | 3-- Module : Data.SBV.SMT.SMTLib2 4-- Copyright : (c) Levent Erkok 5-- License : BSD3 6-- Maintainer: erkokl@gmail.com 7-- Stability : experimental 8-- 9-- Conversion of symbolic programs to SMTLib format, Using v2 of the standard 10----------------------------------------------------------------------------- 11 12{-# LANGUAGE PatternGuards #-} 13{-# LANGUAGE ScopedTypeVariables #-} 14{-# LANGUAGE ViewPatterns #-} 15 16{-# OPTIONS_GHC -Wall -Werror #-} 17 18module Data.SBV.SMT.SMTLib2(cvt, cvtInc) where 19 20import Data.Bits (bit) 21import Data.List (intercalate, partition, nub, sort) 22import Data.Maybe (listToMaybe, fromMaybe, catMaybes) 23 24import qualified Data.Foldable as F (toList) 25import qualified Data.Map.Strict as M 26import qualified Data.IntMap.Strict as IM 27import Data.Set (Set) 28import qualified Data.Set as Set 29 30import Data.SBV.Core.Data 31import Data.SBV.Core.Symbolic (QueryContext(..), SetOp(..), OvOp(..), CnstMap, getUserName', getSV, regExpToSMTString) 32import Data.SBV.Core.Kind (smtType, needsFlattening) 33import Data.SBV.SMT.Utils 34import Data.SBV.Control.Types 35 36import Data.SBV.Utils.PrettyNum (smtRoundingMode, cvToSMTLib) 37 38import qualified Data.Generics.Uniplate.Data as G 39 40tbd :: String -> a 41tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e 42 43-- | Translate a problem into an SMTLib2 script 44cvt :: SMTLibConverter [String] 45cvt ctx kindInfo isSat comments (inputs, trackerVars) skolemInps (allConsts, consts) tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out cfg = pgm 46 where hasInteger = KUnbounded `Set.member` kindInfo 47 hasReal = KReal `Set.member` kindInfo 48 hasFP = not (null [() | KFP{} <- Set.toList kindInfo]) 49 || KFloat `Set.member` kindInfo 50 || KDouble `Set.member` kindInfo 51 hasString = KString `Set.member` kindInfo 52 hasChar = KChar `Set.member` kindInfo 53 hasRounding = not $ null [s | (s, _) <- usorts, s == "RoundingMode"] 54 hasBVs = not (null [() | KBounded{} <- Set.toList kindInfo]) 55 usorts = [(s, dt) | KUserSort s dt <- Set.toList kindInfo] 56 trueUSorts = [s | (s, _) <- usorts, s /= "RoundingMode"] 57 tupleArities = findTupleArities kindInfo 58 hasNonBVArrays = (not . null) [() | (_, (_, (k1, k2), _)) <- arrs, not (isBounded k1 && isBounded k2)] 59 hasArrayInits = (not . null) [() | (_, (_, _, ArrayFree (Just _))) <- arrs] 60 hasOverflows = (not . null) [() | (_ :: OvOp) <- G.universeBi asgnsSeq] 61 hasList = any isList kindInfo 62 hasSets = any isSet kindInfo 63 hasTuples = not . null $ tupleArities 64 hasEither = any isEither kindInfo 65 hasMaybe = any isMaybe kindInfo 66 rm = roundingMode cfg 67 solverCaps = capabilities (solver cfg) 68 69 -- Is there a reason why we can't handle this problem? 70 -- NB. There's probably a lot more checking we can do here, but this is a start: 71 doesntHandle = listToMaybe [nope w | (w, have, need) <- checks, need && not have] 72 where checks = [ ("data types", supportsDataTypes solverCaps, hasTuples || hasEither || hasMaybe) 73 , ("set operations", supportsSets solverCaps, hasSets) 74 , ("bit vectors", supportsBitVectors solverCaps, hasBVs) 75 ] 76 77 nope w = [ "*** Given problem requires support for " ++ w 78 , "*** But the chosen solver (" ++ show (name (solver cfg)) ++ ") doesn't support this feature." 79 ] 80 81 setAll reason = ["(set-logic ALL) ; " ++ reason ++ ", using catch-all."] 82 83 -- Determining the logic is surprisingly tricky! 84 logic 85 -- user told us what to do: so just take it: 86 | Just l <- case [l | SetLogic l <- solverSetOptions cfg] of 87 [] -> Nothing 88 [l] -> Just l 89 ls -> error $ unlines [ "" 90 , "*** Only one setOption call to 'setLogic' is allowed, found: " ++ show (length ls) 91 , "*** " ++ unwords (map show ls) 92 ] 93 = case l of 94 Logic_NONE -> ["; NB. Not setting the logic per user request of Logic_NONE"] 95 _ -> ["(set-logic " ++ show l ++ ") ; NB. User specified."] 96 97 -- There's a reason why we can't handle this problem: 98 | Just cantDo <- doesntHandle 99 = error $ unlines $ [ "" 100 , "*** SBV is unable to choose a proper solver configuration:" 101 , "***" 102 ] 103 ++ cantDo 104 ++ [ "***" 105 , "*** Please report this as a feature request, either for SBV or the backend solver." 106 ] 107 108 -- Otherwise, we try to determine the most suitable logic. 109 -- NB. This isn't really fool proof! 110 111 -- we never set QF_S (ALL seems to work better in all cases) 112 113 -- Things that require ALL 114 | hasInteger = setAll "has unbounded values" 115 | hasReal = setAll "has algebraic reals" 116 | not (null trueUSorts) = setAll "has user-defined sorts" 117 | hasNonBVArrays = setAll "has non-bitvector arrays" 118 | hasTuples = setAll "has tuples" 119 | hasEither = setAll "has either type" 120 | hasMaybe = setAll "has maybe type" 121 | hasSets = setAll "has sets" 122 | hasList = setAll "has lists" 123 | hasChar = setAll "has chars" 124 | hasString = setAll "has strings" 125 | hasArrayInits = setAll "has array initializers" 126 | hasOverflows = setAll "has overflow checks" 127 128 | hasFP || hasRounding 129 = if not (null foralls) 130 then ["(set-logic ALL)"] 131 else if hasBVs 132 then ["(set-logic QF_FPBV)"] 133 else ["(set-logic QF_FP)"] 134 135 -- If we're in a user query context, we'll pick ALL, otherwise 136 -- we'll stick to some bit-vector logic based on what we see in the problem. 137 -- This is controversial, but seems to work well in practice. 138 | True 139 = case ctx of 140 QueryExternal -> ["(set-logic ALL) ; external query, using all logics."] 141 QueryInternal -> if supportsBitVectors solverCaps 142 then ["(set-logic " ++ qs ++ as ++ ufs ++ "BV)"] 143 else ["(set-logic ALL)"] -- fall-thru 144 where qs | null foralls && null axs = "QF_" -- axioms are likely to contain quantifiers 145 | True = "" 146 as | null arrs = "" 147 | True = "A" 148 ufs | null uis && null tbls = "" -- we represent tables as UFs 149 | True = "UF" 150 151 -- SBV always requires the production of models! 152 getModels = "(set-option :produce-models true)" 153 : concat [flattenConfig | any needsFlattening kindInfo, Just flattenConfig <- [supportsFlattenedModels solverCaps]] 154 155 -- process all other settings we're given. If an option cannot be repeated, we only take the last one. 156 userSettings = map setSMTOption $ filter (not . isLogic) $ foldr comb [] $ solverSetOptions cfg 157 where -- Logic is already processed, so drop it: 158 isLogic SetLogic{} = True 159 isLogic _ = False 160 161 -- SBV sets diagnostic-output channel on some solvers. If the user also gives it, let's just 162 -- take it by only taking the last one 163 isDiagOutput DiagnosticOutputChannel{} = True 164 isDiagOutput _ = False 165 166 comb o rest 167 | isDiagOutput o && any isDiagOutput rest = rest 168 | True = o : rest 169 170 settings = userSettings -- NB. Make sure this comes first! 171 ++ getModels 172 ++ logic 173 174 pgm = map ("; " ++) comments 175 ++ settings 176 ++ [ "; --- uninterpreted sorts ---" ] 177 ++ concatMap declSort usorts 178 ++ [ "; --- tuples ---" ] 179 ++ concatMap declTuple tupleArities 180 ++ [ "; --- sums ---" ] 181 ++ (if containsSum kindInfo then declSum else []) 182 ++ (if containsMaybe kindInfo then declMaybe else []) 183 ++ [ "; --- literal constants ---" ] 184 ++ concatMap (declConst cfg) consts 185 ++ [ "; --- skolem constants ---" ] 186 ++ concat [declareFun s (SBVType (map kindOf (ss ++ [s]))) (userName s) | Right (s, ss) <- skolemInps] 187 ++ [ "; --- optimization tracker variables ---" | not (null trackerVars) ] 188 ++ concat [declareFun s (SBVType [kindOf s]) (Just ("tracks " <> nm)) | var <- trackerVars, let s = getSV var, let nm = getUserName' var] 189 ++ [ "; --- constant tables ---" ] 190 ++ concatMap (uncurry (:) . constTable) constTables 191 ++ [ "; --- skolemized tables ---" ] 192 ++ map (skolemTable (unwords (map svType foralls))) skolemTables 193 ++ [ "; --- arrays ---" ] 194 ++ concat arrayConstants 195 ++ [ "; --- uninterpreted constants ---" ] 196 ++ concatMap declUI uis 197 ++ [ "; --- user given axioms ---" ] 198 ++ map declAx axs 199 ++ [ "; --- formula ---" ] 200 201 ++ concatMap (declDef cfg skolemMap tableMap) preQuantifierAssigns 202 ++ ["(assert (forall (" ++ intercalate "\n " 203 ["(" ++ show s ++ " " ++ svType s ++ ")" | s <- foralls] ++ ")" 204 | not (null foralls) 205 ] 206 ++ concatMap mkAssign postQuantifierAssigns 207 208 ++ concat arrayDelayeds 209 210 ++ concat arraySetups 211 212 ++ delayedAsserts delayedEqualities 213 214 ++ finalAssert 215 216 -- identify the assignments that can come before the first quantifier 217 (preQuantifierAssigns, postQuantifierAssigns) 218 | null foralls 219 = ([], asgns) -- the apparent "switch" here is OK; rest of the code works correctly if there are no foralls. 220 | True 221 = span pre asgns 222 where first = nodeId (minimum foralls) 223 pre (s, _) = nodeId s < first 224 225 nodeId (SV _ n) = n 226 227 noOfCloseParens 228 | null foralls = 0 229 | True = length postQuantifierAssigns + 2 + (if null delayedEqualities then 0 else 1) 230 231 foralls = [s | Left s <- skolemInps] 232 forallArgs = concatMap ((" " ++) . show) foralls 233 234 (constTables, skolemTables) = ([(t, d) | (t, Left d) <- allTables], [(t, d) | (t, Right d) <- allTables]) 235 allTables = [(t, genTableData rm skolemMap (not (null foralls), forallArgs) (map fst consts) t) | t <- tbls] 236 (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray cfg (not (null foralls)) allConsts skolemMap) arrs 237 delayedEqualities = concatMap snd skolemTables 238 239 delayedAsserts [] = [] 240 delayedAsserts ds@(deH : deTs) 241 | null foralls = map (\s -> "(assert " ++ s ++ ")") ds 242 | True = map letShift (("(and " ++ deH) : map (align 5) deTs) 243 244 letShift = align 12 245 246 finalAssert 247 | null foralls && noConstraints 248 = [] 249 | null foralls 250 = map (\(attr, v) -> "(assert " ++ addAnnotations attr (mkLiteral v) ++ ")") hardAsserts 251 ++ map (\(attr, v) -> "(assert-soft " ++ addAnnotations attr (mkLiteral v) ++ ")") softAsserts 252 | not (null namedAsserts) 253 = error $ intercalate "\n" [ "SBV: Constraints with attributes and quantifiers cannot be mixed!" 254 , " Quantified variables: " ++ unwords (map show foralls) 255 , " Named constraints : " ++ intercalate ", " (map show namedAsserts) 256 ] 257 | not (null softAsserts) 258 = error $ intercalate "\n" [ "SBV: Soft constraints and quantifiers cannot be mixed!" 259 , " Quantified variables: " ++ unwords (map show foralls) 260 , " Soft constraints : " ++ intercalate ", " (map show softAsserts) 261 ] 262 | True 263 = [impAlign (letShift combined) ++ replicate noOfCloseParens ')'] 264 where mkLiteral (Left v) = cvtSV skolemMap v 265 mkLiteral (Right v) = "(not " ++ cvtSV skolemMap v ++ ")" 266 267 (noConstraints, assertions) = finalAssertions 268 269 namedAsserts = [findName attrs | (_, attrs, _) <- assertions, not (null attrs)] 270 where findName attrs = fromMaybe "<anonymous>" (listToMaybe [nm | (":named", nm) <- attrs]) 271 272 hardAsserts, softAsserts :: [([(String, String)], Either SV SV)] 273 hardAsserts = [(attr, v) | (False, attr, v) <- assertions] 274 softAsserts = [(attr, v) | (True, attr, v) <- assertions] 275 276 combined = case lits of 277 [] -> "true" 278 [x] -> mkLiteral x 279 xs | any bad xs -> "false" 280 | True -> "(and " ++ unwords (map mkLiteral xs) ++ ")" 281 where lits = filter (not . redundant) $ nub (sort (map snd hardAsserts)) 282 redundant (Left v) = v == trueSV 283 redundant (Right v) = v == falseSV 284 bad (Left v) = v == falseSV 285 bad (Right v) = v == trueSV 286 287 impAlign s 288 | null delayedEqualities = s 289 | True = " " ++ s 290 291 align n s = replicate n ' ' ++ s 292 293 finalAssertions :: (Bool, [(Bool, [(String, String)], Either SV SV)]) -- If Left: positive, Right: negative 294 finalAssertions 295 | null finals = (True, [(False, [], Left trueSV)]) 296 | True = (False, finals) 297 298 where finals = cstrs' ++ maybe [] (\r -> [(False, [], r)]) mbO 299 300 cstrs' = [(isSoft, attrs, c') | (isSoft, attrs, c) <- F.toList cstrs, Just c' <- [pos c]] 301 302 mbO | isSat = pos out 303 | True = neg out 304 305 neg s 306 | s == falseSV = Nothing 307 | s == trueSV = Just $ Left falseSV 308 | True = Just $ Right s 309 310 pos s 311 | s == trueSV = Nothing 312 | s == falseSV = Just $ Left falseSV 313 | True = Just $ Left s 314 315 skolemMap = M.fromList [(s, ss) | Right (s, ss) <- skolemInps, not (null ss)] 316 tableMap = IM.fromList $ map mkConstTable constTables ++ map mkSkTable skolemTables 317 where mkConstTable (((t, _, _), _), _) = (t, "table" ++ show t) 318 mkSkTable (((t, _, _), _), _) = (t, "table" ++ show t ++ forallArgs) 319 asgns = F.toList asgnsSeq 320 321 mkAssign a 322 | null foralls = declDef cfg skolemMap tableMap a 323 | True = [letShift (mkLet a)] 324 325 mkLet (s, SBVApp (Label m) [e]) = "(let ((" ++ show s ++ " " ++ cvtSV skolemMap e ++ ")) ; " ++ m 326 mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp solverCaps rm skolemMap tableMap e ++ "))" 327 328 userNameMap = M.fromList $ map ((\nSymVar -> (getSV nSymVar, getUserName' nSymVar)) . snd) inputs 329 userName s = case M.lookup s userNameMap of 330 Just u | show s /= u -> Just $ "tracks user variable " ++ show u 331 _ -> Nothing 332 333-- | Declare new sorts 334declSort :: (String, Maybe [String]) -> [String] 335declSort (s, _) 336 | s == "RoundingMode" -- built-in-sort; so don't declare. 337 = [] 338declSort (s, Nothing) = ["(declare-sort " ++ s ++ " 0) ; N.B. Uninterpreted sort." ] 339declSort (s, Just fs) = [ "(declare-datatypes ((" ++ s ++ " 0)) ((" ++ unwords (map (\c -> "(" ++ c ++ ")") fs) ++ ")))" 340 , "(define-fun " ++ s ++ "_constrIndex ((x " ++ s ++ ")) Int" 341 ] ++ [" " ++ body fs (0::Int)] ++ [")"] 342 where body [] _ = "" 343 body [_] i = show i 344 body (c:cs) i = "(ite (= x " ++ c ++ ") " ++ show i ++ " " ++ body cs (i+1) ++ ")" 345 346-- | Declare tuple datatypes 347-- 348-- eg: 349-- 350-- @ 351-- (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) 352-- ((mkSBVTuple2 (proj_1_SBVTuple2 T1) 353-- (proj_2_SBVTuple2 T2)))))) 354-- @ 355declTuple :: Int -> [String] 356declTuple arity 357 | arity == 0 = ["(declare-datatypes ((SBVTuple0 0)) (((mkSBVTuple0))))"] 358 | arity == 1 = error "Data.SBV.declTuple: Unexpected one-tuple" 359 | True = (l1 ++ "(par (" ++ unwords [param i | i <- [1..arity]] ++ ")") 360 : [pre i ++ proj i ++ post i | i <- [1..arity]] 361 where l1 = "(declare-datatypes ((SBVTuple" ++ show arity ++ " " ++ show arity ++ ")) (" 362 l2 = replicate (length l1) ' ' ++ "((mkSBVTuple" ++ show arity ++ " " 363 tab = replicate (length l2) ' ' 364 365 pre 1 = l2 366 pre _ = tab 367 368 proj i = "(proj_" ++ show i ++ "_SBVTuple" ++ show arity ++ " " ++ param i ++ ")" 369 370 post i = if i == arity then ")))))" else "" 371 372 param i = "T" ++ show i 373 374-- | Find the set of tuple sizes to declare, eg (2-tuple, 5-tuple). 375-- NB. We do *not* need to recursively go into list/tuple kinds here, 376-- because register-kind function automatically registers all subcomponent 377-- kinds, thus everything we need is available at the top-level. 378findTupleArities :: Set Kind -> [Int] 379findTupleArities ks = Set.toAscList 380 $ Set.map length 381 $ Set.fromList [ tupKs | KTuple tupKs <- Set.toList ks ] 382 383-- | Is @Either@ being used? 384containsSum :: Set Kind -> Bool 385containsSum = not . Set.null . Set.filter isEither 386 387-- | Is @Maybe@ being used? 388containsMaybe :: Set Kind -> Bool 389containsMaybe = not . Set.null . Set.filter isMaybe 390 391declSum :: [String] 392declSum = [ "(declare-datatypes ((SBVEither 2)) ((par (T1 T2)" 393 , " ((left_SBVEither (get_left_SBVEither T1))" 394 , " (right_SBVEither (get_right_SBVEither T2))))))" 395 ] 396 397declMaybe :: [String] 398declMaybe = [ "(declare-datatypes ((SBVMaybe 1)) ((par (T)" 399 , " ((nothing_SBVMaybe)" 400 , " (just_SBVMaybe (get_just_SBVMaybe T))))))" 401 ] 402 403-- | Convert in a query context. 404-- NB. We do not store everything in @newKs@ below, but only what we need 405-- to do as an extra in the incremental context. See `Data.SBV.Core.Symbolic.registerKind` 406-- for a list of what we include, in case something doesn't show up 407-- and you need it! 408cvtInc :: SMTLibIncConverter [String] 409cvtInc inps newKs (allConsts, consts) arrs tbls uis (SBVPgm asgnsSeq) cstrs cfg = 410 -- any new settings? 411 settings 412 -- sorts 413 ++ concatMap declSort [(s, dt) | KUserSort s dt <- newKinds] 414 -- tuples. NB. Only declare the new sizes, old sizes persist. 415 ++ concatMap declTuple (findTupleArities newKs) 416 -- sums 417 ++ (if containsSum newKs then declSum else []) 418 ++ (if containsMaybe newKs then declMaybe else []) 419 -- constants 420 ++ concatMap (declConst cfg) consts 421 -- inputs 422 ++ concatMap declInp inps 423 -- arrays 424 ++ concat arrayConstants 425 -- uninterpreteds 426 ++ concatMap declUI uis 427 -- table declarations 428 ++ tableDecls 429 -- expressions 430 ++ concatMap (declDef cfg skolemMap tableMap) (F.toList asgnsSeq) 431 -- delayed equalities 432 ++ concat arrayDelayeds 433 -- table setups 434 ++ concat tableAssigns 435 -- array setups 436 ++ concat arraySetups 437 -- extra constraints 438 ++ map (\(isSoft, attr, v) -> "(assert" ++ (if isSoft then "-soft " else " ") ++ addAnnotations attr (cvtSV skolemMap v) ++ ")") (F.toList cstrs) 439 where -- NB. The below setting of skolemMap to empty is OK, since we do 440 -- not support queries in the context of skolemized variables 441 skolemMap = M.empty 442 443 rm = roundingMode cfg 444 445 newKinds = Set.toList newKs 446 447 declInp (getSV -> s) = declareFun s (SBVType [kindOf s]) Nothing 448 449 (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray cfg False allConsts skolemMap) arrs 450 451 allTables = [(t, either id id (genTableData rm skolemMap (False, []) (map fst consts) t)) | t <- tbls] 452 (tableDecls, tableAssigns) = unzip $ map constTable allTables 453 454 tableMap = IM.fromList $ map mkTable allTables 455 where mkTable (((t, _, _), _), _) = (t, "table" ++ show t) 456 457 -- If we need flattening in models, do emit the required lines if preset 458 settings 459 | any needsFlattening newKinds 460 = concat (catMaybes [supportsFlattenedModels solverCaps]) 461 | True 462 = [] 463 where solverCaps = capabilities (solver cfg) 464 465declDef :: SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> [String] 466declDef cfg skolemMap tableMap (s, expr) = 467 case expr of 468 SBVApp (Label m) [e] -> defineFun cfg (s, cvtSV skolemMap e) (Just m) 469 e -> defineFun cfg (s, cvtExp caps rm skolemMap tableMap e) Nothing 470 where caps = capabilities (solver cfg) 471 rm = roundingMode cfg 472 473defineFun :: SMTConfig -> (SV, String) -> Maybe String -> [String] 474defineFun cfg (s, def) mbComment 475 | hasDefFun = ["(define-fun " ++ varT ++ " " ++ def ++ ")" ++ cmnt] 476 | True = [ "(declare-fun " ++ varT ++ ")" ++ cmnt 477 , "(assert (= " ++ var ++ " " ++ def ++ "))" 478 ] 479 where var = show s 480 varT = var ++ " " ++ svFunType [] s 481 cmnt = maybe "" (" ; " ++) mbComment 482 483 hasDefFun = supportsDefineFun $ capabilities (solver cfg) 484 485-- Declare constants. NB. We don't declare true/false; but just inline those as necessary 486declConst :: SMTConfig -> (SV, CV) -> [String] 487declConst cfg (s, c) 488 | s == falseSV || s == trueSV 489 = [] 490 | True 491 = defineFun cfg (s, cvtCV (roundingMode cfg) c) Nothing 492 493declUI :: (String, SBVType) -> [String] 494declUI (i, t) = declareName i t Nothing 495 496-- NB. We perform no check to as to whether the axiom is meaningful in any way. 497declAx :: (String, [String]) -> String 498declAx (nm, ls) = (";; -- user given axiom: " ++ nm ++ "\n") ++ intercalate "\n" ls 499 500constTable :: (((Int, Kind, Kind), [SV]), [String]) -> (String, [String]) 501constTable (((i, ak, rk), _elts), is) = (decl, zipWith wrap [(0::Int)..] is ++ setup) 502 where t = "table" ++ show i 503 decl = "(declare-fun " ++ t ++ " (" ++ smtType ak ++ ") " ++ smtType rk ++ ")" 504 505 -- Arrange for initializers 506 mkInit idx = "table" ++ show i ++ "_initializer_" ++ show (idx :: Int) 507 initializer = "table" ++ show i ++ "_initializer" 508 509 wrap index s = "(define-fun " ++ mkInit index ++ " () Bool " ++ s ++ ")" 510 511 lis = length is 512 513 setup 514 | lis == 0 = [ "(define-fun " ++ initializer ++ " () Bool true) ; no initializiation needed" 515 ] 516 | lis == 1 = [ "(define-fun " ++ initializer ++ " () Bool " ++ mkInit 0 ++ ")" 517 , "(assert " ++ initializer ++ ")" 518 ] 519 | True = [ "(define-fun " ++ initializer ++ " () Bool (and " ++ unwords (map mkInit [0..lis - 1]) ++ "))" 520 , "(assert " ++ initializer ++ ")" 521 ] 522 523skolemTable :: String -> (((Int, Kind, Kind), [SV]), [String]) -> String 524skolemTable qsIn (((i, ak, rk), _elts), _) = decl 525 where qs = if null qsIn then "" else qsIn ++ " " 526 t = "table" ++ show i 527 decl = "(declare-fun " ++ t ++ " (" ++ qs ++ smtType ak ++ ") " ++ smtType rk ++ ")" 528 529-- Left if all constants, Right if otherwise 530genTableData :: RoundingMode -> SkolemMap -> (Bool, String) -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String] 531genTableData rm skolemMap (_quantified, args) consts ((i, aknd, _), elts) 532 | null post = Left (map (topLevel . snd) pre) 533 | True = Right (map (nested . snd) (pre ++ post)) 534 where ssv = cvtSV skolemMap 535 (pre, post) = partition fst (zipWith mkElt elts [(0::Int)..]) 536 t = "table" ++ show i 537 538 mkElt x k = (isReady, (idx, ssv x)) 539 where idx = cvtCV rm (mkConstCV aknd k) 540 isReady = x `Set.member` constsSet 541 542 topLevel (idx, v) = "(= (" ++ t ++ " " ++ idx ++ ") " ++ v ++ ")" 543 nested (idx, v) = "(= (" ++ t ++ args ++ " " ++ idx ++ ") " ++ v ++ ")" 544 545 constsSet = Set.fromList consts 546 547-- TODO: We currently do not support non-constant arrays when quantifiers are present, as 548-- we might have to skolemize those. Implement this properly. 549-- The difficulty is with the Mutate/Merge: We have to postpone an init if 550-- the components are themselves postponed, so this cannot be implemented as a simple map. 551declArray :: SMTConfig -> Bool -> CnstMap -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String]) 552declArray cfg quantified consts skolemMap (i, (_, (aKnd, bKnd), ctx)) = (adecl : zipWith wrap [(0::Int)..] (map snd pre), zipWith wrap [lpre..] (map snd post), setup) 553 where constMapping = M.fromList [(s, c) | (c, s) <- M.assocs consts] 554 constNames = M.keys constMapping 555 556 topLevel = not quantified || case ctx of 557 ArrayFree mbi -> maybe True (`elem` constNames) mbi 558 ArrayMutate _ a b -> all (`elem` constNames) [a, b] 559 ArrayMerge c _ _ -> c `elem` constNames 560 (pre, post) = partition fst ctxInfo 561 nm = "array_" ++ show i 562 563 ssv sv 564 | topLevel || sv `elem` constNames 565 = cvtSV skolemMap sv 566 | True 567 = tbd "Non-constant array initializer in a quantified context" 568 569 atyp = "(Array " ++ smtType aKnd ++ " " ++ smtType bKnd ++ ")" 570 571 adecl = case ctx of 572 ArrayFree (Just v) -> "(define-fun " ++ nm ++ " () " ++ atyp ++ " ((as const " ++ atyp ++ ") " ++ constInit v ++ "))" 573 ArrayFree Nothing 574 | bKnd == KChar -> -- Can't support yet, because we need to make sure all the elements are length-1 strings. So, punt for now. 575 tbd "Free array declarations containing SChars" 576 _ -> "(declare-fun " ++ nm ++ " () " ++ atyp ++ ")" 577 578 -- CVC4 chokes if the initializer is not a constant. (Z3 is ok with it.) So, print it as 579 -- a constant if we have it in the constants; otherwise, we merely print it and hope for the best. 580 constInit v = case v `M.lookup` constMapping of 581 Nothing -> ssv v -- Z3 will work, CVC4 will choke. Others don't even support this. 582 Just c -> cvtCV (roundingMode cfg) c -- Z3 and CVC4 will work. Other's don't support this. 583 584 ctxInfo = case ctx of 585 ArrayFree _ -> [] 586 ArrayMutate j a b -> [(all (`elem` constNames) [a, b], "(= " ++ nm ++ " (store array_" ++ show j ++ " " ++ ssv a ++ " " ++ ssv b ++ "))")] 587 ArrayMerge t j k -> [(t `elem` constNames, "(= " ++ nm ++ " (ite " ++ ssv t ++ " array_" ++ show j ++ " array_" ++ show k ++ "))")] 588 589 -- Arrange for initializers 590 mkInit idx = "array_" ++ show i ++ "_initializer_" ++ show (idx :: Int) 591 initializer = "array_" ++ show i ++ "_initializer" 592 593 wrap index s = "(define-fun " ++ mkInit index ++ " () Bool " ++ s ++ ")" 594 595 lpre = length pre 596 lAll = lpre + length post 597 598 setup 599 | lAll == 0 = [ "(define-fun " ++ initializer ++ " () Bool true) ; no initializiation needed" | not quantified] 600 | lAll == 1 = [ "(define-fun " ++ initializer ++ " () Bool " ++ mkInit 0 ++ ")" 601 , "(assert " ++ initializer ++ ")" 602 ] 603 | True = [ "(define-fun " ++ initializer ++ " () Bool (and " ++ unwords (map mkInit [0..lAll - 1]) ++ "))" 604 , "(assert " ++ initializer ++ ")" 605 ] 606 607svType :: SV -> String 608svType s = smtType (kindOf s) 609 610svFunType :: [SV] -> SV -> String 611svFunType ss s = "(" ++ unwords (map svType ss) ++ ") " ++ svType s 612 613cvtType :: SBVType -> String 614cvtType (SBVType []) = error "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!" 615cvtType (SBVType xs) = "(" ++ unwords (map smtType body) ++ ") " ++ smtType ret 616 where (body, ret) = (init xs, last xs) 617 618type SkolemMap = M.Map SV [SV] 619type TableMap = IM.IntMap String 620 621-- Present an SV; inline true/false as needed 622cvtSV :: SkolemMap -> SV -> String 623cvtSV skolemMap s@(SV _ (NodeId n)) 624 | Just ss <- s `M.lookup` skolemMap 625 = "(" ++ show s ++ concatMap ((" " ++) . show) ss ++ ")" 626 | s == trueSV 627 = "true" 628 | s == falseSV 629 = "false" 630 | True 631 = 's' : show n 632 633cvtCV :: RoundingMode -> CV -> String 634cvtCV = cvToSMTLib 635 636getTable :: TableMap -> Int -> String 637getTable m i 638 | Just tn <- i `IM.lookup` m = tn 639 | True = "table" ++ show i -- constant tables are always named this way 640 641cvtExp :: SolverCapabilities -> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String 642cvtExp caps rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr 643 where ssv = cvtSV skolemMap 644 645 hasPB = supportsPseudoBooleans caps 646 hasInt2bv = supportsInt2bv caps 647 hasDistinct = supportsDistinct caps 648 649 bvOp = all isBounded arguments 650 intOp = any isUnbounded arguments 651 realOp = any isReal arguments 652 fpOp = any (\a -> isDouble a || isFloat a || isFP a) arguments 653 boolOp = all isBoolean arguments 654 charOp = any isChar arguments 655 stringOp = any isString arguments 656 listOp = any isList arguments 657 658 bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr 659 | True = error $ "SBV.SMTLib2: Unsupported operation on real values: " ++ show expr 660 661 ensureBVOrBool = bvOp || boolOp || bad 662 ensureBV = bvOp || bad 663 664 addRM s = s ++ " " ++ smtRoundingMode rm 665 666 -- lift a binary op 667 lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" 668 lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs) 669 670 -- lift an arbitrary arity operator 671 liftN o _ xs = "(" ++ o ++ " " ++ unwords xs ++ ")" 672 673 -- lift a binary operation with rounding-mode added; used for floating-point arithmetic 674 lift2WM o fo | fpOp = lift2 (addRM fo) 675 | True = lift2 o 676 677 lift1FP o fo | fpOp = lift1 fo 678 | True = lift1 o 679 680 liftAbs sgned args | fpOp = lift1 "fp.abs" sgned args 681 | intOp = lift1 "abs" sgned args 682 | bvOp, sgned = mkAbs (head args) "bvslt" "bvneg" 683 | bvOp = head args 684 | True = mkAbs (head args) "<" "-" 685 where mkAbs x cmp neg = "(ite " ++ ltz ++ " " ++ nx ++ " " ++ x ++ ")" 686 where ltz = "(" ++ cmp ++ " " ++ x ++ " " ++ z ++ ")" 687 nx = "(" ++ neg ++ " " ++ x ++ ")" 688 z = cvtCV rm (mkConstCV (kindOf (head arguments)) (0::Integer)) 689 690 lift2B bOp vOp 691 | boolOp = lift2 bOp 692 | True = lift2 vOp 693 694 lift1B bOp vOp 695 | boolOp = lift1 bOp 696 | True = lift1 vOp 697 698 eqBV = lift2 "=" 699 neqBV = liftN "distinct" 700 701 equal sgn sbvs 702 | fpOp = lift2 "fp.eq" sgn sbvs 703 | True = lift2 "=" sgn sbvs 704 705 notEqual sgn sbvs 706 | fpOp || not hasDistinct = liftP sbvs 707 | True = liftN "distinct" sgn sbvs 708 where liftP [_, _] = "(not " ++ equal sgn sbvs ++ ")" 709 liftP args = "(and " ++ unwords (walk args) ++ ")" 710 711 walk [] = [] 712 walk (e:es) = map (\e' -> liftP [e, e']) es ++ walk es 713 714 lift2S oU oS sgn = lift2 (if sgn then oS else oU) sgn 715 liftNS oU oS sgn = liftN (if sgn then oS else oU) sgn 716 717 lift2Cmp o fo | fpOp = lift2 fo 718 | True = lift2 o 719 720 unintComp o [a, b] 721 | KUserSort s (Just _) <- kindOf (head arguments) 722 = let idx v = "(" ++ s ++ "_constrIndex " ++ v ++ ")" in "(" ++ o ++ " " ++ idx a ++ " " ++ idx b ++ ")" 723 unintComp o sbvs = error $ "SBV.SMT.SMTLib2.sh.unintComp: Unexpected arguments: " ++ show (o, sbvs, map kindOf arguments) 724 725 stringOrChar KString = True 726 stringOrChar KChar = True 727 stringOrChar _ = False 728 stringCmp swap o [a, b] 729 | stringOrChar (kindOf (head arguments)) 730 = let [a1, a2] | swap = [b, a] 731 | True = [a, b] 732 in "(" ++ o ++ " " ++ a1 ++ " " ++ a2 ++ ")" 733 stringCmp _ o sbvs = error $ "SBV.SMT.SMTLib2.sh.stringCmp: Unexpected arguments: " ++ show (o, sbvs) 734 735 -- NB. Likewise for sequences 736 seqCmp swap o [a, b] 737 | KList{} <- kindOf (head arguments) 738 = let [a1, a2] | swap = [b, a] 739 | True = [a, b] 740 in "(" ++ o ++ " " ++ a1 ++ " " ++ a2 ++ ")" 741 seqCmp _ o sbvs = error $ "SBV.SMT.SMTLib2.sh.seqCmp: Unexpected arguments: " ++ show (o, sbvs) 742 743 lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")" 744 lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) 745 746 -- We fully qualify the constructor with their types to work around type checking issues 747 -- Note that this is rather bizarre, as we're tagging the constructor with its *result* type, 748 -- not its full function type as one would expect. But this is per the spec: Pg. 27 of SMTLib 2.6 spec 749 -- says: 750 -- 751 -- To simplify sort checking, a function symbol in a term can be annotated with one of its result sorts sigma. 752 -- 753 -- I wish it was the full type here not just the result, but we go with the spec. Also see: <http://github.com/Z3Prover/z3/issues/2135> 754 -- and in particular <http://github.com/Z3Prover/z3/issues/2135#issuecomment-477636435> 755 dtConstructor fld args res = "((as " ++ fld ++ " " ++ smtType res ++ ") " ++ unwords (map ssv args) ++ ")" 756 757 -- Similarly, we fully qualify the accessors with their types to work around type checking issues 758 -- Unfortunately, z3 and CVC4 are behaving differently, so we tie this ascription to a solver capability. 759 dtAccessor fld params res 760 | supportsDirectAccessors caps = dResult 761 | True = aResult 762 where dResult = "(_ is " ++ fld ++ ")" 763 ps = " (" ++ unwords (map smtType params) ++ ") " 764 aResult = "(_ is (" ++ fld ++ ps ++ smtType res ++ "))" 765 766 sh (SBVApp Ite [a, b, c]) = "(ite " ++ ssv a ++ " " ++ ssv b ++ " " ++ ssv c ++ ")" 767 768 sh (SBVApp (LkUp (t, aKnd, _, l) i e) []) 769 | needsCheck = "(ite " ++ cond ++ ssv e ++ " " ++ lkUp ++ ")" 770 | True = lkUp 771 where needsCheck = case aKnd of 772 KBool -> (2::Integer) > fromIntegral l 773 KBounded _ n -> (2::Integer)^n > fromIntegral l 774 KUnbounded -> True 775 KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index" 776 KFloat -> error "SBV.SMT.SMTLib2.cvtExp: unexpected float valued index" 777 KDouble -> error "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index" 778 KFP{} -> error "SBV.SMT.SMTLib2.cvtExp: unexpected arbitrary float valued index" 779 KChar -> error "SBV.SMT.SMTLib2.cvtExp: unexpected char valued index" 780 KString -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" 781 KList k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected list valued: " ++ show k 782 KSet k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected set valued: " ++ show k 783 KTuple k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected tuple valued: " ++ show k 784 KMaybe k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected maybe valued: " ++ show k 785 KEither k1 k2 -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected sum valued: " ++ show (k1, k2) 786 KUserSort s _ -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s 787 788 lkUp = "(" ++ getTable tableMap t ++ " " ++ ssv i ++ ")" 789 790 cond 791 | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") " 792 | True = gtl ++ " " 793 794 (less, leq) = case aKnd of 795 KBool -> error "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index" 796 KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule") 797 KUnbounded -> ("<", "<=") 798 KReal -> ("<", "<=") 799 KFloat -> ("fp.lt", "fp.leq") 800 KDouble -> ("fp.lt", "fp.geq") 801 KFP{} -> ("fp.lt", "fp.geq") 802 KChar -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" 803 KString -> error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index" 804 KList k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected sequence valued index: " ++ show k 805 KSet k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected set valued index: " ++ show k 806 KTuple k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected tuple valued index: " ++ show k 807 KMaybe k -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected maybe valued index: " ++ show k 808 KEither k1 k2 -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected sum valued index: " ++ show (k1, k2) 809 KUserSort s _ -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s 810 811 mkCnst = cvtCV rm . mkConstCV (kindOf i) 812 le0 = "(" ++ less ++ " " ++ ssv i ++ " " ++ mkCnst 0 ++ ")" 813 gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ ssv i ++ ")" 814 815 sh (SBVApp (KindCast f t) [a]) = handleKindCast hasInt2bv f t (ssv a) 816 817 sh (SBVApp (ArrEq i j) []) = "(= array_" ++ show i ++ " array_" ++ show j ++")" 818 sh (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ ssv a ++ ")" 819 820 sh (SBVApp (Uninterpreted nm) []) = nm 821 sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm ++ " " ++ unwords (map ssv args) ++ ")" 822 823 sh (SBVApp (Extract i j) [a]) | ensureBV = "((_ extract " ++ show i ++ " " ++ show j ++ ") " ++ ssv a ++ ")" 824 825 sh (SBVApp (Rol i) [a]) 826 | bvOp = rot ssv "rotate_left" i a 827 | True = bad 828 829 sh (SBVApp (Ror i) [a]) 830 | bvOp = rot ssv "rotate_right" i a 831 | True = bad 832 833 sh (SBVApp Shl [a, i]) 834 | bvOp = shft ssv "bvshl" "bvshl" a i 835 | True = bad 836 837 sh (SBVApp Shr [a, i]) 838 | bvOp = shft ssv "bvlshr" "bvashr" a i 839 | True = bad 840 841 sh (SBVApp op args) 842 | Just f <- lookup op smtBVOpTable, ensureBVOrBool 843 = f (any hasSign args) (map ssv args) 844 where -- The first 4 operators below do make sense for Integer's in Haskell, but there's 845 -- no obvious counterpart for them in the SMTLib translation. 846 -- TODO: provide support for these. 847 smtBVOpTable = [ (And, lift2B "and" "bvand") 848 , (Or, lift2B "or" "bvor") 849 , (XOr, lift2B "xor" "bvxor") 850 , (Not, lift1B "not" "bvnot") 851 , (Join, lift2 "concat") 852 ] 853 854 sh (SBVApp (Label _) [a]) = cvtSV skolemMap a -- This won't be reached; but just in case! 855 856 sh (SBVApp (IEEEFP (FP_Cast kFrom kTo m)) args) = handleFPCast kFrom kTo (ssv m) (unwords (map ssv args)) 857 sh (SBVApp (IEEEFP w ) args) = "(" ++ show w ++ " " ++ unwords (map ssv args) ++ ")" 858 859 sh (SBVApp (NonLinear w) args) = "(" ++ show w ++ " " ++ unwords (map ssv args) ++ ")" 860 861 sh (SBVApp (PseudoBoolean pb) args) 862 | hasPB = handlePB pb args' 863 | True = reducePB pb args' 864 where args' = map ssv args 865 866 -- NB: Z3 semantics have the predicates reversed: i.e., it returns true if overflow isn't possible. Hence the not. 867 sh (SBVApp (OverflowOp op) args) = "(not (" ++ show op ++ " " ++ unwords (map ssv args) ++ "))" 868 869 -- Note the unfortunate reversal in StrInRe.. 870 sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in.re " ++ unwords (map ssv args) ++ " " ++ regExpToSMTString r ++ ")" 871 -- StrUnit is no-op, since a character in SMTLib is the same as a string 872 sh (SBVApp (StrOp StrUnit) [a]) = ssv a 873 sh (SBVApp (StrOp op) args) = "(" ++ show op ++ " " ++ unwords (map ssv args) ++ ")" 874 875 sh (SBVApp (SeqOp op) args) = "(" ++ show op ++ " " ++ unwords (map ssv args) ++ ")" 876 877 sh (SBVApp (SetOp SetEqual) args) = "(= " ++ unwords (map ssv args) ++ ")" 878 sh (SBVApp (SetOp SetMember) [e, s]) = "(select " ++ ssv s ++ " " ++ ssv e ++ ")" 879 sh (SBVApp (SetOp SetInsert) [e, s]) = "(store " ++ ssv s ++ " " ++ ssv e ++ " true)" 880 sh (SBVApp (SetOp SetDelete) [e, s]) = "(store " ++ ssv s ++ " " ++ ssv e ++ " false)" 881 sh (SBVApp (SetOp SetIntersect) args) = "(intersection " ++ unwords (map ssv args) ++ ")" 882 sh (SBVApp (SetOp SetUnion) args) = "(union " ++ unwords (map ssv args) ++ ")" 883 sh (SBVApp (SetOp SetSubset) args) = "(subset " ++ unwords (map ssv args) ++ ")" 884 sh (SBVApp (SetOp SetDifference) args) = "(setminus " ++ unwords (map ssv args) ++ ")" 885 sh (SBVApp (SetOp SetComplement) args) = "(complement " ++ unwords (map ssv args) ++ ")" 886 sh (SBVApp (SetOp SetHasSize) args) = "(set-has-size " ++ unwords (map ssv args) ++ ")" 887 888 sh (SBVApp (TupleConstructor 0) []) = "mkSBVTuple0" 889 sh (SBVApp (TupleConstructor n) args) = "(mkSBVTuple" ++ show n ++ " " ++ unwords (map ssv args) ++ ")" 890 sh (SBVApp (TupleAccess i n) [tup]) = "(proj_" ++ show i ++ "_SBVTuple" ++ show n ++ " " ++ ssv tup ++ ")" 891 892 sh (SBVApp (EitherConstructor k1 k2 False) [arg]) = dtConstructor "left_SBVEither" [arg] (KEither k1 k2) 893 sh (SBVApp (EitherConstructor k1 k2 True ) [arg]) = dtConstructor "right_SBVEither" [arg] (KEither k1 k2) 894 sh (SBVApp (EitherIs k1 k2 False) [arg]) = '(' : dtAccessor "left_SBVEither" [k1] (KEither k1 k2) ++ " " ++ ssv arg ++ ")" 895 sh (SBVApp (EitherIs k1 k2 True ) [arg]) = '(' : dtAccessor "right_SBVEither" [k2] (KEither k1 k2) ++ " " ++ ssv arg ++ ")" 896 sh (SBVApp (EitherAccess False) [arg]) = "(get_left_SBVEither " ++ ssv arg ++ ")" 897 sh (SBVApp (EitherAccess True ) [arg]) = "(get_right_SBVEither " ++ ssv arg ++ ")" 898 899 sh (SBVApp (MaybeConstructor k False) []) = dtConstructor "nothing_SBVMaybe" [] (KMaybe k) 900 sh (SBVApp (MaybeConstructor k True) [arg]) = dtConstructor "just_SBVMaybe" [arg] (KMaybe k) 901 sh (SBVApp (MaybeIs k False) [arg]) = '(' : dtAccessor "nothing_SBVMaybe" [] (KMaybe k) ++ " " ++ ssv arg ++ ")" 902 sh (SBVApp (MaybeIs k True ) [arg]) = '(' : dtAccessor "just_SBVMaybe" [k] (KMaybe k) ++ " " ++ ssv arg ++ ")" 903 sh (SBVApp MaybeAccess [arg]) = "(get_just_SBVMaybe " ++ ssv arg ++ ")" 904 905 sh inp@(SBVApp op args) 906 | intOp, Just f <- lookup op smtOpIntTable 907 = f True (map ssv args) 908 | boolOp, Just f <- lookup op boolComps 909 = f (map ssv args) 910 | bvOp, Just f <- lookup op smtOpBVTable 911 = f (any hasSign args) (map ssv args) 912 | realOp, Just f <- lookup op smtOpRealTable 913 = f (any hasSign args) (map ssv args) 914 | fpOp, Just f <- lookup op smtOpFloatDoubleTable 915 = f (any hasSign args) (map ssv args) 916 | charOp || stringOp, Just f <- lookup op smtStringTable 917 = f (map ssv args) 918 | listOp, Just f <- lookup op smtListTable 919 = f (map ssv args) 920 | Just f <- lookup op uninterpretedTable 921 = f (map ssv args) 922 | True 923 = if not (null args) && isUserSort (head args) 924 then error $ unlines [ "" 925 , "*** Cannot translate operator : " ++ show op 926 , "*** When applied to arguments of kind: " ++ intercalate ", " (nub (map (show . kindOf) args)) 927 , "*** Found as part of the expression : " ++ show inp 928 , "***" 929 , "*** Note that uninterpreted kinds only support equality." 930 , "*** If you believe this is in error, please report!" 931 ] 932 else error $ "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp 933 where smtOpBVTable = [ (Plus, lift2 "bvadd") 934 , (Minus, lift2 "bvsub") 935 , (Times, lift2 "bvmul") 936 , (UNeg, lift1B "not" "bvneg") 937 , (Abs, liftAbs) 938 , (Quot, lift2S "bvudiv" "bvsdiv") 939 , (Rem, lift2S "bvurem" "bvsrem") 940 , (Equal, eqBV) 941 , (NotEqual, neqBV) 942 , (LessThan, lift2S "bvult" "bvslt") 943 , (GreaterThan, lift2S "bvugt" "bvsgt") 944 , (LessEq, lift2S "bvule" "bvsle") 945 , (GreaterEq, lift2S "bvuge" "bvsge") 946 ] 947 948 -- Boolean comparisons.. SMTLib's bool type doesn't do comparisons, but Haskell does.. Sigh 949 boolComps = [ (LessThan, blt) 950 , (GreaterThan, blt . swp) 951 , (LessEq, blq) 952 , (GreaterEq, blq . swp) 953 ] 954 where blt [x, y] = "(and (not " ++ x ++ ") " ++ y ++ ")" 955 blt xs = error $ "SBV.SMT.SMTLib2.boolComps.blt: Impossible happened, incorrect arity (expected 2): " ++ show xs 956 blq [x, y] = "(or (not " ++ x ++ ") " ++ y ++ ")" 957 blq xs = error $ "SBV.SMT.SMTLib2.boolComps.blq: Impossible happened, incorrect arity (expected 2): " ++ show xs 958 swp [x, y] = [y, x] 959 swp xs = error $ "SBV.SMT.SMTLib2.boolComps.swp: Impossible happened, incorrect arity (expected 2): " ++ show xs 960 961 smtOpRealTable = smtIntRealShared 962 ++ [ (Quot, lift2WM "/" "fp.div") 963 ] 964 965 smtOpIntTable = smtIntRealShared 966 ++ [ (Quot, lift2 "div") 967 , (Rem, lift2 "mod") 968 ] 969 970 smtOpFloatDoubleTable = smtIntRealShared 971 ++ [(Quot, lift2WM "/" "fp.div")] 972 973 smtIntRealShared = [ (Plus, lift2WM "+" "fp.add") 974 , (Minus, lift2WM "-" "fp.sub") 975 , (Times, lift2WM "*" "fp.mul") 976 , (UNeg, lift1FP "-" "fp.neg") 977 , (Abs, liftAbs) 978 , (Equal, equal) 979 , (NotEqual, notEqual) 980 , (LessThan, lift2Cmp "<" "fp.lt") 981 , (GreaterThan, lift2Cmp ">" "fp.gt") 982 , (LessEq, lift2Cmp "<=" "fp.leq") 983 , (GreaterEq, lift2Cmp ">=" "fp.geq") 984 ] 985 986 -- equality and comparisons are the only thing that works on uninterpreted sorts and pretty much everything else 987 uninterpretedTable = [ (Equal, lift2S "=" "=" True) 988 , (NotEqual, liftNS "distinct" "distinct" True) 989 , (LessThan, unintComp "<") 990 , (GreaterThan, unintComp ">") 991 , (LessEq, unintComp "<=") 992 , (GreaterEq, unintComp ">=") 993 ] 994 995 -- For strings, equality and comparisons are the only operators 996 -- TODO: The string comparison operators will most likely change with the new theory! 997 smtStringTable = [ (Equal, lift2S "=" "=" True) 998 , (NotEqual, liftNS "distinct" "distinct" True) 999 , (LessThan, stringCmp False "str.<") 1000 , (GreaterThan, stringCmp True "str.<") 1001 , (LessEq, stringCmp False "str.<=") 1002 , (GreaterEq, stringCmp True "str.<=") 1003 ] 1004 1005 -- For lists, equality is really the only operator 1006 -- Likewise here, things might change for comparisons 1007 smtListTable = [ (Equal, lift2S "=" "=" True) 1008 , (NotEqual, liftNS "distinct" "distinct" True) 1009 , (LessThan, seqCmp False "seq.<") 1010 , (GreaterThan, seqCmp True "seq.<") 1011 , (LessEq, seqCmp False "seq.<=") 1012 , (GreaterEq, seqCmp True "seq.<=") 1013 ] 1014 1015declareFun :: SV -> SBVType -> Maybe String -> [String] 1016declareFun = declareName . show 1017 1018declareName :: String -> SBVType -> Maybe String -> [String] 1019declareName s t@(SBVType inputKS) mbCmnt = decl : restrict 1020 where decl = "(declare-fun " ++ s ++ " " ++ cvtType t ++ ")" ++ maybe "" (" ; " ++) mbCmnt 1021 1022 (args, result) = case inputKS of 1023 [] -> error $ "SBV.declareName: Unexpected empty type for: " ++ show s 1024 _ -> (init inputKS, last inputKS) 1025 1026 -- Does the kind KChar *not* occur in the kind anywhere? 1027 charFree k = null [() | KChar <- G.universe k] 1028 noChars = charFree result 1029 needsQuant = not $ null args 1030 1031 resultVar | needsQuant = "result" 1032 | True = s 1033 1034 argList = ["a" ++ show i | (i, _) <- zip [1::Int ..] args] 1035 argTList = ["(" ++ a ++ " " ++ smtType k ++ ")" | (a, k) <- zip argList args] 1036 resultExp = "(" ++ s ++ " " ++ unwords argList ++ ")" 1037 1038 restrict | noChars = [] 1039 | needsQuant = [ "(assert (forall (" ++ unwords argTList ++ ")" 1040 , " (let ((" ++ resultVar ++ " " ++ resultExp ++ "))" 1041 ] 1042 ++ (case constraints of 1043 [] -> [ " true"] 1044 [x] -> [ " " ++ x] 1045 (x:xs) -> ( " (and " ++ x) 1046 : [ " " ++ c | c <- xs] 1047 ++ [ " )"]) 1048 ++ [ " )))"] 1049 | True = case constraints of 1050 [] -> [] 1051 [x] -> ["(assert " ++ x ++ ")"] 1052 (x:xs) -> ( "(assert (and " ++ x) 1053 : [ " " ++ c | c <- xs] 1054 ++ [ " ))"] 1055 1056 constraints = walk 0 resultVar (\nm -> "(= 1 (str.len " ++ nm ++ "))") result 1057 1058 mkAnd [] = "true" 1059 mkAnd [c] = c 1060 mkAnd cs = "(and " ++ unwords cs ++ ")" 1061 1062 walk :: Int -> String -> (String -> String) -> Kind -> [String] 1063 walk _d _nm _f KBool {} = [] 1064 walk _d _nm _f KBounded {} = [] 1065 walk _d _nm _f KUnbounded{} = [] 1066 walk _d _nm _f KReal {} = [] 1067 walk _d _nm _f KUserSort {} = [] 1068 walk _d _nm _f KFloat {} = [] 1069 walk _d _nm _f KDouble {} = [] 1070 walk _d _nm _f KFP {} = [] 1071 walk _d nm f KChar {} = [f nm] 1072 walk _d _nm _f KString {} = [] 1073 walk d nm _f (KList k) 1074 | charFree k = [] 1075 | True = let fnm = "seq" ++ show d 1076 cstrs = walk (d+1) ("(seq.nth " ++ nm ++ " " ++ fnm ++ ")") 1077 (\snm -> "(= 1 (str.len " ++ snm ++ "))") k 1078 in ["(forall ((" ++ fnm ++ " " ++ smtType KUnbounded ++ ")) " ++ "(=> (and (>= " ++ fnm ++ " 0) (< " ++ fnm ++ " (seq.len " ++ nm ++ "))) " ++ mkAnd cstrs ++ "))"] 1079 walk d nm _f (KSet k) 1080 | charFree k = [] 1081 | True = let fnm = "set" ++ show d 1082 cstrs = walk (d+1) nm (\snm -> "(=> (select " ++ snm ++ " " ++ fnm ++ ") (= 1 (str.len " ++ fnm ++ ")))") k 1083 in ["(forall ((" ++ fnm ++ " " ++ smtType k ++ ")) " ++ mkAnd cstrs ++ ")"] 1084 walk d nm f (KTuple ks) = let tt = "SBVTuple" ++ show (length ks) 1085 project i = "(proj_" ++ show i ++ "_" ++ tt ++ " " ++ nm ++ ")" 1086 nmks = [(project i, k) | (i, k) <- zip [1::Int ..] ks] 1087 in concatMap (\(n, k) -> walk (d+1) n f k) nmks 1088 walk d nm f km@(KMaybe k) = let n = "(get_just_SBVMaybe " ++ nm ++ ")" 1089 in ["(=> " ++ "((_ is (just_SBVMaybe (" ++ smtType k ++ ") " ++ smtType km ++ ")) " ++ nm ++ ") " ++ c ++ ")" | c <- walk (d+1) n f k] 1090 walk d nm f ke@(KEither k1 k2) = let n1 = "(get_left_SBVEither " ++ nm ++ ")" 1091 n2 = "(get_right_SBVEither " ++ nm ++ ")" 1092 c1 = ["(=> " ++ "((_ is (left_SBVEither (" ++ smtType k1 ++ ") " ++ smtType ke ++ ")) " ++ nm ++ ") " ++ c ++ ")" | c <- walk (d+1) n1 f k1] 1093 c2 = ["(=> " ++ "((_ is (right_SBVEither (" ++ smtType k2 ++ ") " ++ smtType ke ++ ")) " ++ nm ++ ") " ++ c ++ ")" | c <- walk (d+1) n2 f k2] 1094 in c1 ++ c2 1095 1096----------------------------------------------------------------------------------------------- 1097-- Casts supported by SMTLib. (From: <http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml>) 1098-- ; from another floating point sort 1099-- ((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb)) 1100-- 1101-- ; from real 1102-- ((_ to_fp eb sb) RoundingMode Real (_ FloatingPoint eb sb)) 1103-- 1104-- ; from signed machine integer, represented as a 2's complement bit vector 1105-- ((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)) 1106-- 1107-- ; from unsigned machine integer, represented as bit vector 1108-- ((_ to_fp_unsigned eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)) 1109-- 1110-- ; to unsigned machine integer, represented as a bit vector 1111-- ((_ fp.to_ubv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m)) 1112-- 1113-- ; to signed machine integer, represented as a 2's complement bit vector 1114-- ((_ fp.to_sbv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m)) 1115-- 1116-- ; to real 1117-- (fp.to_real (_ FloatingPoint eb sb) Real) 1118----------------------------------------------------------------------------------------------- 1119 1120handleFPCast :: Kind -> Kind -> String -> String -> String 1121handleFPCast kFromIn kToIn rm input 1122 | kFrom == kTo 1123 = input 1124 | True 1125 = "(" ++ cast kFrom kTo input ++ ")" 1126 where addRM a s = s ++ " " ++ rm ++ " " ++ a 1127 1128 kFrom = simplify kFromIn 1129 kTo = simplify kToIn 1130 1131 simplify KFloat = KFP 8 24 1132 simplify KDouble = KFP 11 53 1133 simplify k = k 1134 1135 size (eb, sb) = show eb ++ " " ++ show sb 1136 1137 -- To go and back from Ints, we detour through reals 1138 cast KUnbounded (KFP eb sb) a = "(_ to_fp " ++ size (eb, sb) ++ ") " ++ rm ++ " (to_real " ++ a ++ ")" 1139 cast KFP{} KUnbounded a = "to_int (fp.to_real " ++ a ++ ")" 1140 1141 -- To floats 1142 cast (KBounded False _) (KFP eb sb) a = addRM a $ "(_ to_fp_unsigned " ++ size (eb, sb) ++ ")" 1143 cast (KBounded True _) (KFP eb sb) a = addRM a $ "(_ to_fp " ++ size (eb, sb) ++ ")" 1144 cast KReal (KFP eb sb) a = addRM a $ "(_ to_fp " ++ size (eb, sb) ++ ")" 1145 cast KFP{} (KFP eb sb) a = addRM a $ "(_ to_fp " ++ size (eb, sb) ++ ")" 1146 1147 -- From float/double 1148 cast KFP{} (KBounded False m) a = addRM a $ "(_ fp.to_ubv " ++ show m ++ ")" 1149 cast KFP{} (KBounded True m) a = addRM a $ "(_ fp.to_sbv " ++ show m ++ ")" 1150 1151 -- To real 1152 cast KFP{} KReal a = "fp.to_real" ++ " " ++ a 1153 1154 -- Nothing else should come up: 1155 cast f d _ = error $ "SBV.SMTLib2: Unexpected FPCast from: " ++ show f ++ " to " ++ show d 1156 1157rot :: (SV -> String) -> String -> Int -> SV -> String 1158rot ssv o c x = "((_ " ++ o ++ " " ++ show c ++ ") " ++ ssv x ++ ")" 1159 1160shft :: (SV -> String) -> String -> String -> SV -> SV -> String 1161shft ssv oW oS x c = "(" ++ o ++ " " ++ ssv x ++ " " ++ ssv c ++ ")" 1162 where o = if hasSign x then oS else oW 1163 1164-- Various casts 1165handleKindCast :: Bool -> Kind -> Kind -> String -> String 1166handleKindCast hasInt2bv kFrom kTo a 1167 | kFrom == kTo 1168 = a 1169 | True 1170 = case kFrom of 1171 KBounded s m -> case kTo of 1172 KBounded _ n -> fromBV (if s then signExtend else zeroExtend) m n 1173 KUnbounded -> b2i s m 1174 _ -> tryFPCast 1175 1176 KUnbounded -> case kTo of 1177 KReal -> "(to_real " ++ a ++ ")" 1178 KBounded _ n -> i2b n 1179 _ -> tryFPCast 1180 1181 KReal -> case kTo of 1182 KUnbounded -> "(to_int " ++ a ++ ")" 1183 _ -> tryFPCast 1184 1185 _ -> tryFPCast 1186 1187 where -- See if we can push this down to a float-cast, using sRNE. This happens if one of the kinds is a float/double. 1188 -- Otherwise complain 1189 tryFPCast 1190 | any (\k -> isFloat k || isDouble k) [kFrom, kTo] 1191 = handleFPCast kFrom kTo (smtRoundingMode RoundNearestTiesToEven) a 1192 | True 1193 = error $ "SBV.SMTLib2: Unexpected cast from: " ++ show kFrom ++ " to " ++ show kTo 1194 1195 fromBV upConv m n 1196 | n > m = upConv (n - m) 1197 | m == n = a 1198 | True = extract (n - 1) 1199 1200 b2i False _ = "(bv2nat " ++ a ++ ")" 1201 b2i True 1 = "(ite (= " ++ a ++ " #b0) 0 (- 1))" 1202 b2i True m = "(ite (= " ++ msb ++ " #b0" ++ ") " ++ ifPos ++ " " ++ ifNeg ++ ")" 1203 where offset :: Integer 1204 offset = 2^(m-1) 1205 rest = extract (m - 2) 1206 1207 msb = let top = show (m-1) in "((_ extract " ++ top ++ " " ++ top ++ ") " ++ a ++ ")" 1208 ifPos = "(bv2nat " ++ rest ++")" 1209 ifNeg = "(- " ++ ifPos ++ " " ++ show offset ++ ")" 1210 1211 signExtend i = "((_ sign_extend " ++ show i ++ ") " ++ a ++ ")" 1212 zeroExtend i = "((_ zero_extend " ++ show i ++ ") " ++ a ++ ")" 1213 extract i = "((_ extract " ++ show i ++ " 0) " ++ a ++ ")" 1214 1215 -- Some solvers support int2bv, but not all. So, we use a capability to determine. 1216 -- 1217 -- NB. The "manual" implementation works regardless n < 0 or not, because the first thing we 1218 -- do is to compute "reduced" to bring it down to the correct range. It also works 1219 -- regardless were mapping to signed or unsigned bit-vector; because the representation 1220 -- is the same. 1221 i2b n 1222 | hasInt2bv 1223 = "((_ int2bv " ++ show n ++ ") " ++ a ++ ")" 1224 | True 1225 = "(let (" ++ reduced ++ ") (let (" ++ defs ++ ") " ++ body ++ "))" 1226 where b i = show (bit i :: Integer) 1227 reduced = "(__a (mod " ++ a ++ " " ++ b n ++ "))" 1228 mkBit 0 = "(__a0 (ite (= (mod __a 2) 0) #b0 #b1))" 1229 mkBit i = "(__a" ++ show i ++ " (ite (= (mod (div __a " ++ b i ++ ") 2) 0) #b0 #b1))" 1230 defs = unwords (map mkBit [0 .. n - 1]) 1231 body = foldr1 (\c r -> "(concat " ++ c ++ " " ++ r ++ ")") ["__a" ++ show i | i <- [n-1, n-2 .. 0]] 1232 1233-- Translation of pseudo-booleans, in case the solver supports them 1234handlePB :: PBOp -> [String] -> String 1235handlePB (PB_AtMost k) args = "((_ at-most " ++ show k ++ ") " ++ unwords args ++ ")" 1236handlePB (PB_AtLeast k) args = "((_ at-least " ++ show k ++ ") " ++ unwords args ++ ")" 1237handlePB (PB_Exactly k) args = "((_ pbeq " ++ unwords (map show (k : replicate (length args) 1)) ++ ") " ++ unwords args ++ ")" 1238handlePB (PB_Eq cs k) args = "((_ pbeq " ++ unwords (map show (k : cs)) ++ ") " ++ unwords args ++ ")" 1239handlePB (PB_Le cs k) args = "((_ pble " ++ unwords (map show (k : cs)) ++ ") " ++ unwords args ++ ")" 1240handlePB (PB_Ge cs k) args = "((_ pbge " ++ unwords (map show (k : cs)) ++ ") " ++ unwords args ++ ")" 1241 1242-- Translation of pseudo-booleans, in case the solver does *not* support them 1243reducePB :: PBOp -> [String] -> String 1244reducePB op args = case op of 1245 PB_AtMost k -> "(<= " ++ addIf (repeat 1) ++ " " ++ show k ++ ")" 1246 PB_AtLeast k -> "(>= " ++ addIf (repeat 1) ++ " " ++ show k ++ ")" 1247 PB_Exactly k -> "(= " ++ addIf (repeat 1) ++ " " ++ show k ++ ")" 1248 PB_Le cs k -> "(<= " ++ addIf cs ++ " " ++ show k ++ ")" 1249 PB_Ge cs k -> "(>= " ++ addIf cs ++ " " ++ show k ++ ")" 1250 PB_Eq cs k -> "(= " ++ addIf cs ++ " " ++ show k ++ ")" 1251 1252 where addIf :: [Int] -> String 1253 addIf cs = "(+ " ++ unwords ["(ite " ++ a ++ " " ++ show c ++ " 0)" | (a, c) <- zip args cs] ++ ")" 1254