Skip to content

Commit

Permalink
WIP conditional elaboration of theories for cvc5
Browse files Browse the repository at this point in the history
  • Loading branch information
@clayrat
clayrat committed Jan 22, 2025
1 parent c78fa3d commit 39da2a4
Show file tree
Hide file tree
Showing 21 changed files with 563 additions and 475 deletions.
20 changes: 12 additions & 8 deletions src/Language/Fixpoint/Smt/Interface.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,7 @@ checkValids cfg f xts ps
{-# SCC command #-}
command :: Context -> Command -> IO Response
--------------------------------------------------------------------------------
command Ctx {..} !cmd = do
command Ctx{..} !cmd = do
-- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
-- LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
forM_ ctxLog $ \h -> do
Expand All @@ -173,7 +173,9 @@ command Ctx {..} !cmd = do
TE.decodeUtf8With (const $ const $ Just ' ') $
LBS.toStrict resp
parse respTxt
cmdBS = {-# SCC "Command-runSmt2" #-} runSmt2 ctxSymEnv cmd
cmdBS = {-# SCC "Command-runSmt2" #-}
{-let cmd' = tracepp "command" cmd in-}
runSmt2 ctxSymEnv cmd -- '
parse resp = do
case A.parseOnly responseP resp of
Left e -> Misc.errorstar $ "SMTREAD:" ++ e
Expand Down Expand Up @@ -256,7 +258,7 @@ makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context
makeContextWithSEnv cfg f env = do
ctx <- makeContext cfg f
let ctx' = ctx {ctxSymEnv = env}
declare ctx'
declare (solver cfg) ctx'
return ctx'
-- where msg = "makeContextWithSEnv" ++ show env

Expand Down Expand Up @@ -400,7 +402,9 @@ smtCheckSat me p
ans _ = False

smtAssert :: Context -> Expr -> IO ()
smtAssert me p = interact' me (Assert Nothing p)
smtAssert me p =
{- let p' = tracepp "smtAssert" p in -}
interact' me (Assert Nothing p {-p'-})

smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO ()
smtDefineFunc me name symList rsort e =
Expand Down Expand Up @@ -462,9 +466,9 @@ z3_options


--------------------------------------------------------------------------------
declare :: Context -> IO ()
declare :: SMTSolver -> Context -> IO ()
--------------------------------------------------------------------------------
declare me = do
declare slv me = do
forM_ dss $ smtDataDecl me
forM_ thyXTs $ uncurry $ smtDecl me
forM_ qryXTs $ uncurry $ smtDecl me
Expand All @@ -481,7 +485,7 @@ declare me = do
qryXTs = fmap tx <$> filter (isKind 2) xts
isKind n = (n ==) . symKind env . fst
xts = {- tracepp "symbolSorts" $ -} symbolSorts (F.seSort env)
tx = elaborate "declare" env
tx = elaborate slv "declare" env
ats = funcSortVars env

symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]
Expand All @@ -500,7 +504,7 @@ funcSortVars env = [(var applyName t , appSort t) | t <- ts]
++ [(var (lamArgSymbol i) t , argSort t) | t@(_,F.SInt) <- ts, i <- [1..Thy.maxLamArg] ]
where
var n = F.symbolAtSmtName n env ()
ts = M.keys (F.seAppls env)
ts = {- tracepp "funcSortVars" $ -} M.keys (F.seAppls env)
appSort (s,t) = ([F.SInt, s], t)
lamSort (s,t) = ([s, t], F.SInt)
argSort (s,_) = ([] , s)
Expand Down
21 changes: 14 additions & 7 deletions src/Language/Fixpoint/Smt/Serialize.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,15 +147,15 @@ instance SMTLIB2 Expr where
smt2 env (PAnd ps) = parenSeqs ["and", smt2s env ps]
smt2 _ (POr []) = "false"
smt2 env (POr ps) = parenSeqs ["or", smt2s env ps]
smt2 env (PNot p) = parenSeqs ["not", smt2 env p]
smt2 env (PNot p) = parenSeqs ["not", smt2 env p]
smt2 env (PImp p q) = parenSeqs ["=>", smt2 env p, smt2 env q]
smt2 env (PIff p q) = parenSeqs ["=", smt2 env p, smt2 env q]
smt2 env (PExist [] p) = smt2 env p
smt2 env (PExist xs p) = parenSeqs ["exists", parens (smt2s env xs), smt2 env p]
smt2 env (PAll [] p) = smt2 env p
smt2 env (PAll xs p) = parenSeqs ["forall", parens (smt2s env xs), smt2 env p]
smt2 env (PAtom r e1 e2) = mkRel env r e1 e2
smt2 env (ELam b e) = smt2Lam env b e
smt2 env (ELam b e) = smt2Lam env b e
smt2 env (ECoerc t1 t2 e) = smt2Coerc env t1 t2 e
smt2 _ e = panic ("smtlib2 Pred " ++ show e)

Expand All @@ -176,24 +176,29 @@ smt2Var env x t
| otherwise = smt2 env x

smtLamArg :: SymEnv -> Symbol -> Sort -> Builder
smtLamArg env x t = Builder.fromText $ symbolAtName x env () (FFunc t FInt)
smtLamArg env x t =
{-let t' = tracepp "smtLamArg" t in-}
Builder.fromText $ symbolAtName x env () (FFunc t {-t'-} FInt)

smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder
smt2VarAs env x t = parenSeqs ["as", smt2 env x, smt2SortMono x env t]

smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder
smt2Lam env (x, xT) full@(ECst _ eT) = parenSeqs [Builder.fromText lambda, x', smt2 env full]
where
x' = smtLamArg env x xT
lambda = symbolAtName lambdaName env () (FFunc xT eT)
x' = smtLamArg env x xT
lambda =
{- let eT' = tracepp "smt2Lam" eT in -}
symbolAtName lambdaName env () (FFunc xT eT {-eT'-})

smt2Lam _ _ e
= panic ("smtlib2: Cannot serialize unsorted lambda: " ++ showpp e)

smt2App :: SymEnv -> Expr -> Builder
smt2App env e@(EApp (EApp f e1) e2)
| Just t <- unApplyAt f
= parenSeqs [Builder.fromText (symbolAtName applyName env e t), smt2s env [e1, e2]]
= {- let t' = tracepp "smt2App" t in -}
parenSeqs [Builder.fromText (symbolAtName applyName env e t {-t'-}), smt2s env [e1, e2]]
smt2App env e
| Just b <- Thy.smt2App smt2VarAs env f (smt2 env <$> es)
= b
Expand All @@ -207,7 +212,9 @@ smt2Coerc env t1 t2 e
| t1 == t2 = smt2 env e
| otherwise = parenSeqs [Builder.fromText coerceFn , smt2 env e]
where
coerceFn = symbolAtName coerceName env (ECoerc t1 t2 e) t
coerceFn =
{- let t' = tracepp "smt2Coerc" t in -}
symbolAtName coerceName env (ECoerc t1 t2 e) t {-t'-}
t = FFunc t1 t2

splitEApp' :: Expr -> (Expr, [Expr])
Expand Down
89 changes: 50 additions & 39 deletions src/Language/Fixpoint/Smt/Theories.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,12 @@ bvSLeName = "bvsle"
bvSGtName = "bvsgt"
bvSGeName = "bvsge"

setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a -- Symbol
mapDef, mapSel, mapSto :: (IsString a) => a
mapDef = "Map_default"
mapSel = "Map_select"
mapSto = "Map_store"

setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a
setEmpty = "Set_empty"
setEmp = "Set_emp"
setCap = "Set_cap"
Expand All @@ -145,11 +150,6 @@ setCup = "Set_cup"
setDif = "Set_dif"
setSng = "Set_sng"

mapDef, mapSel, mapSto :: (IsString a) => a
mapDef = "Map_default"
mapSel = "Map_select"
mapSto = "Map_store"

bagEmpty, bagSng, bagCount, bagSub, bagCup, bagMax, bagMin :: (IsString a) => a
bagEmpty = "Bag_empty"
bagSng = "Bag_sng"
Expand All @@ -165,7 +165,13 @@ bagMin = "Bag_inter_min"
-- taking either the greatest (bagMax) or the least (bagMin) of them.
-- bagMax, bagMin : Map v Int -> Map v Int -> Map v Int

--- Array operations for sets
--- Array operations for polymorphic maps
arrConstM, arrStoreM, arrSelectM :: Symbol
arrConstM = "arr_const_m"
arrStoreM = "arr_store_m"
arrSelectM = "arr_select_m"

--- Array operations for sets (Z3)
arrConstS, arrStoreS, arrSelectS, arrMapNotS, arrMapOrS, arrMapAndS, arrMapImpS :: Symbol
arrConstS = "arr_const_s"
arrStoreS = "arr_store_s"
Expand All @@ -176,13 +182,7 @@ arrMapOrS = "arr_map_or"
arrMapAndS = "arr_map_and"
arrMapImpS = "arr_map_imp"

--- Array operations for polymorphic maps
arrConstM, arrStoreM, arrSelectM :: Symbol
arrConstM = "arr_const_m"
arrStoreM = "arr_store_m"
arrSelectM = "arr_select_m"

--- Array operations for bags
--- Array operations for bags (Z3)
arrConstB, arrStoreB, arrSelectB :: Symbol
arrConstB = "arr_const_b"
arrStoreB = "arr_store_b"
Expand Down Expand Up @@ -300,8 +300,8 @@ smt2SmtSort SInt = "Int"
smt2SmtSort SReal = "Real"
smt2SmtSort SBool = "Bool"
smt2SmtSort SString = fromText string
--smt2SmtSort SSet = fromText set
--smt2SmtSort SMap = fromText map
smt2SmtSort (SSet a) = key "Set" (smt2SmtSort a)
smt2SmtSort (SBag a) = key "Bag" (smt2SmtSort a)
smt2SmtSort (SArray a b) = key2 "Array" (smt2SmtSort a) (smt2SmtSort b)
smt2SmtSort (SBitVec n) = key "_ BitVec" (bShow n)
smt2SmtSort (SVar n) = "T" <> bShow n
Expand All @@ -321,6 +321,8 @@ smt2App _ env ex@(dropECst -> EVar f) [d]
| f == arrConstS = Just (key (key "as const" (getTarget ex)) d)
| f == arrConstB = Just (key (key "as const" (getTarget ex)) d)
| f == arrConstM = Just (key (key "as const" (getTarget ex)) d)
| f == setEmpty = Just (key "as set.empty" (getTarget ex))
| f == bagEmpty = Just (key "as bag.empty" (getTarget ex))
where
getTarget :: Expr -> Builder
-- const is a function, but SMT expects only the output sort
Expand Down Expand Up @@ -386,8 +388,15 @@ interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
interpSymbols cfg =
[
-- TODO we'll probably need two versions of these - one for sets and one for maps
interpSym arrConstS "const" (FAbs 0 $ FFunc boolSort setArrSort)
-- maps

interpSym arrConstM "const" (FAbs 0 $ FFunc (FVar 1) mapArrSort)
, interpSym arrSelectM "select" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) (FVar 1))
, interpSym arrStoreM "store" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) $ FFunc (FVar 1) mapArrSort)

-- Z3 sets (arrays of bools)

, interpSym arrConstS "const" (FAbs 0 $ FFunc boolSort setArrSort)
, interpSym arrSelectS "select" (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) boolSort)
, interpSym arrStoreS "store" (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) $ FFunc boolSort setArrSort)

Expand All @@ -396,9 +405,7 @@ interpSymbols cfg =
, interpSym arrMapAndS "(_ map and)" (FFunc setArrSort $ FFunc setArrSort setArrSort)
, interpSym arrMapImpS "(_ map =>)" (FFunc setArrSort $ FFunc setArrSort setArrSort)

, interpSym arrConstM "const" (FAbs 0 $ FFunc (FVar 1) mapArrSort)
, interpSym arrSelectM "select" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) (FVar 1))
, interpSym arrStoreM "store" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) $ FFunc (FVar 1) mapArrSort)
-- Z3 bags (arrays of ints)

, interpSym arrConstB "const" (FAbs 0 $ FFunc intSort bagArrSort)
, interpSym arrSelectB "select" (FAbs 0 $ FFunc bagArrSort $ FFunc (FVar 0) intSort)
Expand All @@ -409,28 +416,32 @@ interpSymbols cfg =
, interpSym arrMapGtB "(_ map (> (Int Int) Bool))" (FFunc bagArrSort $ FFunc bagArrSort setArrSort)
, interpSym arrMapIteB "(_ map (ite (Bool Int Int) Int))" (FFunc setArrSort $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)

, interpSym setEmp setEmp (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)
, interpSym setEmpty setEmpty (FAbs 0 $ FFunc intSort (setSort $ FVar 0))
, interpSym setSng setSng (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0))
, interpSym setAdd setAdd setAddSort
, interpSym setCup setCup setBopSort
, interpSym setCap setCap setBopSort
, interpSym setMem setMem setMemSort
, interpSym setDif setDif setBopSort
, interpSym setSub setSub setCmpSort
, interpSym setCom setCom setCmpSort

, interpSym mapDef mapDef mapDefSort
, interpSym mapSel mapSel mapSelSort
, interpSym mapSto mapSto mapStoSort

, interpSym bagEmpty bagEmpty (FAbs 0 $ FFunc intSort (bagSort $ FVar 0))
, interpSym bagSng bagSng (FAbs 0 $ FFunc (FVar 0) $ FFunc intSort (bagSort $ FVar 0))
, interpSym bagCount bagCount bagCountSort
, interpSym bagCup bagCup bagBopSort
, interpSym bagMax bagMax bagBopSort
, interpSym bagMin bagMin bagBopSort
, interpSym bagSub bagSub bagSubSort
-- CVC5 sets

, interpSym setEmp "set.is_empty" (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)
, interpSym setEmpty "set.empty" (FAbs 0 $ FFunc intSort (setSort $ FVar 0))
, interpSym setSng "set.singleton" (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0))
, interpSym setAdd "set.insert" setAddSort -- TODO broken! the order is flipped
, interpSym setCup "set.union" setBopSort
, interpSym setCap "set.inter" setBopSort
, interpSym setMem "set.member" setMemSort
, interpSym setDif "set.minus" setBopSort
, interpSym setSub "set.subset" setCmpSort
, interpSym setCom "set.complement" (FAbs 0 $ FFunc (setSort $ FVar 0) (setSort $ FVar 0))

-- CVC5 bags

, interpSym bagEmpty "bag.empty" (FAbs 0 $ FFunc intSort (bagSort $ FVar 0))
, interpSym bagSng "bag" (FAbs 0 $ FFunc (FVar 0) $ FFunc intSort (bagSort $ FVar 0))
, interpSym bagCount "bag.count" bagCountSort -- TODO broken! the order is flipped
, interpSym bagCup "bag.union_disjoint" bagBopSort
, interpSym bagMax "bag.union_max" bagBopSort
, interpSym bagMin "bag.inter_min" bagBopSort
, interpSym bagSub "bag.subbag" bagSubSort

-- , interpSym bvOrName "bvor" bvBopSort
-- , interpSym bvAndName "bvand" bvBopSort
Expand Down
2 changes: 1 addition & 1 deletion src/Language/Fixpoint/Solver.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ simplifyFInfo !cfg !fi0 = do
-- writeLoud $ "fq file after defunc: \n" ++ render (toFixpoint cfg si4)
-- putStrLn $ "AXIOMS: " ++ showpp (asserts si4)
loudDump 2 cfg si4
let si5 = {- SCC "elaborate" -} elaborate (atLoc dummySpan "solver") (symbolEnv cfg si4) si4
let si5 = {- SCC "elaborate" -} elaborate (solver cfg) (atLoc dummySpan "solver") (symbolEnv cfg si4) si4
-- writeLoud $ "fq file after elaborate: \n" ++ render (toFixpoint cfg si5)
loudDump 3 cfg si5
let si6 = if extensionality cfg then {- SCC "expand" -} expand cfg si5 else si5
Expand Down
4 changes: 2 additions & 2 deletions src/Language/Fixpoint/Solver/Common.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

module Language.Fixpoint.Solver.Common (askSMT, toSMT) where

import Language.Fixpoint.Types.Config (Config)
import Language.Fixpoint.Types.Config (Config, solver)
import Language.Fixpoint.Smt.Interface (Context(..), checkValidWithContext)
import Language.Fixpoint.Types
import Language.Fixpoint.Types.Visitor (kvarsExpr)
Expand All @@ -24,7 +24,7 @@ askSMT cfg ctx xs e
toSMT :: String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Pred
toSMT msg cfg ctx xs e =
defuncAny cfg symenv .
elaborate (dummyLoc msg) (elabEnv xs) .
elaborate (solver cfg) (dummyLoc msg) (elabEnv xs) .
mytracepp ("toSMT from " ++ msg ++ showpp e) $
e
where
Expand Down
Loading

0 comments on commit 39da2a4

Please sign in to comment.