simplify theorySymbols export

ucsd-progsys · Dec 19, 2024 · 5948817 · 5948817
1 parent 46a8b24
commit 5948817
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 11 deletions.
diff --git a/src/Language/Fixpoint/Horn/Transformations.hs b/src/Language/Fixpoint/Horn/Transformations.hs
@@ -647,7 +647,7 @@ rewriteWithEqualities cfg measures n args equalities = preds
       Nothing -> []
       Just vertex -> nub $ filter (/= F.EVar x) $ mconcat [es | ((_, es), _, _) <- vf <$> DG.reachable eGraph vertex]
 
-    argsAndPrims = args `S.union` S.fromList (map fst $ F.toListSEnv $ F.theorySymbols cfg []) `S.union`measures
+    argsAndPrims = args `S.union` S.fromList (map fst $ F.toListSEnv $ F.theorySymbols (F.solver cfg) []) `S.union`measures
 
     isWellFormed :: F.Expr -> Bool
     isWellFormed e = S.fromList (F.syms e) `S.isSubsetOf` argsAndPrims

diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
@@ -375,14 +375,14 @@ sortAppInfo t = case bkFFunc t of
 
 -- | `theorySymbols` contains the list of ALL SMT symbols with interpretations,
 --   i.e. which are given via `define-fun` (as opposed to `declare-fun`)
-theorySymbols :: Config -> [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol
+theorySymbols :: SMTSolver -> [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol
 theorySymbols cfg ds = fromListSEnv $  -- SHIFTLAM uninterpSymbols
                                   interpSymbols cfg
                                ++ concatMap dataDeclSymbols ds
 
 
 --------------------------------------------------------------------------------
-interpSymbols :: Config -> [(Symbol, TheorySymbol)]
+interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)]
 --------------------------------------------------------------------------------
 interpSymbols cfg =
   [
@@ -526,11 +526,10 @@ interpSymbols cfg =
                                          (bagSort $ FVar 0)
     bagSubSort = FAbs 0 $ FFunc (bagSort $ FVar 0) $ FFunc (bagSort $ FVar 0) boolSort
 
-bv2i :: Config -> Int -> Raw
-bv2i cfg size = case solver cfg of
-  Cvc4 -> "bv2nat"
-  Cvc5 -> "bv2nat"
-  _    -> Data.Text.pack $ printf "(_ bv2int %d)" size
+bv2i :: SMTSolver -> Int -> Raw
+bv2i Cvc4 _ = "bv2nat"
+bv2i Cvc5 _ = "bv2nat"
+bv2i _    n = Data.Text.pack $ printf "(_ bv2int %d)" n
 
 interpBvUop :: Symbol -> (Symbol, TheorySymbol)
 interpBvUop name = interpSym' name bvUopSort

diff --git a/src/Language/Fixpoint/Solver/Sanitize.hs b/src/Language/Fixpoint/Solver/Sanitize.hs
@@ -164,7 +164,7 @@ eliminateEta cfg si
       splitApp (fvar, arg:args)
     fapp' e = pure (e, [])
 
-    theorySymbols = F.notracepp "theorySymbols" $ Thy.theorySymbols cfg $ F.ddecls si
+    theorySymbols = F.notracepp "theorySymbols" $ Thy.theorySymbols (Cfg.solver cfg) $ F.ddecls si
 
     splitApp (e, es)
       | isNothing $ F.notracepp ("isSmt2App? " ++ showpp e) $ Thy.isSmt2App theorySymbols $ stripCasts e
@@ -329,7 +329,7 @@ known :: Config -> F.SInfo a -> F.Symbol -> Bool
 known cfg fi  = \x -> F.memberSEnv x lits || F.memberSEnv x prims
   where
     lits  = F.gLits fi
-    prims = Thy.theorySymbols cfg . F.ddecls $ fi
+    prims = Thy.theorySymbols (Cfg.solver cfg) . F.ddecls $ fi
 
 cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol]
 cNoFreeVars fi knownSym c = if S.null fv then Nothing else Just (S.toList fv)
@@ -404,7 +404,7 @@ symbolEnv cfg si = F.symEnv sEnv tEnv ds lits (ts ++ ts')
     ts'          = applySorts ae'
     ae'          = elaborate (F.atLoc E.dummySpan "symbolEnv") env0 (F.ae si)
     env0         = F.symEnv sEnv tEnv ds lits ts
-    tEnv         = Thy.theorySymbols cfg ds
+    tEnv         = Thy.theorySymbols (Cfg.solver cfg) ds
     ds           = F.ddecls si
     ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])
     sEnv         = F.coerceSortEnv $ (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts