Skip to content
This repository has been archived by the owner on Jun 11, 2021. It is now read-only.

Commit

Permalink
Adapt to changes in saw-core for Constant terms.
Browse files Browse the repository at this point in the history
  • Loading branch information
Brian Huffman committed Oct 18, 2019
1 parent 75b3bb2 commit 47655bd
Showing 1 changed file with 3 additions and 4 deletions.
7 changes: 3 additions & 4 deletions src/Verifier/SAW/Simulator/SBV.hs
Original file line number Diff line number Diff line change
Expand Up @@ -533,12 +533,11 @@ muxSbvExtra c x y =
sbvSolveBasic :: ModuleMap -> Map Ident SValue -> [String] -> Term -> IO SValue
sbvSolveBasic m addlPrims unints t = do
let unintSet = Set.fromList unints
let uninterpreted nm ty
let uninterpreted (EC _ nm ty)
| Set.member nm unintSet = Just $ parseUninterpreted [] nm ty
| otherwise = Nothing
cfg <- Sim.evalGlobal m (Map.union constMap addlPrims)
(\ix nm -> parseUninterpreted [] (nm ++ "#" ++ show ix))
uninterpreted
let extcns (EC ix nm ty) = parseUninterpreted [] (nm ++ "#" ++ show ix) ty
cfg <- Sim.evalGlobal m (Map.union constMap addlPrims) extcns uninterpreted
Sim.evalSharedTerm cfg t

parseUninterpreted :: [SVal] -> String -> SValue -> IO SValue
Expand Down

0 comments on commit 47655bd

Please sign in to comment.