g2-0.2.0.0: src/G2/Liquid/Inference/Sygus/LiaSynth.hs
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
module G2.Liquid.Inference.Sygus.LiaSynth ( SynthRes (..)
, Size
, ModelNames (..)
, Iteration (..)
, liaSynth
, MaxSize
, incrMaxSize
, BlockedModels
, emptyBlockedModels
, insertBlockedModel
, blockedHashMap
, unionBlockedModels) where
import G2.Data.Utils
import G2.Language as G2
import qualified G2.Language.ExprEnv as E
import G2.Liquid.Interface
import G2.Liquid.Types
import G2.Liquid.Inference.Config
import G2.Liquid.Inference.FuncConstraint
import G2.Liquid.Inference.G2Calls
import G2.Liquid.Inference.GeneratedSpecs
import G2.Liquid.Inference.PolyRef
import G2.Liquid.Inference.UnionPoly
import G2.Liquid.Inference.Sygus.FCConverter
import G2.Liquid.Inference.Sygus.SpecInfo
import G2.Solver as Solver
import Control.Monad.IO.Class
import Language.Haskell.Liquid.Types as LH hiding (SP, ms, isBool, diff, fresh)
import Language.Fixpoint.Types.Refinements as LH hiding (pAnd, pOr)
import qualified Language.Fixpoint.Types as LH
import qualified Language.Fixpoint.Types as LHF
import qualified Data.HashMap.Lazy as HM
import qualified Data.HashSet as HS
import qualified Data.List as L
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Text as T
import qualified Text.Builder as TB
import qualified Data.Text.IO as T
data SynthRes = SynthEnv
GeneratedSpecs -- ^ The synthesized specifications
Size -- ^ The size that the synthesizer succeeded at
SMTModel -- ^ An SMTModel corresponding to the new specifications
BlockedModels -- ^ SMTModels that should be blocked in the future
| SynthFail FuncConstraints
type Size = Integer
data Iteration = FirstRound | AfterFirstRound
liaSynth :: (InfConfigM m, ProgresserM m, MonadIO m, SMTConverter con)
=> con -> Iteration -> [GhcInfo] -> LiquidReadyState -> Evals Bool -> MeasureExs
-> FuncConstraints
-> UnionedTypes
-> BlockedModels -- ^ SMT Models to block being returned by the synthesizer at various sizes
-> ToBeNames -> ToSynthNames -> m SynthRes
liaSynth con iter ghci lrs evals meas_ex fc ut blk_mdls to_be_ns ns_synth = do
-- Figure out the type of each of the functions we need to synthesize
let eenv = buildNMExprEnv $ expr_env . state $ lr_state lrs
tenv = type_env . state $ lr_state lrs
tc = type_classes . state $ lr_state lrs
meas = lrsMeasures ghci lrs
si <- buildSpecInfo eenv tenv tc meas ghci fc ut to_be_ns ns_synth
liftIO . putStrLn $ "si = " ++ show si
MaxSize max_sz <- maxSynthFormSizeM
synth con iter ghci eenv tenv meas meas_ex evals si fc blk_mdls max_sz
liaSynthOfSize :: (InfConfigM m, ProgresserM m) => Integer -> M.Map Name SpecInfo -> m (M.Map Name SpecInfo)
liaSynthOfSize sz m_si = do
inf_c <- infConfigM
MaxSize max_form_sz <- maxSynthFormSizeM
MaxSize max_coeff_sz <- maxSynthCoeffSizeM
let m_si' =
M.map (\si ->
let
s_syn_pre' =
map (mapPB
(\psi ->
psi { sy_coeffs = mkCNF (>= 1) sz (fromInteger max_form_sz) (sy_name psi) psi }
)
) (s_syn_pre si)
s_syn_post' =
mapPB (\psi ->
psi { sy_coeffs = mkCNF (>= 1) sz (fromInteger max_form_sz) (sy_name psi) psi }
) (s_syn_post si)
in
si { s_syn_pre = s_syn_pre' -- (s_syn_pre si) { sy_coeffs = pre_c }
, s_syn_post = s_syn_post' -- (s_syn_post si) { sy_coeffs = post_c }
, s_max_coeff = if restrict_coeffs inf_c then 1 else max_coeff_sz }) m_si
return m_si'
where
mkCNF :: (Int -> Bool) -> Integer -> Int -> String -> SynthSpec -> CNF
mkCNF prd sz ms s psi_ =
(if length (set_sy_args psi_) + length (set_sy_rets psi_) == 0
then
[
(
s ++ "_c_coeff_act_" ++ show j
,
[ mkCoeffs prd s psi_ j k | k <- [1..sz] ] -- Ors
)
| j <- [1..sz] ] -- Ands
else [])
++
(if length (set_sy_args psi_) + length (set_sy_rets psi_) > 0
then
[
(
s ++ "_c_set_act_" ++ show j
,
[ mkSetForms prd ms s psi_ j k | k <- [1..sz] ] -- Ors
)
| j <- [1..sz] ] -- Ands
else [])
++
(if length (bool_sy_args psi_) + length (bool_sy_rets psi_) > 0
then
[
(
s ++ "_c_bool_act_" ++ show j
,
[ mkBoolForms prd sz ms s psi_ j k | k <- [1..sz] ] -- Ors
)
| j <- [1..sz] ] -- Ands
else [])
mkCoeffs :: (Int -> Bool) -> String -> SynthSpec -> Integer -> Integer -> Forms
mkCoeffs prd s psi j k =
let
ars = length (int_sy_args psi)
rets = length (int_sy_rets psi)
in
LIA
{
c_active = s ++ "_f_act_" ++ show j ++ "_t_" ++ show k
, c_op_branch1 = s ++ "_lia_op1_" ++ show j ++ "_t_" ++ show k
, c_op_branch2 = s ++ "_lia_op2_" ++ show j ++ "_t_" ++ show k
, b0 = s ++ "_b_" ++ show j ++ "_t_" ++ show k
-- We only want solutions that have one or more return values with a
-- non-zero coefficient. Thus, if we have no return values, we
-- don't need to consider any arguments
, ars_coeffs =
if prd rets
then
[ s ++ "_a_c_" ++ show j ++ "_t_" ++ show k ++ "_a_" ++ show a
| a <- [1..ars]]
else
[]
, rets_coeffs =
[ s ++ "_r_c_" ++ show j ++ "_t_" ++ show k ++ "_a_" ++ show a
| a <- [1..rets]]
}
mkSetForms :: (Int -> Bool) -> Int -> String -> SynthSpec -> Integer -> Integer -> Forms
mkSetForms prd max_sz s psi j k =
let
int_ars = length (int_sy_args psi)
int_rets = length (int_sy_rets psi)
ars = length (set_sy_args psi)
rets = length (set_sy_rets psi)
max_sets = min (ars + rets + int_ars + int_rets) 2 -- + max_sz - 1
in
Set
{
c_active = s ++ "_s_act_" ++ show j ++ "_t_" ++ show k
, c_op_branch1 = s ++ "_set_op1_" ++ show j ++ "_t_" ++ show k
, c_op_branch2 = s ++ "_set_op2_" ++ show j ++ "_t_" ++ show k
, int_sing_set_bools_lhs =
if prd rets
then
[
[ s ++ "_a_set_sing_lhs_" ++ show j ++ "_t_" ++ show k
++ "_a_" ++ show a ++ "_int_" ++ show inter | inter <- [1..int_ars + int_rets]]
| a <- [1..max_sets]]
else
[]
, int_sing_set_bools_rhs =
if prd rets
then
[]
{- [
[ s ++ "_a_set_sing_rhs_" ++ show j ++ "_t_" ++ show k
++ "_a_" ++ show a ++ "_int_" ++ show inter | inter <- [1..int_ars + int_rets]]
| a <- [1..ars + rets + max_sz - 1]] -}
else
[]
, ars_bools_lhs =
if prd rets
then
[
[ s ++ "_a_set_lhs_" ++ show j ++ "_t_" ++ show k
++ "_a_" ++ show a ++ "_int_" ++ show inter | inter <- [1..ars]]
| a <- [1..max_sets]]
else
[]
, rets_bools_lhs =
[ [ s ++ "_r_set_lhs_" ++ show j ++ "_t_" ++ show k
++ "_a_" ++ show a ++ "_int_" ++ show inter | inter <- [1..rets]]
| a <- [1..ars + rets + max_sz - 1]]
, ars_bools_rhs =
if prd rets
then
[ [ s ++ "_a_set_rhs_" ++ show j ++ "_t_" ++ show k
++ "_a_" ++ show a ++ "_int_" ++ show inter | inter <- [1..ars]]
| a <- [1..max_sets]]
else
[]
, rets_bools_rhs =
[[ s ++ "_r_set_rhs_" ++ show j ++ "_t_" ++ show k
++ "_a_" ++ show a ++ "_int_" ++ show inter | inter <- [1..rets]]
| a <- [1..max_sets]]
}
mkBoolForms :: (Int -> Bool) -> Integer -> Int -> String -> SynthSpec -> Integer -> Integer -> Forms
mkBoolForms prd sz max_sz s psi j k =
let
ars = length (bool_sy_args psi)
rets = length (bool_sy_rets psi)
in
BoolForm
{
c_active = s ++ "_bool_act_" ++ show j ++ "_t_" ++ show k
, c_op_branch1 = s ++ "_bool_op1_" ++ show j ++ "_t_" ++ show k
, c_op_branch2 = s ++ "_bool_op2_" ++ show j ++ "_t_" ++ show k
, ars_bools =
if prd rets
then
[ s ++ "_a_bool_" ++ show j ++ "_t_" ++ show k ++ "_a_" ++ show a
| a <- [1..ars]]
else
[]
, rets_bools =
[ s ++ "_r_bool_" ++ show j ++ "_t_" ++ show k ++ "_a_" ++ show a
| a <- [1..rets]]
, forms = concat
. map snd
$ mkCNF (const True) sz max_sz (s ++ "_bool_" ++ show j ++ "_t_" ++ show k ++ "_" )
(psi { sy_args = filter (not . isBool . smt_sort) (sy_args psi)
, sy_rets = filter (not . isBool . smt_sort) (sy_rets psi) })
}
where
isBool SortBool = True
isBool _ = False
synth :: (InfConfigM m, ProgresserM m, MonadIO m, SMTConverter con)
=> con
-> Iteration
-> [GhcInfo]
-> NMExprEnv
-> TypeEnv
-> Measures
-> MeasureExs
-> Evals Bool
-> M.Map Name SpecInfo
-> FuncConstraints
-> BlockedModels
-> Size
-> m SynthRes
synth con iter ghci eenv tenv meas meas_ex evals si fc blk_mdls sz = do
si' <- liaSynthOfSize sz si
let zero_coeff_hdrs = softCoeffAssertZero si' ++ softClauseActAssertZero si' -- ++ softFuncActAssertZero si'
-- zero_coeff_hdrs = softFuncActAssertZero si' ++ softClauseActAssertZero si'
-- zero_coeff_hdrs = softCoeffAssertZero si' -- softFuncActAssertZero si' ++ softClauseActAssertZero si'
max_coeffs_cons = maxCoeffConstraints si'
soft_coeff_cons = softCoeffConstraints si'
soft_set_bool_cons = softSetConstraints si'
mdls = lookupBlockedModels sz blk_mdls
rel_mdls = map (uncurry (filterModelToRel si')) mdls
block_mdls = map blockModelDirectly rel_mdls
non_equiv_mdls = lookupNonEquivBlockedModels sz blk_mdls
rel_non_equiv_mdls = map (uncurry (filterModelToRel si')) non_equiv_mdls
fun_block_mdls = concatMap (uncurry (blockModelWithFuns si')) $ zip (map show ([0..] :: [Integer])) rel_non_equiv_mdls
ex_assrts1 = [Comment "enforce maximal and minimal values for coefficients"]
++ max_coeffs_cons
ex_assrts2 = [Comment "favor making coefficients 0"]
++ zero_coeff_hdrs
++ [Comment "favor coefficients being -1, 0, or 1"]
++ soft_coeff_cons
++ [Comment "favor set booleans being false"]
++ soft_set_bool_cons
++ [Comment "block spurious models"]
++ block_mdls
ex_assrts = ex_assrts1 ++ ex_assrts2
drop_if_unknown = [Comment "stronger blocking of spurious models"] ++ fun_block_mdls
MaxSize max_sz <- maxSynthFormSizeM
res <- synth' con ghci eenv tenv meas meas_ex evals si' fc ex_assrts drop_if_unknown blk_mdls sz
case res of
SynthEnv _ _ n_mdl _ -> do
new <- checkModelIsNewFunc con si' n_mdl non_equiv_mdls
case new of
Nothing -> return res
Just (_, eq_mdl) -> do
let sys = concatMap allSynthSpec $ M.elems si'
rel_n_mdl = filterIrrelByConstruction sys n_mdl
rel_eq_mdl = filterIrrelByConstruction sys eq_mdl
mn = determineRelSynthSpecs si' rel_n_mdl rel_eq_mdl
mdls' = foldr (\n -> insertEquivBlockedModel sz (MNOnlySMTNames [n]) n_mdl) blk_mdls mn
liftIO . putStrLn $ "mn = " ++ show mn
synth con iter ghci eenv tenv meas meas_ex evals si fc mdls' sz
SynthFail _
| sz < max_sz -> synth con iter ghci eenv tenv meas meas_ex evals si fc blk_mdls (sz + 1)
| FirstRound <- iter -> do
no_max_res <- synth' con ghci eenv tenv meas meas_ex evals si' fc ex_assrts2 drop_if_unknown blk_mdls sz
case no_max_res of
SynthEnv gs _ _ _ -> do
let lits = concatMap exprIntegers $ allExprs gs
max_lit = maximum $ map abs lits
setMaxSynthCoeffSizeM (MaxSize max_lit)
return no_max_res
_ -> return no_max_res
| otherwise -> return res
synth' :: (InfConfigM m, ProgresserM m, MonadIO m, SMTConverter con)
=> con
-> [GhcInfo]
-> NMExprEnv
-> TypeEnv
-> Measures
-> MeasureExs
-> Evals Bool
-> M.Map Name SpecInfo
-> FuncConstraints
-> [SMTHeader]
-> [SMTHeader]
-> BlockedModels
-> Size
-> m SynthRes
synth' con ghci eenv tenv meas meas_ex evals m_si fc headers drop_if_unknown blk_mdls sz = do
let n_for_m = namesForModel m_si
let consts = arrayConstants m_si
(constraints, nm_fc_map) <- nonMaxCoeffConstraints ghci eenv tenv meas meas_ex evals m_si fc
let hdrs = SetLogic ALL:consts ++ constraints ++ headers ++ drop_if_unknown
liftIO $ if not (null drop_if_unknown) then putStrLn "non empty drop_if_unknown" else return ()
result <- return . adjustRes =<< runConstraintsForSynth hdrs n_for_m
case result of
SAT mdl -> do
let gs' = modelToGS m_si mdl
liftIO $ print gs'
return (SynthEnv gs' sz mdl blk_mdls)
UNSAT uc ->
let
fc_uc = fromSingletonFC . NotFC . AndFC . map (nm_fc_map HM.!) $ HS.toList uc
in
return (SynthFail fc_uc)
Unknown _ maybe_mdl
| not (null drop_if_unknown) ->
synth' con ghci eenv tenv meas meas_ex evals m_si fc headers [] blk_mdls sz
| Just mdl <- maybe_mdl -> do
liftIO $ putStrLn "Unknown model!"
let gs' = modelToGS m_si mdl
liftIO $ print gs'
return (SynthEnv gs' sz mdl blk_mdls)
| otherwise -> error "synth': Unknown"
where
adjustRes (SAT m) = SAT m
adjustRes (UNSAT uc) = UNSAT uc
adjustRes (Unknown e ()) = Unknown e Nothing
runConstraintsForSynth :: (InfConfigM m, MonadIO m)
=> [SMTHeader] -> [(SMTName, Sort)] -> m (Result SMTModel UnsatCore ())
runConstraintsForSynth headers vs = do
inf_con <- infConfigM
if use_binary_minimization inf_con
then do
z3_dir <- liftIO $ getZ3 100000
z3_max <-liftIO $ mkMaximizeSolver =<< getZ3 50000
liftIO $ setProduceUnsatCores z3_dir
liftIO $ setProduceUnsatCores z3_max
-- liftIO $ T.putStrLn (TB.run $ toSolverText headers)
liftIO $ addFormula z3_dir headers
liftIO $ addFormula z3_max headers
liftIO $ checkSatInstr z3_dir
liftIO $ checkSatInstr z3_max
res <- liftIO $ waitForRes2 Nothing Nothing z3_dir z3_max vs
liftIO $ closeIO z3_dir
liftIO $ closeIO z3_max
return res
else do
z3_dir <- liftIO $ getZ3 100000
liftIO $ setProduceUnsatCores z3_dir
liftIO $ addFormula z3_dir headers
liftIO $ checkSatInstr z3_dir
res <- liftIO $ waitForRes z3_dir vs
liftIO $ closeIO z3_dir
return res
waitForRes2 :: (SMTConverter s1, SMTConverter s2) =>
Maybe (Result () () ()) -- ^ Nothing, or an unknown returned by Solver 1
-> Maybe (Result () () ()) -- ^ Nothing, or an unknown returned by Solver 2
-> s1
-> s2
-> [(SMTName, Sort)]
-> IO (Result SMTModel UnsatCore ())
waitForRes2 m_res1 m_res2 s1 s2 vs = do
res1 <- maybe (maybeCheckSatResult s1) (return . Just) m_res1
res2 <- maybe (maybeCheckSatResult s2) (return . Just) m_res2
case (res1, res2) of
(Just res1', _) | isSatOrUnsat res1' -> do
putStrLn $ "res1 = " ++ show res1
putStrLn $ "res2 = " ++ show res2
getModelOrUnsatCore s1 vs res1'
(_, Just res2') | isSatOrUnsat res2' -> do
putStrLn $ "res1 = " ++ show res1
putStrLn $ "res2 = " ++ show res2
getModelOrUnsatCore s2 vs res2'
(Just (Unknown err1 ()), Just (Unknown err2 ())) -> do
return $ Unknown (err1 ++ "\n" ++ err2) ()
_ -> waitForRes2 res1 res2 s1 s2 vs
where
isSatOrUnsat (SAT _) = True
isSatOrUnsat (UNSAT _) = True
isSatOrUnsat _ = False
waitForRes :: SMTConverter s =>
s
-> [(SMTName, Sort)]
-> IO (Result SMTModel UnsatCore ())
waitForRes s vs = do
res <- maybeCheckSatResult s
case res of
Just res' -> getModelOrUnsatCore s vs res'
_ -> waitForRes s vs
getModelOrUnsatCore :: SMTConverter smt => smt -> [(SMTName, Sort)] -> Result () () () -> IO (Result SMTModel UnsatCore ())
getModelOrUnsatCore con vs (SAT ()) = do
mdl <- getModelInstrResult con vs
return (SAT mdl)
getModelOrUnsatCore con _ (UNSAT ()) = do
uc <- getUnsatCoreInstrResult con
return (UNSAT uc)
getModelOrUnsatCore _ _ (Unknown err ()) = return (Unknown err ())
-- | Extract Integer literals from a LH expression
exprIntegers :: LHF.Expr -> [Integer]
exprIntegers (ESym _) = []
exprIntegers (ECon (I i)) = [i]
exprIntegers (ECon _) = []
exprIntegers (EVar _) = []
exprIntegers (EApp e1 e2) = exprIntegers e1 ++ exprIntegers e2
exprIntegers (ENeg e) = exprIntegers e
exprIntegers (EBin _ e1 e2) = exprIntegers e1 ++ exprIntegers e2
exprIntegers (EIte e1 e2 e3) = exprIntegers e1 ++ exprIntegers e2 ++ exprIntegers e3
exprIntegers (ECst e _) = exprIntegers e
exprIntegers (ELam _ e) = exprIntegers e
exprIntegers (ETApp e _) = exprIntegers e
exprIntegers (ETAbs e _) = exprIntegers e
exprIntegers (PAnd es) = concatMap exprIntegers es
exprIntegers (POr es) = concatMap exprIntegers es
exprIntegers (PNot e) = exprIntegers e
exprIntegers (PImp e1 e2) = exprIntegers e1 ++ exprIntegers e2
exprIntegers (PIff e1 e2) = exprIntegers e1 ++ exprIntegers e2
exprIntegers (PAtom _ e1 e2) = exprIntegers e1 ++ exprIntegers e2
exprIntegers _ = error "exprIntegers: unsupported"
------------------------------------
-- Handling Models
------------------------------------
----------------------------------------------------------------------------
-- Blocking Models directly
data BlockedModels = Block { blocked :: HM.HashMap Size [(ModelNames, SMTModel)]
, blocked_equiv :: HM.HashMap Size [(ModelNames, SMTModel)] -- ^ Models that should be blocked, and represent the same specification as a model in `blocked`
}
deriving (Show)
data ModelNames = MNAll | MNOnly [Name] | MNOnlySMTNames [SMTName]
deriving (Eq, Show, Read)
emptyBlockedModels :: BlockedModels
emptyBlockedModels = Block HM.empty HM.empty
insertBlockedModel :: Size -> ModelNames -> SMTModel -> BlockedModels -> BlockedModels
insertBlockedModel sz mdl_nms mdl blk_mdls =
blk_mdls { blocked = HM.insertWith (++) sz [(mdl_nms, mdl)] (blocked blk_mdls) }
insertEquivBlockedModel :: Size -> ModelNames -> SMTModel -> BlockedModels -> BlockedModels
insertEquivBlockedModel sz mdl_nms mdl blk_mdls =
blk_mdls { blocked_equiv = HM.insertWith (++) sz [(mdl_nms, mdl)] (blocked_equiv blk_mdls) }
lookupBlockedModels :: Size -> BlockedModels -> [(ModelNames, SMTModel)]
lookupBlockedModels sz blk_mdls =
HM.lookupDefault [] sz (blocked blk_mdls) ++ HM.lookupDefault [] sz (blocked_equiv blk_mdls)
lookupNonEquivBlockedModels :: Size -> BlockedModels -> [(ModelNames, SMTModel)]
lookupNonEquivBlockedModels sz blk_mdls =
HM.lookupDefault [] sz (blocked blk_mdls)
blockedHashMap :: BlockedModels -> HM.HashMap Size [(ModelNames, SMTModel)]
blockedHashMap blk_mdls = HM.unionWith (++) (blocked blk_mdls) (blocked_equiv blk_mdls)
unionBlockedModels :: BlockedModels -> BlockedModels -> BlockedModels
unionBlockedModels bm1 bm2 =
Block { blocked = HM.unionWith (++) (blocked bm1) (blocked bm2)
, blocked_equiv = HM.unionWith (++) (blocked_equiv bm1) (blocked_equiv bm2) }
----------------------------------------------------------------------------
-- Blocking Models building/manipulation
namesForModel :: M.Map Name SpecInfo -> [(SMTName, Sort)]
namesForModel = concat . map siNamesForModel . M.elems
siNamesForModel :: SpecInfo -> [(SMTName, Sort)]
siNamesForModel si
| s_status si == Synth = concatMap sySpecNamesForModel $ allSynthSpec si
| otherwise = []
sySpecNamesForModel :: SynthSpec -> [(SMTName, Sort)]
sySpecNamesForModel sys =
let
all_coeffs = zip (sySpecGetCoeffs sys) (repeat SortInt)
all_set_bools = zip (sySpecGetSetBools sys) (repeat SortBool)
all_bool_bools = zip (sySpecGetBoolBools sys) (repeat SortBool)
all_acts = zip (sySpecGetActs sys) (repeat SortInt)
all_op_branch = zip (sySpecGetOpBranches sys) (repeat SortBool)
in
all_coeffs ++ all_set_bools ++ all_bool_bools ++ all_acts ++ all_op_branch
modelToGS :: M.Map Name SpecInfo -> SMTModel -> GeneratedSpecs
modelToGS m_si mdl =
let
lh_spec = M.map (\si -> buildLIA_LH si mdl) . M.filter (\si -> s_status si == Synth) $ m_si
in
M.foldrWithKey insertAssertGS emptyGS lh_spec
-- | Generates an Assert that, when added to a formula with the relevant variables,
-- blocks it from returning the model
blockModelDirectly :: SMTModel -> SMTHeader
blockModelDirectly = Solver.Assert . (:!) . foldr (.&&.) (VBool True) . map (\(n, v) -> V n (sortOf v) := v) . M.toList
-- | Filters a model to only those variable bindings relevant to the functions listed in the name bindings
filterModelToRel :: M.Map Name SpecInfo -> ModelNames -> SMTModel -> SMTModel
filterModelToRel m_si ns mdl =
let
sys = case ns of
MNAll -> concatMap allSynthSpec $ M.elems m_si
MNOnly ns' -> concatMap allSynthSpec $ mapMaybe (flip M.lookup m_si) ns'
MNOnlySMTNames ns' -> filter (\sy -> sy_name sy `elem` ns')
. concatMap allSynthSpec
$ M.elems m_si
vs = map fst $ concatMap sySpecNamesForModel sys
in
filterIrrelByConstruction sys $ M.filterWithKey (\n _ -> n `elem` vs) mdl
filterIrrelByConstruction :: Foldable f => f SynthSpec -> SMTModel -> SMTModel
filterIrrelByConstruction = flip (foldr filterIrrelByConstruction')
filterIrrelByConstruction' :: SynthSpec -> SMTModel -> SMTModel
filterIrrelByConstruction' sys =
filterClauseActiveBooleans sys
. filterCoeffActiveBooleans sys
. filterRelOpBranch sys
-- If the clause level boolean is set to true, we remove all the
-- formula level active booleans, since the formulas are
-- irrelevant.
filterClauseActiveBooleans :: SynthSpec -> SMTModel -> SMTModel
filterClauseActiveBooleans si mdl =
let
clauses = sy_coeffs si
in
foldr (\(cl_act, cfs) mdl_ -> if
| M.lookup cl_act mdl_ == Just (VBool True) ->
foldr (\c -> M.delete (c_active c)) mdl_ cfs
| otherwise -> mdl_) mdl clauses
-- If the formula level active booleans are set to false, we remove all the
-- coefficients in the formula, since the formula is now irrelevant.
filterCoeffActiveBooleans :: SynthSpec -> SMTModel -> SMTModel
filterCoeffActiveBooleans si mdl =
let
clauses = sy_coeffs si
cffs = concatMap snd clauses
in
foldr (\cf mdl_ -> if
| M.lookup (c_active cf) mdl_ == Just (VBool False) ->
foldr M.delete mdl_ (coeffs cf)
| otherwise -> mdl_) mdl cffs
filterRelOpBranch :: SynthSpec -> SMTModel -> SMTModel
filterRelOpBranch si mdl =
let
clauses = sy_coeffs si
coeff_nms = concatMap snd clauses
in
-- If we are not using a clause, we don't care about c_op_branch1 and c_op_branch2
-- If we are using a clause but c_op_branch1 is true, we don't care about c_op_branch2
foldr (\form mdl_ -> if
| M.lookup (c_active form) mdl == Just (VBool False) ->
M.delete (c_op_branch2 form) $ M.delete (c_op_branch1 form) mdl_
| M.lookup (c_op_branch1 form) mdl == Just (VBool True) ->
M.delete (c_op_branch2 form) mdl_
| otherwise -> mdl) mdl coeff_nms
-- | Create specification definitions corresponding to previously rejected models,
-- and add assertions that the new synthesized specification definition must
-- have a different output than the old specifications at at least one point.
-- Because this requires a symbolic point being input into the synthesized function
-- (with symbolic coefficients) this requires (undecidable) non linear arithmetic (NIA).
blockModelWithFuns :: M.Map Name SpecInfo -> String -> SMTModel -> [SMTHeader]
blockModelWithFuns si s mdl =
let
e_si = M.elems $ M.filter (\si' -> s_status si' == Synth) si
vrs = map (uncurry blockVars) $ zip (map (\i -> s ++ "_" ++ show i) ([0..] :: [Integer])) e_si
var_defs = concatMap varDefs vrs
si_nsi = map (\(i, si') -> (si', renameByAdding i si'))
. zip (map (\i -> s ++ "_" ++ show i) ([0..] :: [Integer]))
$ e_si
fun_defs = concatMap (defineModelLIAFuns mdl . snd) si_nsi
eqs = map (\(vs, (si', nsi')) -> mkEqualityAST vs si' nsi') $ zip vrs si_nsi
neq = [Solver.Assert . (:!) $ mkSMTAnd eqs]
in
var_defs ++ fun_defs ++ neq
----------------------------------------------------------------------------
-- Blocking Models via checking after the fact
-- | Checks that the first model and each model in the list have at least
-- one point that they classifies differently,
-- i.e. for each model in the list, there must be at least one point that is
-- classified as true by that model, but false by the first model (or vice versa.)
-- As opposed to `blockModelWithFuns`, which enforced this as a constraint when
-- synthesizing the new specification, this function acts as a check on a newly
-- synthesized specification.
-- This avoids the need for non linear arithmetic, but allows us to quickly
-- reject newly synthesized specifications that are identical to some previous
-- specifications.
checkModelIsNewFunc :: (MonadIO m, SMTConverter con) => con -> M.Map Name SpecInfo -> SMTModel -> [(ModelNames, SMTModel)] -> m (Maybe (ModelNames, SMTModel))
checkModelIsNewFunc _ _ _ [] = return Nothing
checkModelIsNewFunc con si mdl ((mdl_nm, mdl'):mdls) = do
b' <- checkModelIsNewFunc' con si mdl mdl'
case b' of
True -> checkModelIsNewFunc con si mdl mdls
False -> do
liftIO $ do
putStrLn "Equiv!"
print mdl_nm
print mdl
print mdl'
putStrLn $ "diff 1 = " ++ show (M.toList mdl' L.\\ M.toList mdl)
putStrLn $ "diff 2 = " ++ show (M.toList mdl L.\\ M.toList mdl')
return (Just (mdl_nm, mdl'))
checkModelIsNewFunc' :: (MonadIO m, SMTConverter con) => con -> M.Map Name SpecInfo -> SMTModel -> SMTModel -> m Bool
checkModelIsNewFunc' con si mdl1 mdl2 = do
let e_si = M.elems $ M.filter (\si' -> s_status si' == Synth) si
vrs = map (uncurry blockVars) $ zip (map (\i -> "_c_" ++ show i) ([0..] :: [Integer])) e_si
var_defs = concatMap varDefs vrs
si_nsi = map (\(i, si') -> (si', renameByAdding i si'))
. zip (map (\i -> "_c_" ++ show i) ([0..] :: [Integer]))
$ e_si
fun_defs1 = concatMap (defineModelLIAFuns mdl1 . fst) si_nsi
fun_defs2 = concatMap (defineModelLIAFuns mdl2 . snd) si_nsi
eqs = map (\(vs, (si', nsi')) -> mkEqualityAST vs si' nsi') $ zip vrs si_nsi
neq = [Solver.Assert . (:!) $ mkSMTAnd eqs]
hdrs = arrayConstants si ++ var_defs ++ fun_defs1 ++ fun_defs2 ++ neq
r <- liftIO $ checkConstraints con hdrs
case r of
SAT _ -> return True
UNSAT _ -> return False
-- If we get a result of Unknown, we might as well optimistically assume that the model is new
Unknown _ _ -> do
liftIO $ putStrLn "checkModelIsNewFunc' unknown result"
return True
defineModelLIAFuns :: SMTModel -> SpecInfo -> [SMTHeader]
defineModelLIAFuns mdl si =
let
fs = L.nubBy (\si1 si2 -> sy_name si1 == sy_name si2)
$ (extractValues $ s_syn_post si) ++ (concatMap extractValues $ s_syn_pre si)
in
if s_status si == Synth
then map (defineModelLIAFuncSF mdl) fs
else []
defineModelLIAFuncSF :: SMTModel -> SynthSpec -> SMTHeader
defineModelLIAFuncSF mdl sf =
let
ars_nm = map smt_var (sy_args_and_ret sf)
ars = zip ars_nm (map smt_sort $ sy_args_and_ret sf)
in
DefineFun (sy_name sf) ars SortBool (buildLIA_SMT_fromModel mdl sf)
renameByAdding :: String -> SpecInfo -> SpecInfo
renameByAdding i si =
si { s_syn_pre = map (mapPB rn) $ s_syn_pre si
, s_syn_post = mapPB rn $ s_syn_post si
}
where
rn s = s { sy_name = sy_name s ++ "_MDL_" ++ i }
buildLIA_SMT_fromModel :: SMTModel -> SynthSpec -> SMTAST
buildLIA_SMT_fromModel mdl sf =
buildSpec (:+) (:*) (.=.) (.=.) (:>) (:>=) Ite Ite
mkSMTAnd mkSMTAnd mkSMTOr
mkSMTUnion mkSMTIntersection smtSingleton
mkSMTIsSubsetOf (flip ArraySelect)
vint VInt vbool vset
falseArray
trueArray
sf
where
vint n
| Just v <- M.lookup n mdl = v
| otherwise = V n SortInt
vbool n
| Just v <- M.lookup n mdl = v
| otherwise = V n SortBool
vset n
| Just v <- M.lookup n mdl = v
| otherwise = V n (SortArray SortInt SortBool)
smtSingleton :: SMTAST -> SMTAST
smtSingleton mem = ArrayStore falseArray mem (VBool True)
blockVars :: String -> SpecInfo -> ([PolyBound [(SMTName, Sort)]], PolyBound [(SMTName, Sort)])
blockVars str si = ( map (uncurry mk_blk_vars) . zip (map show ([0..] :: [Integer])) $ s_syn_pre si
, mk_blk_vars "r" $ s_syn_post si)
where
mk_blk_vars i sy_s =
mapPB (\(j, s) ->
map (\(k, sa) ->
("x_MDL_" ++ str ++ "_" ++ i ++ "_" ++ show j ++ "_" ++ show k, smt_sort sa))
. zip ([0..] :: [Integer])
$ sy_args_and_ret s
)
$ zipPB (uniqueIds sy_s) sy_s
varDefs :: ([PolyBound [(SMTName, Sort)]], PolyBound [(SMTName, Sort)]) -> [SMTHeader]
varDefs = map (\(n, srt) -> VarDecl (TB.text . T.pack $ n) srt)
. concat
. concatMap extractValues
. (\(x, y) -> y:x)
mkEqualityAST :: ([PolyBound [(SMTName, Sort)]], PolyBound [(SMTName, Sort)]) -> SpecInfo -> SpecInfo -> SMTAST
mkEqualityAST (avs, rvs) si nsi =
let
avs' = map (mapPB (map fst)) avs
rvs' = mapPB (map fst) rvs
pre_eq =
map (mapPB (uncurry3 mkFuncEq) . uncurry3 zip3PB)
$ zip3 avs' (s_syn_pre si) (s_syn_pre nsi)
pre_eq' = concatMap extractValues pre_eq
post_eq =
mapPB (uncurry3 mkFuncEq) $ zip3PB rvs' (s_syn_post si) (s_syn_post nsi)
post_eq' = extractValues post_eq
in
mkSMTAnd (post_eq' ++ pre_eq')
mkFuncEq :: [SMTName] -> SynthSpec -> SynthSpec -> SMTAST
mkFuncEq vs s_sp ns_sp =
let
smt_vs = map (flip V SortInt) vs
in
Func (sy_name s_sp) smt_vs := Func (sy_name ns_sp) smt_vs
-- Determines which SynthSpecs have been assigned different values in the two models.
determineRelSynthSpecs :: M.Map Name SpecInfo -> SMTModel -> SMTModel -> [SMTName]
determineRelSynthSpecs m_si mdl1 mdl2 =
let
diff = M.keys
$ M.differenceWith (\v1 v2 -> case v1 == v2 of
True -> Nothing
False -> Just v1) mdl1 mdl2
in
map sy_name
. filter
(\sys -> any (\n -> n `elem` diff) . map fst $ sySpecNamesForModel sys)
. concatMap allSynthSpec
$ M.elems m_si
-- computing F_{Fixed}, i.e. what is the value of known specifications at known points
envToSMT :: Evals (Integer, Bool) -> M.Map Name SpecInfo -> Int -> FuncConstraints
-> ([SMTHeader], HM.HashMap SMTName FuncConstraint)
envToSMT evals si fresh fc =
let
nm_fc = zip ["f" ++ show i ++ "_" ++ show fresh | i <- ([1..] :: [Integer])]
. L.nub
. map fst
$ allCallsFC fc
calls = concatMap (uncurry (flip (envToSMT' evals si))) nm_fc
known_id_calls = map fst calls
real_calls = map snd calls
assrts = map Solver.Assert known_id_calls
in
(assrts, HM.fromList real_calls)
envToSMT' :: Evals (Integer, Bool) -> M.Map Name SpecInfo -> FuncCall -> SMTName -> [(SMTAST, (SMTName, FuncConstraint))]
envToSMT' (Evals {pre_evals = pre_ev, post_evals = post_ev}) m_si fc@(FuncCall { funcName = f }) uc_n =
case M.lookup f m_si of
Just si ->
let
(pre_i, pre_res) = case lookupEvals fc pre_ev of
Just b -> b
Nothing -> error "envToSMT': pre not found"
(post_i, post_res) = case lookupEvals fc post_ev of
Just b -> b
Nothing -> error "envToSMT': post not found"
(pre_op, pre_op_fc) = if pre_res then (id, id) else ((:!), NotFC)
(post_op, post_op_fc) = if post_res then (id, id) else ((:!), NotFC)
pre = pre_op $ Func (s_known_pre_name si) [VInt pre_i]
post = post_op $ Func (s_known_post_name si) [VInt post_i]
pre_real = pre_op_fc (Call Pre fc [])
post_real = post_op_fc (Call Post fc [])
pre_name = "pre_" ++ uc_n
post_name = "post_" ++ uc_n
-- In the case that we get an unsat core, we are only interested in knowing which specifications
-- that have already been chosen must be changed. Thus, we only name those pieeces of the environment.
named_sp = case s_status si of
Known -> Named
_ -> \x _ -> x
in
[ (named_sp pre pre_name, (pre_name, pre_real))
, (named_sp post post_name, (post_name, post_real))]
Nothing -> error "envToSMT': function not found"
mkRetNonZero :: M.Map Name SpecInfo -> [SMTHeader]
mkRetNonZero = concatMap mkRetNonZero' . filter (\si -> s_status si == Synth) . M.elems
mkRetNonZero' :: SpecInfo -> [SMTHeader]
mkRetNonZero' si =
let
sy_sps = allSynthSpec si
in
concatMap (\sys ->
let
cffs = sy_coeffs sys
in
map
(\(act, cff) ->
Solver.Assert (((:!) $ V act SortBool)
:=>
mkSMTOr (concatMap (\c -> mkCoeffRetNonZero c) cff))
) cffs
) sy_sps
mkCoeffRetNonZero :: Forms -> [SMTAST]
mkCoeffRetNonZero cffs@(LIA {}) =
let
act = c_active cffs
ret_cffs = rets_coeffs cffs
in
case null ret_cffs of
True -> [VBool True]
False ->
[V act SortBool :=> mkSMTOr (map (\r -> V r SortInt :/= VInt 0) ret_cffs)]
mkCoeffRetNonZero cffs@(Set {}) =
let
act = c_active cffs
ret_bools = concat $ rets_bools_lhs cffs ++ rets_bools_rhs cffs
in
case null ret_bools of
True -> [VBool True]
False ->
[V act SortBool :=> mkSMTOr (map (\r -> V r SortBool) ret_bools)]
mkCoeffRetNonZero cffs@(BoolForm {}) =
let
act = c_active cffs
ret_bools = rets_bools cffs
in
case null ret_bools of
True -> [VBool True]
False ->
[V act SortBool :=> mkSMTOr (map (\r -> (:!) (V r SortBool)) ret_bools)]
-- This function aims to limit the number of different models that can be produced
-- that result in equivalent specifications.
-- This is important, because as a fallback when counterexamples are not
-- blocking bad solutions, we instead negate SMT models. So we want as
-- few different, but ultimately equivalent, models as possible.
-- In particualar:
-- (1) If the formula level active booleans are set to false, we force all the
-- coefficients in the formula to be 0, since the formula is now irrelevant.
-- (2) Similarly, if the clause level boolean is set to true, we force all the
-- formula level active booleans to be false, since the formulas are
-- irrelevant.
-- (3) If the n^th "or" is deactivated (by it's boolean being true),
-- then the n + 1^th "or" must also be deactivated
-- (4) If the n^th "and" is deactivated (by it's boolean being false),
-- then the n + 1^th "and" must also be deactivated
limitEquivModels :: M.Map Name SpecInfo -> [SMTHeader]
limitEquivModels m_si =
let
a_si = filter (\si -> s_status si == Synth) $ M.elems m_si
-- (1)
clauses = concatMap allCNFs a_si
cl_imp_coeff = concatMap
(\(cl_act, cff) ->
map (\cf -> V cl_act SortBool :=> ((:!) $ V (c_active cf) SortBool)) cff
) clauses
-- (2)
cffs = concatMap snd clauses
coeff_act_imp_zero = concatMap
(\cf ->
map (\c -> ((:!) $ V (c_active cf) SortBool) :=> (V c SortInt := VInt 0)) (coeffs cf)
) cffs
-- (3)
or_acts = map (map (map fst) . allCNFsSeparated) a_si :: [[[SMTName]]]
or_neighbors_deact =
concatMap
(concatMap
(map (\(n1, n2) -> ((:!) $ V n2 SortBool) :=> ((:!) $ V n1 SortBool)) . neighbors)
) $ or_acts
-- (4)
and_neighbors_deact = and_block (\case LIA {} -> True; _ -> False) a_si
++ and_block (\case Set {} -> True; _ -> False) a_si
in
map Solver.Assert $ cl_imp_coeff ++ coeff_act_imp_zero -- ++ or_neighbors_deact ++ and_neighbors_deact
where
neighbors [] = []
neighbors [_] = []
neighbors (x:xs@(y:_)) = (x, y):neighbors xs
and_block p a_si' =
let
and_acts = concatMap (map (map snd) . allCNFsSeparated) a_si'
in
concatMap
(concatMap
( mapMaybe
(\(n1, n2) -> if p n1 && p n2
then Just (V (c_active n2) SortBool :=> V (c_active n1) SortBool)
else Nothing)
. neighbors
)
) $ and_acts
softCoeffAssertZero :: M.Map Name SpecInfo -> [SMTHeader]
softCoeffAssertZero = map (\n -> AssertSoft (V n SortInt := VInt 0) (Just "minimal_size")) . getCoeffs
softFuncActAssertZero :: M.Map Name SpecInfo -> [SMTHeader]
softFuncActAssertZero = map (\n -> AssertSoft ((:!) $ V n SortBool) (Just "minimal_size")) . getFuncActs
softClauseActAssertZero :: M.Map Name SpecInfo -> [SMTHeader]
softClauseActAssertZero = map (\n -> AssertSoft (V n SortBool) (Just "minimal_size")) . getClauseActs
maxCoeffConstraints :: M.Map Name SpecInfo -> [SMTHeader]
maxCoeffConstraints = maxCoeffConstraints' Solver.Assert s_max_coeff
softCoeffConstraints :: M.Map Name SpecInfo -> [SMTHeader]
softCoeffConstraints = maxCoeffConstraints' (flip Solver.AssertSoft (Just "coeff")) (const 1)
maxCoeffConstraints' :: (SMTAST -> SMTHeader) -> (SpecInfo -> Integer) -> M.Map Name SpecInfo -> [SMTHeader]
maxCoeffConstraints' to_header max_c =
map to_header
. concatMap
(\si ->
let
cffs = concatMap coeffs . concatMap snd $ allPreCoeffs si ++ allPostCoeffs si
in
if s_status si == Synth
then map (\c -> (Neg (VInt (max_c si)) :<= V c SortInt)
.&&. (V c SortInt :<= VInt (max_c si))) cffs
else []) . M.elems
softSetConstraints :: M.Map Name SpecInfo -> [SMTHeader]
softSetConstraints =
map (\n -> AssertSoft ((:!) (V n SortBool)) (Just "minimal_sets")) . getSetBools
arrayConstants :: M.Map Name SpecInfo -> [SMTHeader]
arrayConstants si =
let
frms = concatMap allForms $ M.elems si
in
if any (\case Set {} -> True; _ -> False) frms
then
[ VarDecl (TB.text "true_array") (SortArray SortInt SortBool)
, Solver.Assert (trueArray := (mkSMTUniversalArray SortInt SortBool))
, VarDecl (TB.text "false_array") (SortArray SortInt SortBool)
, Solver.Assert (falseArray := (mkSMTEmptyArray SortInt SortBool))]
else []
trueArray :: SMTAST
trueArray = V "true_array" (SortArray SortInt SortBool)
falseArray :: SMTAST
falseArray = V "false_array" (SortArray SortInt SortBool)
nonMaxCoeffConstraints :: (InfConfigM m, ProgresserM m) => [GhcInfo] -> NMExprEnv -> TypeEnv -> Measures -> MeasureExs -> Evals Bool -> M.Map Name SpecInfo -> FuncConstraints
-> m ([SMTHeader], HM.HashMap SMTName FuncConstraint)
nonMaxCoeffConstraints ghci eenv tenv meas meas_ex evals m_si fc = do
synth_fresh <- synthFreshM
incrSynthFreshM
let evals' = assignIds evals
all_acts = getActs m_si
all_coeffs = getCoeffs m_si
all_set_bools = getSetBools m_si
all_bool_bools = getBoolBools m_si
get_ops = getOpBranches m_si
var_act_hdrs = map (flip VarDecl SortBool . TB.text . T.pack) $ L.nub all_acts
var_int_hdrs = map (flip VarDecl SortInt . TB.text . T.pack) $ L.nub all_coeffs
var_bool_set_hdrs = map (flip VarDecl SortBool . TB.text . T.pack) $ L.nub all_set_bools
var_bool_bool_hdrs = map (flip VarDecl SortBool . TB.text . T.pack) $ L.nub all_bool_bools
var_op_hdrs = map (flip VarDecl SortBool . TB.text . T.pack) $ L.nub get_ops
def_funs = concatMap defineLIAFuns $ M.elems m_si
(env_smt, nm_fc) = envToSMT evals' m_si synth_fresh fc
ret_is_non_zero = mkRetNonZero m_si
lim_equiv_smt = limitEquivModels m_si
poly_access = polyAccessConstraints2 ghci meas m_si
fc_smt <- constraintsToSMT eenv tenv meas meas_ex evals' m_si fc
return
( var_act_hdrs
++ var_int_hdrs
++ var_bool_set_hdrs
++ var_bool_bool_hdrs
++ var_op_hdrs
++ def_funs
++ [Comment "encode specification constraints"]
++ fc_smt
++ [Comment "encode the environment"]
++ env_smt
++ [Comment "force return values to be nonzero"]
++ ret_is_non_zero
++ [Comment "block equivalent formulas"]
++ lim_equiv_smt
++ [Comment "polymorphic access constraints"]
++ poly_access
, nm_fc)
constraintsToSMT :: (InfConfigM m, ProgresserM m) =>
NMExprEnv
-> TypeEnv
-> Measures
-> MeasureExs
-> Evals (Integer, Bool)
-> M.Map Name SpecInfo
-> FuncConstraints
-> m [SMTHeader]
constraintsToSMT eenv tenv meas meas_ex evals si fc =
return . map (Solver.Assert) =<<
convertConstraints
convertExprToSMT
(ifNotNull mkSMTAnd (VBool True))
(ifNotNull mkSMTOr (VBool False))
(:!)
(:=>)
Func
(\n i _ -> Func n [VInt i])
(\n i _ -> Func n [VInt i])
eenv tenv meas meas_ex evals si fc
where
ifNotNull _ def [] = def
ifNotNull f _ xs = f xs
convertExprToSMT :: G2.Expr -> SMTAST
convertExprToSMT e =
case e of
(App (App (Data (DataCon _ _)) _) ls)
| Just is <- extractInts ls ->
foldr (\i arr -> ArrayStore arr (VInt i) (VBool True)) falseArray is
_ -> exprToSMT e
extractInts :: G2.Expr -> Maybe [Integer]
extractInts (App (App (App (Data _ ) (Type _)) (App _ (Lit (LitInt i)))) xs) =
return . (i:) =<< extractInts xs
extractInts (App (Data _) _) = Just []
extractInts _ = Nothing
---
getCoeffs :: M.Map Name SpecInfo -> [SMTName]
getCoeffs = concatMap siGetCoeffs . M.elems
sySpecGetCoeffsNoB :: SynthSpec -> [SMTName]
sySpecGetCoeffsNoB = concatMap coeffsNoB . concatMap snd . sy_coeffs
siGetCoeffs :: SpecInfo -> [SMTName]
siGetCoeffs si
| s_status si == Synth = concatMap sySpecGetCoeffs $ allSynthSpec si
| otherwise = []
sySpecGetCoeffs :: SynthSpec -> [SMTName]
sySpecGetCoeffs = concatMap coeffs . concatMap snd . sy_coeffs
getSetBools :: M.Map Name SpecInfo -> [SMTName]
getSetBools = concatMap siGetSetBools . M.elems
siGetSetBools :: SpecInfo -> [SMTName]
siGetSetBools si
| s_status si == Synth = concatMap sySpecGetSetBools $ allSynthSpec si
| otherwise = []
sySpecGetSetBools :: SynthSpec -> [SMTName]
sySpecGetSetBools = concatMap setBools . concatMap snd . sy_coeffs
getBoolBools :: M.Map Name SpecInfo -> [SMTName]
getBoolBools = concatMap siGetBoolBools . M.elems
siGetBoolBools :: SpecInfo -> [SMTName]
siGetBoolBools si
| s_status si == Synth = concatMap sySpecGetBoolBools $ allSynthSpec si
| otherwise = []
sySpecGetBoolBools :: SynthSpec -> [SMTName]
sySpecGetBoolBools = concatMap boolBools . concatMap snd . sy_coeffs
---
getOpBranches:: M.Map Name SpecInfo -> [SMTName]
getOpBranches = concatMap siGetOpBranches . M.elems
siGetOpBranches :: SpecInfo -> [SMTName]
siGetOpBranches si
| s_status si == Synth =
concatMap sySpecGetOpBranches $ allSynthSpec si
| otherwise = []
sySpecGetOpBranches :: SynthSpec -> [SMTName]
sySpecGetOpBranches = concatMap sySpecGetOpBranchesForm . concatMap snd . sy_coeffs
sySpecGetOpBranchesForm :: Forms -> [SMTName]
sySpecGetOpBranchesForm c@(BoolForm {}) =
[c_op_branch1 c, c_op_branch2 c] ++ concatMap sySpecGetOpBranchesForm (forms c)
sySpecGetOpBranchesForm c = [c_op_branch1 c, c_op_branch2 c]
---
sySpecGetActs :: SynthSpec -> [SMTName]
sySpecGetActs sys = sySpecGetClauseActs sys ++ sySpecGetFuncActs sys
sySpecGetClauseActs :: SynthSpec -> [SMTName]
sySpecGetClauseActs = map fst . sy_coeffs
sySpecGetFuncActs :: SynthSpec -> [SMTName]
sySpecGetFuncActs = concatMap formActives . concatMap snd . sy_coeffs
getActs :: M.Map Name SpecInfo -> [SMTName]
getActs si = getClauseActs si ++ getFuncActs si
getClauseActs :: M.Map Name SpecInfo -> [SMTName]
getClauseActs m_si =
concatMap siGetClauseActs $ M.elems m_si
siGetClauseActs :: SpecInfo -> [SMTName]
siGetClauseActs si
| s_status si == Synth = map fst $ allCNFs si
| otherwise = []
getFuncActs :: M.Map Name SpecInfo -> [SMTName]
getFuncActs m_si =
concatMap siGetFuncActs $ M.elems m_si
siGetFuncActs :: SpecInfo -> [SMTName]
siGetFuncActs si
| s_status si == Synth = concatMap formActives . concatMap snd $ allCNFs si
| otherwise = []
formActives :: Forms -> [SMTName]
formActives cffs@(BoolForm {}) = c_active cffs:concatMap formActives (forms cffs)
formActives cffs = [c_active cffs]
defineLIAFuns :: SpecInfo -> [SMTHeader]
defineLIAFuns si =
(if s_status si == Synth
then
let
funcs = L.nubBy (\si1 si2 -> sy_name si1 == sy_name si2)
$ (extractValues $ s_syn_post si) ++ (concatMap extractValues $ s_syn_pre si)
in
map defineSynthLIAFuncSF funcs
else [])
++
[ defineFixedLIAFuncSF (s_known_pre si)
, defineFixedLIAFuncSF (s_known_post si)
, defineToBeFuncSF (s_to_be_pre si)
, defineToBeFuncSF (s_to_be_post si)]
defineFixedLIAFuncSF :: FixedSpec -> SMTHeader
defineFixedLIAFuncSF fs =
DeclareFun (fs_name fs) [SortInt] SortBool
defineToBeFuncSF :: ToBeSpec -> SMTHeader
defineToBeFuncSF tb =
DeclareFun (tb_name tb) [SortInt] SortBool
defineSynthLIAFuncSF :: SynthSpec -> SMTHeader
defineSynthLIAFuncSF sf =
let
ars_nm = map smt_var (sy_args_and_ret sf)
ars = zip ars_nm (map smt_sort $ sy_args_and_ret sf)
in
DefineFun (sy_name sf) ars SortBool (buildLIA_SMT sf)
------------------------------------
-- Building LIA Formulas
------------------------------------
type Plus a = a -> a -> a
type Mult a = a -> a -> a
type EqF a b = a -> a -> b
type Gt a b = a -> a -> b
type GEq a b = a -> a -> b
type Ite b a = b -> a -> a -> a
type And b c = [b] -> c
type Or b = [b] -> b
type IsSubsetOf a b = a -> a -> b
type IsMember a b = a -> a -> b
type Union a = a -> a -> a
type Intersection a = a -> a -> a
type Singleton a = a -> a
type VInt a = SMTName -> a
type CInt a = Integer -> a
type VBool b = SMTName -> b
type VSet s = SMTName -> s
type EmptySet s = s
type UniversalSet s = s
buildLIA_SMT :: SynthSpec -> SMTAST
buildLIA_SMT sf =
buildSpec (:+) (:*) (.=.) (.=.) (:>) (:>=) Ite Ite
mkSMTAnd mkSMTAnd mkSMTOr mkSMTUnion mkSMTIntersection smtSingleton
mkSMTIsSubsetOf (flip ArraySelect)
(flip V SortInt) VInt (flip V SortBool) (flip V $ SortArray SortInt SortBool)
falseArray
trueArray
sf
-- Get a list of all LIA formulas. We raise these as high in a PolyBound as possible,
-- because checking leaves is more expensive. Also, checking leaves only happens if those
-- leaves exists, i.e. consider a refinement on the elements of a list [{x:a | p x}],
-- p is only checked in the nonempty case.
buildLIA_LH :: SpecInfo -> SMTModel -> [PolyBound LHF.Expr]
buildLIA_LH si mv = map (mapPB pAnd) {- . map (uncurry raiseSpecs) . zip synth_specs -} $ buildLIA_LH' si mv
where
pAnd xs =
case any (== PFalse) xs of
True -> PFalse
False -> PAnd $ filter (/= PTrue) xs
buildLIA_LH' :: SpecInfo -> SMTModel -> [PolyBound [LH.Expr]]
buildLIA_LH' si mv =
let
post_ars = allPostSpecArgs si
build ars = buildSpec ePlus eTimes
bEq bIff bGt bGeq
eIte eIte id
pAnd pOr
eUnion eIntersection eSingleton
bIsSubset bIsMember
(detVar ars) (ECon . I) (detBool ars)
(detSet ars) eEmptySet eUnivSet
pre = map (mapPB (\psi -> build (all_sy_args_and_ret psi) psi)) $ s_syn_pre si
post = mapPB (build post_ars) $ s_syn_post si
in
pre ++ [post]
where
detVar ars v
| Just (VInt c) <- M.lookup v mv = ECon (I c)
| Just sa <- L.find (\sa_ -> v == smt_var sa_) ars = lh_rep sa
| otherwise = error "detVar: variable not found"
detBool ars v
| Just (VBool b) <- M.lookup v mv = if b then PTrue else PFalse
| Just sa <- L.find (\sa_ -> v == smt_var sa_) ars = lh_rep sa
| otherwise = error $ "detBool: variable not found" ++ " " ++ show v ++ "\nars = " ++ show ars
detSet ars v
| Just sa <- L.find (\sa_ -> v == smt_var sa_) ars = lh_rep sa
| otherwise = error "detSet: variable not found"
eTimes (ECon (I 0)) _ = ECon (I 0)
eTimes _ (ECon (I 0)) = ECon (I 0)
eTimes (ECon (I 1)) x = x
eTimes x (ECon (I 1)) = x
eTimes (ECon (I (-1))) x = ENeg x
eTimes x (ECon (I (-1))) = ENeg x
eTimes x y = EBin LH.Times x y
ePlus (ECon (I 0)) x = x
ePlus x (ECon (I 0)) = x
ePlus x (ENeg y) = EBin LH.Minus x y
ePlus (ENeg x) y = EBin LH.Minus y x
ePlus (ENeg x) y = EBin LH.Minus y x
ePlus x (EBin LH.Times (ECon (I i)) y) | i < 0 = EBin LH.Minus x (EBin LH.Times (ECon (I $ - i)) y)
ePlus (EBin LH.Times (ECon (I i)) x) y | i < 0 = EBin LH.Minus y (EBin LH.Times (ECon (I $ - i)) x)
ePlus x y = EBin LH.Plus x y
eIte PTrue x _ = x
eIte PFalse _ y = y
eIte _ _ _ = error "eIte: Should never have non-concrete bool"
pAnd xs =
case any (== PFalse) xs of
True -> PFalse
False -> PAnd $ filter (/= PTrue) xs
pOr xs =
case any (== PTrue) xs of
True -> PTrue
False -> POr $ filter (/= PFalse) xs
bEq (ECon (I x)) (ECon (I y)) =
if x == y then PTrue else PFalse
bEq x y
| x == y = PTrue
| x == eUnivSet
, y == eUnivSet = PTrue
| x == eUnivSet || y == eUnivSet = PFalse
| EBin LH.Minus e1 e2 <- x
, ECon (I 0) <- y = PAtom LH.Eq e1 e2
| otherwise = PAtom LH.Eq x y
bIff x y
| x == y = PTrue
| otherwise = PIff x y
bGt (ECon (I x)) (ECon (I y)) =
if x > y then PTrue else PFalse
bGt x y
| x == y = PFalse
| EBin LH.Minus e1 e2 <- x
, ECon (I 0) <- y = PAtom LH.Gt e1 e2
| otherwise = PAtom LH.Gt x y
bGeq (ECon (I x)) (ECon (I y)) =
if x >= y then PTrue else PFalse
bGeq x y
| x == y = PTrue
| EBin LH.Minus e1 e2 <- x
, ECon (I 0) <- y = PAtom LH.Ge e1 e2
| otherwise = PAtom LH.Ge x y
eUnion x y
| x == eEmptySet = y
| y == eEmptySet = x
| x == eUnivSet = eUnivSet
| y == eUnivSet = eUnivSet
| x == y = x
| otherwise = EApp (EApp (EVar "Set_cup") x) y
eIntersection x y
| x == eUnivSet = y
| y == eUnivSet = x
| x == eEmptySet = eEmptySet
| y == eEmptySet = eEmptySet
| x == y = x
| otherwise = EApp (EApp (EVar "Set_cap") x) y
eSingleton = EApp (EVar "Set_sng")
bIsSubset x y
| x == eEmptySet = PTrue
| y == eUnivSet = PTrue
| x == eUnivSet = PFalse
| x == y = PTrue
| otherwise = EApp (EApp (EVar "Set_sub") x) y
bIsMember x y
| y == eEmptySet = PFalse
| y == eUnivSet = PTrue
| otherwise = EApp (EApp (EVar "Set_mem") x) y
eEmptySet = EApp (EVar "Set_empty") (ECon (I 0))
eUnivSet = EVar ("Set_univ")
buildSpec :: Show b => Plus a
-> Mult a
-> EqF a b
-> EqF b b
-> Gt a b
-> GEq a b
-> Ite b b
-> Ite b a
-> And b c
-> And b b
-> Or b
-> Union a
-> Intersection a
-> Singleton a
-> IsSubsetOf a b
-> IsMember a b
-> VInt a
-> CInt a
-> VBool b
-> VSet a
-> EmptySet a
-> UniversalSet a
-> SynthSpec
-> c
buildSpec plus mult eq eq_bool gt geq ite ite_set mk_and_sp mk_and mk_or mk_union mk_intersection mk_sing is_subset is_member vint cint vbool vset cemptyset cunivset sf =
let
all_coeffs = sy_coeffs sf
lin_ineqs = map (\(cl_act, cl) -> vbool cl_act:map toLinInEqs cl) all_coeffs
in
mk_and_sp . map mk_or $ lin_ineqs
where
int_args = map smt_var (int_sy_args_and_ret sf)
set_args = map smt_var (set_sy_args_and_ret sf)
bool_args = map smt_var (bool_sy_args_and_ret sf)
toLinInEqs (LIA { c_active = act
, c_op_branch1 = op_br1
, c_op_branch2 = op_br2
, b0 = b
, ars_coeffs = acs
, rets_coeffs = rcs }) =
let
sm = lia_form acs rcs
in
mk_and [vbool act, ite (vbool op_br1)
(sm `eq` vint b)
(ite (vbool op_br2) (sm `gt` vint b)
(sm `geq` vint b)
)
]
toLinInEqs (Set { c_active = act
, int_sing_set_bools_lhs = int_sing_bools_lhs
, int_sing_set_bools_rhs = int_sing_bools_rhs
, ars_bools_lhs = ars_b1
, rets_bools_lhs = rets_b1
, ars_bools_rhs = ars_b2
, rets_bools_rhs = rets_b2 }) =
let
sm1 = set_form ars_b1 rets_b1 int_sing_bools_lhs
sm2 = set_form ars_b2 rets_b2 int_sing_bools_rhs
in
mk_and [vbool act, sm1 `eq` sm2]
toLinInEqs (BoolForm { c_active = act
, ars_bools = as
, rets_bools = rs
, forms = frms }) =
let
bb = zipWith (\x y -> mk_or [x, y]) (map vbool $ as ++ rs) (map vbool bool_args)
in
mk_and [vbool act, mk_and bb `eq_bool` mk_and (map toLinInEqs frms)]
lia_form acs rcs = foldr plus (cint 0)
. map (uncurry mult)
$ zip (map vint $ acs ++ rcs) (map vint int_args)
set_form ars rts is_bools =
let
sets = map vset set_args
ars_rts = map (map vbool) $ zipWith (++) ars rts
ite_sets = map (zipWith (\s a -> ite_set a s cunivset) sets) ars_rts
ints = map vint int_args
ite_sing_sets = map (:[]) $ map (foldr (\(i, b) -> ite_set (vbool b) (mk_sing i)) cunivset . zip ints) is_bools -- map (zipWith (\s a -> ite_set (vbool a) (mk_sing s) cunivset) ints) is_bools
ite_sets' = if not (null ite_sing_sets)
then zipWith (++) ite_sets ite_sing_sets
else ite_sets
in
if not (null ite_sets') && any (not . null) ite_sets'
then foldr1 mk_union
. map (foldr1 mk_intersection)
$ ite_sets'
else cemptyset
-- foldr mk_union cemptyset
-- . map (\(b, s) -> ite_set b s cemptyset)
-- $ zip (map vbool $ ars ++ rts) (map vset set_args)
----------------------------------------------------------------------------
-- Polymorphic access measures
-- A measure is a polymorphic access measure if it returns a value of a polymorphic type.
-- For example, `fst :: (a, b) -> a`.
-- Specifications that use both tuple style specs i.e. ( {x:Int > 0 }, Int)
-- and measure style specs i.e. { t:(Int, Int) | fst t > 0 } together can cause strange
-- errors from LH. Thus, we add softer assertions to, when possible,
-- avoid using polymorphic access measures.
polyAccessConstraints2 :: [GhcInfo] -> Measures -> M.Map Name SpecInfo -> [SMTHeader]
polyAccessConstraints2 ghci meas =
let
pa_meas = getPolyAccessMeasures ghci meas
in
map (flip AssertSoft Nothing)
. polyAccessConstraints2' pa_meas
. M.filter (\si -> s_status si == Synth)
polyAccessConstraints2' :: [(LH.Symbol, Type, Type)] -> M.Map Name SpecInfo -> [SMTAST]
polyAccessConstraints2' meas = concatMap (polyAccessConstraints2'' meas) . M.elems
polyAccessConstraints2'' :: [(LH.Symbol, Type, Type)] -> SpecInfo -> [SMTAST]
polyAccessConstraints2'' meas si =
let
poly = allSynthSpecPoly si
in
concatMap (polyAccessConstraints2''' meas) $ concatMap extractValues poly
polyAccessConstraints2''' :: [(LH.Symbol, Type, Type)] -> SynthSpec -> [SMTAST]
polyAccessConstraints2''' meas sys =
let
cffs = sySpecGetCoeffsNoB sys
ars_cffs =
if not (null (sy_args sys)) || not (null (sy_rets sys))
then zip (cycle (sy_args sys ++ sy_rets sys)) cffs
else []
in
concatMap (\(sy, c) -> if usesPolyAcc (lh_rep sy)
then [V c SortInt := VInt 0]
else []) ars_cffs
where
meas' = map (\(m, _, _) -> m) meas
usesPolyAcc (EApp (EVar lh) e) = lh `elem` meas' || usesPolyAcc e
usesPolyAcc _ = False
getPolyAccessMeasures :: [GhcInfo] -> Measures -> [(LH.Symbol, Type, Type)]
getPolyAccessMeasures ghci =
map (\(n, at, rt) -> (getLHMeasureName ghci n, at, rt))
. mapMaybe (\(n, (t:ts, rt)) -> if null ts then Just (n, t, rt) else Nothing)
. HM.toList
. E.map' (\e -> (filter (not . isLHDict) $ anonArgumentTypes e, returnType e))
. E.filter (isTyVar . returnType)
where
isLHDict t
| (TyCon (Name n _ _ _) _):_ <- unTyApp t = n == "lh"
| otherwise = False
----------------------------------------------------------------------------
-- Helpers for SynthInfo
allSynthSpec :: SpecInfo -> [SynthSpec]
allSynthSpec si = allPreSynthSpec si ++ allPostSynthSpec si
allPreSynthSpec :: SpecInfo -> [SynthSpec]
allPreSynthSpec = concatMap extractValues . s_syn_pre
allPostSynthSpec :: SpecInfo -> [SynthSpec]
allPostSynthSpec = extractValues . s_syn_post
allSynthSpecPoly :: SpecInfo -> [PolyBound SynthSpec]
allSynthSpecPoly si = s_syn_pre si ++ [s_syn_post si]
allCNFs :: SpecInfo -> CNF
allCNFs si = allPreCoeffs si ++ allPostCoeffs si
allPreCoeffs :: SpecInfo -> CNF
allPreCoeffs = concatMap sy_coeffs . allPreSynthSpec
allPostCoeffs :: SpecInfo -> CNF
allPostCoeffs = concatMap sy_coeffs . allPostSynthSpec
allPostSpecArgs :: SpecInfo -> [SpecArg]
allPostSpecArgs = concatMap sy_args_and_ret . allPostSynthSpec
allCNFsSeparated :: SpecInfo -> [CNF]
allCNFsSeparated si = allPreCoeffsSeparated si ++ allPostCoeffsSeparated si
allPreCoeffsSeparated :: SpecInfo -> [CNF]
allPreCoeffsSeparated = map sy_coeffs . allPreSynthSpec
allPostCoeffsSeparated :: SpecInfo -> [CNF]
allPostCoeffsSeparated = map sy_coeffs . allPostSynthSpec
allForms :: SpecInfo -> [Forms]
allForms = concatMap allFormsFromForm
. concatMap snd
. allCNFs
allFormsFromForm :: Forms -> [Forms]
allFormsFromForm frm@(BoolForm { forms = frms }) = frm:concatMap allFormsFromForm frms
allFormsFromForm frm = [frm]