From 764fcc21919fe43e6c227d45b94c815014f569a6 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 16 Jul 2024 19:30:38 +1000 Subject: [PATCH] House-keeping: adjust `-l Abort` log switch, update llvm.k test definition (#3980) * Adds the new `request ` prefix in front of the `proxy` context to the `-l Aborts` short-hand * updates `llvm.k` to use `symbol(Bla)` instead of `klabel(Bla), symbol` to avoid warnings --- booster/library/Booster/CLOptions.hs | 4 +- booster/test/llvm-integration/LLVM.hs | 2972 ++++++++++------- .../test/llvm-integration/definition/llvm.k | 20 +- 3 files changed, 1713 insertions(+), 1283 deletions(-) diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs index 42c9fa516f..72420f49cc 100644 --- a/booster/library/Booster/CLOptions.hs +++ b/booster/library/Booster/CLOptions.hs @@ -297,8 +297,8 @@ levelToContext = , [ [ctxt| request*,booster>rewrite*,detail. |] , [ctxt| request*,booster>rewrite*,match|definedness|constraint,abort. |] - , [ctxt| proxy. |] - , [ctxt| proxy,abort. |] + , [ctxt| request*,proxy. |] + , [ctxt| request*,proxy,abort. |] , [ctxt| request*,booster>failure,abort |] ] ) diff --git a/booster/test/llvm-integration/LLVM.hs b/booster/test/llvm-integration/LLVM.hs index 520251f05b..a6b335fa39 100644 --- a/booster/test/llvm-integration/LLVM.hs +++ b/booster/test/llvm-integration/LLVM.hs @@ -1,5 +1,4 @@ {-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE QuasiQuotes #-} {- | Copyright : (c) Runtime Verification, 2023 @@ -42,11 +41,13 @@ import Booster.Definition.Base import Booster.LLVM qualified as LLVM import Booster.LLVM.Internal qualified as Internal import Booster.Pattern.Base +import Booster.SMT.Base (SExpr (..), SMTId (..)) import Booster.Syntax.Json.Externalise (externaliseTerm) import Booster.Syntax.Json.Internalise (pattern AllowAlias, pattern IgnoreSubsorts) import Booster.Syntax.Json.Internalise qualified as Syntax -import Booster.Syntax.ParsedKore.Internalise (buildDefinitions, symb) +import Booster.Syntax.ParsedKore.Internalise (buildDefinitions) import Booster.Syntax.ParsedKore.Parser (parseDefinition) +import Booster.Util (Flag (..)) import Kore.Syntax.Json.Types qualified as Syntax -- A prerequisite for all tests in this suite is that a fixed K @@ -403,72 +404,72 @@ defSorts = Map.fromList [ ( "SortBool" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortBool"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortBool"]) ) , ( "SortBytes" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortBytes"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortBytes"]) ) , ( "SortEndianness" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortEndianness"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortEndianness"]) ) , ( "SortEven" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortEven"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortEven"]) ) , ( "SortGeneratedCounterCell" , - ( SortAttributes{collectionAttributes = Nothing, argCount = 0} + ( SortAttributes{argCount = 0, collectionAttributes = Nothing} , Set.fromList ["SortGeneratedCounterCell"] ) ) , ( "SortGeneratedCounterCellOpt" , - ( SortAttributes{collectionAttributes = Nothing, argCount = 0} + ( SortAttributes{argCount = 0, collectionAttributes = Nothing} , Set.fromList ["SortGeneratedCounterCell", "SortGeneratedCounterCellOpt"] ) ) , ( "SortGeneratedTopCell" , - ( SortAttributes{collectionAttributes = Nothing, argCount = 0} + ( SortAttributes{argCount = 0, collectionAttributes = Nothing} , Set.fromList ["SortGeneratedTopCell"] ) ) , ( "SortGeneratedTopCellFragment" , - ( SortAttributes{collectionAttributes = Nothing, argCount = 0} + ( SortAttributes{argCount = 0, collectionAttributes = Nothing} , Set.fromList ["SortGeneratedTopCellFragment"] ) ) , ( "SortInt" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortInt"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortInt"]) ) - , ("SortK", (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortK"])) + , ("SortK", (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortK"])) , ( "SortKCell" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortKCell"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortKCell"]) ) , ( "SortKCellOpt" , - ( SortAttributes{collectionAttributes = Nothing, argCount = 0} + ( SortAttributes{argCount = 0, collectionAttributes = Nothing} , Set.fromList ["SortKCell", "SortKCellOpt"] ) ) , ( "SortKConfigVar" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortKConfigVar"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortKConfigVar"]) ) , ( "SortKItem" , - ( SortAttributes{collectionAttributes = Nothing, argCount = 0} + ( SortAttributes{argCount = 0, collectionAttributes = Nothing} , Set.fromList [ "SortBool" , "SortBytes" @@ -485,57 +486,118 @@ defSorts = , "SortKItem" , "SortList" , "SortMap" + , "SortMapValToVal" , "SortNum" , "SortOdd" , "SortSet" , "SortSignedness" , "SortString" + , "SortVal" + , "SortWrappedInt" ] ) ) , ( "SortList" , - ( SortAttributes{collectionAttributes = Just (sortListKList.symbolNames, KListTag), argCount = 0} + ( SortAttributes + { argCount = 0 + , collectionAttributes = + Just + ( KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'List" + , elementSymbolName = "LblListItem" + , concatSymbolName = "Lbl'Unds'List'Unds'" + } + , KListTag + ) + } , Set.fromList ["SortList"] ) ) , - ( "SortSet" + ( "SortMap" , - ( SortAttributes{collectionAttributes = Just (sortSetKSet.symbolNames, KSetTag), argCount = 0} - , Set.fromList ["SortSet"] + ( SortAttributes + { argCount = 0 + , collectionAttributes = + Just + ( KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'Map" + , elementSymbolName = "Lbl'UndsPipe'-'-GT-Unds'" + , concatSymbolName = "Lbl'Unds'Map'Unds'" + } + , KMapTag + ) + } + , Set.fromList ["SortMap"] ) ) , - ( "SortMap" + ( "SortMapValToVal" , - ( SortAttributes{collectionAttributes = Just (sortMapKmap.symbolNames, KMapTag), argCount = 0} - , Set.fromList ["SortMap"] + ( SortAttributes + { argCount = 0 + , collectionAttributes = + Just + ( KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'MapValToVal" + , elementSymbolName = "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'" + , concatSymbolName = "Lbl'Unds'MapValToVal'Unds'" + } + , KMapTag + ) + } + , Set.fromList ["SortMapValToVal"] ) ) , ( "SortNum" , - ( SortAttributes{collectionAttributes = Nothing, argCount = 0} + ( SortAttributes{argCount = 0, collectionAttributes = Nothing} , Set.fromList ["SortEven", "SortNum", "SortOdd"] ) ) , ( "SortOdd" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortOdd"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortOdd"]) ) , ( "SortSet" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortSet"]) + , + ( SortAttributes + { argCount = 0 + , collectionAttributes = + Just + ( KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'Set" + , elementSymbolName = "LblSetItem" + , concatSymbolName = "Lbl'Unds'Set'Unds'" + } + , KSetTag + ) + } + , Set.fromList ["SortSet"] + ) ) , ( "SortSignedness" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortSignedness"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortSignedness"]) ) , ( "SortString" - , (SortAttributes{collectionAttributes = Nothing, argCount = 0}, Set.fromList ["SortString"]) + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortString"]) + ) + , + ( "SortVal" + , + ( SortAttributes{argCount = 0, collectionAttributes = Nothing} + , Set.fromList ["SortVal", "SortWrappedInt"] + ) + ) + , + ( "SortWrappedInt" + , (SortAttributes{argCount = 0, collectionAttributes = Nothing}, Set.fromList ["SortWrappedInt"]) ) ] @@ -551,12 +613,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedCounterCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -571,12 +633,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedTopCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -591,12 +653,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedTopCellFragment" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -611,33 +673,12 @@ defSymbols = , resultSort = SortApp "SortKCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing - } - } - ) - , - ( "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort" - , Symbol - { name = - "Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort" - , sortVars = ["SortSort"] - , argSorts = [SortApp "SortBool" [], SortVar "SortSort", SortVar "SortSort"] - , resultSort = SortVar "SortSort" - , attributes = - SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -652,14 +693,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.empty" } } ) @@ -672,14 +713,14 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KListMeta sortListKList - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KListMeta sortListKList + , smt = Just (SMTLib "smt_seq_nil") + , hook = Just "LIST.unit" } } ) @@ -692,14 +733,49 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KMapMeta sortMapKmap - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KMapMeta sortMapKmap , smt = Nothing - , hook = Nothing + , hook = Just "MAP.unit" + } + } + ) + , + ( "Lbl'Stop'MapValToVal" + , Symbol + { name = "Lbl'Stop'MapValToVal" + , sortVars = [] + , argSorts = [] + , resultSort = SortApp "SortMapValToVal" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = + Just + ( KMapMeta + ( KMapDefinition + { symbolNames = + KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'MapValToVal" + , elementSymbolName = "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'" + , concatSymbolName = "Lbl'Unds'MapValToVal'Unds'" + } + , keySortName = "SortVal" + , elementSortName = "SortVal" + , mapSortName = "SortMapValToVal" + } + ) + ) + , smt = Nothing + , hook = Just "MAP.unit" } } ) @@ -712,14 +788,14 @@ defSymbols = , resultSort = SortApp "SortSet" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KSetMeta sortSetKSet - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KSetMeta sortSetKSet , smt = Nothing - , hook = Nothing + , hook = Just "SET.unit" } } ) @@ -732,14 +808,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTLib "notInt") + , hook = Just "INT.not" } } ) @@ -752,14 +828,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "-"}))) + , hook = Just "INT.sub" } } ) @@ -772,14 +848,14 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.difference" } } ) @@ -792,14 +868,14 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KListMeta sortListKList - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KListMeta sortListKList + , smt = Just (SMTLib "smt_seq_concat") + , hook = Just "LIST.concat" } } ) @@ -812,14 +888,49 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KMapMeta sortMapKmap - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KMapMeta sortMapKmap , smt = Nothing - , hook = Nothing + , hook = Just "MAP.concat" + } + } + ) + , + ( "Lbl'Unds'MapValToVal'Unds'" + , Symbol + { name = "Lbl'Unds'MapValToVal'Unds'" + , sortVars = [] + , argSorts = [SortApp "SortMapValToVal" [], SortApp "SortMapValToVal" []] + , resultSort = SortApp "SortMapValToVal" [] + , attributes = + SymbolAttributes + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = + Just + ( KMapMeta + ( KMapDefinition + { symbolNames = + KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'MapValToVal" + , elementSymbolName = "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'" + , concatSymbolName = "Lbl'Unds'MapValToVal'Unds'" + } + , keySortName = "SortVal" + , elementSortName = "SortVal" + , mapSortName = "SortMapValToVal" + } + ) + ) + , smt = Nothing + , hook = Just "MAP.concat" } } ) @@ -832,14 +943,49 @@ defSymbols = , resultSort = SortApp "SortSet" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KSetMeta sortSetKSet - , symbolType = Function Partial - , isIdem = IsIdem - , isAssoc = IsAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag True + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KSetMeta sortSetKSet , smt = Nothing - , hook = Nothing + , hook = Just "SET.concat" + } + } + ) + , + ( "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'" + , Symbol + { name = "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'" + , sortVars = [] + , argSorts = [SortApp "SortVal" [], SortApp "SortVal" []] + , resultSort = SortApp "SortMapValToVal" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = + Just + ( KMapMeta + ( KMapDefinition + { symbolNames = + KCollectionSymbolNames + { unitSymbolName = "Lbl'Stop'MapValToVal" + , elementSymbolName = "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'" + , concatSymbolName = "Lbl'Unds'MapValToVal'Unds'" + } + , keySortName = "SortVal" + , elementSortName = "SortVal" + , mapSortName = "SortMapValToVal" + } + ) + ) + , smt = Nothing + , hook = Just "MAP.element" } } ) @@ -852,14 +998,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "and"}))) + , hook = Just "BOOL.and" } } ) @@ -872,14 +1018,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "and"}))) + , hook = Just "BOOL.andThen" } } ) @@ -892,14 +1038,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "div"}))) + , hook = Just "INT.ediv" } } ) @@ -912,12 +1058,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -932,14 +1078,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "=>"}))) + , hook = Just "BOOL.implies" } } ) @@ -952,34 +1098,34 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.in_keys" } } ) , - ( "Lbl'Unds'in'UndsUnds'LIST'Unds'Bool'Unds'KItem'Unds'List" + ( "Lbl'Unds'inList'Unds'" , Symbol - { name = "Lbl'Unds'in'UndsUnds'LIST'Unds'Bool'Unds'KItem'Unds'List" + { name = "Lbl'Unds'inList'Unds'" , sortVars = [] , argSorts = [SortApp "SortKItem" [], SortApp "SortList" []] , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "LIST.in" } } ) @@ -992,14 +1138,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "mod"}))) + , hook = Just "INT.emod" } } ) @@ -1012,14 +1158,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "or"}))) + , hook = Just "BOOL.or" } } ) @@ -1032,14 +1178,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "or"}))) + , hook = Just "BOOL.orElse" } } ) @@ -1052,14 +1198,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "xor"}))) + , hook = Just "BOOL.xor" } } ) @@ -1072,14 +1218,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTLib "xorInt") + , hook = Just "INT.xor" } } ) @@ -1092,14 +1238,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = ">"}))) + , hook = Just "INT.gt" } } ) @@ -1112,14 +1258,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTLib "shrInt") + , hook = Just "INT.shr" } } ) @@ -1132,14 +1278,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = ">="}))) + , hook = Just "INT.ge" } } ) @@ -1152,14 +1298,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "<"}))) + , hook = Just "INT.lt" } } ) @@ -1172,14 +1318,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTLib "shlInt") + , hook = Just "INT.shl" } } ) @@ -1192,14 +1338,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "<="}))) + , hook = Just "INT.le" } } ) @@ -1212,14 +1358,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.inclusion" } } ) @@ -1232,14 +1378,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "SET.inclusion" } } ) @@ -1252,14 +1398,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTLib "andInt") + , hook = Just "INT.and" } } ) @@ -1272,14 +1418,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "="}))) + , hook = Just "BOOL.eq" } } ) @@ -1292,14 +1438,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "="}))) + , hook = Just "INT.eq" } } ) @@ -1312,14 +1458,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "="}))) + , hook = Just "KEQUAL.eq" } } ) @@ -1332,14 +1478,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "distinct"}))) + , hook = Just "BOOL.ne" } } ) @@ -1352,14 +1498,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "distinct"}))) + , hook = Just "INT.ne" } } ) @@ -1372,14 +1518,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "distinct"}))) + , hook = Just "KEQUAL.ne" } } ) @@ -1392,34 +1538,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing - } - } - ) - , - ( "Lbl'UndsLSqBUnds-LT-'-'UndsRSqBUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'KItem" - , Symbol - { name = "Lbl'UndsLSqBUnds-LT-'-'UndsRSqBUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'KItem" - , sortVars = [] - , argSorts = [SortApp "SortList" [], SortApp "SortInt" [], SortApp "SortKItem" []] - , resultSort = SortApp "SortList" [] - , attributes = - SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.update" } } ) @@ -1432,34 +1558,14 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing - } - } - ) - , - ( "Lbl'UndsLSqBUndsRSqB'orDefault'UndsUnds'MAP'Unds'KItem'Unds'Map'Unds'KItem'Unds'KItem" - , Symbol - { name = "Lbl'UndsLSqBUndsRSqB'orDefault'UndsUnds'MAP'Unds'KItem'Unds'Map'Unds'KItem'Unds'KItem" - , sortVars = [] - , argSorts = [SortApp "SortMap" [], SortApp "SortKItem" [], SortApp "SortKItem" []] - , resultSort = SortApp "SortKItem" [] - , attributes = - SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.remove" } } ) @@ -1472,14 +1578,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.get" } } ) @@ -1492,14 +1598,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "mod"}))) + , hook = Just "INT.tmod" } } ) @@ -1512,14 +1618,14 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KMapMeta sortMapKmap - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KMapMeta sortMapKmap , smt = Nothing - , hook = Nothing + , hook = Just "MAP.element" } } ) @@ -1532,14 +1638,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTLib "orInt") + , hook = Just "INT.or" } } ) @@ -1552,14 +1658,14 @@ defSymbols = , resultSort = SortApp "SortSet" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "SET.union" } } ) @@ -1572,14 +1678,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.concat" } } ) @@ -1592,14 +1698,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "+"}))) + , hook = Just "INT.add" } } ) @@ -1612,14 +1718,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "div"}))) + , hook = Just "INT.tdiv" } } ) @@ -1632,14 +1738,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "*"}))) + , hook = Just "INT.mul" } } ) @@ -1652,14 +1758,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "^"}))) + , hook = Just "INT.pow" } } ) @@ -1672,14 +1778,23 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = + Just + ( SMTHook + ( List + [ Atom (SMTId{bs = "mod"}) + , List [Atom (SMTId{bs = "^"}), Atom (SMTId{bs = "#1"}), Atom (SMTId{bs = "#2"})] + , Atom (SMTId{bs = "#3"}) + ] + ) + ) + , hook = Just "INT.powmod" } } ) @@ -1693,14 +1808,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.bytes2int" } } ) @@ -1713,14 +1828,14 @@ defSymbols = , resultSort = SortApp "SortString" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.bytes2string" } } ) @@ -1733,12 +1848,12 @@ defSymbols = , resultSort = SortApp "SortEven" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -1753,12 +1868,12 @@ defSymbols = , resultSort = SortApp "SortOdd" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -1773,54 +1888,53 @@ defSymbols = , resultSort = SortApp "SortEven" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } } ) , - ( "LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Endianness'Unds'Signedness" + ( "LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Int'Unds'Endianness" , Symbol { name = - "LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Endianness'Unds'Signedness" + "LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Int'Unds'Endianness" , sortVars = [] - , argSorts = [SortApp "SortInt" [], SortApp "SortEndianness" [], SortApp "SortSignedness" []] + , argSorts = [SortApp "SortInt" [], SortApp "SortInt" [], SortApp "SortEndianness" []] , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.int2bytes" } } ) , - ( "LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Int'Unds'Endianness" + ( "LblInt2BytesNoLen" , Symbol - { name = - "LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Int'Unds'Endianness" + { name = "LblInt2BytesNoLen" , sortVars = [] - , argSorts = [SortApp "SortInt" [], SortApp "SortInt" [], SortApp "SortEndianness" []] + , argSorts = [SortApp "SortInt" [], SortApp "SortEndianness" [], SortApp "SortSignedness" []] , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -1835,14 +1949,14 @@ defSymbols = , resultSort = SortApp "SortKItem" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "LIST.get" } } ) @@ -1855,14 +1969,34 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "LIST.range" + } + } + ) + , + ( "LblList'Coln'set" + , Symbol + { name = "LblList'Coln'set" + , sortVars = [] + , argSorts = [SortApp "SortList" [], SortApp "SortInt" [], SortApp "SortKItem" []] + , resultSort = SortApp "SortList" [] + , attributes = + SymbolAttributes + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Just "LIST.update" } } ) @@ -1875,14 +2009,34 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KListMeta sortListKList - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KListMeta sortListKList + , smt = Just (SMTLib "smt_seq_elem") + , hook = Just "LIST.element" + } + } + ) + , + ( "LblMap'Coln'choice" + , Symbol + { name = "LblMap'Coln'choice" + , sortVars = [] + , argSorts = [SortApp "SortMap" []] + , resultSort = SortApp "SortKItem" [] + , attributes = + SymbolAttributes + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.choice" } } ) @@ -1895,14 +2049,34 @@ defSymbols = , resultSort = SortApp "SortKItem" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.lookup" + } + } + ) + , + ( "LblMap'Coln'lookupOrDefault" + , Symbol + { name = "LblMap'Coln'lookupOrDefault" + , sortVars = [] + , argSorts = [SortApp "SortMap" [], SortApp "SortKItem" [], SortApp "SortKItem" []] + , resultSort = SortApp "SortKItem" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Just "MAP.lookupOrDefault" } } ) @@ -1915,12 +2089,52 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Just "MAP.update" + } + } + ) + , + ( "LblMapVal2Val'Coln'update" + , Symbol + { name = "LblMapVal2Val'Coln'update" + , sortVars = [] + , argSorts = [SortApp "SortMapValToVal" [], SortApp "SortVal" [], SortApp "SortVal" []] + , resultSort = SortApp "SortMapValToVal" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Just "MAP.update" + } + } + ) + , + ( "LblMapValToVal'Coln'primitiveUpdate" + , Symbol + { name = "LblMapValToVal'Coln'primitiveUpdate" + , sortVars = [] + , argSorts = [SortApp "SortMapValToVal" [], SortApp "SortVal" [], SortApp "SortVal" []] + , resultSort = SortApp "SortMapValToVal" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -1935,12 +2149,12 @@ defSymbols = , resultSort = SortApp "SortOdd" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -1955,17 +2169,37 @@ defSymbols = , resultSort = SortApp "SortOdd" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } } ) + , + ( "LblSet'Coln'choice" + , Symbol + { name = "LblSet'Coln'choice" + , sortVars = [] + , argSorts = [SortApp "SortSet" []] + , resultSort = SortApp "SortKItem" [] + , attributes = + SymbolAttributes + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Just "SET.choice" + } + } + ) , ( "LblSet'Coln'difference" , Symbol @@ -1975,14 +2209,14 @@ defSymbols = , resultSort = SortApp "SortSet" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "SET.difference" } } ) @@ -1995,14 +2229,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "SET.in" } } ) @@ -2015,14 +2249,14 @@ defSymbols = , resultSort = SortApp "SortSet" [] , attributes = SymbolAttributes - { collectionMetadata = Just $ KSetMeta sortSetKSet - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Just $ KSetMeta sortSetKSet , smt = Nothing - , hook = Nothing + , hook = Just "SET.element" } } ) @@ -2035,12 +2269,12 @@ defSymbols = , resultSort = SortApp "SortOdd" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2055,12 +2289,12 @@ defSymbols = , resultSort = SortApp "SortEven" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2075,14 +2309,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.string2bytes" } } ) @@ -2095,12 +2329,12 @@ defSymbols = , resultSort = SortApp "SortEven" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2115,12 +2349,12 @@ defSymbols = , resultSort = SortApp "SortOdd" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2135,12 +2369,12 @@ defSymbols = , resultSort = SortApp "SortEven" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2155,12 +2389,12 @@ defSymbols = , resultSort = SortApp "SortEven" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2175,14 +2409,24 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = + Just + ( SMTHook + ( List + [ Atom (SMTId{bs = "ite"}) + , List [Atom (SMTId{bs = "<"}), Atom (SMTId{bs = "#1"}), Atom (SMTId{bs = "0"})] + , List [Atom (SMTId{bs = "-"}), Atom (SMTId{bs = "0"}), Atom (SMTId{bs = "#1"})] + , Atom (SMTId{bs = "#1"}) + ] + ) + ) + , hook = Just "INT.abs" } } ) @@ -2195,12 +2439,12 @@ defSymbols = , resultSort = SortApp "SortEndianness" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2216,54 +2460,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing - } - } - ) - , - ( "Lblchoice'LParUndsRParUnds'MAP'Unds'KItem'Unds'Map" - , Symbol - { name = "Lblchoice'LParUndsRParUnds'MAP'Unds'KItem'Unds'Map" - , sortVars = [] - , argSorts = [SortApp "SortMap" []] - , resultSort = SortApp "SortKItem" [] - , attributes = - SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing - } - } - ) - , - ( "Lblchoice'LParUndsRParUnds'SET'Unds'KItem'Unds'Set" - , Symbol - { name = "Lblchoice'LParUndsRParUnds'SET'Unds'KItem'Unds'Set" - , sortVars = [] - , argSorts = [SortApp "SortSet" []] - , resultSort = SortApp "SortKItem" [] - , attributes = - SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "INT.bitRange" } } ) @@ -2276,12 +2480,12 @@ defSymbols = , resultSort = SortApp "SortNum" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2296,12 +2500,12 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2318,14 +2522,14 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "LIST.fill" } } ) @@ -2338,12 +2542,12 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2358,12 +2562,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedCounterCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2378,12 +2582,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedCounterCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2398,12 +2602,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedTopCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2418,12 +2622,12 @@ defSymbols = , resultSort = SortApp "SortKCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2438,14 +2642,14 @@ defSymbols = , resultSort = SortApp "SortSet" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "SET.intersection" } } ) @@ -2458,12 +2662,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2478,12 +2682,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2498,12 +2702,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2518,12 +2722,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2538,12 +2742,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2558,12 +2762,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2578,12 +2782,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2598,12 +2802,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2618,12 +2822,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2638,12 +2842,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2658,12 +2862,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2678,12 +2882,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2698,12 +2902,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2718,12 +2922,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2738,12 +2942,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2758,12 +2962,32 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Nothing + } + } + ) + , + ( "LblisMapValToVal" + , Symbol + { name = "LblisMapValToVal" + , sortVars = [] + , argSorts = [SortApp "SortK" []] + , resultSort = SortApp "SortBool" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2778,12 +3002,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2798,12 +3022,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2818,12 +3042,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2838,12 +3062,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2858,17 +3082,77 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Nothing + } + } + ) + , + ( "LblisVal" + , Symbol + { name = "LblisVal" + , sortVars = [] + , argSorts = [SortApp "SortK" []] + , resultSort = SortApp "SortBool" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Nothing + } + } + ) + , + ( "LblisWrappedInt" + , Symbol + { name = "LblisWrappedInt" + , sortVars = [] + , argSorts = [SortApp "SortK" []] + , resultSort = SortApp "SortBool" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } } ) + , + ( "Lblite" + , Symbol + { name = "Lblite" + , sortVars = ["SortSort"] + , argSorts = [SortApp "SortBool" [], SortVar "SortSort", SortVar "SortSort"] + , resultSort = SortVar "SortSort" + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "ite"}))) + , hook = Just "KEQUAL.ite" + } + } + ) , ( "Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map" , Symbol @@ -2878,14 +3162,14 @@ defSymbols = , resultSort = SortApp "SortSet" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.keys" } } ) @@ -2898,14 +3182,14 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.keys_list" } } ) @@ -2918,14 +3202,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTLib "lengthBytes") + , hook = Just "BYTES.length" } } ) @@ -2938,12 +3222,12 @@ defSymbols = , resultSort = SortApp "SortEndianness" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -2958,14 +3242,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "INT.log2" } } ) @@ -2978,14 +3262,14 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "LIST.make" } } ) @@ -2998,14 +3282,46 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = + Just + ( SMTHook + ( List + [ Atom (SMTId{bs = "ite"}) + , List [Atom (SMTId{bs = "<"}), Atom (SMTId{bs = "#1"}), Atom (SMTId{bs = "#2"})] + , Atom (SMTId{bs = "#2"}) + , Atom (SMTId{bs = "#1"}) + ] + ) + ) + , hook = Just "INT.max" + } + } + ) + , + ( "LblmemsetBytes'LParUndsCommUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Bytes'Unds'Int'Unds'Int'Unds'Int" + , Symbol + { name = + "LblmemsetBytes'LParUndsCommUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Bytes'Unds'Int'Unds'Int'Unds'Int" + , sortVars = [] + , argSorts = + [SortApp "SortBytes" [], SortApp "SortInt" [], SortApp "SortInt" [], SortApp "SortInt" []] + , resultSort = SortApp "SortBytes" [] + , attributes = + SymbolAttributes + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.memset" } } ) @@ -3018,14 +3334,24 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = + Just + ( SMTHook + ( List + [ Atom (SMTId{bs = "ite"}) + , List [Atom (SMTId{bs = "<"}), Atom (SMTId{bs = "#1"}), Atom (SMTId{bs = "#2"})] + , Atom (SMTId{bs = "#1"}) + , Atom (SMTId{bs = "#2"}) + ] + ) + ) + , hook = Just "INT.min" } } ) @@ -3038,12 +3364,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedCounterCellOpt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3058,12 +3384,12 @@ defSymbols = , resultSort = SortApp "SortKCellOpt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3078,14 +3404,14 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTHook (Atom (SMTId{bs = "not"}))) + , hook = Just "BOOL.not" } } ) @@ -3099,14 +3425,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.padLeft" } } ) @@ -3120,14 +3446,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.padRight" } } ) @@ -3140,12 +3466,12 @@ defSymbols = , resultSort = SortApp "SortNum" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3160,12 +3486,12 @@ defSymbols = , resultSort = SortApp "SortBool" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3180,12 +3506,12 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3200,12 +3526,12 @@ defSymbols = , resultSort = SortApp "SortEndianness" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3220,12 +3546,12 @@ defSymbols = , resultSort = SortApp "SortEven" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3240,12 +3566,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedCounterCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3260,12 +3586,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedCounterCellOpt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3280,12 +3606,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedTopCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3300,12 +3626,12 @@ defSymbols = , resultSort = SortApp "SortGeneratedTopCellFragment" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3320,12 +3646,12 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3340,12 +3666,12 @@ defSymbols = , resultSort = SortApp "SortK" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3360,12 +3686,12 @@ defSymbols = , resultSort = SortApp "SortKCell" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3380,12 +3706,12 @@ defSymbols = , resultSort = SortApp "SortKCellOpt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3400,12 +3726,12 @@ defSymbols = , resultSort = SortApp "SortKItem" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3420,12 +3746,12 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3440,12 +3766,32 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Nothing + } + } + ) + , + ( "Lblproject'Coln'MapValToVal" + , Symbol + { name = "Lblproject'Coln'MapValToVal" + , sortVars = [] + , argSorts = [SortApp "SortK" []] + , resultSort = SortApp "SortMapValToVal" [] + , attributes = + SymbolAttributes + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3460,12 +3806,12 @@ defSymbols = , resultSort = SortApp "SortNum" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3480,12 +3826,12 @@ defSymbols = , resultSort = SortApp "SortOdd" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3500,12 +3846,12 @@ defSymbols = , resultSort = SortApp "SortSet" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3520,12 +3866,12 @@ defSymbols = , resultSort = SortApp "SortSignedness" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3540,17 +3886,77 @@ defSymbols = , resultSort = SortApp "SortString" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Nothing + } + } + ) + , + ( "Lblproject'Coln'Val" + , Symbol + { name = "Lblproject'Coln'Val" + , sortVars = [] + , argSorts = [SortApp "SortK" []] + , resultSort = SortApp "SortVal" [] + , attributes = + SymbolAttributes + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Nothing + } + } + ) + , + ( "Lblproject'Coln'WrappedInt" + , Symbol + { name = "Lblproject'Coln'WrappedInt" + , sortVars = [] + , argSorts = [SortApp "SortK" []] + , resultSort = SortApp "SortWrappedInt" [] + , attributes = + SymbolAttributes + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } } ) + , + ( "LblpushList" + , Symbol + { name = "LblpushList" + , sortVars = [] + , argSorts = [SortApp "SortKItem" [], SortApp "SortList" []] + , resultSort = SortApp "SortList" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Just "LIST.push" + } + } + ) , ( "LblrandInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int" , Symbol @@ -3560,14 +3966,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "INT.rand" } } ) @@ -3580,14 +3986,14 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.removeAll" } } ) @@ -3601,14 +4007,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.replaceAt" } } ) @@ -3621,14 +4027,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.reverse" } } ) @@ -3642,14 +4048,14 @@ defSymbols = , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "INT.signExtendBitRange" } } ) @@ -3662,74 +4068,74 @@ defSymbols = , resultSort = SortApp "SortSignedness" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } } ) , - ( "Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List" + ( "Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set" , Symbol - { name = "Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List" + { name = "Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set" , sortVars = [] - , argSorts = [SortApp "SortList" []] + , argSorts = [SortApp "SortSet" []] , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "SET.size" } } ) , - ( "Lblsize'LParUndsRParUnds'MAP'Unds'Int'Unds'Map" + ( "LblsizeList" , Symbol - { name = "Lblsize'LParUndsRParUnds'MAP'Unds'Int'Unds'Map" + { name = "LblsizeList" , sortVars = [] - , argSorts = [SortApp "SortMap" []] + , argSorts = [SortApp "SortList" []] , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated - , smt = Nothing - , hook = Nothing + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Just (SMTLib "smt_seq_len") + , hook = Just "LIST.size" } } ) , - ( "Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set" + ( "LblsizeMap" , Symbol - { name = "Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set" + { name = "LblsizeMap" , sortVars = [] - , argSorts = [SortApp "SortSet" []] + , argSorts = [SortApp "SortMap" []] , resultSort = SortApp "SortInt" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.size" } } ) @@ -3742,14 +4148,14 @@ defSymbols = , resultSort = SortApp "SortK" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "INT.srand" } } ) @@ -3763,14 +4169,14 @@ defSymbols = , resultSort = SortApp "SortBytes" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "BYTES.substr" } } ) @@ -3783,12 +4189,32 @@ defSymbols = , resultSort = SortApp "SortSignedness" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Nothing + } + } + ) + , + ( "LblunwrapInt" + , Symbol + { name = "LblunwrapInt" + , sortVars = [] + , argSorts = [SortApp "SortWrappedInt" []] + , resultSort = SortApp "SortInt" [] + , attributes = + SymbolAttributes + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3803,14 +4229,14 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "LIST.updateAll" } } ) @@ -3823,14 +4249,14 @@ defSymbols = , resultSort = SortApp "SortMap" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing - , hook = Nothing + , hook = Just "MAP.updateAll" } } ) @@ -3843,12 +4269,32 @@ defSymbols = , resultSort = SortApp "SortList" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Partial - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Partial + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing + , smt = Nothing + , hook = Just "MAP.values" + } + } + ) + , + ( "LblwrapInt" + , Symbol + { name = "LblwrapInt" + , sortVars = [] + , argSorts = [SortApp "SortInt" []] + , resultSort = SortApp "SortWrappedInt" [] + , attributes = + SymbolAttributes + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3863,12 +4309,12 @@ defSymbols = , resultSort = SortApp "SortK" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Function Total - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Function Total + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3883,12 +4329,12 @@ defSymbols = , resultSort = SortApp "SortK" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3903,12 +4349,12 @@ defSymbols = , resultSort = SortVar "To" , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } @@ -3923,31 +4369,15 @@ defSymbols = , resultSort = SortApp "SortK" [] , attributes = SymbolAttributes - { collectionMetadata = Nothing - , symbolType = Constructor - , isIdem = IsNotIdem - , isAssoc = IsNotAssoc - , isMacroOrAlias = IsNotMacroOrAlias - , hasEvaluators = CanBeEvaluated + { symbolType = Constructor + , isIdem = Flag False + , isAssoc = Flag False + , isMacroOrAlias = Flag False + , hasEvaluators = Flag True + , collectionMetadata = Nothing , smt = Nothing , hook = Nothing } } ) - , - ( "LblwrapInt" - , [symb| symbol LblwrapInt{}(SortInt{}) : SortWrappedInt{} [constructor{}(), functional{}(), injective{}()] |] - ) - , - ( "Lbl'Stop'MapValToVal" - , [symb| symbol Lbl'Stop'MapValToVal{}() : SortMapValToVal{} [function{}(), functional{}(), total{}()] |] - ) - , - ( "LblMapValToVal'Coln'primitiveUpdate" - , [symb| symbol LblMapValToVal'Coln'primitiveUpdate{}(SortMapValToVal{}, SortVal{}, SortVal{}) : SortMapValToVal{} [function{}(), functional{}(), klabel{}("MapValToVal:primitiveUpdate"), total{}()] |] - ) - , - ( "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'" - , [symb| symbol Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'{}(SortVal{}, SortVal{}) : SortMapValToVal{} [function{}(), functional{}(), klabel{}("_Val2Val|->_"), total{}()] |] - ) ] diff --git a/booster/test/llvm-integration/definition/llvm.k b/booster/test/llvm-integration/definition/llvm.k index 5aabc1be36..88da57d8a6 100644 --- a/booster/test/llvm-integration/definition/llvm.k +++ b/booster/test/llvm-integration/definition/llvm.k @@ -49,23 +49,22 @@ module MAP-VAL-TO-VAL syntax MapValToVal [hook(MAP.Map)] syntax MapValToVal ::= MapValToVal MapValToVal - [ left, function, hook(MAP.concat), klabel(_MapValToVal_), - symbol, assoc, comm, unit(.MapValToVal), element(_Val2Val|->_) + [ left, function, hook(MAP.concat), symbol(_MapValToVal_), + assoc, comm, unit(.MapValToVal), element(_Val2Val|->_) ] syntax MapValToVal ::= ".MapValToVal" - [function, total, hook(MAP.unit),klabel(.MapValToVal), symbol] + [function, total, hook(MAP.unit),symbol(.MapValToVal)] syntax MapValToVal ::= Val "Val2Val|->" Val - [function, total, hook(MAP.element), klabel(_Val2Val|->_), symbol] + [function, total, hook(MAP.element), symbol(_Val2Val|->_)] - syntax MapValToVal ::= MapValToVal "[" key: Val "<-" value: Val "]" [function, total, klabel(MapVal2Val:update), symbol, hook(MAP.update), prefer] + syntax MapValToVal ::= MapValToVal "[" key: Val "<-" value: Val "]" + [function, total, symbol(MapVal2Val:update), hook(MAP.update), prefer] syntax priority _Val2Val|->_ > _MapValToVal_ .MapValToVal syntax non-assoc _Val2Val|->_ syntax MapValToVal ::= MapValToVal "{{" key: Val "<-" value: Val "}}" - [ function, total, klabel(MapValToVal:primitiveUpdate), symbol, - prefer - ] + [ function, total, symbol(MapValToVal:primitiveUpdate), prefer] rule M:MapValToVal {{ Key:Val <- Value:Val }} => M[Key <- Value] @@ -74,10 +73,11 @@ endmodule module WRAPPED-INT imports INT - syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)] + syntax WrappedInt ::= wrap(Int) [symbol(wrapInt)] // ------------------------------------------------------- - syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)] + syntax Int ::= unwrap(WrappedInt) + [function, total, injective, symbol(unwrapInt)] // --------------------------------------------------------------------------------------- rule unwrap(wrap(A:Int)) => A endmodule